Proofgold Address

Known df_salgen__df_sumge0__df_mea__df_ome__df_caragen__df_ovoln__df_voln__df_smblfn__df_dfat__df_afv__df_aov__df_nelbr__df_iccp__df_pfx__df_fmtno__df_even__df_odd__df_gbe : ∀ x0 : ο . (wceq csalgen (cmpt (λ x1 . cvv) (λ x1 . cint (crab (λ x2 . wa (wceq (cuni (cv x2)) (cuni (cv x1))) (wss (cv x1) (cv x2))) (λ x2 . csalg)))) ⟶ wceq csumge0 (cmpt (λ x1 . cvv) (λ x1 . cif (wcel cpnf (crn (cv x1))) cpnf (csup (crn (cmpt (λ x2 . cin (cpw (cdm (cv x1))) cfn) (λ x2 . csu (cv x2) (λ x3 . cfv (cv x3) (cv x1))))) cxr clt))) ⟶ wceq cmea (cab (λ x1 . wa (wa (wa (wf (cdm (cv x1)) (co cc0 cpnf cicc) (cv x1)) (wcel (cdm (cv x1)) csalg)) (wceq (cfv c0 (cv x1)) cc0)) (wral (λ x2 . wa (wbr (cv x2) com cdom) (wdisj (λ x3 . cv x2) cv) ⟶ wceq (cfv (cuni (cv x2)) (cv x1)) (cfv (cres (cv x1) (cv x2)) csumge0)) (λ x2 . cpw (cdm (cv x1)))))) ⟶ wceq come (cab (λ x1 . wa (wa (wa (wa (wf (cdm (cv x1)) (co cc0 cpnf cicc) (cv x1)) (wceq (cdm (cv x1)) (cpw (cuni (cdm (cv x1)))))) (wceq (cfv c0 (cv x1)) cc0)) (wral (λ x2 . wral (λ x3 . wbr (cfv (cv x3) (cv x1)) (cfv (cv x2) (cv x1)) cle) (λ x3 . cpw (cv x2))) (λ x2 . cpw (cuni (cdm (cv x1)))))) (wral (λ x2 . wbr (cv x2) com cdom ⟶ wbr (cfv (cuni (cv x2)) (cv x1)) (cfv (cres (cv x1) (cv x2)) csumge0) cle) (λ x2 . cpw (cdm (cv x1)))))) ⟶ wceq ccaragen (cmpt (λ x1 . come) (λ x1 . crab (λ x2 . wral (λ x3 . wceq (co (cfv (cin (cv x3) (cv x2)) (cv x1)) (cfv (cdif (cv x3) (cv x2)) (cv x1)) cxad) (cfv (cv x3) (cv x1))) (λ x3 . cpw (cuni (cdm (cv x1))))) (λ x2 . cpw (cuni (cdm (cv x1)))))) ⟶ wceq covoln (cmpt (λ x1 . cfn) (λ x1 . cmpt (λ x2 . cpw (co cr (cv x1) cmap)) (λ x2 . cif (wceq (cv x1) c0) cc0 (cinf (crab (λ x3 . wrex (λ x4 . wa (wss (cv x2) (ciun (λ x5 . cn) (λ x5 . cixp (λ x6 . cv x1) (λ x6 . cfv (cv x6) (ccom cico (cfv (cv x5) (cv x4))))))) (wceq (cv x3) (cfv (cmpt (λ x5 . cn) (λ x5 . cprod (λ x6 . cv x1) (λ x6 . cfv (cfv (cv x6) (ccom cico (cfv (cv x5) (cv x4)))) cvol))) csumge0))) (λ x4 . co (co (cxp cr cr) (cv x1) cmap) cn cmap)) (λ x3 . cxr)) cxr clt)))) ⟶ wceq cvoln (cmpt (λ x1 . cfn) (λ x1 . cres (cfv (cv x1) covoln) (cfv (cfv (cv x1) covoln) ccaragen))) ⟶ wceq csmblfn (cmpt (λ x1 . csalg) (λ x1 . crab (λ x2 . wral (λ x3 . wcel (cima (ccnv (cv x2)) (co cmnf (cv x3) cioo)) (co (cv x1) (cdm (cv x2)) crest)) (λ x3 . cr)) (λ x2 . co cr (cuni (cv x1)) cpm))) ⟶ (∀ x1 x2 : ι → ο . wb (wdfat x1 x2) (wa (wcel x1 (cdm x2)) (wfun (cres x2 (csn x1))))) ⟶ (∀ x1 x2 : ι → ο . wceq (cafv x1 x2) (cif (wdfat x1 x2) (cio (λ x3 . wbr x1 (cv x3) x2)) cvv)) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (caov x1 x2 x3) (cafv (cop x1 x2) x3)) ⟶ wceq cnelbr (copab (λ x1 x2 . wn (wcel (cv x1) (cv x2)))) ⟶ wceq ciccp (cmpt (λ x1 . cn) (λ x1 . crab (λ x2 . wral (λ x3 . wbr (cfv (cv x3) (cv x2)) (cfv (co (cv x3) c1 caddc) (cv x2)) clt) (λ x3 . co cc0 (cv x1) cfzo)) (λ x2 . co cxr (co cc0 (cv x1) cfz) cmap))) ⟶ wceq cpfx (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cn0) (λ x1 x2 . co (cv x1) (cop cc0 (cv x2)) csubstr)) ⟶ wceq cfmtno (cmpt (λ x1 . cn0) (λ x1 . co (co c2 (co c2 (cv x1) cexp) cexp) c1 caddc)) ⟶ wceq ceven (crab (λ x1 . wcel (co (cv x1) c2 cdiv) cz) (λ x1 . cz)) ⟶ wceq codd (crab (λ x1 . wcel (co (co (cv x1) c1 caddc) c2 cdiv) cz) (λ x1 . cz)) ⟶ wceq cgbe (crab (λ x1 . wrex (λ x2 . wrex (λ x3 . w3a (wcel (cv x2) codd) (wcel (cv x3) codd) (wceq (cv x1) (co (cv x2) (cv x3) caddc))) (λ x3 . cprime)) (λ x2 . cprime)) (λ x1 . ceven)) ⟶ x0) ⟶ x0
Theorem df_salgen : wceq csalgen (cmpt (λ x0 . cvv) (λ x0 . cint (crab (λ x1 . wa (wceq (cuni (cv x1)) (cuni (cv x0))) (wss (cv x0) (cv x1))) (λ x1 . csalg)))) (proof)
Theorem df_sumge0 : wceq csumge0 (cmpt (λ x0 . cvv) (λ x0 . cif (wcel cpnf (crn (cv x0))) cpnf (csup (crn (cmpt (λ x1 . cin (cpw (cdm (cv x0))) cfn) (λ x1 . csu (cv x1) (λ x2 . cfv (cv x2) (cv x0))))) cxr clt))) (proof)
Theorem df_mea : wceq cmea (cab (λ x0 . wa (wa (wa (wf (cdm (cv x0)) (co cc0 cpnf cicc) (cv x0)) (wcel (cdm (cv x0)) csalg)) (wceq (cfv c0 (cv x0)) cc0)) (wral (λ x1 . wa (wbr (cv x1) com cdom) (wdisj (λ x2 . cv x1) cv) ⟶ wceq (cfv (cuni (cv x1)) (cv x0)) (cfv (cres (cv x0) (cv x1)) csumge0)) (λ x1 . cpw (cdm (cv x0)))))) (proof)
Theorem df_ome : wceq come (cab (λ x0 . wa (wa (wa (wa (wf (cdm (cv x0)) (co cc0 cpnf cicc) (cv x0)) (wceq (cdm (cv x0)) (cpw (cuni (cdm (cv x0)))))) (wceq (cfv c0 (cv x0)) cc0)) (wral (λ x1 . wral (λ x2 . wbr (cfv (cv x2) (cv x0)) (cfv (cv x1) (cv x0)) cle) (λ x2 . cpw (cv x1))) (λ x1 . cpw (cuni (cdm (cv x0)))))) (wral (λ x1 . wbr (cv x1) com cdom ⟶ wbr (cfv (cuni (cv x1)) (cv x0)) (cfv (cres (cv x0) (cv x1)) csumge0) cle) (λ x1 . cpw (cdm (cv x0)))))) (proof)
Theorem df_caragen : wceq ccaragen (cmpt (λ x0 . come) (λ x0 . crab (λ x1 . wral (λ x2 . wceq (co (cfv (cin (cv x2) (cv x1)) (cv x0)) (cfv (cdif (cv x2) (cv x1)) (cv x0)) cxad) (cfv (cv x2) (cv x0))) (λ x2 . cpw (cuni (cdm (cv x0))))) (λ x1 . cpw (cuni (cdm (cv x0)))))) (proof)
Theorem df_ovoln : wceq covoln (cmpt (λ x0 . cfn) (λ x0 . cmpt (λ x1 . cpw (co cr (cv x0) cmap)) (λ x1 . cif (wceq (cv x0) c0) cc0 (cinf (crab (λ x2 . wrex (λ x3 . wa (wss (cv x1) (ciun (λ x4 . cn) (λ x4 . cixp (λ x5 . cv x0) (λ x5 . cfv (cv x5) (ccom cico (cfv (cv x4) (cv x3))))))) (wceq (cv x2) (cfv (cmpt (λ x4 . cn) (λ x4 . cprod (λ x5 . cv x0) (λ x5 . cfv (cfv (cv x5) (ccom cico (cfv (cv x4) (cv x3)))) cvol))) csumge0))) (λ x3 . co (co (cxp cr cr) (cv x0) cmap) cn cmap)) (λ x2 . cxr)) cxr clt)))) (proof)
Theorem df_voln : wceq cvoln (cmpt (λ x0 . cfn) (λ x0 . cres (cfv (cv x0) covoln) (cfv (cfv (cv x0) covoln) ccaragen))) (proof)
Theorem df_smblfn : wceq csmblfn (cmpt (λ x0 . csalg) (λ x0 . crab (λ x1 . wral (λ x2 . wcel (cima (ccnv (cv x1)) (co cmnf (cv x2) cioo)) (co (cv x0) (cdm (cv x1)) crest)) (λ x2 . cr)) (λ x1 . co cr (cuni (cv x0)) cpm))) (proof)
Theorem df_dfat : ∀ x0 x1 : ι → ο . wb (wdfat x0 x1) (wa (wcel x0 (cdm x1)) (wfun (cres x1 (csn x0)))) (proof)
Theorem df_afv : ∀ x0 x1 : ι → ο . wceq (cafv x0 x1) (cif (wdfat x0 x1) (cio (λ x2 . wbr x0 (cv x2) x1)) cvv) (proof)
Theorem df_aov : ∀ x0 x1 x2 : ι → ο . wceq (caov x0 x1 x2) (cafv (cop x0 x1) x2) (proof)
Theorem df_nelbr : wceq cnelbr (copab (λ x0 x1 . wn (wcel (cv x0) (cv x1)))) (proof)
Theorem df_iccp : wceq ciccp (cmpt (λ x0 . cn) (λ x0 . crab (λ x1 . wral (λ x2 . wbr (cfv (cv x2) (cv x1)) (cfv (co (cv x2) c1 caddc) (cv x1)) clt) (λ x2 . co cc0 (cv x0) cfzo)) (λ x1 . co cxr (co cc0 (cv x0) cfz) cmap))) (proof)
Theorem df_pfx : wceq cpfx (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cn0) (λ x0 x1 . co (cv x0) (cop cc0 (cv x1)) csubstr)) (proof)
Theorem df_fmtno : wceq cfmtno (cmpt (λ x0 . cn0) (λ x0 . co (co c2 (co c2 (cv x0) cexp) cexp) c1 caddc)) (proof)
Theorem df_even : wceq ceven (crab (λ x0 . wcel (co (cv x0) c2 cdiv) cz) (λ x0 . cz)) (proof)
Theorem df_odd : wceq codd (crab (λ x0 . wcel (co (co (cv x0) c1 caddc) c2 cdiv) cz) (λ x0 . cz)) (proof)
Theorem df_gbe : wceq cgbe (crab (λ x0 . wrex (λ x1 . wrex (λ x2 . w3a (wcel (cv x1) codd) (wcel (cv x2) codd) (wceq (cv x0) (co (cv x1) (cv x2) caddc))) (λ x2 . cprime)) (λ x1 . cprime)) (λ x0 . ceven)) (proof)