Proofgold Asset

Known df_rtrcl__df_relexp__df_rtrclrec__df_shft__df_sgn__df_cj__df_re__df_im__df_sqrt__df_abs__df_limsup__df_clim__df_rlim__df_o1__df_lo1__df_sum__df_prod__df_risefac : ∀ x0 : ο . (wceq crtcl (cmpt (λ x1 . cvv) (λ x1 . cint (cab (λ x2 . w3a (wss (cres cid (cun (cdm (cv x1)) (crn (cv x1)))) (cv x2)) (wss (cv x1) (cv x2)) (wss (ccom (cv x2) (cv x2)) (cv x2)))))) ⟶ wceq crelexp (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cn0) (λ x1 x2 . cif (wceq (cv x2) cc0) (cres cid (cun (cdm (cv x1)) (crn (cv x1)))) (cfv (cv x2) (cseq (cmpt2 (λ x3 x4 . cvv) (λ x3 x4 . cvv) (λ x3 x4 . ccom (cv x3) (cv x1))) (cmpt (λ x3 . cvv) (λ x3 . cv x1)) c1)))) ⟶ wceq crtrcl (cmpt (λ x1 . cvv) (λ x1 . ciun (λ x2 . cn0) (λ x2 . co (cv x1) (cv x2) crelexp))) ⟶ wceq cshi (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cc) (λ x1 x2 . copab (λ x3 x4 . wa (wcel (cv x3) cc) (wbr (co (cv x3) (cv x2) cmin) (cv x4) (cv x1))))) ⟶ wceq csgn (cmpt (λ x1 . cxr) (λ x1 . cif (wceq (cv x1) cc0) cc0 (cif (wbr (cv x1) cc0 clt) (cneg c1) c1))) ⟶ wceq ccj (cmpt (λ x1 . cc) (λ x1 . crio (λ x2 . wa (wcel (co (cv x1) (cv x2) caddc) cr) (wcel (co ci (co (cv x1) (cv x2) cmin) cmul) cr)) (λ x2 . cc))) ⟶ wceq cre (cmpt (λ x1 . cc) (λ x1 . co (co (cv x1) (cfv (cv x1) ccj) caddc) c2 cdiv)) ⟶ wceq cim (cmpt (λ x1 . cc) (λ x1 . cfv (co (cv x1) ci cdiv) cre)) ⟶ wceq csqrt (cmpt (λ x1 . cc) (λ x1 . crio (λ x2 . w3a (wceq (co (cv x2) c2 cexp) (cv x1)) (wbr cc0 (cfv (cv x2) cre) cle) (wnel (co ci (cv x2) cmul) crp)) (λ x2 . cc))) ⟶ wceq cabs (cmpt (λ x1 . cc) (λ x1 . cfv (co (cv x1) (cfv (cv x1) ccj) cmul) csqrt)) ⟶ wceq clsp (cmpt (λ x1 . cvv) (λ x1 . cinf (crn (cmpt (λ x2 . cr) (λ x2 . csup (cin (cima (cv x1) (co (cv x2) cpnf cico)) cxr) cxr clt))) cxr clt)) ⟶ wceq cli (copab (λ x1 x2 . wa (wcel (cv x2) cc) (wral (λ x3 . wrex (λ x4 . wral (λ x5 . wa (wcel (cfv (cv x5) (cv x1)) cc) (wbr (cfv (co (cfv (cv x5) (cv x1)) (cv x2) cmin) cabs) (cv x3) clt)) (λ x5 . cfv (cv x4) cuz)) (λ x4 . cz)) (λ x3 . crp)))) ⟶ wceq crli (copab (λ x1 x2 . wa (wa (wcel (cv x1) (co cc cr cpm)) (wcel (cv x2) cc)) (wral (λ x3 . wrex (λ x4 . wral (λ x5 . wbr (cv x4) (cv x5) cle ⟶ wbr (cfv (co (cfv (cv x5) (cv x1)) (cv x2) cmin) cabs) (cv x3) clt) (λ x5 . cdm (cv x1))) (λ x4 . cr)) (λ x3 . crp)))) ⟶ wceq co1 (crab (λ x1 . wrex (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cfv (cfv (cv x4) (cv x1)) cabs) (cv x3) cle) (λ x4 . cin (cdm (cv x1)) (co (cv x2) cpnf cico))) (λ x3 . cr)) (λ x2 . cr)) (λ x1 . co cc cr cpm)) ⟶ wceq clo1 (crab (λ x1 . wrex (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cfv (cv x4) (cv x1)) (cv x3) cle) (λ x4 . cin (cdm (cv x1)) (co (cv x2) cpnf cico))) (λ x3 . cr)) (λ x2 . cr)) (λ x1 . co cr cr cpm)) ⟶ (∀ x1 x2 : ι → ι → ο . ∀ x3 . wceq (csu (x1 x3) x2) (cio (λ x4 . wo (wrex (λ x5 . wa (wss (x1 x3) (cfv (cv x5) cuz)) (wbr (cseq caddc (cmpt (λ x6 . cz) (λ x6 . cif (wcel (cv x6) (x1 x3)) (csb (cv x6) x2) cc0)) (cv x5)) (cv x4) cli)) (λ x5 . cz)) (wrex (λ x5 . wex (λ x6 . wa (wf1o (co c1 (cv x5) cfz) (x1 x3) (cv x6)) (wceq (cv x4) (cfv (cv x5) (cseq caddc (cmpt (λ x7 . cn) (λ x7 . csb (cfv (cv x7) (cv x6)) x2)) c1))))) (λ x5 . cn))))) ⟶ (∀ x1 x2 : ι → ι → ο . ∀ x3 . wceq (cprod x1 x2) (cio (λ x4 . wo (wrex (λ x5 . w3a (wss (x1 x3) (cfv (cv x5) cuz)) (wrex (λ x6 . wex (λ x7 . wa (wne (cv x7) cc0) (wbr (cseq cmul (cmpt (λ x8 . cz) (λ x8 . cif (wcel (cv x8) (x1 x8)) (x2 x8) c1)) (cv x6)) (cv x7) cli))) (λ x6 . cfv (cv x5) cuz)) (wbr (cseq cmul (cmpt (λ x6 . cz) (λ x6 . cif (wcel (cv x6) (x1 x6)) (x2 x6) c1)) (cv x5)) (cv x4) cli)) (λ x5 . cz)) (wrex (λ x5 . wex (λ x6 . wa (wf1o (co c1 (cv x5) cfz) (x1 x3) (cv x6)) (wceq (cv x4) (cfv (cv x5) (cseq cmul (cmpt (λ x7 . cn) (λ x7 . csb (cfv (cv x7) (cv x6)) x2)) c1))))) (λ x5 . cn))))) ⟶ wceq crisefac (cmpt2 (λ x1 x2 . cc) (λ x1 x2 . cn0) (λ x1 x2 . cprod (λ x3 . co cc0 (co (cv x2) c1 cmin) cfz) (λ x3 . co (cv x1) (cv x3) caddc))) ⟶ x0) ⟶ x0
Theorem df_rtrcl : wceq crtcl (cmpt (λ x0 . cvv) (λ x0 . cint (cab (λ x1 . w3a (wss (cres cid (cun (cdm (cv x0)) (crn (cv x0)))) (cv x1)) (wss (cv x0) (cv x1)) (wss (ccom (cv x1) (cv x1)) (cv x1)))))) (proof)
Theorem df_relexp : wceq crelexp (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cn0) (λ x0 x1 . cif (wceq (cv x1) cc0) (cres cid (cun (cdm (cv x0)) (crn (cv x0)))) (cfv (cv x1) (cseq (cmpt2 (λ x2 x3 . cvv) (λ x2 x3 . cvv) (λ x2 x3 . ccom (cv x2) (cv x0))) (cmpt (λ x2 . cvv) (λ x2 . cv x0)) c1)))) (proof)
Theorem df_rtrclrec : wceq crtrcl (cmpt (λ x0 . cvv) (λ x0 . ciun (λ x1 . cn0) (λ x1 . co (cv x0) (cv x1) crelexp))) (proof)
Theorem df_shft : wceq cshi (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cc) (λ x0 x1 . copab (λ x2 x3 . wa (wcel (cv x2) cc) (wbr (co (cv x2) (cv x1) cmin) (cv x3) (cv x0))))) (proof)
Theorem df_sgn : wceq csgn (cmpt (λ x0 . cxr) (λ x0 . cif (wceq (cv x0) cc0) cc0 (cif (wbr (cv x0) cc0 clt) (cneg c1) c1))) (proof)
Theorem df_cj : wceq ccj (cmpt (λ x0 . cc) (λ x0 . crio (λ x1 . wa (wcel (co (cv x0) (cv x1) caddc) cr) (wcel (co ci (co (cv x0) (cv x1) cmin) cmul) cr)) (λ x1 . cc))) (proof)
Theorem df_re : wceq cre (cmpt (λ x0 . cc) (λ x0 . co (co (cv x0) (cfv (cv x0) ccj) caddc) c2 cdiv)) (proof)
Theorem df_im : wceq cim (cmpt (λ x0 . cc) (λ x0 . cfv (co (cv x0) ci cdiv) cre)) (proof)
Theorem df_sqrt : wceq csqrt (cmpt (λ x0 . cc) (λ x0 . crio (λ x1 . w3a (wceq (co (cv x1) c2 cexp) (cv x0)) (wbr cc0 (cfv (cv x1) cre) cle) (wnel (co ci (cv x1) cmul) crp)) (λ x1 . cc))) (proof)
Theorem df_abs : wceq cabs (cmpt (λ x0 . cc) (λ x0 . cfv (co (cv x0) (cfv (cv x0) ccj) cmul) csqrt)) (proof)
Theorem df_limsup : wceq clsp (cmpt (λ x0 . cvv) (λ x0 . cinf (crn (cmpt (λ x1 . cr) (λ x1 . csup (cin (cima (cv x0) (co (cv x1) cpnf cico)) cxr) cxr clt))) cxr clt)) (proof)
Theorem df_clim : wceq cli (copab (λ x0 x1 . wa (wcel (cv x1) cc) (wral (λ x2 . wrex (λ x3 . wral (λ x4 . wa (wcel (cfv (cv x4) (cv x0)) cc) (wbr (cfv (co (cfv (cv x4) (cv x0)) (cv x1) cmin) cabs) (cv x2) clt)) (λ x4 . cfv (cv x3) cuz)) (λ x3 . cz)) (λ x2 . crp)))) (proof)
Theorem df_rlim : wceq crli (copab (λ x0 x1 . wa (wa (wcel (cv x0) (co cc cr cpm)) (wcel (cv x1) cc)) (wral (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cv x3) (cv x4) cle ⟶ wbr (cfv (co (cfv (cv x4) (cv x0)) (cv x1) cmin) cabs) (cv x2) clt) (λ x4 . cdm (cv x0))) (λ x3 . cr)) (λ x2 . crp)))) (proof)
Theorem df_o1 : wceq co1 (crab (λ x0 . wrex (λ x1 . wrex (λ x2 . wral (λ x3 . wbr (cfv (cfv (cv x3) (cv x0)) cabs) (cv x2) cle) (λ x3 . cin (cdm (cv x0)) (co (cv x1) cpnf cico))) (λ x2 . cr)) (λ x1 . cr)) (λ x0 . co cc cr cpm)) (proof)
Theorem df_lo1 : wceq clo1 (crab (λ x0 . wrex (λ x1 . wrex (λ x2 . wral (λ x3 . wbr (cfv (cv x3) (cv x0)) (cv x2) cle) (λ x3 . cin (cdm (cv x0)) (co (cv x1) cpnf cico))) (λ x2 . cr)) (λ x1 . cr)) (λ x0 . co cr cr cpm)) (proof)
Theorem df_sum : ∀ x0 x1 : ι → ι → ο . ∀ x2 . wceq (csu (x0 x2) x1) (cio (λ x3 . wo (wrex (λ x4 . wa (wss (x0 x2) (cfv (cv x4) cuz)) (wbr (cseq caddc (cmpt (λ x5 . cz) (λ x5 . cif (wcel (cv x5) (x0 x2)) (csb (cv x5) x1) cc0)) (cv x4)) (cv x3) cli)) (λ x4 . cz)) (wrex (λ x4 . wex (λ x5 . wa (wf1o (co c1 (cv x4) cfz) (x0 x2) (cv x5)) (wceq (cv x3) (cfv (cv x4) (cseq caddc (cmpt (λ x6 . cn) (λ x6 . csb (cfv (cv x6) (cv x5)) x1)) c1))))) (λ x4 . cn)))) (proof)
Theorem df_prod : ∀ x0 x1 : ι → ι → ο . ∀ x2 . wceq (cprod x0 x1) (cio (λ x3 . wo (wrex (λ x4 . w3a (wss (x0 x2) (cfv (cv x4) cuz)) (wrex (λ x5 . wex (λ x6 . wa (wne (cv x6) cc0) (wbr (cseq cmul (cmpt (λ x7 . cz) (λ x7 . cif (wcel (cv x7) (x0 x7)) (x1 x7) c1)) (cv x5)) (cv x6) cli))) (λ x5 . cfv (cv x4) cuz)) (wbr (cseq cmul (cmpt (λ x5 . cz) (λ x5 . cif (wcel (cv x5) (x0 x5)) (x1 x5) c1)) (cv x4)) (cv x3) cli)) (λ x4 . cz)) (wrex (λ x4 . wex (λ x5 . wa (wf1o (co c1 (cv x4) cfz) (x0 x2) (cv x5)) (wceq (cv x3) (cfv (cv x4) (cseq cmul (cmpt (λ x6 . cn) (λ x6 . csb (cfv (cv x6) (cv x5)) x1)) c1))))) (λ x4 . cn)))) (proof)
Theorem df_risefac : wceq crisefac (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cn0) (λ x0 x1 . cprod (λ x2 . co cc0 (co (cv x1) c1 cmin) cfz) (λ x2 . co (cv x0) (cv x2) caddc))) (proof)