Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNeb../4b50d..
PUaCs../4e914..
vout
PrNeb../57ce0.. 0.00 bars
TMTLQ../30d27.. ownership of 73d02.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNVD../8f1ef.. ownership of 5a43b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbKX../f9384.. ownership of 881af.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY9p../83732.. ownership of 31602.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEyM../b781b.. ownership of 56b91.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRA4../bf13b.. ownership of 94f6b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVsi../28143.. ownership of 34adf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLmj../0ce8b.. ownership of 4d750.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYDh../1304d.. ownership of 894e6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa83../85c16.. ownership of 03f29.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMErJ../82909.. ownership of dfa13.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbvX../a5527.. ownership of dae74.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUXM../295e8.. ownership of 168dc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG8R../efe37.. ownership of d1933.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVQj../75e76.. ownership of d3df9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaeH../42e86.. ownership of 59ffd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN5C../64443.. ownership of c8753.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMUN../9e815.. ownership of 23930.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFrx../72bfa.. ownership of 6291c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFRG../a5206.. ownership of 91927.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGQF../23ea4.. ownership of ccbc7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEi6../7ea20.. ownership of ec23b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNM4../0d016.. ownership of da7b3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdcs../faa76.. ownership of 89e29.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPS9../6a1eb.. ownership of 8747c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW6C../49b99.. ownership of 2bda8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR8z../928af.. ownership of e4d7f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRuW../338d4.. ownership of b6333.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYw7../a70e2.. ownership of 1dafb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT2b../8ecc0.. ownership of d7879.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNRQ../6a4e3.. ownership of 351c3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLif../4e1e9.. ownership of 79e88.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQA3../c3966.. ownership of 46c6a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSMd../43b49.. ownership of ce127.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWWk../e36ce.. ownership of 7edab.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML12../e299b.. ownership of 53941.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMeY../9fe09.. ownership of a6f8f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSav../c6dcf.. ownership of e771c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSPj../99781.. ownership of 0ccbf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJBj../cc1ce.. ownership of 0f1dd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHBw../f996b.. ownership of 54897.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNY3../de3cd.. ownership of 5e9d5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTLt../fe91c.. ownership of 8134e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYcK../b967e.. ownership of d6bc3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPHY../198f4.. ownership of e4db6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXGT../c99d3.. ownership of cfc36.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMuU../f7b0c.. ownership of 78206.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRzf../31a89.. ownership of f34ad.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRyM../31207.. ownership of 080bd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMP8../06830.. ownership of 882e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHpT../89665.. ownership of 9bb14.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHfE../b8afe.. ownership of 01b56.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbMH../9f55b.. ownership of ff041.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML6w../c23d2.. ownership of 9a1d6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZSS../bec60.. ownership of 5211d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHof../e41bf.. ownership of 3bbef.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKar../b8553.. ownership of f9fad.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFKt../e0e17.. ownership of 6e4ff.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMxw../83822.. ownership of b65ee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXTY../5e229.. ownership of 57960.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWgU../1885c.. ownership of b0c29.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbQD../a7ce0.. ownership of 8e63a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNGD../9bfab.. ownership of b904d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbSZ../dedd3.. ownership of 1a3b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb6D../65c8e.. ownership of 42258.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMjM../b7048.. ownership of 0d9bf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbpp../a756c.. ownership of ca69e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMmp../26b07.. ownership of 33594.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbbB../2b608.. ownership of b5ed6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN5m../258d5.. ownership of 85a86.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPBC../2d1fe.. ownership of 8912c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXey../f7bbb.. ownership of f1347.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML36../2b431.. ownership of 1e9ba.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ8p../5d0f5.. ownership of 4be05.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbNM../71266.. ownership of d8721.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRGo../d5ffa.. ownership of 3ecd9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdh9../a6935.. ownership of 2c425.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRtu../8a448.. ownership of f8168.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVoo../80b3c.. ownership of a8c42.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM2Y../c5c24.. ownership of 6c208.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTU8../de8a8.. ownership of 79ab2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF1Z../0da0e.. ownership of 57767.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb8w../cf079.. ownership of c7e3d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMjk../83d8e.. ownership of 49f3c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJDv../b07ae.. ownership of 1932b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR6t../c6a61.. ownership of a00d0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF7L../45b0d.. ownership of b63e9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNxt../bb57e.. ownership of 4dacc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcrE../6aad6.. ownership of 80a5b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYGG../b76b5.. ownership of 6df04.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRzJ../70ce9.. ownership of 2fac0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLwh../5e846.. ownership of 7f97c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJHE../9d291.. ownership of 15fd0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTPf../8bd1c.. ownership of af0b1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVg6../241fd.. ownership of 4f721.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcBz../94f55.. ownership of efd7d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaxh../d7bd1.. ownership of 31582.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaW9../94e5c.. ownership of b3da9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZre../b6a04.. ownership of 48968.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJUp../5b580.. ownership of 4929c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGwi../8b548.. ownership of 37e7d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdTV../9d0d9.. ownership of d25bf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQne../2de7f.. ownership of 886f5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP7U../ff5e6.. ownership of 66d2d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUNr2../7a3db.. doc published by PrGxv..
Param SNoSNo : ιο
Param SNoLeSNoLe : ιιο
Param mul_SNomul_SNo : ιιι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Param SNoLtSNoLt : ιιο
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Known SNo_0SNo_0 : SNo 0
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0
Known neg_mul_SNo_Ltneg_mul_SNo_Lt : ∀ x0 x1 x2 . SNo x0SNoLt x0 0SNo x1SNo x2SNoLt x2 x1SNoLt (mul_SNo x0 x1) (mul_SNo x0 x2)
Known nonneg_mul_SNo_Lenonneg_mul_SNo_Le : ∀ x0 x1 x2 . SNo x0SNoLe 0 x0SNo x1SNo x2SNoLe x1 x2SNoLe (mul_SNo x0 x1) (mul_SNo x0 x2)
Theorem SNo_sqr_nonnegSNo_sqr_nonneg : ∀ x0 . SNo x0SNoLe 0 (mul_SNo x0 x0) (proof)
Known SNoLt_trichotomy_or_impredSNoLt_trichotomy_or_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (SNoLt x0 x1x2)(x0 = x1x2)(SNoLt x1 x0x2)x2
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known mul_SNo_neg_negmul_SNo_neg_neg : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 0SNoLt x1 0SNoLt 0 (mul_SNo x0 x1)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known mul_SNo_pos_posmul_SNo_pos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt 0 x1SNoLt 0 (mul_SNo x0 x1)
Theorem SNo_zero_or_sqr_posSNo_zero_or_sqr_pos : ∀ x0 . SNo x0or (x0 = 0) (SNoLt 0 (mul_SNo x0 x0)) (proof)
Param CSNoCSNo : ιο
Param CSNo_ReCSNo_Re : ιι
Param SNo_pairSNo_pair : ιιι
Param minus_SNominus_SNo : ιι
Param CSNo_ImCSNo_Im : ιι
Definition minus_CSNominus_CSNo := λ x0 . SNo_pair (minus_SNo (CSNo_Re x0)) (minus_SNo (CSNo_Im x0))
Known CSNo_Re2CSNo_Re2 : ∀ x0 x1 . SNo x0SNo x1CSNo_Re (SNo_pair x0 x1) = x0
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known CSNo_ReRCSNo_ReR : ∀ x0 . CSNo x0SNo (CSNo_Re x0)
Known CSNo_ImRCSNo_ImR : ∀ x0 . CSNo x0SNo (CSNo_Im x0)
Theorem 31582..minus_CSNo_CRe : ∀ x0 . CSNo x0CSNo_Re (minus_CSNo x0) = minus_SNo (CSNo_Re x0) (proof)
Known CSNo_Im2CSNo_Im2 : ∀ x0 x1 . SNo x0SNo x1CSNo_Im (SNo_pair x0 x1) = x1
Theorem 4f721..minus_CSNo_CIm : ∀ x0 . CSNo x0CSNo_Im (minus_CSNo x0) = minus_SNo (CSNo_Im x0) (proof)
Param add_SNoadd_SNo : ιιι
Definition add_CSNoadd_CSNo := λ x0 x1 . SNo_pair (add_SNo (CSNo_Re x0) (CSNo_Re x1)) (add_SNo (CSNo_Im x0) (CSNo_Im x1))
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Theorem 15fd0..add_CSNo_CRe : ∀ x0 x1 . CSNo x0CSNo x1CSNo_Re (add_CSNo x0 x1) = add_SNo (CSNo_Re x0) (CSNo_Re x1) (proof)
Theorem 2fac0..add_CSNo_CIm : ∀ x0 x1 . CSNo x0CSNo x1CSNo_Im (add_CSNo x0 x1) = add_SNo (CSNo_Im x0) (CSNo_Im x1) (proof)
Known CSNo_ReIm_splitCSNo_ReIm_split : ∀ x0 x1 . CSNo x0CSNo x1CSNo_Re x0 = CSNo_Re x1CSNo_Im x0 = CSNo_Im x1x0 = x1
Known CSNo_add_CSNoCSNo_add_CSNo : ∀ x0 x1 . CSNo x0CSNo x1CSNo (add_CSNo x0 x1)
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
Theorem 80a5b..add_CSNo_com : ∀ x0 x1 . CSNo x0CSNo x1add_CSNo x0 x1 = add_CSNo x1 x0 (proof)
Known f_eq_if_eq_i : ∀ x0 : ι → ι . ∀ x1 x2 . x1 = x2x0 x1 = x0 x2
Known add_SNo_assocadd_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Theorem b63e9..add_CSNo_assoc : ∀ x0 x1 x2 . CSNo x0CSNo x1CSNo x2add_CSNo x0 (add_CSNo x1 x2) = add_CSNo (add_CSNo x0 x1) x2 (proof)
Known add_SNo_com_4_inner_midadd_SNo_com_4_inner_mid : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3add_SNo (add_SNo x0 x1) (add_SNo x2 x3) = add_SNo (add_SNo x0 x2) (add_SNo x1 x3)
Theorem add_SNo_rotate_4_0312add_SNo_rotate_4_0312 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3add_SNo (add_SNo x0 x1) (add_SNo x2 x3) = add_SNo (add_SNo x0 x3) (add_SNo x1 x2) (proof)
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Theorem c7e3d..mul_CSNo_ReR : ∀ x0 x1 . CSNo x0CSNo x1SNo (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x1)) (minus_SNo (mul_SNo (CSNo_Im x0) (CSNo_Im x1)))) (proof)
Theorem 79ab2..mul_CSNo_ImR : ∀ x0 x1 . CSNo x0CSNo x1SNo (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Im x1)) (mul_SNo (CSNo_Im x0) (CSNo_Re x1))) (proof)
Definition mul_CSNomul_CSNo := λ x0 x1 . SNo_pair (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x1)) (minus_SNo (mul_SNo (CSNo_Im x0) (CSNo_Im x1)))) (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Im x1)) (mul_SNo (CSNo_Im x0) (CSNo_Re x1)))
Theorem a8c42..mul_CSNo_CRe : ∀ x0 x1 . CSNo x0CSNo x1CSNo_Re (mul_CSNo x0 x1) = add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x1)) (minus_SNo (mul_SNo (CSNo_Im x0) (CSNo_Im x1))) (proof)
Theorem 2c425..mul_CSNo_CIm : ∀ x0 x1 . CSNo x0CSNo x1CSNo_Im (mul_CSNo x0 x1) = add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Im x1)) (mul_SNo (CSNo_Im x0) (CSNo_Re x1)) (proof)
Known CSNo_ICSNo_I : ∀ x0 x1 . SNo x0SNo x1CSNo (SNo_pair x0 x1)
Theorem d8721..CSNo_mul_CSNo : ∀ x0 x1 . CSNo x0CSNo x1CSNo (mul_CSNo x0 x1) (proof)
Known mul_SNo_commul_SNo_com : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_SNo x1 x0
Theorem 1e9ba..mul_CSNo_com : ∀ x0 x1 . CSNo x0CSNo x1mul_CSNo x0 x1 = mul_CSNo x1 x0 (proof)
Known mul_SNo_distrLmul_SNo_distrL : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (add_SNo x1 x2) = add_SNo (mul_SNo x0 x1) (mul_SNo x0 x2)
Known mul_SNo_minus_distrRmul_minus_SNo_distrR : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)
Known minus_add_SNo_distrminus_add_SNo_distr : ∀ x0 x1 . SNo x0SNo x1minus_SNo (add_SNo x0 x1) = add_SNo (minus_SNo x0) (minus_SNo x1)
Known SNo_mul_SNo_3SNo_mul_SNo_3 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNo (mul_SNo x0 (mul_SNo x1 x2))
Known mul_SNo_assocmul_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Known mul_SNo_minus_distrLmul_SNo_minus_distrL : ∀ x0 x1 . SNo x0SNo x1mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1)
Known mul_SNo_distrRmul_SNo_distrR : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo (add_SNo x0 x1) x2 = add_SNo (mul_SNo x0 x2) (mul_SNo x1 x2)
Theorem 8912c..mul_CSNo_assoc : ∀ x0 x1 x2 . CSNo x0CSNo x1CSNo x2mul_CSNo x0 (mul_CSNo x1 x2) = mul_CSNo (mul_CSNo x0 x1) x2 (proof)
Known SNo_CSNoSNo_CSNo : ∀ x0 . SNo x0CSNo x0
Theorem b5ed6..CSNo_0 : CSNo 0 (proof)
Param ordsuccordsucc : ιι
Known SNo_1SNo_1 : SNo 1
Theorem ca69e..CSNo_1 : CSNo 1 (proof)
Known SNo_pair_0SNo_pair_0 : ∀ x0 . SNo_pair x0 0 = x0
Known mul_SNo_oneLmul_SNo_oneL : ∀ x0 . SNo x0mul_SNo 1 x0 = x0
Known minus_SNo_0minus_SNo_0 : minus_SNo 0 = 0
Known mul_SNo_zeroLmul_SNo_zeroL : ∀ x0 . SNo x0mul_SNo 0 x0 = 0
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Theorem 42258..mul_CSNo_oneL : ∀ x0 . CSNo x0mul_CSNo 1 x0 = x0 (proof)
Theorem b904d..mul_CSNo_distrL : ∀ x0 x1 x2 . CSNo x0CSNo x1CSNo x2mul_CSNo x0 (add_CSNo x1 x2) = add_CSNo (mul_CSNo x0 x1) (mul_CSNo x0 x2) (proof)
Theorem b0c29.. : ∀ x0 x1 x2 . CSNo x0CSNo x1CSNo x2mul_CSNo (add_CSNo x0 x1) x2 = add_CSNo (mul_CSNo x0 x2) (mul_CSNo x1 x2) (proof)
Known SNo_ReSNo_Re : ∀ x0 . SNo x0CSNo_Re x0 = x0
Known SNo_ImSNo_Im : ∀ x0 . SNo x0CSNo_Im x0 = 0
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0
Theorem 15de6..mul_SNo_mul_CSNo : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_CSNo x0 x1 (proof)
Definition Complex_iComplex_i := SNo_pair 0 1
Known SNo_Complex_iSNo_Complex_i : CSNo Complex_i
Known CSNo_minus_CSNoCSNo_minus_CSNo : ∀ x0 . CSNo x0CSNo (minus_CSNo x0)
Known Re_iRe_i : CSNo_Re Complex_i = 0
Known Im_iIm_i : CSNo_Im Complex_i = 1
Known Re_1Re_1 : CSNo_Re 1 = 1
Known Im_1Im_1 : CSNo_Im 1 = 0
Theorem b65ee..Complex_i_sqr : mul_CSNo Complex_i Complex_i = minus_CSNo 1 (proof)
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known mul_SNo_com_3_0_1mul_SNo_com_3_0_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo x1 (mul_SNo x0 x2)
Known add_SNo_minus_SNo_linvadd_SNo_minus_SNo_linv : ∀ x0 . SNo x0add_SNo (minus_SNo x0) x0 = 0
Theorem f9fad..CSNo_relative_recip : ∀ x0 . CSNo x0∀ x1 . SNo x1mul_SNo (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Im x0))) x1 = 1mul_CSNo x0 (add_CSNo (mul_CSNo x1 (CSNo_Re x0)) (minus_CSNo (mul_CSNo Complex_i (mul_CSNo x1 (CSNo_Im x0))))) = 1 (proof)
Param lamSigma : ι(ιι) → ι
Definition setprodsetprod := λ x0 x1 . lam x0 (λ x2 . x1)
Param realreal : ι
Param apap : ιιι
Definition complexcomplex := {SNo_pair (ap x0 0) (ap x0 1)|x0 ∈ setprod real real}
Param If_iIf_i : οιιι
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Known tuple_2_setprodtuple_2_setprod : ∀ x0 x1 x2 . x2x0∀ x3 . x3x1lam 2 (λ x4 . If_i (x4 = 0) x2 x3)setprod x0 x1
Theorem complex_Icomplex_I : ∀ x0 . x0real∀ x1 . x1realSNo_pair x0 x1complex (proof)
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Known ap0_Sigmaap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 0x0
Known ap1_Sigmaap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 1x1 (ap x2 0)
Theorem complex_Ecomplex_E : ∀ x0 . x0complex∀ x1 : ο . (∀ x2 . x2real∀ x3 . x3realx0 = SNo_pair x2 x3x1)x1 (proof)
Known real_SNoreal_SNo : ∀ x0 . x0realSNo x0
Theorem complex_CSNocomplex_CSNo : ∀ x0 . x0complexCSNo x0 (proof)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known real_0real_0 : 0real
Theorem real_complexreal_complex : realcomplex (proof)
Theorem complex_0complex_0 : 0complex (proof)
Known real_1real_1 : 1real
Theorem complex_1complex_1 : 1complex (proof)
Theorem complex_icomplex_i : Complex_icomplex (proof)
Theorem complex_Re_eqcomplex_Re_eq : ∀ x0 . x0real∀ x1 . x1realCSNo_Re (SNo_pair x0 x1) = x0 (proof)
Theorem complex_Im_eqcomplex_Im_eq : ∀ x0 . x0real∀ x1 . x1realCSNo_Im (SNo_pair x0 x1) = x1 (proof)
Known CSNo_ReImCSNo_ReIm : ∀ x0 . CSNo x0x0 = SNo_pair (CSNo_Re x0) (CSNo_Im x0)
Theorem a6f8f.. : ∀ x0 . x0complexx0 = SNo_pair (CSNo_Re x0) (CSNo_Im x0) (proof)
Theorem complex_Re_realcomplex_Re_real : ∀ x0 . x0complexCSNo_Re x0real (proof)
Theorem complex_Im_realcomplex_Im_real : ∀ x0 . x0complexCSNo_Im x0real (proof)
Theorem complex_ReIm_splitcomplex_ReIm_split : ∀ x0 . x0complex∀ x1 . x1complexCSNo_Re x0 = CSNo_Re x1CSNo_Im x0 = CSNo_Im x1x0 = x1 (proof)
Known real_minus_SNoreal_minus_SNo : ∀ x0 . x0realminus_SNo x0real
Theorem complex_minus_CSNocomplex_minus_CSNo : ∀ x0 . x0complexminus_CSNo x0complex (proof)
Known real_add_SNoreal_add_SNo : ∀ x0 . x0real∀ x1 . x1realadd_SNo x0 x1real
Theorem complex_add_CSNocomplex_add_CSNo : ∀ x0 . x0complex∀ x1 . x1complexadd_CSNo x0 x1complex (proof)
Known real_mul_SNoreal_mul_SNo : ∀ x0 . x0real∀ x1 . x1realmul_SNo x0 x1real
Theorem complex_mul_CSNocomplex_mul_CSNo : ∀ x0 . x0complex∀ x1 . x1complexmul_CSNo x0 x1complex (proof)
Theorem real_Re_eqreal_Re_eq : ∀ x0 . x0realCSNo_Re x0 = x0 (proof)
Theorem real_Im_eqreal_Im_eq : ∀ x0 . x0realCSNo_Im x0 = 0 (proof)
Theorem mul_i_real_eqmul_i_real_eq : ∀ x0 . x0realmul_CSNo Complex_i x0 = SNo_pair 0 x0 (proof)
Theorem real_Re_i_eqreal_Re_i_eq : ∀ x0 . x0realCSNo_Re (mul_CSNo Complex_i x0) = 0 (proof)
Theorem real_Im_i_eqreal_Im_i_eq : ∀ x0 . x0realCSNo_Im (mul_CSNo Complex_i x0) = x0 (proof)
Theorem complex_etacomplex_eta : ∀ x0 . x0complexx0 = add_CSNo (CSNo_Re x0) (mul_CSNo Complex_i (CSNo_Im x0)) (proof)
Theorem dfa13.. : ∀ x0 . x0real∀ x1 . x1realadd_CSNo x0 (mul_CSNo Complex_i x1)complex (proof)
Theorem 894e6.. : ∀ x0 . x0complex∀ x1 : ο . (∀ x2 . x2real∀ x3 . x3realx0 = add_CSNo x2 (mul_CSNo Complex_i x3)x1)x1 (proof)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known nonzero_real_recip_exnonzero_real_recip_ex : ∀ x0 . x0real(x0 = 0∀ x1 : ο . x1)∀ x1 : ο . (∀ x2 . and (x2real) (mul_SNo x0 x2 = 1)x1)x1
Known Re_0Re_0 : CSNo_Re 0 = 0
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known SNoLtLe_traSNoLtLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLe x1 x2SNoLt x0 x2
Known add_SNo_Le2add_SNo_Le2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x1 x2SNoLe (add_SNo x0 x1) (add_SNo x0 x2)
Known Im_0Im_0 : CSNo_Im 0 = 0
Known add_SNo_Le1add_SNo_Le1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x2SNoLe (add_SNo x0 x1) (add_SNo x2 x1)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem nonzero_complex_recip_exnonzero_complex_recip_ex : ∀ x0 . x0complex(x0 = 0∀ x1 : ο . x1)∀ x1 : ο . (∀ x2 . and (x2complex) (mul_CSNo x0 x2 = 1)x1)x1 (proof)
Param SepSep : ι(ιο) → ι
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2)
Theorem complex_real_set_eqcomplex_real_set_eq : real = {x1 ∈ complex|CSNo_Re x1 = x1} (proof)
Param explicit_Fieldexplicit_Field : ιιι(ιιι) → (ιιι) → ο
Known explicit_Field_Iexplicit_Field_I : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . (∀ x5 . x5x0∀ x6 . x6x0x3 x5 x6x0)(∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0x3 x5 (x3 x6 x7) = x3 (x3 x5 x6) x7)(∀ x5 . x5x0∀ x6 . x6x0x3 x5 x6 = x3 x6 x5)x1x0(∀ x5 . x5x0x3 x1 x5 = x5)(∀ x5 . x5x0∀ x6 : ο . (∀ x7 . and (x7x0) (x3 x5 x7 = x1)x6)x6)(∀ x5 . x5x0∀ x6 . x6x0x4 x5 x6x0)(∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0x4 x5 (x4 x6 x7) = x4 (x4 x5 x6) x7)(∀ x5 . x5x0∀ x6 . x6x0x4 x5 x6 = x4 x6 x5)x2x0(x2 = x1∀ x5 : ο . x5)(∀ x5 . x5x0x4 x2 x5 = x5)(∀ x5 . x5x0(x5 = x1∀ x6 : ο . x6)∀ x6 : ο . (∀ x7 . and (x7x0) (x4 x5 x7 = x2)x6)x6)(∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7))explicit_Field x0 x1 x2 x3 x4
Known add_CSNo_0Ladd_CSNo_0L : ∀ x0 . CSNo x0add_CSNo 0 x0 = x0
Known add_CSNo_minus_CSNo_rinvadd_CSNo_minus_CSNo_rinv : ∀ x0 . CSNo x0add_CSNo x0 (minus_CSNo x0) = 0
Known neq_1_0neq_1_0 : 1 = 0∀ x0 : ο . x0
Theorem 881af.. : explicit_Field complex 0 1 add_CSNo mul_CSNo (proof)
Param explicit_Complexexplicit_Complex : ι(ιι) → (ιι) → ιιι(ιιι) → (ιιι) → ο
Param explicit_Realsexplicit_Reals : ιιι(ιιι) → (ιιι) → (ιιο) → ο
Known explicit_Complex_Iexplicit_Complex_I : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 x5 . ∀ x6 x7 : ι → ι → ι . explicit_Field x0 x3 x4 x6 x7(∀ x8 : ο . (∀ x9 : ι → ι → ο . explicit_Reals {x10 ∈ x0|x1 x10 = x10} x3 x4 x6 x7 x9x8)x8)(∀ x8 . x8x0x2 x8{x9 ∈ x0|x1 x9 = x9})x5x0(∀ x8 . x8x0x1 x8x0)(∀ x8 . x8x0x2 x8x0)(∀ x8 . x8x0x8 = x6 (x1 x8) (x7 x5 (x2 x8)))(∀ x8 . x8x0∀ x9 . x9x0x1 x8 = x1 x9x2 x8 = x2 x9x8 = x9)x6 (x7 x5 x5) x4 = x3explicit_Complex x0 x1 x2 x3 x4 x5 x6 x7
Param bijbij : ιι(ιι) → ο
Param iffiff : οοο
Known explicit_Reals_transferexplicit_Reals_transfer : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 x7 x8 . ∀ x9 x10 : ι → ι → ι . ∀ x11 : ι → ι → ο . ∀ x12 : ι → ι . explicit_Reals x0 x1 x2 x3 x4 x5bij x0 x6 x12x12 x1 = x7x12 x2 = x8(∀ x13 . x13x0∀ x14 . x14x0x12 (x3 x13 x14) = x9 (x12 x13) (x12 x14))(∀ x13 . x13x0∀ x14 . x14x0x12 (x4 x13 x14) = x10 (x12 x13) (x12 x14))(∀ x13 . x13x0∀ x14 . x14x0iff (x5 x13 x14) (x11 (x12 x13) (x12 x14)))explicit_Reals x6 x7 x8 x9 x10 x11
Known explicit_Reals_real : explicit_Reals real 0 1 add_SNo mul_SNo SNoLe
Known bij_idbij_id : ∀ x0 . bij x0 x0 (λ x1 . x1)
Known add_SNo_add_CSNoadd_SNo_add_CSNo : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_CSNo x0 x1
Known iff_refliff_refl : ∀ x0 : ο . iff x0 x0
Known add_CSNo_minus_CSNo_linvadd_CSNo_minus_CSNo_linv : ∀ x0 . CSNo x0add_CSNo (minus_CSNo x0) x0 = 0
Theorem 73d02.. : explicit_Complex complex CSNo_Re CSNo_Im 0 1 Complex_i add_CSNo mul_CSNo (proof)