Proofgold Address

Known df_tayl__df_ana__df_ulm__df_log__df_cxp__df_logb__df_asin__df_acos__df_atan__df_area__df_em__df_zeta__df_lgam__df_gam__df_igam__df_cht__df_vma__df_chp : ∀ x0 : ο . (wceq ctayl (cmpt2 (λ x1 x2 . cpr cr cc) (λ x1 x2 . co cc (cv x1) cpm) (λ x1 x2 . cmpt2 (λ x3 x4 . cun cn0 (csn cpnf)) (λ x3 x4 . ciin (λ x5 . cin (co cc0 (cv x3) cicc) cz) (λ x5 . cdm (cfv (cv x5) (co (cv x1) (cv x2) cdvn)))) (λ x3 x4 . ciun (λ x5 . cc) (λ x5 . cxp (csn (cv x5)) (co ccnfld (cmpt (λ x6 . cin (co cc0 (cv x3) cicc) cz) (λ x6 . co (co (cfv (cv x4) (cfv (cv x6) (co (cv x1) (cv x2) cdvn))) (cfv (cv x6) cfa) cdiv) (co (co (cv x5) (cv x4) cmin) (cv x6) cexp) cmul)) ctsu))))) ⟶ wceq cana (cmpt (λ x1 . cpr cr cc) (λ x1 . crab (λ x2 . wral (λ x3 . wcel (cv x3) (cfv (cdm (cin (cv x2) (co cpnf (cv x3) (co (cv x1) (cv x2) ctayl)))) (cfv (co (cfv ccnfld ctopn) (cv x1) crest) cnt))) (λ x3 . cdm (cv x2))) (λ x2 . co cc (cv x1) cpm))) ⟶ wceq culm (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wrex (λ x4 . w3a (wf (cfv (cv x4) cuz) (co cc (cv x1) cmap) (cv x2)) (wf (cv x1) cc (cv x3)) (wral (λ x5 . wrex (λ x6 . wral (λ x7 . wral (λ x8 . wbr (cfv (co (cfv (cv x8) (cfv (cv x7) (cv x2))) (cfv (cv x8) (cv x3)) cmin) cabs) (cv x5) clt) (λ x8 . cv x1)) (λ x7 . cfv (cv x6) cuz)) (λ x6 . cfv (cv x4) cuz)) (λ x5 . crp))) (λ x4 . cz)))) ⟶ wceq clog (ccnv (cres ce (cima (ccnv cim) (co (cneg cpi) cpi cioc)))) ⟶ wceq ccxp (cmpt2 (λ x1 x2 . cc) (λ x1 x2 . cc) (λ x1 x2 . cif (wceq (cv x1) cc0) (cif (wceq (cv x2) cc0) c1 cc0) (cfv (co (cv x2) (cfv (cv x1) clog) cmul) ce))) ⟶ wceq clogb (cmpt2 (λ x1 x2 . cdif cc (cpr cc0 c1)) (λ x1 x2 . cdif cc (csn cc0)) (λ x1 x2 . co (cfv (cv x2) clog) (cfv (cv x1) clog) cdiv)) ⟶ wceq casin (cmpt (λ x1 . cc) (λ x1 . co (cneg ci) (cfv (co (co ci (cv x1) cmul) (cfv (co c1 (co (cv x1) c2 cexp) cmin) csqrt) caddc) clog) cmul)) ⟶ wceq cacos (cmpt (λ x1 . cc) (λ x1 . co (co cpi c2 cdiv) (cfv (cv x1) casin) cmin)) ⟶ wceq catan (cmpt (λ x1 . cdif cc (cpr (cneg ci) ci)) (λ x1 . co (co ci c2 cdiv) (co (cfv (co c1 (co ci (cv x1) cmul) cmin) clog) (cfv (co c1 (co ci (cv x1) cmul) caddc) clog) cmin) cmul)) ⟶ wceq carea (cmpt (λ x1 . crab (λ x2 . wa (wral (λ x3 . wcel (cima (cv x2) (csn (cv x3))) (cima (ccnv cvol) cr)) (λ x3 . cr)) (wcel (cmpt (λ x3 . cr) (λ x3 . cfv (cima (cv x2) (csn (cv x3))) cvol)) cibl)) (λ x2 . cpw (cxp cr cr))) (λ x1 . citg (λ x2 . cr) (λ x2 . cfv (cima (cv x1) (csn (cv x2))) cvol))) ⟶ wceq cem (csu cn (λ x1 . co (co c1 (cv x1) cdiv) (cfv (co c1 (co c1 (cv x1) cdiv) caddc) clog) cmin)) ⟶ wceq czeta (crio (λ x1 . wral (λ x2 . wceq (co (co c1 (co c2 (co c1 (cv x2) cmin) ccxp) cmin) (cfv (cv x2) (cv x1)) cmul) (csu cn0 (λ x3 . co (csu (co cc0 (cv x3) cfz) (λ x4 . co (co (co (cneg c1) (cv x4) cexp) (co (cv x3) (cv x4) cbc) cmul) (co (co (cv x4) c1 caddc) (cv x2) ccxp) cmul)) (co c2 (co (cv x3) c1 caddc) cexp) cdiv))) (λ x2 . cdif cc (csn c1))) (λ x1 . co (cdif cc (csn c1)) cc ccncf)) ⟶ wceq clgam (cmpt (λ x1 . cdif cc (cdif cz cn)) (λ x1 . co (csu cn (λ x2 . co (co (cv x1) (cfv (co (co (cv x2) c1 caddc) (cv x2) cdiv) clog) cmul) (cfv (co (co (cv x1) (cv x2) cdiv) c1 caddc) clog) cmin)) (cfv (cv x1) clog) cmin)) ⟶ wceq cgam (ccom ce clgam) ⟶ wceq cigam (cmpt (λ x1 . cc) (λ x1 . cif (wcel (cv x1) (cdif cz cn)) cc0 (co c1 (cfv (cv x1) cgam) cdiv))) ⟶ wceq ccht (cmpt (λ x1 . cr) (λ x1 . csu (cin (co cc0 (cv x1) cicc) cprime) (λ x2 . cfv (cv x2) clog))) ⟶ wceq cvma (cmpt (λ x1 . cn) (λ x1 . csb (crab (λ x2 . wbr (cv x2) (cv x1) cdvds) (λ x2 . cprime)) (λ x2 . cif (wceq (cfv (cv x2) chash) c1) (cfv (cuni (cv x2)) clog) cc0))) ⟶ wceq cchp (cmpt (λ x1 . cr) (λ x1 . csu (co c1 (cfv (cv x1) cfl) cfz) (λ x2 . cfv (cv x2) cvma))) ⟶ x0) ⟶ x0
Theorem df_tayl : wceq ctayl (cmpt2 (λ x0 x1 . cpr cr cc) (λ x0 x1 . co cc (cv x0) cpm) (λ x0 x1 . cmpt2 (λ x2 x3 . cun cn0 (csn cpnf)) (λ x2 x3 . ciin (λ x4 . cin (co cc0 (cv x2) cicc) cz) (λ x4 . cdm (cfv (cv x4) (co (cv x0) (cv x1) cdvn)))) (λ x2 x3 . ciun (λ x4 . cc) (λ x4 . cxp (csn (cv x4)) (co ccnfld (cmpt (λ x5 . cin (co cc0 (cv x2) cicc) cz) (λ x5 . co (co (cfv (cv x3) (cfv (cv x5) (co (cv x0) (cv x1) cdvn))) (cfv (cv x5) cfa) cdiv) (co (co (cv x4) (cv x3) cmin) (cv x5) cexp) cmul)) ctsu))))) (proof)
Theorem df_ana : wceq cana (cmpt (λ x0 . cpr cr cc) (λ x0 . crab (λ x1 . wral (λ x2 . wcel (cv x2) (cfv (cdm (cin (cv x1) (co cpnf (cv x2) (co (cv x0) (cv x1) ctayl)))) (cfv (co (cfv ccnfld ctopn) (cv x0) crest) cnt))) (λ x2 . cdm (cv x1))) (λ x1 . co cc (cv x0) cpm))) (proof)
Theorem df_ulm : wceq culm (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wrex (λ x3 . w3a (wf (cfv (cv x3) cuz) (co cc (cv x0) cmap) (cv x1)) (wf (cv x0) cc (cv x2)) (wral (λ x4 . wrex (λ x5 . wral (λ x6 . wral (λ x7 . wbr (cfv (co (cfv (cv x7) (cfv (cv x6) (cv x1))) (cfv (cv x7) (cv x2)) cmin) cabs) (cv x4) clt) (λ x7 . cv x0)) (λ x6 . cfv (cv x5) cuz)) (λ x5 . cfv (cv x3) cuz)) (λ x4 . crp))) (λ x3 . cz)))) (proof)
Theorem df_log : wceq clog (ccnv (cres ce (cima (ccnv cim) (co (cneg cpi) cpi cioc)))) (proof)
Theorem df_cxp : wceq ccxp (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cc) (λ x0 x1 . cif (wceq (cv x0) cc0) (cif (wceq (cv x1) cc0) c1 cc0) (cfv (co (cv x1) (cfv (cv x0) clog) cmul) ce))) (proof)
Theorem df_logb : wceq clogb (cmpt2 (λ x0 x1 . cdif cc (cpr cc0 c1)) (λ x0 x1 . cdif cc (csn cc0)) (λ x0 x1 . co (cfv (cv x1) clog) (cfv (cv x0) clog) cdiv)) (proof)
Theorem df_asin : wceq casin (cmpt (λ x0 . cc) (λ x0 . co (cneg ci) (cfv (co (co ci (cv x0) cmul) (cfv (co c1 (co (cv x0) c2 cexp) cmin) csqrt) caddc) clog) cmul)) (proof)
Theorem df_acos : wceq cacos (cmpt (λ x0 . cc) (λ x0 . co (co cpi c2 cdiv) (cfv (cv x0) casin) cmin)) (proof)
Theorem df_atan : wceq catan (cmpt (λ x0 . cdif cc (cpr (cneg ci) ci)) (λ x0 . co (co ci c2 cdiv) (co (cfv (co c1 (co ci (cv x0) cmul) cmin) clog) (cfv (co c1 (co ci (cv x0) cmul) caddc) clog) cmin) cmul)) (proof)
Theorem df_area : wceq carea (cmpt (λ x0 . crab (λ x1 . wa (wral (λ x2 . wcel (cima (cv x1) (csn (cv x2))) (cima (ccnv cvol) cr)) (λ x2 . cr)) (wcel (cmpt (λ x2 . cr) (λ x2 . cfv (cima (cv x1) (csn (cv x2))) cvol)) cibl)) (λ x1 . cpw (cxp cr cr))) (λ x0 . citg (λ x1 . cr) (λ x1 . cfv (cima (cv x0) (csn (cv x1))) cvol))) (proof)
Theorem df_em : wceq cem (csu cn (λ x0 . co (co c1 (cv x0) cdiv) (cfv (co c1 (co c1 (cv x0) cdiv) caddc) clog) cmin)) (proof)
Theorem df_zeta : wceq czeta (crio (λ x0 . wral (λ x1 . wceq (co (co c1 (co c2 (co c1 (cv x1) cmin) ccxp) cmin) (cfv (cv x1) (cv x0)) cmul) (csu cn0 (λ x2 . co (csu (co cc0 (cv x2) cfz) (λ x3 . co (co (co (cneg c1) (cv x3) cexp) (co (cv x2) (cv x3) cbc) cmul) (co (co (cv x3) c1 caddc) (cv x1) ccxp) cmul)) (co c2 (co (cv x2) c1 caddc) cexp) cdiv))) (λ x1 . cdif cc (csn c1))) (λ x0 . co (cdif cc (csn c1)) cc ccncf)) (proof)
Theorem df_lgam : wceq clgam (cmpt (λ x0 . cdif cc (cdif cz cn)) (λ x0 . co (csu cn (λ x1 . co (co (cv x0) (cfv (co (co (cv x1) c1 caddc) (cv x1) cdiv) clog) cmul) (cfv (co (co (cv x0) (cv x1) cdiv) c1 caddc) clog) cmin)) (cfv (cv x0) clog) cmin)) (proof)
Theorem df_gam : wceq cgam (ccom ce clgam) (proof)
Theorem df_igam : wceq cigam (cmpt (λ x0 . cc) (λ x0 . cif (wcel (cv x0) (cdif cz cn)) cc0 (co c1 (cfv (cv x0) cgam) cdiv))) (proof)
Theorem df_cht : wceq ccht (cmpt (λ x0 . cr) (λ x0 . csu (cin (co cc0 (cv x0) cicc) cprime) (λ x1 . cfv (cv x1) clog))) (proof)
Theorem df_vma : wceq cvma (cmpt (λ x0 . cn) (λ x0 . csb (crab (λ x1 . wbr (cv x1) (cv x0) cdvds) (λ x1 . cprime)) (λ x1 . cif (wceq (cfv (cv x1) chash) c1) (cfv (cuni (cv x1)) clog) cc0))) (proof)
Theorem df_chp : wceq cchp (cmpt (λ x0 . cr) (λ x0 . csu (co c1 (cfv (cv x0) cfl) cfz) (λ x1 . cfv (cv x1) cvma))) (proof)