Beginning of Section SurComplex

Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.

Theorem. (complex_tag_fresh)

∀x, SNo x → ∀u ∈ x, {2} ∉ u

In Proofgold the corresponding term root is 3d8064... and proposition id is e01e5b...

Proof:
Proof not loaded.

Definition. We define SNo_pair to be pair_tag {2} of type set → set → set.

In Proofgold the corresponding term root is 7a69f6... and object id is 23fbcd...

Theorem. (SNo_pair_0)

∀x, SNo_pair x 0 = x

In Proofgold the corresponding term root is 1cb458... and proposition id is f7bb55...

Proof:
Proof not loaded.

Theorem. (SNo_pair_prop_1)

∀x1 y1 x2 y2, SNo x1 → SNo x2 → SNo_pair x1 y1 = SNo_pair x2 y2 → x1 = x2

In Proofgold the corresponding term root is 070aac... and proposition id is b7a761...

Proof:
Proof not loaded.

Theorem. (SNo_pair_prop_2)

∀x1 y1 x2 y2, SNo x1 → SNo y1 → SNo x2 → SNo y2 → SNo_pair x1 y1 = SNo_pair x2 y2 → y1 = y2

In Proofgold the corresponding term root is 3e9308... and proposition id is f4146d...

Proof:
Proof not loaded.

Definition. We define CSNo to be CD_carr {2} SNo of type set → prop.

In Proofgold the corresponding term root is 4235a7... and object id is a08f56...

Theorem. (CSNo_I)

∀x y, SNo x → SNo y → CSNo (SNo_pair x y)

In Proofgold the corresponding term root is cad32d... and proposition id is dd6f38...

Proof:
Proof not loaded.

Theorem. (CSNo_E)

∀z, CSNo z → ∀p : set → prop, (∀x y, SNo x → SNo y → z = SNo_pair x y → p (SNo_pair x y)) → p z

In Proofgold the corresponding term root is cc5af4... and proposition id is 58f9bd...

Proof:
Proof not loaded.

Theorem. (SNo_CSNo)

∀x, SNo x → CSNo x

In Proofgold the corresponding term root is 9b0483... and proposition id is 04d332...

Proof:
Proof not loaded.

Theorem. (CSNo_0)

CSNo 0

In Proofgold the corresponding term root is 77c1b5... and proposition id is fc59ef...

Proof:
Proof not loaded.

Theorem. (CSNo_1)

CSNo 1

In Proofgold the corresponding term root is 8cf686... and proposition id is 14c184...

Proof:
Proof not loaded.

Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {2}

Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.

Theorem. (CSNo_ExtendedSNoElt_3)

∀z, CSNo z → ExtendedSNoElt_ 3 z

In Proofgold the corresponding term root is 5700d1... and proposition id is 4b578b...

Proof:
Proof not loaded.

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.

Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.

Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.

Definition. We define Complex_i to be SNo_pair 0 1 of type set.

In Proofgold the corresponding term root is ace1d5... and object id is 04654a...

Definition. We define CSNo_Re to be CD_proj0 {2} SNo of type set → set.

In Proofgold the corresponding term root is a3c3be... and object id is 39e73f...

Definition. We define CSNo_Im to be CD_proj1 {2} SNo of type set → set.

In Proofgold the corresponding term root is 9a1a1e... and object id is 784bb4...

Let i ≝ Complex_i

Let Re : set → set ≝ CSNo_Re

Let Im : set → set ≝ CSNo_Im

Let pa : set → set → set ≝ SNo_pair

Theorem. (CSNo_Re1)

∀z, CSNo z → SNo (Re z) ∧ ∃y, SNo y ∧ z = pa (Re z) y

In Proofgold the corresponding term root is 107683... and proposition id is 6e4a86...

Proof:
Proof not loaded.

Theorem. (CSNo_Re2)

∀x y, SNo x → SNo y → Re (pa x y) = x

In Proofgold the corresponding term root is d6dd63... and proposition id is c7769d...

Proof:
Proof not loaded.

Theorem. (CSNo_Im1)

∀z, CSNo z → SNo (Im z) ∧ z = pa (Re z) (Im z)

In Proofgold the corresponding term root is e5de1d... and proposition id is 63974e...

Proof:
Proof not loaded.

Theorem. (CSNo_Im2)

∀x y, SNo x → SNo y → Im (pa x y) = y

In Proofgold the corresponding term root is 01dd37... and proposition id is 71ee31...

Proof:
Proof not loaded.

Theorem. (CSNo_ReR)

∀z, CSNo z → SNo (Re z)

In Proofgold the corresponding term root is 6ff298... and proposition id is 39509b...

Proof:
Proof not loaded.

Theorem. (CSNo_ImR)

∀z, CSNo z → SNo (Im z)

In Proofgold the corresponding term root is c1dc53... and proposition id is f2d16d...

Proof:
Proof not loaded.

Theorem. (CSNo_ReIm)

∀z, CSNo z → z = pa (Re z) (Im z)

In Proofgold the corresponding term root is 06dc6f... and proposition id is 1fdc97...

Proof:
Proof not loaded.

Theorem. (CSNo_ReIm_split)

∀z w, CSNo z → CSNo w → Re z = Re w → Im z = Im w → z = w

In Proofgold the corresponding term root is b4ba0e... and proposition id is 5191fd...

Proof:
Proof not loaded.

Definition. We define CSNoLev to be λz ⇒ SNoLev (Re z) ∪ SNoLev (Im z) of type set → set.

In Proofgold the corresponding term root is f29582... and object id is 5ebbe9...

Theorem. (CSNoLev_ordinal)

∀z, CSNo z → ordinal (CSNoLev z)

In Proofgold the corresponding term root is 143261... and proposition id is 973671...

Proof:
Proof not loaded.

Let conj : set → set ≝ λx ⇒ x

Definition. We define minus_CSNo to be CD_minus {2} SNo minus_SNo of type set → set.

In Proofgold the corresponding term root is 84edf6... and object id is d06e08...

Definition. We define conj_CSNo to be CD_conj {2} SNo minus_SNo conj of type set → set.

In Proofgold the corresponding term root is f0317b... and object id is 35fddb...

Definition. We define add_CSNo to be CD_add {2} SNo add_SNo of type set → set → set.

In Proofgold the corresponding term root is 1c8cce... and object id is 756300...

Definition. We define mul_CSNo to be CD_mul {2} SNo minus_SNo conj add_SNo mul_SNo of type set → set → set.

In Proofgold the corresponding term root is fbcd2a... and object id is 46d4cd...

Definition. We define exp_CSNo_nat to be CD_exp_nat {2} SNo minus_SNo conj add_SNo mul_SNo of type set → set → set.

In Proofgold the corresponding term root is 1ff646... and object id is dce27b...

Definition. We define abs_sqr_CSNo to be λz ⇒ Re z ^ 2 + Im z ^ 2 of type set → set.

In Proofgold the corresponding term root is 8363b8... and object id is 5fbf97...

Definition. We define recip_CSNo to be λz ⇒ pa (Re z :/: abs_sqr_CSNo z) (- (Im z :/: abs_sqr_CSNo z)) of type set → set.

In Proofgold the corresponding term root is 6e6e74... and object id is 42648e...

Let plus' ≝ add_CSNo

Let mult' ≝ mul_CSNo

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term minus_CSNo.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term conj_CSNo.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_CSNo.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_CSNo.

Notation. We use :^: as an infix operator with priority 355 and which associates to the right corresponding to applying term exp_CSNo_nat.

Definition. We define div_CSNo to be λz w ⇒ z ⨯ recip_CSNo w of type set → set → set.

In Proofgold the corresponding term root is 3a99f0... and object id is 51b5b9...

Theorem. (CSNo_Complex_i)

CSNo i

In Proofgold the corresponding term root is c1ad38... and proposition id is 92db43...

Proof:
Proof not loaded.

Theorem. (CSNo_minus_CSNo)

∀z, CSNo z → CSNo (minus_CSNo z)

In Proofgold the corresponding term root is ed113e... and proposition id is 876b1c...

Proof:
Proof not loaded.

Theorem. (minus_CSNo_CRe)

∀z, CSNo z → Re (:-: z) = - Re z

In Proofgold the corresponding term root is 3d4fc3... and proposition id is 8a656a...

Proof:
Proof not loaded.

Theorem. (minus_CSNo_CIm)

∀z, CSNo z → Im (:-: z) = - Im z

In Proofgold the corresponding term root is e7712f... and proposition id is 901983...

Proof:
Proof not loaded.

Theorem. (CSNo_conj_CSNo)

∀z, CSNo z → CSNo (conj_CSNo z)

In Proofgold the corresponding term root is 131b13... and proposition id is e9cc63...

Proof:
Proof not loaded.

Theorem. (conj_CSNo_CRe)

∀z, CSNo z → Re (z ') = Re z

In Proofgold the corresponding term root is c50c46... and proposition id is a8772e...

Proof:
Proof not loaded.

Theorem. (conj_CSNo_CIm)

∀z, CSNo z → Im (z ') = - Im z

In Proofgold the corresponding term root is ad25ad... and proposition id is d3861c...

Proof:
Proof not loaded.

Theorem. (CSNo_add_CSNo)

∀z w, CSNo z → CSNo w → CSNo (add_CSNo z w)

In Proofgold the corresponding term root is 03ed30... and proposition id is 9bf062...

Proof:
Proof not loaded.

Theorem. (CSNo_add_CSNo_3)

∀z w v, CSNo z → CSNo w → CSNo v → CSNo (z + w + v)

In Proofgold the corresponding term root is 2bfa20... and proposition id is 8b5121...

Proof:
Proof not loaded.

Theorem. (add_CSNo_CRe)

∀z w, CSNo z → CSNo w → Re (plus' z w) = Re z + Re w

In Proofgold the corresponding term root is c9a95c... and proposition id is c220af...

Proof:
Proof not loaded.

Theorem. (add_CSNo_CIm)

∀z w, CSNo z → CSNo w → Im (plus' z w) = Im z + Im w

In Proofgold the corresponding term root is 5e4827... and proposition id is 568f7b...

Proof:
Proof not loaded.

Theorem. (CSNo_mul_CSNo)

∀z w, CSNo z → CSNo w → CSNo (z ⨯ w)

In Proofgold the corresponding term root is 960670... and proposition id is 866107...

Proof:
Proof not loaded.

Theorem. (CSNo_mul_CSNo_3)

∀z w v, CSNo z → CSNo w → CSNo v → CSNo (z ⨯ w ⨯ v)

In Proofgold the corresponding term root is 71c203... and proposition id is fb3c1b...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_CRe)

∀z w, CSNo z → CSNo w → Re (mult' z w) = Re z * Re w + - (Im w * Im z)

In Proofgold the corresponding term root is 06f6e3... and proposition id is ea0bfe...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_CIm)

∀z w, CSNo z → CSNo w → Im (mult' z w) = Im w * Re z + Im z * Re w

In Proofgold the corresponding term root is c8110c... and proposition id is 5587f2...

Proof:
Proof not loaded.

Theorem. (SNo_Re)

∀x, SNo x → Re x = x

In Proofgold the corresponding term root is 50191e... and proposition id is a39bef...

Proof:
Proof not loaded.

Theorem. (SNo_Im)

∀x, SNo x → Im x = 0

In Proofgold the corresponding term root is e827aa... and proposition id is 021995...

Proof:
Proof not loaded.

Theorem. (Re_0)

Re 0 = 0

In Proofgold the corresponding term root is cd467c... and proposition id is e48eab...

Proof:
Proof not loaded.

Theorem. (Im_0)

Im 0 = 0

In Proofgold the corresponding term root is 3d0622... and proposition id is cec939...

Proof:
Proof not loaded.

Theorem. (Re_1)

Re 1 = 1

In Proofgold the corresponding term root is df187f... and proposition id is 5672d2...

Proof:
Proof not loaded.

Theorem. (Im_1)

Im 1 = 0

In Proofgold the corresponding term root is ca8804... and proposition id is 389106...

Proof:
Proof not loaded.

Theorem. (Re_i)

Re i = 0

In Proofgold the corresponding term root is 016d84... and proposition id is 64299d...

Proof:
Proof not loaded.

Theorem. (Im_i)

Im i = 1

In Proofgold the corresponding term root is a6da12... and proposition id is 6d4781...

Proof:
Proof not loaded.

Theorem. (conj_CSNo_id_SNo)

∀x, SNo x → x ' = x

In Proofgold the corresponding term root is 119723... and proposition id is baaa35...

Proof:
Proof not loaded.

Theorem. (conj_CSNo_0)

0 ' = 0

In Proofgold the corresponding term root is 4e40f8... and proposition id is ee56ed...

Proof:
Proof not loaded.

Theorem. (conj_CSNo_1)

1 ' = 1

In Proofgold the corresponding term root is 632854... and proposition id is f32e05...

Proof:
Proof not loaded.

Theorem. (conj_CSNo_i)

i ' = :-: i

In Proofgold the corresponding term root is b17555... and proposition id is 3ef34f...

Proof:
Proof not loaded.

Theorem. (minus_CSNo_minus_SNo)

∀x, SNo x → :-: x = - x

In Proofgold the corresponding term root is c7c7a2... and proposition id is b2e3bc...

Proof:
Proof not loaded.

Theorem. (minus_CSNo_0)

:-: 0 = 0

In Proofgold the corresponding term root is 733a71... and proposition id is 781e00...

Proof:
Proof not loaded.

Theorem. (add_CSNo_add_SNo)

∀x y, SNo x → SNo y → x + y = x + y

In Proofgold the corresponding term root is 9bf667... and proposition id is 78adb6...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_mul_SNo)

∀x y, SNo x → SNo y → x ⨯ y = x * y

In Proofgold the corresponding term root is d07924... and proposition id is 35fd7f...

Proof:
Proof not loaded.

Theorem. (minus_CSNo_invol)

∀z, CSNo z → :-: :-: z = z

In Proofgold the corresponding term root is 718eca... and proposition id is 1133eb...

Proof:
Proof not loaded.

Theorem. (conj_CSNo_invol)

∀z, CSNo z → z ' ' = z

In Proofgold the corresponding term root is 80a94e... and proposition id is 01ed39...

Proof:
Proof not loaded.

Theorem. (conj_minus_CSNo)

∀z, CSNo z → (:-: z) ' = :-: (z ')

In Proofgold the corresponding term root is e285c3... and proposition id is f32597...

Proof:
Proof not loaded.

Theorem. (minus_add_CSNo)

∀z w, CSNo z → CSNo w → :-: (z + w) = :-: z + :-: w

In Proofgold the corresponding term root is 7d8b27... and proposition id is f2c713...

Proof:
Proof not loaded.

Theorem. (conj_add_CSNo)

∀z w, CSNo z → CSNo w → (z + w) ' = z ' + w '

In Proofgold the corresponding term root is af649d... and proposition id is 884e86...

Proof:
Proof not loaded.

Theorem. (add_CSNo_com)

∀z w, CSNo z → CSNo w → z + w = w + z

In Proofgold the corresponding term root is 4b7106... and proposition id is 7214c5...

Proof:
Proof not loaded.

Theorem. (add_CSNo_assoc)

∀z w v, CSNo z → CSNo w → CSNo v → (z + w) + v = z + (w + v)

In Proofgold the corresponding term root is d8944b... and proposition id is 76142e...

Proof:
Proof not loaded.

Theorem. (add_CSNo_0L)

∀z, CSNo z → add_CSNo 0 z = z

In Proofgold the corresponding term root is 192e4f... and proposition id is f071aa...

Proof:
Proof not loaded.

Theorem. (add_CSNo_0R)

∀z, CSNo z → add_CSNo z 0 = z

In Proofgold the corresponding term root is 5d190c... and proposition id is f422cd...

Proof:
Proof not loaded.

Theorem. (add_CSNo_minus_CSNo_linv)

∀z, CSNo z → add_CSNo (minus_CSNo z) z = 0

In Proofgold the corresponding term root is 02ca9b... and proposition id is b8f406...

Proof:
Proof not loaded.

Theorem. (add_CSNo_minus_CSNo_rinv)

∀z, CSNo z → add_CSNo z (minus_CSNo z) = 0

In Proofgold the corresponding term root is a39e67... and proposition id is cef63c...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_0R)

∀z, CSNo z → z ⨯ 0 = 0

In Proofgold the corresponding term root is cc1bfb... and proposition id is a20c54...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_0L)

∀z, CSNo z → 0 ⨯ z = 0

In Proofgold the corresponding term root is a0f420... and proposition id is 491817...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_1R)

∀z, CSNo z → z ⨯ 1 = z

In Proofgold the corresponding term root is 0cbbac... and proposition id is ddbaab...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_1L)

∀z, CSNo z → 1 ⨯ z = z

In Proofgold the corresponding term root is 2c05ca... and proposition id is 88f311...

Proof:
Proof not loaded.

Theorem. (conj_mul_CSNo)

∀z w, CSNo z → CSNo w → (z ⨯ w) ' = w ' ⨯ z '

In Proofgold the corresponding term root is d18a4e... and proposition id is 43023c...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_distrL)

∀z w u, CSNo z → CSNo w → CSNo u → z ⨯ (w + u) = z ⨯ w + z ⨯ u

In Proofgold the corresponding term root is 4300b1... and proposition id is 146a23...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_distrR)

∀z w u, CSNo z → CSNo w → CSNo u → (z + w) ⨯ u = z ⨯ u + w ⨯ u

In Proofgold the corresponding term root is 6eb197... and proposition id is 7fab8b...

Proof:
Proof not loaded.

Theorem. (minus_mul_CSNo_distrR)

∀z w, CSNo z → CSNo w → z ⨯ (:-: w) = :-: z ⨯ w

In Proofgold the corresponding term root is 11bf1c... and proposition id is 79b3b3...

Proof:
Proof not loaded.

Theorem. (minus_mul_CSNo_distrL)

∀z w, CSNo z → CSNo w → (:-: z) ⨯ w = :-: z ⨯ w

In Proofgold the corresponding term root is 995a36... and proposition id is 1b56a5...

Proof:
Proof not loaded.

Theorem. (exp_CSNo_nat_0)

∀z, z⁰ = 1

In Proofgold the corresponding term root is 4ac193... and proposition id is c694c7...

Proof:
Proof not loaded.

Theorem. (exp_CSNo_nat_S)

∀z n, nat_p n → z^{(ordsucc n)} = z ⨯ zⁿ

In Proofgold the corresponding term root is cc896c... and proposition id is ce5d58...

Proof:
Proof not loaded.

Theorem. (exp_CSNo_nat_1)

∀z, CSNo z → z¹ = z

In Proofgold the corresponding term root is 00324b... and proposition id is 4f5719...

Proof:
Proof not loaded.

Theorem. (exp_CSNo_nat_2)

∀z, CSNo z → z² = z ⨯ z

In Proofgold the corresponding term root is 3de725... and proposition id is b58c27...

Proof:
Proof not loaded.

Theorem. (CSNo_exp_CSNo_nat)

∀z, CSNo z → ∀n, nat_p n → CSNo (zⁿ)

In Proofgold the corresponding term root is 11b0c7... and proposition id is 0d7167...

Proof:
Proof not loaded.

Theorem. (add_SNo_rotate_4_0312)

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) + (z + w) = (x + w) + (y + z)

In Proofgold the corresponding term root is a00d0b... and proposition id is 1932b8...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_com)

∀z w, CSNo z → CSNo w → z ⨯ w = w ⨯ z

In Proofgold the corresponding term root is d89de4... and proposition id is 8f3381...

Proof:
Proof not loaded.

Theorem. (mul_CSNo_assoc)

∀z w v, CSNo z → CSNo w → CSNo v → z ⨯ (w ⨯ v) = (z ⨯ w) ⨯ v

In Proofgold the corresponding term root is 227f96... and proposition id is 9f937c...

Proof:
Proof not loaded.

Theorem. (Complex_i_sqr)

i ⨯ i = :-: 1

In Proofgold the corresponding term root is 665bcb... and proposition id is 0ce587...

Proof:
Proof not loaded.

Theorem. (SNo_abs_sqr_CSNo)

∀z, CSNo z → SNo (abs_sqr_CSNo z)

In Proofgold the corresponding term root is 3c670d... and proposition id is 487405...

Proof:
Proof not loaded.

Theorem. (abs_sqr_CSNo_nonneg)

∀z, CSNo z → 0 ≤ abs_sqr_CSNo z

In Proofgold the corresponding term root is 8b1a65... and proposition id is 7810f8...

Proof:
Proof not loaded.

Theorem. (abs_sqr_CSNo_zero)

∀z, CSNo z → abs_sqr_CSNo z = 0 → z = 0

In Proofgold the corresponding term root is 717eb1... and proposition id is d8e809...

Proof:
Proof not loaded.

Theorem. (CSNo_recip_CSNo)

∀z, CSNo z → CSNo (recip_CSNo z)

In Proofgold the corresponding term root is fad212... and proposition id is 05a416...

Proof:
Proof not loaded.

Theorem. (CSNo_relative_recip)

∀z, CSNo z → ∀u, SNo u → (Re z ^ 2 + Im z ^ 2) * u = 1 → z ⨯ (u ⨯ Re z + :-: i ⨯ u ⨯ Im z) = 1

In Proofgold the corresponding term root is dbb71a... and proposition id is d15820...

Proof:
Proof not loaded.

Theorem. (recip_CSNo_invR)

∀z, CSNo z → z ≠ 0 → z ⨯ recip_CSNo z = 1

In Proofgold the corresponding term root is 838352... and proposition id is c71b18...

Proof:
Proof not loaded.

Theorem. (recip_CSNo_invL)

∀z, CSNo z → z ≠ 0 → recip_CSNo z ⨯ z = 1

In Proofgold the corresponding term root is a9e4b7... and proposition id is 223581...

Proof:
Proof not loaded.

Theorem. (CSNo_div_CSNo)

∀z w, CSNo z → CSNo w → CSNo (div_CSNo z w)

In Proofgold the corresponding term root is 91055e... and proposition id is ca203c...

Proof:
Proof not loaded.

Theorem. (mul_div_CSNo_invL)

∀z w, CSNo z → CSNo w → w ≠ 0 → (div_CSNo z w) ⨯ w = z

In Proofgold the corresponding term root is 9a03b4... and proposition id is 27df05...

Proof:
Proof not loaded.

Theorem. (mul_div_CSNo_invR)

∀z w, CSNo z → CSNo w → w ≠ 0 → w ⨯ (div_CSNo z w) = z

In Proofgold the corresponding term root is 442304... and proposition id is ab3599...

Proof:
Proof not loaded.

Theorem. (sqrt_SNo_nonneg_sqr_id)

∀x, SNo x → 0 ≤ x → sqrt_SNo_nonneg (x ^ 2) = x

In Proofgold the corresponding term root is 4482ad... and proposition id is 21b2de...

Proof:
Proof not loaded.

Theorem. (sqrt_SNo_nonneg_mon_strict)

∀x y, SNo x → SNo y → 0 ≤ x → x < y → sqrt_SNo_nonneg x < sqrt_SNo_nonneg y

In Proofgold the corresponding term root is 544c39... and proposition id is 02624d...

Proof:
Proof not loaded.

Theorem. (sqrt_SNo_nonneg_mon)

∀x y, SNo x → SNo y → 0 ≤ x → x ≤ y → sqrt_SNo_nonneg x ≤ sqrt_SNo_nonneg y

In Proofgold the corresponding term root is 317df1... and proposition id is 30ecc9...

Proof:
Proof not loaded.

Theorem. (sqrt_SNo_nonneg_mul_SNo)

∀x y, SNo x → SNo y → 0 ≤ x → 0 ≤ y → sqrt_SNo_nonneg (x * y) = sqrt_SNo_nonneg x * sqrt_SNo_nonneg y

In Proofgold the corresponding term root is c83ae6... and proposition id is c2dc6b...

Proof:
Proof not loaded.

Definition. We define modulus_CSNo to be λz ⇒ sqrt_SNo_nonneg (abs_sqr_CSNo z) of type set → set.

In Proofgold the corresponding term root is 181351... and object id is 30af8e...

Theorem. (SNo_modulus_CSNo)

∀z, CSNo z → SNo (modulus_CSNo z)

In Proofgold the corresponding term root is fac03c... and proposition id is 5c6052...

Proof:
Proof not loaded.

Theorem. (modulus_CSNo_nonneg)

∀z, CSNo z → 0 ≤ modulus_CSNo z

In Proofgold the corresponding term root is 9e4a15... and proposition id is 834a2a...

Proof:
Proof not loaded.

Definition. We define sqrt_CSNo to be λz ⇒ if Im z < 0 ∨ Im z = 0 ∧ Re z < 0 then pa (sqrt_SNo_nonneg (eps_ 1 * (Re z + modulus_CSNo z))) (- sqrt_SNo_nonneg (eps_ 1 * (- Re z + modulus_CSNo z))) else pa (sqrt_SNo_nonneg (eps_ 1 * (Re z + modulus_CSNo z))) (sqrt_SNo_nonneg (eps_ 1 * (- Re z + modulus_CSNo z))) of type set → set.

In Proofgold the corresponding term root is d9166c... and object id is c77a46...

Theorem. (sqrt_CSNo_sqrt)

∀z, CSNo z → sqrt_CSNo z² = z

In Proofgold the corresponding term root is 41ae0b... and proposition id is 025230...

Proof:
Proof not loaded.

End of Section SurComplex

Beginning of Section Complex

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_CSNo.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_CSNo.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_CSNo.

Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.

Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.

Let i ≝ Complex_i

Let Re : set → set ≝ CSNo_Re

Let Im : set → set ≝ CSNo_Im

Let pa : set → set → set ≝ SNo_pair

Definition. We define complex to be {pa (u 0) (u 1)|u ∈ real ⨯ real} of type set.

In Proofgold the corresponding term root is c599ee... and object id is f73979...

Theorem. (complex_I)

∀x y ∈ real, pa x y ∈ complex

In Proofgold the corresponding term root is 179d8d... and proposition id is 1f9d1b...

Proof:
Proof not loaded.

Theorem. (complex_E)

∀z ∈ complex, ∀p : prop, (∀x y ∈ real, z = pa x y → p) → p

In Proofgold the corresponding term root is d4f71b... and proposition id is aee8b5...

Proof:
Proof not loaded.

Theorem. (complex_CSNo)

∀z ∈ complex, CSNo z

In Proofgold the corresponding term root is 582187... and proposition id is 4bb77f...

Proof:
Proof not loaded.

Theorem. (real_complex)

real ⊆ complex

In Proofgold the corresponding term root is 2e80dd... and proposition id is 303d34...

Proof:
Proof not loaded.

Theorem. (complex_0)

0 ∈ complex

In Proofgold the corresponding term root is c4c56d... and proposition id is e71ee2...

Proof:
Proof not loaded.

Theorem. (complex_1)

1 ∈ complex

In Proofgold the corresponding term root is 5b4c72... and proposition id is 614efe...

Proof:
Proof not loaded.

Theorem. (complex_i)

i ∈ complex

In Proofgold the corresponding term root is f45bb2... and proposition id is 61712b...

Proof:
Proof not loaded.

Theorem. (complex_Re_eq)

∀x y ∈ real, Re (pa x y) = x

In Proofgold the corresponding term root is 7b2cad... and proposition id is 14b73d...

Proof:
Proof not loaded.

Theorem. (complex_Im_eq)

∀x y ∈ real, Im (pa x y) = y

In Proofgold the corresponding term root is db9a6a... and proposition id is 1f8050...

Proof:
Proof not loaded.

Theorem. (complex_Re_real)

∀z ∈ complex, Re z ∈ real

In Proofgold the corresponding term root is 9febfe... and proposition id is c0c90f...

Proof:
Proof not loaded.

Theorem. (complex_Im_real)

∀z ∈ complex, Im z ∈ real

In Proofgold the corresponding term root is c46a91... and proposition id is 21df46...

Proof:
Proof not loaded.

Theorem. (complex_ReIm_split)

∀z w ∈ complex, Re z = Re w → Im z = Im w → z = w

In Proofgold the corresponding term root is 1bd022... and proposition id is 98bc08...

Proof:
Proof not loaded.

Theorem. (complex_minus_CSNo)

∀z ∈ complex, - z ∈ complex

In Proofgold the corresponding term root is 520df6... and proposition id is c94747...

Proof:
Proof not loaded.

Theorem. (complex_conj_CSNo)

∀z ∈ complex, conj_CSNo z ∈ complex

In Proofgold the corresponding term root is e2bf24... and proposition id is d48643...

Proof:
Proof not loaded.

Theorem. (complex_add_CSNo)

∀z w ∈ complex, z + w ∈ complex

In Proofgold the corresponding term root is 5605eb... and proposition id is cd011e...

Proof:
Proof not loaded.

Theorem. (complex_mul_CSNo)

∀z w ∈ complex, z * w ∈ complex

In Proofgold the corresponding term root is 1caebd... and proposition id is 2d494f...

Proof:
Proof not loaded.

Theorem. (real_Re_eq)

∀x ∈ real, Re x = x

In Proofgold the corresponding term root is c8dfe7... and proposition id is de9b16...

Proof:
Proof not loaded.

Theorem. (real_Im_eq)

∀x ∈ real, Im x = 0

In Proofgold the corresponding term root is b04b30... and proposition id is 0ec6b4...

Proof:
Proof not loaded.

Theorem. (mul_i_real_eq)

∀x ∈ real, i * x = pa 0 x

In Proofgold the corresponding term root is c137fe... and proposition id is 59baae...

Proof:
Proof not loaded.

Theorem. (real_Re_i_eq)

∀x ∈ real, Re (i * x) = 0

In Proofgold the corresponding term root is 93568a... and proposition id is b18615...

Proof:
Proof not loaded.

Theorem. (real_Im_i_eq)

∀x ∈ real, Im (i * x) = x

In Proofgold the corresponding term root is 0dabe6... and proposition id is b8efce...

Proof:
Proof not loaded.

Theorem. (complex_eta)

∀z ∈ complex, z = Re z + i * Im z

In Proofgold the corresponding term root is 233acb... and proposition id is 9c8714...

Proof:
Proof not loaded.

Beginning of Section ComplexDiv

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.

Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.

Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.

Theorem. (complex_recip_CSNo)

∀z ∈ complex, recip_CSNo z ∈ complex

In Proofgold the corresponding term root is a91c24... and proposition id is 310f5f...

Proof:
Proof not loaded.

Theorem. (complex_div_CSNo)

∀z w ∈ complex, div_CSNo z w ∈ complex

In Proofgold the corresponding term root is efba54... and proposition id is b82141...

Proof:
Proof not loaded.

End of Section ComplexDiv

Theorem. (complex_real_set_eq)

real = {z ∈ complex|Re z = z}

In Proofgold the corresponding term root is 6d3ae0... and proposition id is 3414d9...

Proof:
Proof not loaded.

End of Section Complex