Beginning of Section SurComplex

L28

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

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

L30

Axiom. (complex_tag_fresh) We take the following as an axiom:

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

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

L31

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...

L32

Axiom. (SNo_pair_0) We take the following as an axiom:

∀x, SNo_pair x 0 = x

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

L33

Axiom. (SNo_pair_prop_1) We take the following as an axiom:

∀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...

L34

Axiom. (SNo_pair_prop_2) We take the following as an axiom:

∀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...

L35

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...

L36

Axiom. (CSNo_I) We take the following as an axiom:

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

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

L37

Axiom. (CSNo_E) We take the following as an axiom:

∀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...

L38

Axiom. (SNo_CSNo) We take the following as an axiom:

∀x, SNo x → CSNo x

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

L39

Axiom. (CSNo_0) We take the following as an axiom:

CSNo 0

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

L40

Axiom. (CSNo_1) We take the following as an axiom:

CSNo 1

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

L41

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

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

L43

Axiom. (CSNo_ExtendedSNoElt_3) We take the following as an axiom:

∀z, CSNo z → ExtendedSNoElt_ 3 z

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

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.

L49

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...

L50

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...

L51

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...

L52

Let i ≝ Complex_i

L53

Let Re : set → set ≝ CSNo_Re

L54

Let Im : set → set ≝ CSNo_Im

L55

Let pa : set → set → set ≝ SNo_pair

L56

Axiom. (CSNo_Re1) We take the following as an axiom:

∀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...

L57

Axiom. (CSNo_Re2) We take the following as an axiom:

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

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

L58

Axiom. (CSNo_Im1) We take the following as an axiom:

∀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...

L59

Axiom. (CSNo_Im2) We take the following as an axiom:

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

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

L60

Axiom. (CSNo_ReR) We take the following as an axiom:

∀z, CSNo z → SNo (Re z)

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

L61

Axiom. (CSNo_ImR) We take the following as an axiom:

∀z, CSNo z → SNo (Im z)

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

L62

Axiom. (CSNo_ReIm) We take the following as an axiom:

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

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

L63

Axiom. (CSNo_ReIm_split) We take the following as an axiom:

∀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...

L64

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...

L65

Axiom. (CSNoLev_ordinal) We take the following as an axiom:

∀z, CSNo z → ordinal (CSNoLev z)

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

L66

Let conj : set → set ≝ λx ⇒ x

L67

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...

L68

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...

L69

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...

L70

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...

L71

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...

L72

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...

L73

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...

L74

Let plus' ≝ add_CSNo

L75

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.

L81

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...

L82

Axiom. (CSNo_Complex_i) We take the following as an axiom:

CSNo i

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

L83

Axiom. (CSNo_minus_CSNo) We take the following as an axiom:

∀z, CSNo z → CSNo (minus_CSNo z)

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

L84

Axiom. (minus_CSNo_CRe) We take the following as an axiom:

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

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

L85

Axiom. (minus_CSNo_CIm) We take the following as an axiom:

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

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

L86

Axiom. (CSNo_conj_CSNo) We take the following as an axiom:

∀z, CSNo z → CSNo (conj_CSNo z)

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

L87

Axiom. (conj_CSNo_CRe) We take the following as an axiom:

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

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

L88

Axiom. (conj_CSNo_CIm) We take the following as an axiom:

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

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

L89

Axiom. (CSNo_add_CSNo) We take the following as an axiom:

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

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

L90

Axiom. (CSNo_add_CSNo_3) We take the following as an axiom:

∀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...

L91

Axiom. (add_CSNo_CRe) We take the following as an axiom:

∀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...

L92

Axiom. (add_CSNo_CIm) We take the following as an axiom:

∀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...

L93

Axiom. (CSNo_mul_CSNo) We take the following as an axiom:

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

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

L94

Axiom. (CSNo_mul_CSNo_3) We take the following as an axiom:

∀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...

L95

Axiom. (mul_CSNo_CRe) We take the following as an axiom:

∀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...

L96

Axiom. (mul_CSNo_CIm) We take the following as an axiom:

∀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...

L97

Axiom. (SNo_Re) We take the following as an axiom:

∀x, SNo x → Re x = x

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

L98

Axiom. (SNo_Im) We take the following as an axiom:

∀x, SNo x → Im x = 0

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

L99

Axiom. (Re_0) We take the following as an axiom:

Re 0 = 0

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

L100

Axiom. (Im_0) We take the following as an axiom:

Im 0 = 0

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

L101

Axiom. (Re_1) We take the following as an axiom:

Re 1 = 1

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

L102

Axiom. (Im_1) We take the following as an axiom:

Im 1 = 0

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

L103

Axiom. (Re_i) We take the following as an axiom:

Re i = 0

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

L104

Axiom. (Im_i) We take the following as an axiom:

Im i = 1

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

L105

Axiom. (conj_CSNo_id_SNo) We take the following as an axiom:

∀x, SNo x → x ' = x

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

L106

Axiom. (conj_CSNo_0) We take the following as an axiom:

0 ' = 0

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

L107

Axiom. (conj_CSNo_1) We take the following as an axiom:

1 ' = 1

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

L108

Axiom. (conj_CSNo_i) We take the following as an axiom:

i ' = :-: i

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

L109

Axiom. (minus_CSNo_minus_SNo) We take the following as an axiom:

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

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

L110

Axiom. (minus_CSNo_0) We take the following as an axiom:

:-: 0 = 0

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

L111

Axiom. (add_CSNo_add_SNo) We take the following as an axiom:

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

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

L112

Axiom. (mul_CSNo_mul_SNo) We take the following as an axiom:

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

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

L113

Axiom. (minus_CSNo_invol) We take the following as an axiom:

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

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

L114

Axiom. (conj_CSNo_invol) We take the following as an axiom:

∀z, CSNo z → z ' ' = z

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

L115

Axiom. (conj_minus_CSNo) We take the following as an axiom:

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

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

L116

Axiom. (minus_add_CSNo) We take the following as an axiom:

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

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

L117

Axiom. (conj_add_CSNo) We take the following as an axiom:

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

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

L118

Axiom. (add_CSNo_com) We take the following as an axiom:

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

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

L119

Axiom. (add_CSNo_assoc) We take the following as an axiom:

∀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...

L120

Axiom. (add_CSNo_0L) We take the following as an axiom:

∀z, CSNo z → add_CSNo 0 z = z

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

L121

Axiom. (add_CSNo_0R) We take the following as an axiom:

∀z, CSNo z → add_CSNo z 0 = z

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

L122

Axiom. (add_CSNo_minus_CSNo_linv) We take the following as an axiom:

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

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

L123

Axiom. (add_CSNo_minus_CSNo_rinv) We take the following as an axiom:

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

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

L124

Axiom. (mul_CSNo_0R) We take the following as an axiom:

∀z, CSNo z → z ⨯ 0 = 0

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

L125

Axiom. (mul_CSNo_0L) We take the following as an axiom:

∀z, CSNo z → 0 ⨯ z = 0

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

L126

Axiom. (mul_CSNo_1R) We take the following as an axiom:

∀z, CSNo z → z ⨯ 1 = z

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

L127

Axiom. (mul_CSNo_1L) We take the following as an axiom:

∀z, CSNo z → 1 ⨯ z = z

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

L128

Axiom. (conj_mul_CSNo) We take the following as an axiom:

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

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

L129

Axiom. (mul_CSNo_distrL) We take the following as an axiom:

∀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...

L130

Axiom. (mul_CSNo_distrR) We take the following as an axiom:

∀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...

L131

Axiom. (minus_mul_CSNo_distrR) We take the following as an axiom:

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

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

L132

Axiom. (minus_mul_CSNo_distrL) We take the following as an axiom:

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

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

L133

Axiom. (exp_CSNo_nat_0) We take the following as an axiom:

∀z, z⁰ = 1

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

L134

Axiom. (exp_CSNo_nat_S) We take the following as an axiom:

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

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

L135

Axiom. (exp_CSNo_nat_1) We take the following as an axiom:

∀z, CSNo z → z¹ = z

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

L136

Axiom. (exp_CSNo_nat_2) We take the following as an axiom:

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

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

L137

Axiom. (CSNo_exp_CSNo_nat) We take the following as an axiom:

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

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

L138

Axiom. (add_SNo_rotate_4_0312) We take the following as an axiom:

∀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...

L139

Axiom. (mul_CSNo_com) We take the following as an axiom:

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

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

L140

Axiom. (mul_CSNo_assoc) We take the following as an axiom:

∀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...

L141

Axiom. (Complex_i_sqr) We take the following as an axiom:

i ⨯ i = :-: 1

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

L142

Axiom. (SNo_abs_sqr_CSNo) We take the following as an axiom:

∀z, CSNo z → SNo (abs_sqr_CSNo z)

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

L143

Axiom. (abs_sqr_CSNo_nonneg) We take the following as an axiom:

∀z, CSNo z → 0 ≤ abs_sqr_CSNo z

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

L144

Axiom. (abs_sqr_CSNo_zero) We take the following as an axiom:

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

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

L145

Axiom. (CSNo_recip_CSNo) We take the following as an axiom:

∀z, CSNo z → CSNo (recip_CSNo z)

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

L146

Axiom. (CSNo_relative_recip) We take the following as an axiom:

∀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...

L147

Axiom. (recip_CSNo_invR) We take the following as an axiom:

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

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

L148

Axiom. (recip_CSNo_invL) We take the following as an axiom:

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

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

L149

Axiom. (CSNo_div_CSNo) We take the following as an axiom:

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

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

L150

Axiom. (mul_div_CSNo_invL) We take the following as an axiom:

∀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...

L151

Axiom. (mul_div_CSNo_invR) We take the following as an axiom:

∀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...

L152

Axiom. (sqrt_SNo_nonneg_sqr_id) We take the following as an axiom:

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

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

L153

Axiom. (sqrt_SNo_nonneg_mon_strict) We take the following as an axiom:

∀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...

L154

Axiom. (sqrt_SNo_nonneg_mon) We take the following as an axiom:

∀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...

L155

Axiom. (sqrt_SNo_nonneg_mul_SNo) We take the following as an axiom:

∀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...

L156

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...

L157

Axiom. (SNo_modulus_CSNo) We take the following as an axiom:

∀z, CSNo z → SNo (modulus_CSNo z)

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

L158

Axiom. (modulus_CSNo_nonneg) We take the following as an axiom:

∀z, CSNo z → 0 ≤ modulus_CSNo z

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

L159

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...

L160

Axiom. (sqrt_CSNo_sqrt) We take the following as an axiom:

∀z, CSNo z → sqrt_CSNo z² = z

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

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.

L169

Let i ≝ Complex_i

L170

Let Re : set → set ≝ CSNo_Re

L171

Let Im : set → set ≝ CSNo_Im

L172

Let pa : set → set → set ≝ SNo_pair

L173

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...

L174

Axiom. (complex_I) We take the following as an axiom:

∀x y ∈ real, pa x y ∈ complex

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

L175

Axiom. (complex_E) We take the following as an axiom:

∀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...

L176

Axiom. (complex_CSNo) We take the following as an axiom:

∀z ∈ complex, CSNo z

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

L177

Axiom. (real_complex) We take the following as an axiom:

real ⊆ complex

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

L178

Axiom. (complex_0) We take the following as an axiom:

0 ∈ complex

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

L179

Axiom. (complex_1) We take the following as an axiom:

1 ∈ complex

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

L180

Axiom. (complex_i) We take the following as an axiom:

i ∈ complex

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

L181

Axiom. (complex_Re_eq) We take the following as an axiom:

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

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

L182

Axiom. (complex_Im_eq) We take the following as an axiom:

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

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

L183

Axiom. (complex_Re_real) We take the following as an axiom:

∀z ∈ complex, Re z ∈ real

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

L184

Axiom. (complex_Im_real) We take the following as an axiom:

∀z ∈ complex, Im z ∈ real

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

L185

Axiom. (complex_ReIm_split) We take the following as an axiom:

∀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...

L186

Axiom. (complex_minus_CSNo) We take the following as an axiom:

∀z ∈ complex, - z ∈ complex

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

L187

Axiom. (complex_conj_CSNo) We take the following as an axiom:

∀z ∈ complex, conj_CSNo z ∈ complex

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

L188

Axiom. (complex_add_CSNo) We take the following as an axiom:

∀z w ∈ complex, z + w ∈ complex

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

L189

Axiom. (complex_mul_CSNo) We take the following as an axiom:

∀z w ∈ complex, z * w ∈ complex

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

L190

Axiom. (real_Re_eq) We take the following as an axiom:

∀x ∈ real, Re x = x

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

L191

Axiom. (real_Im_eq) We take the following as an axiom:

∀x ∈ real, Im x = 0

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

L192

Axiom. (mul_i_real_eq) We take the following as an axiom:

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

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

L193

Axiom. (real_Re_i_eq) We take the following as an axiom:

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

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

L194

Axiom. (real_Im_i_eq) We take the following as an axiom:

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

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

L195

Axiom. (complex_eta) We take the following as an axiom:

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

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

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.

L202

Axiom. (complex_recip_CSNo) We take the following as an axiom:

∀z ∈ complex, recip_CSNo z ∈ complex

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

L203

Axiom. (complex_div_CSNo) We take the following as an axiom:

∀z w ∈ complex, div_CSNo z w ∈ complex

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

End of Section ComplexDiv

L205

Axiom. (complex_real_set_eq) We take the following as an axiom:

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

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

End of Section Complex