Construction of Numbers in Set Theory Part 9

Beginning of Section Eq

Variable A : SType

Definition. We define eq to be λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type A → A → prop.

Definition. We define neq to be λx y : A ⇒ ¬ eq x y of type A → A → prop.

End of Section Eq

Beginning of Section FE

Variable A B : SType

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

∀f g : A → B, (∀x : A, f x = g x) → f = g

End of Section FE

Beginning of Section Ex

Variable A : SType

Definition. We define ex to be λQ : A → prop ⇒ ∀P : prop, (∀x : A, Q x → P) → P of type (A → prop) → prop.

End of Section Ex

Beginning of Section PropN

Variable P1 P2 P3 : prop

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

P1 → P2 → P3 → P1 ∧ P2 ∧ P3

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

P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)

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

P1 → P1 ∨ P2 ∨ P3

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

P2 → P1 ∨ P2 ∨ P3

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

P3 → P1 ∨ P2 ∨ P3

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

P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)

Variable P4 : prop

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

P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4

Variable P5 : prop

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

P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5

End of Section PropN

Beginning of Section SepSec

Variable X : set

Variable P : set → prop

Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z)

Let F : set → set ≝ λx ⇒ if P x then x else z

Object. The name Sep is a term of type set.

End of Section SepSec

Beginning of Section SchroederBernstein

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

∀A, ∀F : set → set, (∀U ∈ 𝒫 A, F U ∈ 𝒫 A) → (∀U V ∈ 𝒫 A, U ⊆ V → F U ⊆ F V) → ∃Y ∈ 𝒫 A, F Y = Y

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

∀A B, ∀f : set → set, (∀x ∈ A, f x ∈ B) → ∀U ∈ 𝒫 A, {f x|x ∈ U} ∈ 𝒫 B

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

∀f : set → set, ∀U V, U ⊆ V → {f x|x ∈ U} ⊆ {f x|x ∈ V}

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

∀A U V, U ⊆ V → A ∖ V ⊆ A ∖ U

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

∀A B, ∀f g : set → set, inj A B f → inj B A g → equip A B

End of Section SchroederBernstein

Beginning of Section PigeonHole

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

∀n, nat_p n → ∀f : set → set, (∀i ∈ ordsucc n, f i ∈ n) → ¬ (∀i j ∈ ordsucc n, f i = f j → i = j)

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

∀n, nat_p n → ∀f : set → set, (∀i ∈ n, f i ∈ n) → (∀i j ∈ n, f i = f j → i = j) → bij n n f

End of Section PigeonHole

Beginning of Section Descr_ii

Variable P : (set → set) → prop

Object. The name Descr_ii is a term of type set → set.

Hypothesis Pex : ∃f : set → set, P f

Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g

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

P Descr_ii

End of Section Descr_ii

Beginning of Section Descr_iii

Variable P : (set → set → set) → prop

Object. The name Descr_iii is a term of type set → set → set.

Hypothesis Pex : ∃f : set → set → set, P f

Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g

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

P Descr_iii

End of Section Descr_iii

Beginning of Section Descr_Vo1

Variable P : Vo 1 → prop

Object. The name Descr_Vo1 is a term of type Vo 1.

Hypothesis Pex : ∃f : Vo 1, P f

Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g

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

P Descr_Vo1

End of Section Descr_Vo1

Beginning of Section If_ii

Variable p : prop

Variable f g : set → set

Object. The name If_ii is a term of type set → set.

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

p → If_ii = f

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

¬ p → If_ii = g

End of Section If_ii

Beginning of Section If_iii

Variable p : prop

Variable f g : set → set → set

Object. The name If_iii is a term of type set → set → set.

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

p → If_iii = f

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

¬ p → If_iii = g

End of Section If_iii

Beginning of Section EpsilonRec_i

Variable F : set → (set → set) → set

Object. The name In_rec_i is a term of type set → set.

Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h

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

∀X : set, In_rec_i X = F X In_rec_i

End of Section EpsilonRec_i

Beginning of Section EpsilonRec_ii

Variable F : set → (set → (set → set)) → (set → set)

Object. The name In_rec_ii is a term of type set → (set → set).

Hypothesis Fr : ∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h

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

∀X : set, In_rec_ii X = F X In_rec_ii

End of Section EpsilonRec_ii

Beginning of Section EpsilonRec_iii

Variable F : set → (set → (set → set → set)) → (set → set → set)

Object. The name In_rec_iii is a term of type set → (set → set → set).

Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → set), (∀x ∈ X, g x = h x) → F X g = F X h

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

∀X : set, In_rec_iii X = F X In_rec_iii

End of Section EpsilonRec_iii

Beginning of Section NatRec

Variable z : set

Variable f : set → set → set

Let F : set → (set → set) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n) (g (⋃ n)) else z

Definition. We define nat_primrec to be In_rec_i F of type set → set.

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

∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h

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

nat_primrec 0 = z

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

∀n : set, nat_p n → nat_primrec (ordsucc n) = f n (nat_primrec n)

End of Section NatRec

Beginning of Section NatArith

Definition. We define add_nat to be λn m : set ⇒ nat_primrec n (λ_ r ⇒ ordsucc r) m of type set → set → set.

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

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

∀n : set, n + 0 = n

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

∀n m : set, nat_p m → n + ordsucc m = ordsucc (n + m)

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

∀n : set, nat_p n → ∀m : set, nat_p m → nat_p (n + m)

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

1 + 1 = 2

Definition. We define mul_nat to be λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r) m of type set → set → set.

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

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

∀n : set, n * 0 = 0

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

∀n m : set, nat_p m → n * ordsucc m = n + n * m

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

∀n : set, nat_p n → ∀m : set, nat_p m → nat_p (n * m)

End of Section NatArith

Beginning of Section pair_setsum

Let pair ≝ setsum

Definition. We define proj0 to be λZ ⇒ {Unj z|z ∈ Z, ∃x : set, Inj0 x = z} of type set → set.

Definition. We define proj1 to be λZ ⇒ {Unj z|z ∈ Z, ∃y : set, Inj1 y = z} of type set → set.

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

Inj0 = pair 0

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

Inj1 = pair 1

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

∀X Y x, x ∈ X → pair 0 x ∈ pair X Y

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

∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y

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

∀X Y z, z ∈ pair X Y → (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)

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

∀X Y x, pair 0 x ∈ pair X Y → x ∈ X

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

∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y

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

∀w u : set, pair 0 u ∈ w → u ∈ proj0 w

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

∀w u : set, u ∈ proj0 w → pair 0 u ∈ w

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

∀w u : set, pair 1 u ∈ w → u ∈ proj1 w

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

∀w u : set, u ∈ proj1 w → pair 1 u ∈ w

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

∀X Y : set, proj0 (pair X Y) = X

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

∀X Y : set, proj1 (pair X Y) = Y

Definition. We define Sigma to be λX Y ⇒ ⋃_{x ∈ X}{pair x y|y ∈ Y x} of type set → (set → set) → set.

Notation. We use ∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.

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

∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, pair x y ∈ ∑x ∈ X, Y x

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

∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = z ∧ proj0 z ∈ X ∧ proj1 z ∈ Y (proj0 z)

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

∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = z

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

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj0 z ∈ X

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

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj1 z ∈ Y (proj0 z)

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

∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → y ∈ Y x

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

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → ∃x ∈ X, ∃y ∈ Y x, z = pair x y

Definition. We define setprod to be λX Y : set ⇒ ∑x ∈ X, Y of type set → set → set.

Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.

Let lam : set → (set → set) → set ≝ Sigma

Definition. We define ap to be λf x ⇒ {proj1 z|z ∈ f, ∃y : set, z = pair x y} of type set → set → set.

Notation. When x is a set, a term x y is notation for ap x y.

Notation. λ x ∈ A ⇒ B is notation for the set Sigma A (λ x : set ⇒ B).

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

∀X : set, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, pair x y ∈ λx ∈ X ⇒ F x

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

∀X : set, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = pair x y

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

∀f x y, pair x y ∈ f → y ∈ f x

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

∀f x y, y ∈ f x → pair x y ∈ f

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

∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x

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

∀u, proj0 u = u 0

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

∀u, proj1 u = u 1

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

∀x y : set, (pair x y) 0 = x

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

∀x y : set, (pair x y) 1 = y

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

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X

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

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 1) ∈ (Y (z 0))

Definition. We define pair_p to be λu : set ⇒ pair (u 0) (u 1) = u of type set → prop.

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

∀x y, pair_p (pair x y)

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

2 ⊆ {0,1}

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

∀x y : set, pair x y = (x,y)

Definition. We define Pi to be λX Y ⇒ {f ∈ 𝒫 (∑x ∈ X, ⋃ (Y x))|∀x ∈ X, f x ∈ Y x} of type set → (set → set) → set.

Notation. We use ∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.

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

∀X : set, ∀Y : set → set, ∀f : set, (∀u ∈ f, pair_p u ∧ u 0 ∈ X) → (∀x ∈ X, f x ∈ Y x) → f ∈ ∏x ∈ X, Y x

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

∀X : set, ∀Y : set → set, ∀F : set → set, (∀x ∈ X, F x ∈ Y x) → (λx ∈ X ⇒ F x) ∈ (∏x ∈ X, Y x)

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

∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (∏x ∈ X, Y x) → x ∈ X → f x ∈ Y x

Definition. We define setexp to be λX Y : set ⇒ ∏y ∈ Y, X of type set → set → set.

Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.

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

pair = (λx y ⇒ (x,y))

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

∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x

Beginning of Section Tuples

Variable x0 x1 : set

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

(x0,x1) 0 = x0

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

(x0,x1) 1 = x1

End of Section Tuples

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

∀X Y, ∀F G : set → set → set, (∀x ∈ X, ∀y ∈ Y, F x y = G x y) → {F (w 0) (w 1)|w ∈ X ⨯ Y} = {G (w 0) (w 1)|w ∈ X ⨯ Y}

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

∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, (x,y) ∈ ∑x ∈ X, Y x

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

∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y

End of Section pair_setsum

Beginning of Section TaggedSets

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

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

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

¬ TransSet {1}

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

¬ ordinal {1}

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

∀y, ¬ ordinal (y ')

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

∀alpha y, ordinal alpha → (y ') ∉ alpha

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

∀alpha beta, ordinal alpha → alpha ' = beta ' → alpha ⊆ beta

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

∀alpha beta, ordinal alpha → ordinal beta → alpha ' = beta ' → alpha = beta

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

∀alpha beta, ordinal alpha → ordinal beta → beta ' ∈ {gamma '|gamma ∈ alpha} → beta ∈ alpha

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

∀alpha Y, ordinal alpha → alpha ∉ {y '|y ∈ Y}

Definition. We define SNoElts_ to be λalpha ⇒ alpha ∪ {beta '|beta ∈ alpha} of type set → set.

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

∀alpha beta, alpha ⊆ beta → SNoElts_ alpha ⊆ SNoElts_ beta

Definition. We define SNo_ to be λalpha x ⇒ x ⊆ SNoElts_ alpha ∧ ∀beta ∈ alpha, exactly1of2 (beta ' ∈ x) (beta ∈ x) of type set → set → prop.

Definition. We define PSNo to be λalpha p ⇒ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta} of type set → (set → prop) → set.

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

∀alpha, ordinal alpha → ∀p : set → prop, PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo alpha p) p

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

∀alpha, ordinal alpha → ∀p : set → prop, SNo_ alpha (PSNo alpha p)

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

∀alpha x, ordinal alpha → SNo_ alpha x → x = PSNo alpha (λbeta ⇒ beta ∈ x)

Object. The name SNo is a term of type set → prop.

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

∀alpha, ordinal alpha → ∀z, SNo_ alpha z → SNo z

Object. The name SNoLev is a term of type set → set.

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

∀x alpha beta, ordinal alpha → ordinal beta → SNo_ alpha x → SNo_ beta x → alpha ⊆ beta

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

∀x alpha beta, ordinal alpha → ordinal beta → SNo_ alpha x → SNo_ beta x → alpha = beta

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

∀x, SNo x → ordinal (SNoLev x) ∧ SNo_ (SNoLev x) x

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

∀x, SNo x → ordinal (SNoLev x)

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

∀x, SNo x → SNo_ (SNoLev x) x

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

∀x, SNo x → x = PSNo (SNoLev x) (λbeta ⇒ beta ∈ x)

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

∀alpha, ordinal alpha → ∀p : set → prop, SNoLev (PSNo alpha p) = alpha

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

∀x y, SNo x → SNo y → SNoLev x ⊆ SNoLev y → (∀alpha ∈ SNoLev x, alpha ∈ x ↔ alpha ∈ y) → x ⊆ y

Definition. We define SNoEq_ to be λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y) of type set → set → set → prop.

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

∀alpha x y, (∀beta ∈ alpha, beta ∈ x ↔ beta ∈ y) → SNoEq_ alpha x y

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

∀x y, SNo x → SNo y → SNoLev x = SNoLev y → SNoEq_ (SNoLev x) x y → x = y

End of Section TaggedSets

Beginning of Section TaggedSets2

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

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

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

∀alpha, ordinal alpha → ∀x, ∀beta ∈ alpha, SNo_ beta x → x ∈ SNoS_ alpha

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

∀x y, SNo x → SNo y → SNoLev x ∈ SNoLev y → x ∈ SNoS_ (SNoLev y)

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

∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → SNoS_ alpha ⊆ SNoS_ beta

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

∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNoLev x = alpha

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

∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, ∀p : prop, (SNoLev x ∈ alpha → ordinal (SNoLev x) → SNo x → SNo_ (SNoLev x) x → p) → p

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

∀w, SNo w → ∀x ∈ SNoS_ (SNoLev w), x ≠ w

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

∀z, SNo z → z ∈ SNoS_ (ordsucc (SNoLev z))

Definition. We define SNoL to be λz ⇒ {x ∈ SNoS_ (SNoLev z)|x < z} of type set → set.

Definition. We define SNoR to be λz ⇒ {y ∈ SNoS_ (SNoLev z)|z < y} of type set → set.

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

∀z, SNo z → SNoCutP (SNoL z) (SNoR z)

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

∀x, SNo x → ∀w ∈ SNoL x, ∀p : prop, (SNo w → SNoLev w ∈ SNoLev x → w < x → p) → p

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

∀x, SNo x → ∀z ∈ SNoR x, ∀p : prop, (SNo z → SNoLev z ∈ SNoLev x → x < z → p) → p

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

∀z, SNoL z ⊆ SNoS_ (SNoLev z)

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

∀z, SNoR z ⊆ SNoS_ (SNoLev z)

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

∀x, SNo x → ∀w ∈ SNoL x, w ∈ SNoS_ (SNoLev x)

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

∀x, SNo x → ∀z ∈ SNoR x, z ∈ SNoS_ (SNoLev x)

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

∀z, SNo z → ∀x, SNo x → SNoLev x ∈ SNoLev z → x < z → x ∈ SNoL z

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

∀z, SNo z → ∀y, SNo y → SNoLev y ∈ SNoLev z → z < y → y ∈ SNoR z

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

∀z, SNo z → z = SNoCut (SNoL z) (SNoR z)

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

∀L R, SNoCutP L R → SNo (SNoCut L R)

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

∀L R, SNoCutP L R → ∀x ∈ L, x < SNoCut L R

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

∀L R, SNoCutP L R → ∀y ∈ R, SNoCut L R < y

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

∀L R, SNoCutP L R → ∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z

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

∀L1 R1 L2 R2, SNoCutP L1 R1 → SNoCutP L2 R2 → (∀w ∈ L1, w < SNoCut L2 R2) → (∀z ∈ R2, SNoCut L1 R1 < z) → SNoCut L1 R1 ≤ SNoCut L2 R2

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

∀L1 R1 L2 R2, SNoCutP L1 R1 → SNoCutP L2 R2 → (∀w ∈ L1, w < SNoCut L2 R2) → (∀z ∈ R1, SNoCut L2 R2 < z) → (∀w ∈ L2, w < SNoCut L1 R1) → (∀z ∈ R2, SNoCut L1 R1 < z) → SNoCut L1 R1 = SNoCut L2 R2

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

∀x y, SNo x → SNo y → x < y → ∀p : prop, (∀z ∈ SNoL y, z ∈ SNoR x → p) → (x ∈ SNoL y → p) → (y ∈ SNoR x → p) → p

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

∀x y, SNo x → SNo y → ∀p : prop, (x = y → p) → (∀z ∈ SNoL y, z ∈ SNoR x → p) → (x ∈ SNoL y → p) → (y ∈ SNoR x → p) → (∀z ∈ SNoR y, z ∈ SNoL x → p) → (x ∈ SNoR y → p) → (y ∈ SNoL x → p) → p

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

∀alpha, ordinal alpha → SNo_ alpha alpha

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

∀alpha, ordinal alpha → SNo alpha

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

∀alpha, ordinal alpha → SNoLev alpha = alpha

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

∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ alpha → z < alpha

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

∀alpha, ordinal alpha → SNoL alpha = SNoS_ alpha

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

∀alpha, ordinal alpha → SNoR alpha = Empty

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

∀n, nat_p n → SNo n

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

∀n ∈ ω, SNo n

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

ω ⊆ SNoS_ ω

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

∀alpha, ordinal alpha → ∀beta ∈ alpha, beta < alpha

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

∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → z ≤ alpha

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

∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → alpha ≤ beta

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

∀alpha beta, ordinal alpha → ordinal beta → alpha < beta → alpha ∈ beta

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

∀m ∈ ω, 0 ≤ m

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

SNo 0

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

SNo 1

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

SNo 2

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

SNoLev 0 = 0

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

SNoCut 0 0 = 0

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

SNoL 0 = 0

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

SNoR 0 = 0

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

SNoL 1 = 1

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

SNoR 1 = 0

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

∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → SNoLev x = x

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

∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → ordinal x

Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∧ delta ≠ SNoLev x) of type set → set.

Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∨ delta = SNoLev x) of type set → set.

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

∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)

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

∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)

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

∀x, SNo x → SNo (SNo_extend0 x)

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

∀x, SNo x → SNo (SNo_extend1 x)

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

∀x, SNo x → SNoLev (SNo_extend0 x) = ordsucc (SNoLev x)

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

∀x, SNo x → SNoLev (SNo_extend1 x) = ordsucc (SNoLev x)

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

∀x, SNo x → SNoLev x ∉ SNo_extend0 x

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

∀x, SNo x → SNoLev x ∈ SNo_extend1 x

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

∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend0 x) x

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

∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend1 x) x

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

∀x, SNo x → SNoLev x = 0 → x = 0

Definition. We define eps_ to be λn ⇒ {0} ∪ {(ordsucc m) '|m ∈ n} of type set → set.

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

∀n alpha, ordinal alpha → alpha ∈ eps_ n → alpha = 0

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

eps_ 0 = 1

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

∀n ∈ ω, SNo_ (ordsucc n) (eps_ n)

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

∀n ∈ ω, SNo (eps_ n)

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

SNo (eps_ 1)

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

∀n ∈ ω, SNoLev (eps_ n) = ordsucc n

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

∀n ∈ ω, eps_ n ∈ SNoS_ ω

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

∀n ∈ ω, ∀m ∈ n, eps_ n < eps_ m

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

∀n ∈ ω, 0 < eps_ n

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

∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → eps_ n < x

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

∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc (ordsucc n)), 0 < x → eps_ n ≤ x

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

∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → SNoEq_ (SNoLev x) (eps_ n) x → ∃m ∈ n, x = eps_ m

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

∀n ∈ ω, SNoCutP {0} {eps_ m|m ∈ n}

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

∀n ∈ ω, eps_ n = SNoCut {0} {eps_ m|m ∈ n}

End of Section TaggedSets2

Beginning of Section SurrealRecI

Variable F : set → (set → set) → set

Let default : set ≝ Eps_i (λ_ ⇒ True)

Let G : set → (set → set → set) → set → set ≝ λalpha g ⇒ If_ii (ordinal alpha) (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : set ⇒ default)

Object. The name SNo_rec_i is a term of type set → set.

Hypothesis Fr : ∀z, SNo z → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h

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

∀z, SNo z → SNo_rec_i z = F z SNo_rec_i

End of Section SurrealRecI

Beginning of Section SurrealRecII

Variable F : set → (set → (set → set)) → (set → set)

Let default : (set → set) ≝ Descr_ii (λ_ ⇒ True)

Let G : set → (set → set → (set → set)) → set → (set → set) ≝ λalpha g ⇒ If_iii (ordinal alpha) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : set ⇒ default)

Object. The name SNo_rec_ii is a term of type set → (set → set).

Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set), (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h

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

∀z, SNo z → SNo_rec_ii z = F z SNo_rec_ii

End of Section SurrealRecII

Beginning of Section SurrealRec2

Variable F : set → set → (set → set → set) → set

Let G : set → (set → set → set) → set → (set → set) → set ≝ λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y)

Let H : set → (set → set → set) → set → set ≝ λw f z ⇒ if SNo z then SNo_rec_i (G w f) z else Empty

Object. The name SNo_rec2 is a term of type set → set → set.

Hypothesis Fr : ∀w, SNo w → ∀z, SNo z → ∀g h : set → set → set, (∀x ∈ SNoS_ (SNoLev w), ∀y, SNo y → g x y = h x y) → (∀y ∈ SNoS_ (SNoLev z), g w y = h w y) → F w z g = F w z h

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

∀w, SNo w → ∀f k : set → set → set, (∀x ∈ SNoS_ (SNoLev w), f x = k x) → ∀z, SNo z → ∀g h : set → set, (∀u ∈ SNoS_ (SNoLev z), g u = h u) → G w f z g = G w k z h

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

∀w, SNo w → ∀f : set → set → set, ∀z, SNo z → SNo_rec_i (G w f) z = G w f z (SNo_rec_i (G w f))

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

∀w, SNo w → ∀z, SNo z → SNo_rec2 w z = F w z SNo_rec2

End of Section SurrealRec2

Beginning of Section SurrealMinus

Object. The name minus_SNo is a term of type set → set.

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 490 and no associativity corresponding to applying term SNoLe.

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

∀x, SNo x → - x = SNoCut {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}

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

∀x, SNo x → SNo (- x) ∧ (∀u ∈ SNoL x, - x < - u) ∧ (∀u ∈ SNoR x, - u < - x) ∧ SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}

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

∀x, SNo x → SNo (- x)

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

∀x y, SNo x → SNo y → x < y → - y < - x

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

∀x y, SNo x → SNo y → x ≤ y → - y ≤ - x

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

∀x, SNo x → SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}

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

∀L R, SNoCutP L R → SNoCutP {- z|z ∈ R} {- w|w ∈ L}

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

∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, SNoLev (- x) ⊆ SNoLev x

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

∀x, SNo x → SNoLev (- x) ⊆ SNoLev x

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

∀x, SNo x → - - x = x

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

∀x, SNo x → SNoLev (- x) = SNoLev x

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

∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNo_ alpha (- x)

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

∀alpha, ordinal alpha → ∀x, x ∈ SNoS_ alpha → - x ∈ SNoS_ alpha

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

∀v, SNo v → ∀L R, SNoCutP L R → v = SNoCut L R → - v = SNoCut {- z|z ∈ R} {- w|w ∈ L}

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

∀L R, SNoCutP L R → - SNoCut L R = SNoCut {- z|z ∈ R} {- w|w ∈ L}

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

∀x y, SNo x → SNo y → - x < y → - y < x

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

∀x y, SNo x → SNo y → x < - y → y < - x

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

∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → - alpha ≤ z

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

∀x ∈ SNoS_ ω, - x ∈ SNoS_ ω

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

∀x, SNo x → SNoL (- x) = {- w|w ∈ SNoR x}

End of Section SurrealMinus

Beginning of Section SurrealAdd

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

Object. The name add_SNo is a term of type set → set → set.

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

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

∀x, SNo x → ∀y, SNo y → x + y = SNoCut ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})

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

∀x y, SNo x → SNo y → SNo (x + y) ∧ (∀u ∈ SNoL x, u + y < x + y) ∧ (∀u ∈ SNoR x, x + y < u + y) ∧ (∀u ∈ SNoL y, x + u < x + y) ∧ (∀u ∈ SNoR y, x + y < x + u) ∧ SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})

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

∀x y, SNo x → SNo y → SNo (x + y)

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

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

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

∀x y z, SNo x → SNo y → SNo z → SNo (x + y + - z)

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

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

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

∀x y z, SNo x → SNo y → SNo z → x < z → x + y < z + y

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

∀x y z, SNo x → SNo y → SNo z → x ≤ z → x + y ≤ z + y

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

∀x y z, SNo x → SNo y → SNo z → y < z → x + y < x + z

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

∀x y z, SNo x → SNo y → SNo z → y ≤ z → x + y ≤ x + z

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

∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y ≤ w → x + y < z + w

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

∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y < w → x + y < z + w

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

∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y < w → x + y < z + w

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

∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y ≤ w → x + y ≤ z + w

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

∀x y, SNo x → SNo y → SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})

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

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

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

∀x, SNo x → 0 + x = x

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

∀x, SNo x → x + 0 = x

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

∀x, SNo x → - x + x = 0

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

∀x, SNo x → x + - x = 0

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

∀alpha, ordinal alpha → ∀beta, ordinal beta → SNoCutP ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty

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

∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + beta = SNoCut ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty

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

∀alpha, ordinal alpha → ∀beta, ordinal beta → ordinal (alpha + beta)

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

∀alpha, ordinal alpha → ∀beta, ordinal beta → ordsucc alpha + beta = ordsucc (alpha + beta)

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

∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + ordsucc beta = ordsucc (alpha + beta)

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

∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ alpha, gamma + beta ∈ alpha + beta

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

∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ beta, alpha + gamma ∈ alpha + beta

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

∀n m ∈ ω, add_nat n m = n + m

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

∀n m ∈ ω, n + m ∈ ω

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

1 + 1 = 2

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

∀x y, SNo x → SNo y → ∀u ∈ SNoL (x + y), (∃v ∈ SNoL x, u ≤ v + y) ∨ (∃v ∈ SNoL y, u ≤ x + v)

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

∀x y, SNo x → SNo y → ∀u ∈ SNoR (x + y), (∃v ∈ SNoR x, v + y ≤ u) ∨ (∃v ∈ SNoR y, x + v ≤ u)

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

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

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

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

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

- 0 = 0

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

∀x y, SNo x → SNo y → - (x + y) = (- x) + (- y)

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

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

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

∀x y, SNo x → SNo y → SNoLev (x + y) ⊆ SNoLev x + SNoLev y

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

∀x y ∈ SNoS_ ω, x + y ∈ SNoS_ ω

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

∀x y, SNo x → SNo y → (x + y) + - y = x

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

∀x y, SNo x → SNo y → (x + - y) + y = x

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

∀x y, SNo x → SNo y → - x + (x + y) = y

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

∀x y, SNo x → SNo y → x + (- x + y) = y

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

∀x y z, SNo x → SNo y → SNo z → x + y < z + y → x < z

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

∀x y z, SNo x → SNo y → SNo z → x + y < x + z → y < z

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

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

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

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

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

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

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

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

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

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

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

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

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

∀x y z w v, SNo x → SNo y → SNo z → SNo w → SNo v → x + y + z + w + v = v + x + y + z + w

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

∀x y z w v, SNo x → SNo y → SNo z → SNo w → SNo v → x + y + z + w + v = w + v + x + y + z

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

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

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

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

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

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

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

∀x y z, SNo x → SNo y → SNo z → x + - y < z → x < z + y

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

∀x y z, SNo x → SNo y → SNo z → z < x + - y → z + y < x

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

∀x y z, SNo x → SNo y → SNo z → x < z + y → x + - y < z

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

∀x y z, SNo x → SNo y → SNo z → z + y < x → z < x + - y

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

∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y < w + z → x + y + - z < w

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

∀x y z w, SNo x → SNo y → SNo z → SNo w → w + z < x + y → w < x + y + - z

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

∀x y z u v w, SNo x → SNo y → SNo z → SNo u → SNo v → SNo w → x + y + w < u + v + z → x + y + - z < u + v + - w

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

∀x y z, SNo x → SNo y → SNo z → z ≤ x + - y → z + y ≤ x

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

∀x y z, SNo x → SNo y → SNo z → z + y ≤ x → z ≤ x + - y

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

∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + u < z + v → y + v < w + u → x + y < z + w

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

∀x y z w u a, SNo x → SNo y → SNo z → SNo w → SNo u → SNo a → x + z < w + a → y + a < u → x + y + z < w + u

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

∀x y w u v a, SNo x → SNo y → SNo w → SNo u → SNo v → SNo a → x + a < w + v → y < a + u → x + y < w + u + v

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

∀x y z w u a b c, SNo x → SNo y → SNo z → SNo w → SNo u → SNo a → SNo b → SNo c → x + a < b + c → y + c < u → b + z < w + a → x + y + z < w + u

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

∀x y w u v a b c, SNo x → SNo y → SNo w → SNo u → SNo v → SNo a → SNo b → SNo c → x + a < b + v → y < c + u → b + c < w + a → x + y < w + u + v

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

∀alpha, ordinal alpha → ordsucc alpha = 1 + alpha

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

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

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

∀n ∈ ω, n + 1 = ordsucc n

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

∀x, SNo x → ∀n ∈ ω, x < x + eps_ n

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

∀x y, SNo x → SNo y → ∀n ∈ ω, x < y → x < y + eps_ n

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

∀x y, SNo x → SNo y → x < y → 0 < y + - x

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

∀m, ∀n ∈ ω, ∀k, nat_p k → m ∈ n + k → m ∈ n ∨ m + - n ∈ k

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

∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x < w → y < u → z < v → x + y + z < w + u + v

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

∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → x + y < z + w → x + y + u < z + w + u

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

∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → y + x < z + w → x + u + y < z + w + u

End of Section SurrealAdd

Beginning of Section SurrealMul

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.

Definition. We define mul_SNo to be SNo_rec2 (λx y m ⇒ SNoCut ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|z ∈ SNoR x ⨯ SNoL y})) of type set → set → set.

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

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

∀x, SNo x → ∀y, SNo y → x * y = SNoCut ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoL y})

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

∀x y, SNo x → SNo y → ∀p : prop, (∀L R, (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p

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

∀x, SNo x → ∀y, SNo y → ∀p : prop, (SNo (x * y) → (∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v) → (∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v) → p) → p

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

∀x y, SNo x → SNo y → SNo (x * y)

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

∀x y u v, SNo x → SNo y → SNo u → SNo v → SNo (u * y + x * v + - (u * v))

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

∀x y z, SNo x → SNo y → SNo z → SNo (x * y * z)

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

∀x y, SNo x → SNo y → ∀p : prop, (∀L R, SNoCutP L R → (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p

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

∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v

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

∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v

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

∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), (∃v ∈ SNoL x, ∃w ∈ SNoL y, u + v * w ≤ v * y + x * w) ∨ (∃v ∈ SNoR x, ∃w ∈ SNoR y, u + v * w ≤ v * y + x * w)

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

∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL y, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoR y, u + v * w ≤ v * y + x * w → p) → p

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

∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), (∃v ∈ SNoL x, ∃w ∈ SNoR y, v * y + x * w ≤ u + v * w) ∨ (∃v ∈ SNoR x, ∃w ∈ SNoL y, v * y + x * w ≤ u + v * w)

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

∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR y, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoL y, v * y + x * w ≤ u + v * w → p) → p

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

∀x y X Y Z W, ∀U U', (∀u, u ∈ U → (∀q : prop, (∀w0 ∈ X, ∀w1 ∈ Y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ Z, ∀z1 ∈ W, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ X, ∀w1 ∈ Y, w0 * y + x * w1 + - w0 * w1 ∈ U') → (∀w0 ∈ Z, ∀w1 ∈ W, w0 * y + x * w1 + - w0 * w1 ∈ U') → U ⊆ U'

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

∀x, SNo x → x * 0 = 0

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

∀x, SNo x → x * 1 = x

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

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

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

∀x y, SNo x → SNo y → (- x) * y = - x * y

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

∀x y, SNo x → SNo y → x * (- y) = - (x * y)

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

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

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

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

Beginning of Section mul_SNo_assoc_lems

Variable M : set → set → set

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

Hypothesis SNo_M : ∀x y, SNo x → SNo y → SNo (x * y)

Hypothesis DL : ∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z

Hypothesis DR : ∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z

Hypothesis IL : ∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL y, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoR y, u + v * w ≤ v * y + x * w → p) → p

Hypothesis IR : ∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR y, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoL y, v * y + x * w ≤ u + v * w → p) → p

Hypothesis M_Lt : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v

Hypothesis M_Le : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v

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

∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), u * (y * z) = (u * y) * z) → (∀v ∈ SNoS_ (SNoLev y), x * (v * z) = (x * v) * z) → (∀w ∈ SNoS_ (SNoLev z), x * (y * w) = (x * y) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), u * (v * z) = (u * v) * z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), u * (y * w) = (u * y) * w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), x * (v * w) = (x * v) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), u * (v * w) = (u * v) * w) → ∀L, (∀u ∈ L, ∀q : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL (y * z), u = v * (y * z) + x * w + - v * w → q) → (∀v ∈ SNoR x, ∀w ∈ SNoR (y * z), u = v * (y * z) + x * w + - v * w → q) → q) → ∀u ∈ L, u < (x * y) * z

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

∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), u * (y * z) = (u * y) * z) → (∀v ∈ SNoS_ (SNoLev y), x * (v * z) = (x * v) * z) → (∀w ∈ SNoS_ (SNoLev z), x * (y * w) = (x * y) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), u * (v * z) = (u * v) * z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), u * (y * w) = (u * y) * w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), x * (v * w) = (x * v) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), u * (v * w) = (u * v) * w) → ∀R, (∀u ∈ R, ∀q : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR (y * z), u = v * (y * z) + x * w + - v * w → q) → (∀v ∈ SNoR x, ∀w ∈ SNoL (y * z), u = v * (y * z) + x * w + - v * w → q) → q) → ∀u ∈ R, (x * y) * z < u

End of Section mul_SNo_assoc_lems

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

∀x y z, SNo x → SNo y → SNo z → x * (y * z) = (x * y) * z

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

∀n m ∈ ω, mul_nat n m = n * m

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

∀n m ∈ ω, n * m ∈ ω

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

∀x, SNo x → 0 * x = 0

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

∀x, SNo x → 1 * x = x

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

∀x y z, SNo x → 0 < x → SNo y → SNo z → y < z → x * y < x * z

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

∀x y z, SNo x → 0 ≤ x → SNo y → SNo z → y ≤ z → x * y ≤ x * z

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

∀x y z, SNo x → x < 0 → SNo y → SNo z → z < y → x * y < x * z

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

∀x y z, SNo x → SNo y → SNo z → 0 < z → x < y → x * z < y * z

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

∀x y, SNo x → SNo y → x < 1 → 0 < y → x * y < y

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

∀x y z, SNo x → SNo y → SNo z → 0 ≤ z → x ≤ y → x * z ≤ y * z

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

∀x y, SNo x → SNo y → x ≤ 1 → 0 ≤ y → x * y ≤ y

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

∀x y z w, SNo x → SNo y → SNo z → SNo w → 0 < x → 0 < y → x < z → y < w → x * y < z * w

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

∀x y z w, SNo x → SNo y → SNo z → SNo w → 0 ≤ x → 0 ≤ y → x ≤ z → y ≤ w → x * y ≤ z * w

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

∀x y, SNo x → SNo y → 0 < x → 0 < y → 0 < x * y

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

∀x y, SNo x → SNo y → 0 < x → y < 0 → x * y < 0

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

∀x y, SNo x → SNo y → x < 0 → 0 < y → x * y < 0

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

∀x y, SNo x → SNo y → x < 0 → y < 0 → 0 < x * y

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

∀x, SNo x → 0 ≤ x * x

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

∀x, SNo x → x = 0 ∨ 0 < x * x

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

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

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

∀x y, SNo x → SNo y → (- x) * (- y) = x * y

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

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

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

∀x y z, SNo x → SNo y → SNo z → (x * y) * z = (x * z) * y

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

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

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

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

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

∀x y z w, SNo x → SNo y → SNo z → SNo w → x * y * z * w = w * x * y * z

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

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

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

∀x y z, SNo x → x ≠ 0 → SNo y → SNo z → x * y = x * z → y = z

End of Section SurrealMul

Beginning of Section SurrealExp

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.

Definition. We define exp_SNo_nat to be λn m : set ⇒ nat_primrec 1 (λ_ r ⇒ n * r) m of type set → set → set.

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

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

∀x, SNo x → x ^ 0 = 1

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

∀x, SNo x → ∀n, nat_p n → x ^ (ordsucc n) = x * x ^ n

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

∀x, SNo x → ∀n, nat_p n → SNo (x ^ n)

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

∀x, nat_p x → ∀n, nat_p n → nat_p (x ^ n)

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

∀n, nat_p n → eps_ (ordsucc n) + eps_ (ordsucc n) = eps_ n

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

eps_ 1 + eps_ 1 = 1

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

2 * eps_ 1 = 1

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

∀x y z, SNo x → SNo y → SNo z → x + x = y + z → x = eps_ 1 * (y + z)

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

∀x, SNo x → 1 ≤ x → ∀n, nat_p n → 1 ≤ x ^ n

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

∀n, nat_p n → n < 2 ^ n

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

∀n, nat_p n → eps_ n * 2 ^ n = 1

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

∀n ∈ ω, eps_ n ≤ 1

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

∀n, nat_p n → 2 ^ n * eps_ n = 1

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

∀x, SNo x → ∀m, nat_p m → ∀n, nat_p n → x ^ m * x ^ n = x ^ (m + n)

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

∀x, SNo x → ∀m n ∈ ω, x ^ m * x ^ n = x ^ (m + n)

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

∀x, SNo x → 0 < x → ∀n, nat_p n → 0 < x ^ n

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

∀m n ∈ ω, eps_ m * eps_ n = eps_ (m + n)

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

∀n, nat_p n → equip {x ∈ SNoS_ ω|SNoLev x = n} (2 ^ n)

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

∀n ∈ ω, finite (SNoS_ n)

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

∀x ∈ SNoS_ ω, finite (SNoL x)

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

∀x ∈ SNoS_ ω, finite (SNoR x)

End of Section SurrealExp

Beginning of Section Int

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.

Object. The name int is a term of type set.

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

∀p : set → prop, (∀n ∈ ω, p n) → (∀n ∈ ω, p (- n)) → ∀x ∈ int, p x

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

∀x ∈ int, SNo x

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

ω ⊆ int

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

∀n ∈ ω, - n ∈ int

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

∀n ∈ ω, ∀m, nat_p m → - n + m ∈ int

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

∀x y ∈ int, x + y ∈ int

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

∀x ∈ int, - x ∈ int

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

∀x y ∈ int, x * y ∈ int

End of Section Int

Beginning of Section SurrealAbs

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.

Definition. We define abs_SNo to be λx ⇒ if 0 ≤ x then x else - x of type set → set.

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

∀x, 0 ≤ x → abs_SNo x = x

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

∀x, ¬ (0 ≤ x) → abs_SNo x = - x

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

abs_SNo 0 = 0

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

∀x, 0 < x → abs_SNo x = x

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

∀x, SNo x → x < 0 → abs_SNo x = - x

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

∀x, SNo x → SNo (abs_SNo x)

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

∀x, SNo x → SNoLev (abs_SNo x) = SNoLev x

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

∀x, SNo x → abs_SNo (- x) = abs_SNo x

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

∀x y, SNo x → SNo y → abs_SNo (x + - y) = abs_SNo (y + - x)

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

∀x y, SNo x → SNo y → abs_SNo (x + y) ≤ abs_SNo x + abs_SNo y

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

∀x y z, SNo x → SNo y → SNo z → abs_SNo (x + - z) ≤ abs_SNo (x + - y) + abs_SNo (y + - z)

End of Section SurrealAbs

Beginning of Section SNoMaxMin

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 342 and which associates to the right corresponding to applying term exp_SNo_nat.

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.

Definition. We define SNo_max_of to be λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X, SNo y → y ≤ x of type set → set → prop.

Definition. We define SNo_min_of to be λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X, SNo y → x ≤ y of type set → set → prop.

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

∀X y, (∀x ∈ X, SNo x) → SNo_max_of X y → SNo_min_of {- x|x ∈ X} (- y)

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

∀X y, (∀x ∈ X, SNo x) → SNo_max_of {- x|x ∈ X} y → SNo_min_of X (- y)

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

∀X y, (∀x ∈ X, SNo x) → SNo_min_of X y → SNo_max_of {- x|x ∈ X} (- y)

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

∀x y, SNo x → SNo_max_of (SNoL x) y → ∀z, SNo z → x < z → y + z < x + x → ∃w ∈ SNoR z, y + w = x + x

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

∀x y, SNo x → SNo_min_of (SNoR x) y → ∀z, SNo z → z < x → x + x < y + z → ∃w ∈ SNoL z, y + w = x + x

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

∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_max_of X x

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

∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_min_of X x

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

∀x ∈ SNoS_ ω, SNoL x = 0 ∨ ∃y, SNo_max_of (SNoL x) y

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

∀x ∈ SNoS_ ω, SNoR x = 0 ∨ ∃y, SNo_min_of (SNoR x) y

End of Section SNoMaxMin

Beginning of Section DiadicRationals

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

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

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

∀k ∈ ω, ∀n, nat_p n → eps_ k * n ∈ SNoS_ ω

Definition. We define diadic_rational_p to be λx ⇒ ∃k ∈ ω, ∃m ∈ int, x = eps_ k * m of type set → prop.

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

∀x, diadic_rational_p x → x ∈ SNoS_ ω

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

∀m ∈ int, diadic_rational_p m

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

∀m ∈ ω, diadic_rational_p m

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

∀k ∈ ω, diadic_rational_p (eps_ k)

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

∀x, diadic_rational_p x → diadic_rational_p (- x)

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

∀x y, diadic_rational_p x → diadic_rational_p y → diadic_rational_p (x * y)

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

∀x y, diadic_rational_p x → diadic_rational_p y → diadic_rational_p (x + y)

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

∀n, nat_p n → ∀x, SNo x → SNoLev x = n → diadic_rational_p x

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

∀x ∈ SNoS_ ω, diadic_rational_p x

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

∀x y ∈ SNoS_ ω, x * y ∈ SNoS_ ω

End of Section DiadicRationals

Beginning of Section Reals

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

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

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

∀x ∈ SNoS_ ω, ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k

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

∀x ∈ SNoS_ (ordsucc ω), x < ω → ∃N ∈ ω, x < N

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

∀x ∈ SNoS_ (ordsucc ω), - ω < x → ∃N ∈ ω, - N < x

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

∀x ∈ SNoS_ (ordsucc ω), - ω < x → x < ω → ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k

Object. The name real is a term of type set.

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

∀x ∈ SNoS_ (ordsucc ω), x ≠ ω → x ≠ - ω → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → x ∈ real

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

∀x ∈ real, ∀p : prop, (SNo x → SNoLev x ∈ ordsucc ω → x ∈ SNoS_ (ordsucc ω) → - ω < x → x < ω → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → p) → p

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

∀x ∈ real, SNo x

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

∀x ∈ real, ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x

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

SNoS_ ω ⊆ real

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

0 ∈ real

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

1 ∈ real

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

∀x ∈ real, ∀w, SNo w → SNoLev w ∈ SNoLev x → w ∈ SNoS_ ω

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

∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - - x) < eps_ k) → q = - x)

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

∀x, SNo x → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < - x ∧ - x < q + eps_ k)

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

∀x, SNo x → 0 < x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∀k ∈ ω, ∀p : prop, (∀q ∈ SNoS_ ω, 0 < q → q < x → x < q + eps_ k → p) → p

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

∀x ∈ real, - x ∈ real

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

∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∃f ∈ SNoS_ ω^ω, ∀n ∈ ω, f n < x ∧ x < f n + eps_ n ∧ ∀i ∈ n, f i < f n

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

∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∃g ∈ SNoS_ ω^ω, ∀n ∈ ω, g n + - eps_ n < x ∧ x < g n ∧ ∀i ∈ n, g n < g i

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

∀lambda, ordinal lambda → (∀alpha ∈ lambda, ordsucc alpha ∈ lambda) → ∀L R ⊆ SNoS_ lambda, SNoCutP L R → SNoLev (SNoCut L R) ∈ ordsucc lambda

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

∀L R ⊆ SNoS_ ω, SNoCutP L R → SNoLev (SNoCut L R) ∈ ordsucc ω

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

∀f g ∈ SNoS_ ω^ω, (∀n m ∈ ω, f n < g m) → ∀p : prop, (SNoCutP {f n|n ∈ ω} {g n|n ∈ ω} → SNo (SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) → SNoLev (SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) ∈ ordsucc ω → SNoCut {f n|n ∈ ω} {g n|n ∈ ω} ∈ SNoS_ (ordsucc ω) → (∀n ∈ ω, f n < SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) → (∀n ∈ ω, SNoCut {f n|n ∈ ω} {g n|n ∈ ω} < g n) → p) → p

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

∀x, SNo x → ∀f g ∈ SNoS_ ω^ω, (∀n ∈ ω, f n < x) → (∀n ∈ ω, x < f n + eps_ n) → (∀n ∈ ω, ∀i ∈ n, f i < f n) → (∀n ∈ ω, x < g n) → (∀n ∈ ω, ∀i ∈ n, g n < g i) → x = SNoCut {f n|n ∈ ω} {g n|n ∈ ω} → x ∈ real

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

∀x ∈ real, ∀p : prop, (∀f g ∈ SNoS_ ω^ω, (∀n ∈ ω, f n < x) → (∀n ∈ ω, x < f n + eps_ n) → (∀n ∈ ω, ∀i ∈ n, f i < f n) → (∀n ∈ ω, g n + - eps_ n < x) → (∀n ∈ ω, x < g n) → (∀n ∈ ω, ∀i ∈ n, g n < g i) → SNoCutP {f n|n ∈ ω} {g n|n ∈ ω} → x = SNoCut {f n|n ∈ ω} {g n|n ∈ ω} → p) → p

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

∀x y ∈ real, x + y ∈ real

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

∀x ∈ SNoS_ (ordsucc ω), 0 < x → x < ω → ∃N ∈ ω, eps_ N * x < 1

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

∀x y ∈ real, 0 < x → 0 < y → x * y ∈ real

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

∀x y ∈ real, x * y ∈ real

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

∀x y z, SNo x → SNo y → SNo z → x ≤ y → y < x + z → abs_SNo (y + - x) < z

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

∀x ∈ real, 0 < x → x < 1 → ∃y ∈ real, x * y = 1

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

∀x ∈ real, 0 < x → ∃y ∈ real, x * y = 1

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

∀x ∈ real, x ≠ 0 → ∃y ∈ real, x * y = 1

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

∀x y ∈ real, 0 < x → 0 ≤ y → ∃n ∈ ω, y ≤ n * x

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

∀a b ∈ real^ω, (∀n ∈ ω, a n ≤ b n ∧ a n ≤ a (ordsucc n) ∧ b (ordsucc n) ≤ b n) → ∃x ∈ real, ∀n ∈ ω, a n ≤ x ∧ x ≤ b n

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

∀a b ∈ real^ω, (∀n ∈ ω, a n ≤ b n ∧ a n ≤ a (n + 1) ∧ b (n + 1) ≤ b n) → ∃x ∈ real, ∀n ∈ ω, a n ≤ x ∧ x ≤ b n

End of Section Reals

Beginning of Section ComplexSNo

Beginning of Section CTaggedSets

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

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

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

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

Theorem. (not_TransSet_Sing2) The following is provable:

¬ TransSet {2}

Proof:

Assume H1: TransSet {2}.

We prove the intermediate claim L1: 0 ∈ {2}.

An exact proof term for the current goal is H1 2 (SingI 2) 0 In_0_2.

Apply neq_0_2 to the current goal.

An exact proof term for the current goal is SingE 2 0 L1.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (not_ordinal_Sing2) The following is provable:

¬ ordinal {2}

Proof:

Assume H1.

Apply H1 to the current goal.

Assume H2 _.

An exact proof term for the current goal is not_TransSet_Sing2 H2.

∎

Try to prove it yourself. Main Goal

Theorem. (ctagged_not_ordinal) The following is provable:

∀y, ¬ ordinal (y '')

Proof:

Let y be given.

Assume H1: ordinal (y '').

We prove the intermediate claim L1: {2} ∈ y ''.

We will prove {2} ∈ y ∪ {{2}}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is SingI {2}.

Apply not_ordinal_Sing2 to the current goal.

An exact proof term for the current goal is ordinal_Hered (y '') H1 {2} L1.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (ctagged_notin_ordinal) The following is provable:

∀alpha y, ordinal alpha → (y '') ∉ alpha

Proof:

Let alpha and y be given.

Assume H1 H2.

Apply ctagged_not_ordinal y to the current goal.

An exact proof term for the current goal is ordinal_Hered alpha H1 (y '') H2.

∎

Try to prove it yourself. Main Goal

Theorem. (Sing2_notin_SingSing1) The following is provable:

{2} ∉ {{1}}

Proof:

Assume H1: {2} ∈ {{1}}.

We prove the intermediate claim L1: 1 ∈ {2}.

rewrite the current goal using SingE {1} {2} H1 (from left to right).

An exact proof term for the current goal is SingI 1.

Apply neq_1_2 to the current goal.

We will prove 1 = 2.

An exact proof term for the current goal is SingE 2 1 L1.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (ctagged_notin_SNo) The following is provable:

∀x y, SNo x → (y '') ∉ x

Proof:

Let x and y be given.

Assume Hx: SNo x.

Assume Hyc: (y '') ∈ x.

We will prove False.

Set alpha to be the term SNoLev x.

Apply SNoLev_prop x Hx to the current goal.

Assume Ha: ordinal alpha.

Assume Hxa: SNo_ alpha x.

Apply Hxa to the current goal.

Assume Hxa1: x ⊆ SNoElts_ (SNoLev x).

We will prove False.

We prove the intermediate claim L1: y '' ∈ alpha ∪ {beta '|beta ∈ alpha}.

An exact proof term for the current goal is Hxa1 (y '') Hyc.

Apply binunionE alpha {beta '|beta ∈ alpha} (y '') L1 to the current goal.

Assume H1: y '' ∈ alpha.

An exact proof term for the current goal is ctagged_notin_ordinal alpha y Ha H1.

Assume H1: y '' ∈ {beta '|beta ∈ alpha}.

Apply ReplE_impred alpha (λbeta ⇒ beta ') (y '') H1 to the current goal.

Let beta be given.

Assume Hb: beta ∈ alpha.

Assume Hyb: y '' = beta '.

We prove the intermediate claim Lb: ordinal beta.

An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.

We prove the intermediate claim L2: {2} ∈ beta '.

rewrite the current goal using Hyb (from right to left).

We will prove {2} ∈ y ∪ {{2}}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is SingI {2}.

Apply binunionE beta {{1}} {2} L2 to the current goal.

Assume H2: {2} ∈ beta.

Apply not_ordinal_Sing2 to the current goal.

An exact proof term for the current goal is ordinal_Hered beta Lb {2} H2.

An exact proof term for the current goal is Sing2_notin_SingSing1.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal

Theorem. (ctagged_eqE_Subq) The following is provable:

∀x y, SNo x → SNo y → ∀u ∈ x, ∀v ∈ y, u '' = v '' → u ⊆ v

Proof:

Let x and y be given.

Assume Hx Hy.

Let u be given.

Assume Hu.

Let v be given.

Assume Hv Huv.

Let w be given.

Assume Hw: w ∈ u.

We prove the intermediate claim L1: w ∈ v ''.

rewrite the current goal using Huv (from right to left).

We will prove w ∈ u ∪ {{2}}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hw.

Apply binunionE v {{2}} w L1 to the current goal.

Assume H1: w ∈ v.

An exact proof term for the current goal is H1.

Assume H1: w ∈ {{2}}.

We will prove False.

We prove the intermediate claim L2: w = {2}.

An exact proof term for the current goal is SingE {2} w H1.

We prove the intermediate claim L3: {2} ∈ u.

rewrite the current goal using L2 (from right to left).

An exact proof term for the current goal is Hw.

Set alpha to be the term SNoLev x.

Apply SNoLev_prop x Hx to the current goal.

Assume Ha: ordinal alpha.

Assume Hxa: SNo_ alpha x.

Apply Hxa to the current goal.

Assume Hxa1: x ⊆ SNoElts_ alpha.

We will prove False.

Apply binunionE alpha {beta '|beta ∈ alpha} u (Hxa1 u Hu) to the current goal.

Assume H2: u ∈ alpha.

We prove the intermediate claim Lu: ordinal u.

An exact proof term for the current goal is ordinal_Hered alpha Ha u H2.

Apply not_ordinal_Sing2 to the current goal.

An exact proof term for the current goal is ordinal_Hered u Lu {2} L3.

Assume H2: u ∈ {beta '|beta ∈ alpha}.

Apply ReplE_impred alpha (λbeta ⇒ beta ') u H2 to the current goal.

Let beta be given.

Assume Hb: beta ∈ alpha.

Assume Hub: u = beta '.

We prove the intermediate claim Lb: ordinal beta.

An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.

We prove the intermediate claim L4: {2} ∈ beta '.

rewrite the current goal using Hub (from right to left).

An exact proof term for the current goal is L3.

Apply binunionE beta {{1}} {2} L4 to the current goal.

Assume H3: {2} ∈ beta.

Apply not_ordinal_Sing2 to the current goal.

An exact proof term for the current goal is ordinal_Hered beta Lb {2} H3.

An exact proof term for the current goal is Sing2_notin_SingSing1.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Main Goal

Theorem. (ctagged_eqE_eq) The following is provable:

∀x y, SNo x → SNo y → ∀u ∈ x, ∀v ∈ y, u '' = v '' → u = v

Proof:

Let x and y be given.

Assume Hx Hy.

Let u be given.

Assume Hu.

Let v be given.

Assume Hv Huv.

Apply set_ext to the current goal.

An exact proof term for the current goal is ctagged_eqE_Subq x y Hx Hy u Hu v Hv Huv.

Apply ctagged_eqE_Subq y x Hy Hx v Hv u Hu to the current goal.

Use symmetry.

An exact proof term for the current goal is Huv.

∎

Try to prove it yourself. Main Goal

Definition. We define SNo_pair to be λx y ⇒ x ∪ {u ''|u ∈ y} of type set → set → set.

Theorem. (SNo_pair_prop_1_Subq) The following is provable:

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

Proof:

Let x1, y1, x2 and y2 be given.

Assume Hx1.

Assume H1: SNo_pair x1 y1 = SNo_pair x2 y2.

Let v be given.

Assume Hv: v ∈ x1.

We prove the intermediate claim L1: v ∈ SNo_pair x2 y2.

rewrite the current goal using H1 (from right to left).

We will prove v ∈ x1 ∪ {u ''|u ∈ y1}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hv.

Apply binunionE x2 {u ''|u ∈ y2} v L1 to the current goal.

Assume H2: v ∈ x2.

An exact proof term for the current goal is H2.

Assume H2: v ∈ {u ''|u ∈ y2}.

We will prove False.

Apply ReplE_impred y2 (λu ⇒ u '') v H2 to the current goal.

Let u be given.

Assume Hu: u ∈ y2.

Assume Hvu: v = u ''.

Apply ctagged_notin_SNo x1 u Hx1 to the current goal.

We will prove u '' ∈ x1.

rewrite the current goal using Hvu (from right to left).

An exact proof term for the current goal is Hv.

∎

Try to prove it yourself. Subgoal 1 Main Goal

Theorem. (SNo_pair_prop_1) The following is provable:

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

Proof:

Let x1, y1, x2 and y2 be given.

Assume Hx1 Hx2.

Assume H1: SNo_pair x1 y1 = SNo_pair x2 y2.

Apply set_ext to the current goal.

An exact proof term for the current goal is SNo_pair_prop_1_Subq x1 y1 x2 y2 Hx1 H1.

Apply SNo_pair_prop_1_Subq x2 y2 x1 y1 Hx2 to the current goal.

Use symmetry.

An exact proof term for the current goal is H1.

∎

Try to prove it yourself. Main Goal

Theorem. (SNo_pair_prop_2_Subq) The following is provable:

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

Proof:

Let x1, y1, x2 and y2 be given.

Assume Hy1 Hx2 Hy2.

Assume H1: SNo_pair x1 y1 = SNo_pair x2 y2.

Let v be given.

Assume Hv: v ∈ y1.

We prove the intermediate claim L1: v '' ∈ SNo_pair x2 y2.

rewrite the current goal using H1 (from right to left).

We will prove v '' ∈ x1 ∪ {u ''|u ∈ y1}.

Apply binunionI2 to the current goal.

We will prove v '' ∈ {u ''|u ∈ y1}.

An exact proof term for the current goal is ReplI y1 (λu ⇒ u '') v Hv.

Apply binunionE x2 {u ''|u ∈ y2} (v '') L1 to the current goal.

Assume H2: v '' ∈ x2.

We will prove False.

An exact proof term for the current goal is ctagged_notin_SNo x2 v Hx2 H2.

Assume H2: v '' ∈ {u ''|u ∈ y2}.

Apply ReplE_impred y2 (λu ⇒ u '') (v '') H2 to the current goal.

Let u be given.

Assume Hu: u ∈ y2.

Assume Hvu: v '' = u ''.

We prove the intermediate claim L2: v = u.

An exact proof term for the current goal is ctagged_eqE_eq y1 y2 Hy1 Hy2 v Hv u Hu Hvu.

We will prove v ∈ y2.

rewrite the current goal using L2 (from left to right).

An exact proof term for the current goal is Hu.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (SNo_pair_prop_2) The following is provable:

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

Proof:

Let x1, y1, x2 and y2 be given.

Assume Hx1 Hy1 Hx2 Hy2.

Assume H1: SNo_pair x1 y1 = SNo_pair x2 y2.

Apply set_ext to the current goal.

An exact proof term for the current goal is SNo_pair_prop_2_Subq x1 y1 x2 y2 Hy1 Hx2 Hy2 H1.

Apply SNo_pair_prop_2_Subq x2 y2 x1 y1 Hy2 Hx1 Hy1 to the current goal.

Use symmetry.

An exact proof term for the current goal is H1.

∎

Try to prove it yourself. Main Goal

Theorem. (SNo_pair_0) The following is provable:

∀x, SNo_pair x 0 = x

Proof:

Let x be given.

We will prove x ∪ {u ''|u ∈ 0} = x.

rewrite the current goal using Repl_Empty (λu ⇒ u '') (from left to right).

We will prove x ∪ 0 = x.

An exact proof term for the current goal is binunion_idr x.

∎

Try to prove it yourself. Main Goal

End of Section CTaggedSets

Definition. We define CSNo to be λz ⇒ ∃x, SNo x ∧ ∃y, SNo y ∧ z = SNo_pair x y of type set → prop.

Theorem. (CSNo_I) The following is provable:

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

Proof:

Let x and y be given.

Assume Hx Hy.

We will prove ∃x', SNo x' ∧ ∃y', SNo y' ∧ SNo_pair x y = SNo_pair x' y'.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hx.

We use y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hy.

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_E) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

Let p be given.

Assume Hp.

Apply Hz to the current goal.

Let x be given.

Assume H1.

Apply H1 to the current goal.

Assume Hx.

Assume H1.

Apply H1 to the current goal.

Let y be given.

Assume H1.

Apply H1 to the current goal.

Assume Hy Hzxy.

rewrite the current goal using Hzxy (from left to right).

An exact proof term for the current goal is Hp x y Hx Hy Hzxy.

∎

Try to prove it yourself. Main Goal

Theorem. (SNo_CSNo) The following is provable:

∀x, SNo x → CSNo x

Proof:

Let x be given.

Assume Hx.

We will prove ∃x', SNo x' ∧ ∃y, SNo y ∧ x = SNo_pair x' y.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hx.

We use 0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is SNo_0.

Use symmetry.

An exact proof term for the current goal is SNo_pair_0 x.

∎

Try to prove it yourself. Main Goal

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.

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

Definition. We define CSNo_Re to be λz ⇒ Eps_i (λx ⇒ SNo x ∧ ∃y, SNo y ∧ z = SNo_pair x y) of type set → set.

Definition. We define CSNo_Im to be λz ⇒ Eps_i (λy ⇒ SNo y ∧ z = SNo_pair (CSNo_Re z) y) of type set → set.

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) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

Apply Eps_i_ex (λx ⇒ SNo x ∧ ∃y, SNo y ∧ z = pa x y) to the current goal.

We will prove ∃x, SNo x ∧ ∃y, SNo y ∧ z = pa x y.

An exact proof term for the current goal is Hz.

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_Re2) The following is provable:

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

Proof:

Let x and y be given.

Assume Hx Hy.

Apply CSNo_Re1 (pa x y) (CSNo_I x y Hx Hy) to the current goal.

Assume H1: SNo (Re (pa x y)).

Assume H2: ∃y', SNo y' ∧ pa x y = pa (Re (pa x y)) y'.

Apply H2 to the current goal.

Let y' be given.

Assume H3.

Apply H3 to the current goal.

Assume Hy': SNo y'.

Assume H4: pa x y = pa (Re (pa x y)) y'.

Use symmetry.

An exact proof term for the current goal is SNo_pair_prop_1 x y (Re (pa x y)) y' Hx H1 H4.

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_Im1) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

Apply Eps_i_ex (λy ⇒ SNo y ∧ z = pa (Re z) y) to the current goal.

We will prove ∃y, SNo y ∧ z = pa (Re z) y.

Apply CSNo_E z Hz to the current goal.

Let x and y be given.

Assume Hx Hy.

Assume Hzxy: z = pa x y.

We use y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hy.

We will prove pa x y = pa (Re (pa x y)) y.

Apply CSNo_Re2 x y Hx Hy (λu v ⇒ pa x y = pa v y) to the current goal.

We will prove pa x y = pa x y.

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_Im2) The following is provable:

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

Proof:

Let x and y be given.

Assume Hx Hy.

Use symmetry.

Apply CSNo_Im1 (pa x y) (CSNo_I x y Hx Hy) to the current goal.

Assume H1: SNo (Im (pa x y)).

Apply CSNo_Re2 x y Hx Hy (λu v ⇒ pa x y = pa v (Im (pa x y)) → y = Im (pa x y)) to the current goal.

Assume H2: pa x y = pa x (Im (pa x y)).

An exact proof term for the current goal is SNo_pair_prop_2 x y x (Im (pa x y)) Hx Hy Hx H1 H2.

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_ReR) The following is provable:

∀z, CSNo z → SNo (Re z)

Proof:

Let z be given.

Assume Hz.

Apply CSNo_Re1 z Hz to the current goal.

An exact proof term for the current goal is (λH _ ⇒ H).

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_ImR) The following is provable:

∀z, CSNo z → SNo (Im z)

Proof:

Let z be given.

Assume Hz.

Apply CSNo_Im1 z Hz to the current goal.

An exact proof term for the current goal is (λH _ ⇒ H).

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_ReIm) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

Apply CSNo_Im1 z Hz to the current goal.

An exact proof term for the current goal is (λ_ H ⇒ H).

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_ReIm_split) The following is provable:

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

Proof:

Let z and w be given.

Assume Hz Hw.

Assume H1 H2.

Use transitivity with and (pa (Re z) (Im z)).

An exact proof term for the current goal is CSNo_ReIm z Hz.

Use transitivity with and (pa (Re w) (Im w)).

rewrite the current goal using H1 (from left to right).

rewrite the current goal using H2 (from left to right).

Use reflexivity.

Use symmetry.

An exact proof term for the current goal is CSNo_ReIm w Hw.

∎

Try to prove it yourself. Main Goal

Definition. We define minus_CSNo to be λz ⇒ pa (- Re z) (- Im z) of type set → set.

Definition. We define add_CSNo to be λz w ⇒ pa (Re z + Re w) (Im z + Im w) of type set → set → set.

Definition. We define mul_CSNo to be λz w ⇒ pa (Re z * Re w + - (Im z * Im w)) (Re z * Im w + Im z * Re w) of type set → set → set.

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

Theorem. (CSNo_Complex_i) The following is provable:

CSNo i

Proof:

We will prove CSNo (pa 0 1).

Apply CSNo_I to the current goal.

An exact proof term for the current goal is SNo_0.

An exact proof term for the current goal is SNo_1.

∎

Try to prove it yourself. Main Goal

Theorem. (minus_CSNo_CRe) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

An exact proof term for the current goal is CSNo_Re2 (- Re z) (- Im z) (SNo_minus_SNo (Re z) (CSNo_ReR z Hz)) (SNo_minus_SNo (Im z) (CSNo_ImR z Hz)).

∎

Try to prove it yourself. Main Goal

Theorem. (minus_CSNo_CIm) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

An exact proof term for the current goal is CSNo_Im2 (- Re z) (- Im z) (SNo_minus_SNo (Re z) (CSNo_ReR z Hz)) (SNo_minus_SNo (Im z) (CSNo_ImR z Hz)).

∎

Try to prove it yourself. Main Goal

Theorem. (add_CSNo_CRe) The following is provable:

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

Proof:

Let z and w be given.

Assume Hz Hw.

An exact proof term for the current goal is CSNo_Re2 (Re z + Re w) (Im z + Im w) (SNo_add_SNo (Re z) (Re w) (CSNo_ReR z Hz) (CSNo_ReR w Hw)) (SNo_add_SNo (Im z) (Im w) (CSNo_ImR z Hz) (CSNo_ImR w Hw)).

∎

Try to prove it yourself. Main Goal

Theorem. (add_CSNo_CIm) The following is provable:

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

Proof:

Let z and w be given.

Assume Hz Hw.

An exact proof term for the current goal is CSNo_Im2 (Re z + Re w) (Im z + Im w) (SNo_add_SNo (Re z) (Re w) (CSNo_ReR z Hz) (CSNo_ReR w Hw)) (SNo_add_SNo (Im z) (Im w) (CSNo_ImR z Hz) (CSNo_ImR w Hw)).

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_minus_CSNo) The following is provable:

∀z, CSNo z → CSNo (minus_CSNo z)

Proof:

Let z be given.

Assume Hz.

We will prove CSNo (pa (- Re z) (- Im z)).

Apply CSNo_I to the current goal.

Apply SNo_minus_SNo to the current goal.

Apply CSNo_ReR to the current goal.

An exact proof term for the current goal is Hz.

Apply SNo_minus_SNo to the current goal.

Apply CSNo_ImR to the current goal.

An exact proof term for the current goal is Hz.

∎

Try to prove it yourself. Main Goal

Theorem. (SNo_Re) The following is provable:

∀x, SNo x → Re x = x

Proof:

Let x be given.

Assume Hx.

rewrite the current goal using SNo_pair_0 x (from right to left) at position 1.

We will prove Re (pa x 0) = x.

An exact proof term for the current goal is CSNo_Re2 x 0 Hx SNo_0.

∎

Try to prove it yourself. Main Goal

Theorem. (SNo_Im) The following is provable:

∀x, SNo x → Im x = 0

Proof:

Let x be given.

Assume Hx.

rewrite the current goal using SNo_pair_0 x (from right to left) at position 1.

We will prove Im (pa x 0) = 0.

An exact proof term for the current goal is CSNo_Im2 x 0 Hx SNo_0.

∎

Try to prove it yourself. Main Goal

Theorem. (Re_0) The following is provable:

Re 0 = 0

Proof:

An exact proof term for the current goal is SNo_Re 0 SNo_0.

∎

Try to prove it yourself. Main Goal

Theorem. (Im_0) The following is provable:

Im 0 = 0

Proof:

An exact proof term for the current goal is SNo_Im 0 SNo_0.

∎

Try to prove it yourself. Main Goal

Theorem. (Re_1) The following is provable:

Re 1 = 1

Proof:

An exact proof term for the current goal is SNo_Re 1 SNo_1.

∎

Try to prove it yourself. Main Goal

Theorem. (Im_1) The following is provable:

Im 1 = 0

Proof:

An exact proof term for the current goal is SNo_Im 1 SNo_1.

∎

Try to prove it yourself. Main Goal

Theorem. (Re_i) The following is provable:

Re i = 0

Proof:

An exact proof term for the current goal is CSNo_Re2 0 1 SNo_0 SNo_1.

∎

Try to prove it yourself. Main Goal

Theorem. (Im_i) The following is provable:

Im i = 1

Proof:

An exact proof term for the current goal is CSNo_Im2 0 1 SNo_0 SNo_1.

∎

Try to prove it yourself. Main Goal

Theorem. (add_SNo_add_CSNo) The following is provable:

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

Proof:

Let x and y be given.

Assume Hx Hy.

Use transitivity with Re x + Re y, and pa (Re x + Re y) 0.

rewrite the current goal using SNo_Re x Hx (from left to right).

rewrite the current goal using SNo_Re y Hy (from left to right).

Use reflexivity.

Use symmetry.

An exact proof term for the current goal is SNo_pair_0 (Re x + Re y).

We will prove pa (Re x + Re y) 0 = pa (Re x + Re y) (Im x + Im y).

Use f_equal.

rewrite the current goal using SNo_Im x Hx (from left to right).

rewrite the current goal using SNo_Im y Hy (from left to right).

We will prove 0 = 0 + 0.

Use symmetry.

An exact proof term for the current goal is add_SNo_0L 0 SNo_0.

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_add_CSNo) The following is provable:

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

Proof:

Let z and w be given.

Assume Hz Hw.

We will prove CSNo (pa (Re z + Re w) (Im z + Im w)).

Apply CSNo_I to the current goal.

Apply SNo_add_SNo to the current goal.

An exact proof term for the current goal is CSNo_ReR z Hz.

An exact proof term for the current goal is CSNo_ReR w Hw.

Apply SNo_add_SNo to the current goal.

An exact proof term for the current goal is CSNo_ImR z Hz.

An exact proof term for the current goal is CSNo_ImR w Hw.

∎

Try to prove it yourself. Main Goal

Theorem. (add_CSNo_0L) The following is provable:

∀z, CSNo z → add_CSNo 0 z = z

Proof:

Let z be given.

Assume Hz.

We will prove pa (Re 0 + Re z) (Im 0 + Im z) = z.

rewrite the current goal using Re_0 (from left to right).

rewrite the current goal using Im_0 (from left to right).

We will prove pa (0 + Re z) (0 + Im z) = z.

rewrite the current goal using add_SNo_0L (Re z) (CSNo_ReR z Hz) (from left to right).

rewrite the current goal using add_SNo_0L (Im z) (CSNo_ImR z Hz) (from left to right).

Use symmetry.

An exact proof term for the current goal is CSNo_ReIm z Hz.

∎

Try to prove it yourself. Main Goal

Theorem. (add_CSNo_0R) The following is provable:

∀z, CSNo z → add_CSNo z 0 = z

Proof:

Let z be given.

Assume Hz.

We will prove pa (Re z + Re 0) (Im z + Im 0) = z.

rewrite the current goal using Re_0 (from left to right).

rewrite the current goal using Im_0 (from left to right).

We will prove pa (Re z + 0) (Im z + 0) = z.

rewrite the current goal using add_SNo_0R (Re z) (CSNo_ReR z Hz) (from left to right).

rewrite the current goal using add_SNo_0R (Im z) (CSNo_ImR z Hz) (from left to right).

Use symmetry.

An exact proof term for the current goal is CSNo_ReIm z Hz.

∎

Try to prove it yourself. Main Goal

Theorem. (add_CSNo_minus_CSNo_linv) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

We will prove pa (Re (pa (- Re z) (- Im z)) + Re z) (Im (pa (- Re z) (- Im z)) + Im z) = 0.

We prove the intermediate claim LmRez: SNo (- Re z).

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is CSNo_ReR z Hz.

We prove the intermediate claim LmImz: SNo (- Im z).

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is CSNo_ImR z Hz.

rewrite the current goal using CSNo_Re2 (- Re z) (- Im z) LmRez LmImz (from left to right).

rewrite the current goal using CSNo_Im2 (- Re z) (- Im z) LmRez LmImz (from left to right).

We will prove pa ((- Re z) + Re z) ((- Im z) + Im z) = 0.

rewrite the current goal using add_SNo_minus_SNo_linv (Re z) (CSNo_ReR z Hz) (from left to right).

rewrite the current goal using add_SNo_minus_SNo_linv (Im z) (CSNo_ImR z Hz) (from left to right).

We will prove pa 0 0 = 0.

An exact proof term for the current goal is SNo_pair_0 0.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (add_CSNo_minus_CSNo_rinv) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim LmRez: SNo (- Re z).

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is CSNo_ReR z Hz.

We prove the intermediate claim LmImz: SNo (- Im z).

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is CSNo_ImR z Hz.

We will prove pa (Re z + Re (pa (- Re z) (- Im z))) (Im z + Im (pa (- Re z) (- Im z))) = 0.

rewrite the current goal using CSNo_Re2 (- Re z) (- Im z) LmRez LmImz (from left to right).

rewrite the current goal using CSNo_Im2 (- Re z) (- Im z) LmRez LmImz (from left to right).

We will prove pa (Re z + - Re z) (Im z + - Im z) = 0.

rewrite the current goal using add_SNo_minus_SNo_rinv (Re z) (CSNo_ReR z Hz) (from left to right).

rewrite the current goal using add_SNo_minus_SNo_rinv (Im z) (CSNo_ImR z Hz) (from left to right).

We will prove pa 0 0 = 0.

An exact proof term for the current goal is SNo_pair_0 0.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (minus_SNo_minus_CSNo) The following is provable:

∀x, SNo x → - x = minus_CSNo x

Proof:

Let x be given.

Assume Hx.

We will prove - x = pa (- Re x) (- Im x).

rewrite the current goal using SNo_Re x Hx (from left to right).

rewrite the current goal using SNo_Im x Hx (from left to right).

We will prove - x = pa (- x) (- 0).

rewrite the current goal using minus_SNo_0 (from left to right).

Use symmetry.

An exact proof term for the current goal is SNo_pair_0 (- x).

∎

Try to prove it yourself. Main Goal

Theorem. (add_CSNo_com) The following is provable:

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

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lzw: CSNo (plus' z w).

An exact proof term for the current goal is CSNo_add_CSNo z w Hz Hw.

We prove the intermediate claim Lwz: CSNo (plus' w z).

An exact proof term for the current goal is CSNo_add_CSNo w z Hw Hz.

Apply CSNo_ReIm_split (plus' z w) (plus' w z) Lzw Lwz to the current goal.

We will prove Re (plus' z w) = Re (plus' w z).

Use transitivity with and (Re z + Re w).

An exact proof term for the current goal is add_CSNo_CRe z w Hz Hw.

Use transitivity with and (Re w + Re z).

An exact proof term for the current goal is add_SNo_com (Re z) (Re w) (CSNo_ReR z Hz) (CSNo_ReR w Hw).

Use symmetry.

An exact proof term for the current goal is add_CSNo_CRe w z Hw Hz.

We will prove Im (plus' z w) = Im (plus' w z).

Use transitivity with and (Im z + Im w).

An exact proof term for the current goal is add_CSNo_CIm z w Hz Hw.

Use transitivity with and (Im w + Im z).

An exact proof term for the current goal is add_SNo_com (Im z) (Im w) (CSNo_ImR z Hz) (CSNo_ImR w Hw).

Use symmetry.

An exact proof term for the current goal is add_CSNo_CIm w z Hw Hz.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (add_CSNo_assoc) The following is provable:

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

Proof:

Let z, w and v be given.

Assume Hz Hw Hv.

We prove the intermediate claim Lwv: CSNo (plus' w v).

An exact proof term for the current goal is CSNo_add_CSNo w v Hw Hv.

We prove the intermediate claim Lzw: CSNo (plus' z w).

An exact proof term for the current goal is CSNo_add_CSNo z w Hz Hw.

We prove the intermediate claim Lzwv1: CSNo (plus' z (plus' w v)).

An exact proof term for the current goal is CSNo_add_CSNo z (plus' w v) Hz Lwv.

We prove the intermediate claim Lzwv2: CSNo (plus' (plus' z w) v).

An exact proof term for the current goal is CSNo_add_CSNo (plus' z w) v Lzw Hv.

Apply CSNo_ReIm_split (plus' z (plus' w v)) (plus' (plus' z w) v) Lzwv1 Lzwv2 to the current goal.

We will prove Re (plus' z (plus' w v)) = Re (plus' (plus' z w) v).

Use transitivity with and (Re z + Re (plus' w v)).

An exact proof term for the current goal is add_CSNo_CRe z (plus' w v) Hz Lwv.

Use transitivity with and (Re (plus' z w) + Re v).

We will prove Re z + Re (plus' w v) = Re (plus' z w) + Re v.

Use transitivity with and (Re z + (Re w + Re v)).

Apply f_eq_i (λV ⇒ Re z + V) to the current goal.

An exact proof term for the current goal is add_CSNo_CRe w v Hw Hv.

We will prove Re z + (Re w + Re v) = Re (plus' z w) + Re v.

Use transitivity with and (Re z + Re w) + Re v.

An exact proof term for the current goal is add_SNo_assoc (Re z) (Re w) (Re v) (CSNo_ReR z Hz) (CSNo_ReR w Hw) (CSNo_ReR v Hv).

Use symmetry.

We will prove Re (plus' z w) + Re v = (Re z + Re w) + Re v.

We will prove (λU : set ⇒ U + Re v) (Re (plus' z w)) = (λU : set ⇒ U + Re v) (Re z + Re w).

Use f_equal.

We will prove Re (plus' z w) = Re z + Re w.

An exact proof term for the current goal is add_CSNo_CRe z w Hz Hw.

Use symmetry.

An exact proof term for the current goal is add_CSNo_CRe (plus' z w) v Lzw Hv.

We will prove Im (plus' z (plus' w v)) = Im (plus' (plus' z w) v).

Use transitivity with and (Im z + Im (plus' w v)).

An exact proof term for the current goal is add_CSNo_CIm z (plus' w v) Hz Lwv.

Use transitivity with and (Im (plus' z w) + Im v).

We will prove Im z + Im (plus' w v) = Im (plus' z w) + Im v.

Use transitivity with and (Im z + (Im w + Im v)).

Apply f_eq_i (λV ⇒ Im z + V) to the current goal.

An exact proof term for the current goal is add_CSNo_CIm w v Hw Hv.

We will prove Im z + (Im w + Im v) = Im (plus' z w) + Im v.

Use transitivity with and (Im z + Im w) + Im v.

An exact proof term for the current goal is add_SNo_assoc (Im z) (Im w) (Im v) (CSNo_ImR z Hz) (CSNo_ImR w Hw) (CSNo_ImR v Hv).

Use symmetry.

We will prove Im (plus' z w) + Im v = (Im z + Im w) + Im v.

We will prove (λU : set ⇒ U + Im v) (Im (plus' z w)) = (λU : set ⇒ U + Im v) (Im z + Im w).

Apply f_eq_i (λU ⇒ U + Im v) to the current goal.

We will prove Im (plus' z w) = Im z + Im w.

An exact proof term for the current goal is add_CSNo_CIm z w Hz Hw.

Use symmetry.

An exact proof term for the current goal is add_CSNo_CIm (plus' z w) v Lzw Hv.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Main Goal

Theorem. (add_SNo_rotate_4_0312) The following is provable:

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

Proof:

Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using add_SNo_com z w Hz Hw (from left to right).

We will prove (x + y) + (w + z) = (x + w) + (y + z).

An exact proof term for the current goal is add_SNo_com_4_inner_mid x y w z Hx Hy Hw Hz.

∎

Try to prove it yourself. Main Goal

Theorem. (mul_CSNo_ReR) The following is provable:

∀z w, CSNo z → CSNo w → SNo (Re z * Re w + - (Im z * Im w))

Proof:

Let z and w be given.

Assume Hz Hw.

Apply SNo_add_SNo to the current goal.

Apply SNo_mul_SNo to the current goal.

Apply CSNo_ReR to the current goal.

An exact proof term for the current goal is Hz.

Apply CSNo_ReR to the current goal.

An exact proof term for the current goal is Hw.

Apply SNo_minus_SNo to the current goal.

Apply SNo_mul_SNo to the current goal.

Apply CSNo_ImR to the current goal.

An exact proof term for the current goal is Hz.

Apply CSNo_ImR to the current goal.

An exact proof term for the current goal is Hw.

∎

Try to prove it yourself. Main Goal

Theorem. (mul_CSNo_ImR) The following is provable:

∀z w, CSNo z → CSNo w → SNo (Re z * Im w + Im z * Re w)

Proof:

Let z and w be given.

Assume Hz Hw.

Apply SNo_add_SNo to the current goal.

Apply SNo_mul_SNo to the current goal.

Apply CSNo_ReR to the current goal.

An exact proof term for the current goal is Hz.

Apply CSNo_ImR to the current goal.

An exact proof term for the current goal is Hw.

Apply SNo_mul_SNo to the current goal.

Apply CSNo_ImR to the current goal.

An exact proof term for the current goal is Hz.

Apply CSNo_ReR to the current goal.

An exact proof term for the current goal is Hw.

∎

Try to prove it yourself. Main Goal

Theorem. (mul_CSNo_CRe) The following is provable:

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

Proof:

Let z and w be given.

Assume Hz Hw.

An exact proof term for the current goal is CSNo_Re2 (Re z * Re w + - (Im z * Im w)) (Re z * Im w + Im z * Re w) (mul_CSNo_ReR z w Hz Hw) (mul_CSNo_ImR z w Hz Hw).

∎

Try to prove it yourself. Main Goal

Theorem. (mul_CSNo_CIm) The following is provable:

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

Proof:

Let z and w be given.

Assume Hz Hw.

An exact proof term for the current goal is CSNo_Im2 (Re z * Re w + - (Im z * Im w)) (Re z * Im w + Im z * Re w) (mul_CSNo_ReR z w Hz Hw) (mul_CSNo_ImR z w Hz Hw).

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_mul_CSNo) The following is provable:

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

Proof:

Let z and w be given.

Assume Hz Hw.

We will prove CSNo (pa (Re z * Re w + - (Im z * Im w)) (Re z * Im w + Im z * Re w)).

Apply CSNo_I to the current goal.

An exact proof term for the current goal is mul_CSNo_ReR z w Hz Hw.

An exact proof term for the current goal is mul_CSNo_ImR z w Hz Hw.

∎

Try to prove it yourself. Main Goal

Theorem. (mul_CSNo_com) The following is provable:

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

Proof:

Let z and w be given.

Assume Hz Hw.

We prove the intermediate claim Lzw: CSNo (mult' z w).

An exact proof term for the current goal is CSNo_mul_CSNo z w Hz Hw.

We prove the intermediate claim Lwz: CSNo (mult' w z).

An exact proof term for the current goal is CSNo_mul_CSNo w z Hw Hz.

We prove the intermediate claim LRezR: SNo (Re z).

An exact proof term for the current goal is CSNo_ReR z Hz.

We prove the intermediate claim LRewR: SNo (Re w).

An exact proof term for the current goal is CSNo_ReR w Hw.

We prove the intermediate claim LImzR: SNo (Im z).

An exact proof term for the current goal is CSNo_ImR z Hz.

We prove the intermediate claim LImwR: SNo (Im w).

An exact proof term for the current goal is CSNo_ImR w Hw.

Apply CSNo_ReIm_split (mult' z w) (mult' w z) Lzw Lwz to the current goal.

We will prove Re (mult' z w) = Re (mult' w z).

Use transitivity with Re z * Re w + - (Im z * Im w), and Re w * Re z + - (Im w * Im z).

An exact proof term for the current goal is mul_CSNo_CRe z w Hz Hw.

Use f_equal.

An exact proof term for the current goal is mul_SNo_com (Re z) (Re w) LRezR LRewR.

Use f_equal.

An exact proof term for the current goal is mul_SNo_com (Im z) (Im w) LImzR LImwR.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CRe w z Hw Hz.

We will prove Im (mult' z w) = Im (mult' w z).

Use transitivity with Re z * Im w + Im z * Re w, Im z * Re w + Re z * Im w, and Re w * Im z + Im w * Re z.

An exact proof term for the current goal is mul_CSNo_CIm z w Hz Hw.

An exact proof term for the current goal is add_SNo_com (Re z * Im w) (Im z * Re w) (SNo_mul_SNo (Re z) (Im w) LRezR LImwR) (SNo_mul_SNo (Im z) (Re w) LImzR LRewR).

Use f_equal.

An exact proof term for the current goal is mul_SNo_com (Im z) (Re w) LImzR LRewR.

An exact proof term for the current goal is mul_SNo_com (Re z) (Im w) LRezR LImwR.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CIm w z Hw Hz.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Main Goal

Theorem. (mul_CSNo_assoc) The following is provable:

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

Proof:

Let z, w and v be given.

Assume Hz Hw Hv.

We prove the intermediate claim Lwv: CSNo (mult' w v).

An exact proof term for the current goal is CSNo_mul_CSNo w v Hw Hv.

We prove the intermediate claim Lzw: CSNo (mult' z w).

An exact proof term for the current goal is CSNo_mul_CSNo z w Hz Hw.

We prove the intermediate claim Lzwv1: CSNo (mult' z (mult' w v)).

An exact proof term for the current goal is CSNo_mul_CSNo z (mult' w v) Hz Lwv.

We prove the intermediate claim Lzwv2: CSNo (mult' (mult' z w) v).

An exact proof term for the current goal is CSNo_mul_CSNo (mult' z w) v Lzw Hv.

We prove the intermediate claim LRezR: SNo (Re z).

An exact proof term for the current goal is CSNo_ReR z Hz.

We prove the intermediate claim LRewR: SNo (Re w).

An exact proof term for the current goal is CSNo_ReR w Hw.

We prove the intermediate claim LRevR: SNo (Re v).

An exact proof term for the current goal is CSNo_ReR v Hv.

We prove the intermediate claim LImzR: SNo (Im z).

An exact proof term for the current goal is CSNo_ImR z Hz.

We prove the intermediate claim LImwR: SNo (Im w).

An exact proof term for the current goal is CSNo_ImR w Hw.

We prove the intermediate claim LImvR: SNo (Im v).

An exact proof term for the current goal is CSNo_ImR v Hv.

Apply CSNo_ReIm_split (mult' z (mult' w v)) (mult' (mult' z w) v) Lzwv1 Lzwv2 to the current goal.

We will prove Re (mult' z (mult' w v)) = Re (mult' (mult' z w) v).

Use transitivity with (Re z * Re (mult' w v) + - (Im z * Im (mult' w v))), ((Re z * Re w * Re v + - (Re z * Im w * Im v)) + (- (Im z * Re w * Im v) + - (Im z * Im w * Re v))), ((Re z * Re w * Re v + - (Im z * Im w * Re v)) + (- (Re z * Im w * Im v) + - (Im z * Re w * Im v))), and (Re (mult' z w) * Re v + - (Im (mult' z w) * Im v)).

An exact proof term for the current goal is mul_CSNo_CRe z (mult' w v) Hz Lwv.

Use f_equal.

We will prove Re z * Re (mult' w v) = Re z * Re w * Re v + - (Re z * Im w * Im v).

Use transitivity with Re z * (Re w * Re v + - (Im w * Im v)), and Re z * Re w * Re v + Re z * (- (Im w * Im v)).

Use f_equal.

An exact proof term for the current goal is mul_CSNo_CRe w v Hw Hv.

Apply mul_SNo_distrL (Re z) (Re w * Re v) (- (Im w * Im v)) LRezR (SNo_mul_SNo (Re w) (Re v) LRewR LRevR) to the current goal.

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is SNo_mul_SNo (Im w) (Im v) LImwR LImvR.

Use f_equal.

We will prove Re z * (- (Im w * Im v)) = - (Re z * Im w * Im v).

An exact proof term for the current goal is mul_SNo_minus_distrR (Re z) (Im w * Im v) LRezR (SNo_mul_SNo (Im w) (Im v) LImwR LImvR).

We will prove - (Im z * Im (mult' w v)) = - (Im z * Re w * Im v) + - (Im z * Im w * Re v).

Use transitivity with and - (Im z * Re w * Im v + Im z * Im w * Re v).

Use f_equal.

We will prove Im z * Im (mult' w v) = Im z * Re w * Im v + Im z * Im w * Re v.

Use transitivity with and Im z * (Re w * Im v + Im w * Re v).

Use f_equal.

An exact proof term for the current goal is mul_CSNo_CIm w v Hw Hv.

An exact proof term for the current goal is mul_SNo_distrL (Im z) (Re w * Im v) (Im w * Re v) LImzR (SNo_mul_SNo (Re w) (Im v) LRewR LImvR) (SNo_mul_SNo (Im w) (Re v) LImwR LRevR).

Apply minus_add_SNo_distr to the current goal.

An exact proof term for the current goal is SNo_mul_SNo_3 (Im z) (Re w) (Im v) LImzR LRewR LImvR.

An exact proof term for the current goal is SNo_mul_SNo_3 (Im z) (Im w) (Re v) LImzR LImwR LRevR.

Apply add_SNo_rotate_4_0312 to the current goal.

An exact proof term for the current goal is SNo_mul_SNo_3 (Re z) (Re w) (Re v) LRezR LRewR LRevR.

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is SNo_mul_SNo_3 (Re z) (Im w) (Im v) LRezR LImwR LImvR.

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is SNo_mul_SNo_3 (Im z) (Re w) (Im v) LImzR LRewR LImvR.

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is SNo_mul_SNo_3 (Im z) (Im w) (Re v) LImzR LImwR LRevR.

Use f_equal.

We will prove Re z * Re w * Re v + - (Im z * Im w * Re v) = Re (mult' z w) * Re v.

Use transitivity with (Re z * Re w) * Re v + (- (Im z * Im w)) * Re v, and (Re z * Re w + - (Im z * Im w)) * Re v.

Use f_equal.

We will prove Re z * Re w * Re v = (Re z * Re w) * Re v.

An exact proof term for the current goal is mul_SNo_assoc (Re z) (Re w) (Re v) LRezR LRewR LRevR.

We will prove - (Im z * Im w * Re v) = (- (Im z * Im w)) * Re v.

Use transitivity with and - ((Im z * Im w) * Re v).

Use f_equal.

An exact proof term for the current goal is mul_SNo_assoc (Im z) (Im w) (Re v) LImzR LImwR LRevR.

Use symmetry.

An exact proof term for the current goal is mul_SNo_minus_distrL (Im z * Im w) (Re v) (SNo_mul_SNo (Im z) (Im w) LImzR LImwR) LRevR.

Use symmetry.

An exact proof term for the current goal is mul_SNo_distrR (Re z * Re w) (- (Im z * Im w)) (Re v) (SNo_mul_SNo (Re z) (Re w) LRezR LRewR) (SNo_minus_SNo (Im z * Im w) (SNo_mul_SNo (Im z) (Im w) LImzR LImwR)) LRevR.

Use f_equal.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CRe z w Hz Hw.

We will prove - (Re z * Im w * Im v) + - (Im z * Re w * Im v) = - (Im (mult' z w) * Im v).

Use transitivity with and - (Re z * Im w * Im v + Im z * Re w * Im v).

Use symmetry.

Apply minus_add_SNo_distr to the current goal.

An exact proof term for the current goal is SNo_mul_SNo_3 (Re z) (Im w) (Im v) LRezR LImwR LImvR.

An exact proof term for the current goal is SNo_mul_SNo_3 (Im z) (Re w) (Im v) LImzR LRewR LImvR.

Use f_equal.

Use transitivity with (Re z * Im w) * Im v + (Im z * Re w) * Im v, and (Re z * Im w + Im z * Re w) * Im v.

Use f_equal.

An exact proof term for the current goal is mul_SNo_assoc (Re z) (Im w) (Im v) LRezR LImwR LImvR.

An exact proof term for the current goal is mul_SNo_assoc (Im z) (Re w) (Im v) LImzR LRewR LImvR.

Use symmetry.

An exact proof term for the current goal is mul_SNo_distrR (Re z * Im w) (Im z * Re w) (Im v) (SNo_mul_SNo (Re z) (Im w) LRezR LImwR) (SNo_mul_SNo (Im z) (Re w) LImzR LRewR) LImvR.

Use f_equal.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CIm z w Hz Hw.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CRe (mult' z w) v Lzw Hv.

We will prove Im (mult' z (mult' w v)) = Im (mult' (mult' z w) v).

Use transitivity with (Re z * Im (mult' w v) + (Im z * Re (mult' w v))), ((Re z * Re w * Im v + Re z * Im w * Re v) + (Im z * Re w * Re v + - (Im z * Im w * Im v))), ((Re z * Re w * Im v + - (Im z * Im w * Im v)) + (Re z * Im w * Re v + Im z * Re w * Re v)), and (Re (mult' z w) * Im v + Im (mult' z w) * Re v).

An exact proof term for the current goal is mul_CSNo_CIm z (mult' w v) Hz Lwv.

Use f_equal.

We will prove Re z * Im (mult' w v) = Re z * Re w * Im v + Re z * Im w * Re v.

Use transitivity with and Re z * (Re w * Im v + Im w * Re v).

Use f_equal.

An exact proof term for the current goal is mul_CSNo_CIm w v Hw Hv.

An exact proof term for the current goal is mul_SNo_distrL (Re z) (Re w * Im v) (Im w * Re v) LRezR (SNo_mul_SNo (Re w) (Im v) LRewR LImvR) (SNo_mul_SNo (Im w) (Re v) LImwR LRevR).

We will prove Im z * Re (mult' w v) = Im z * Re w * Re v + - (Im z * Im w * Im v).

Use transitivity with Im z * (Re w * Re v + - (Im w * Im v)), and Im z * Re w * Re v + Im z * (- (Im w * Im v)).

Use f_equal.

An exact proof term for the current goal is mul_CSNo_CRe w v Hw Hv.

An exact proof term for the current goal is mul_SNo_distrL (Im z) (Re w * Re v) (- (Im w * Im v)) LImzR (SNo_mul_SNo (Re w) (Re v) LRewR LRevR) (SNo_minus_SNo (Im w * Im v) (SNo_mul_SNo (Im w) (Im v) LImwR LImvR)).

Use f_equal.

An exact proof term for the current goal is mul_SNo_minus_distrR (Im z) (Im w * Im v) LImzR (SNo_mul_SNo (Im w) (Im v) LImwR LImvR).

Apply add_SNo_rotate_4_0312 to the current goal.

An exact proof term for the current goal is SNo_mul_SNo_3 (Re z) (Re w) (Im v) LRezR LRewR LImvR.

An exact proof term for the current goal is SNo_mul_SNo_3 (Re z) (Im w) (Re v) LRezR LImwR LRevR.

An exact proof term for the current goal is SNo_mul_SNo_3 (Im z) (Re w) (Re v) LImzR LRewR LRevR.

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is SNo_mul_SNo_3 (Im z) (Im w) (Im v) LImzR LImwR LImvR.

Use f_equal.

We will prove Re z * Re w * Im v + - (Im z * Im w * Im v) = Re (mult' z w) * Im v.

Use transitivity with (Re z * Re w) * Im v + (- (Im z * Im w)) * Im v, and (Re z * Re w + - (Im z * Im w)) * Im v.

Use f_equal.

We will prove Re z * Re w * Im v = (Re z * Re w) * Im v.

An exact proof term for the current goal is mul_SNo_assoc (Re z) (Re w) (Im v) LRezR LRewR LImvR.

We will prove - (Im z * Im w * Im v) = (- (Im z * Im w)) * Im v.

Use transitivity with and - ((Im z * Im w) * Im v).

Use f_equal.

An exact proof term for the current goal is mul_SNo_assoc (Im z) (Im w) (Im v) LImzR LImwR LImvR.

Use symmetry.

We will prove (- (Im z * Im w)) * Im v = - ((Im z * Im w) * Im v).

An exact proof term for the current goal is mul_SNo_minus_distrL (Im z * Im w) (Im v) (SNo_mul_SNo (Im z) (Im w) LImzR LImwR) LImvR.

Use symmetry.

An exact proof term for the current goal is mul_SNo_distrR (Re z * Re w) (- (Im z * Im w)) (Im v) (SNo_mul_SNo (Re z) (Re w) LRezR LRewR) (SNo_minus_SNo (Im z * Im w) (SNo_mul_SNo (Im z) (Im w) LImzR LImwR)) LImvR.

Use f_equal.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CRe z w Hz Hw.

We will prove Re z * Im w * Re v + Im z * Re w * Re v = Im (mult' z w) * Re v.

Use transitivity with (Re z * Im w) * Re v + (Im z * Re w) * Re v, and (Re z * Im w + Im z * Re w) * Re v.

Use f_equal.

An exact proof term for the current goal is mul_SNo_assoc (Re z) (Im w) (Re v) LRezR LImwR LRevR.

An exact proof term for the current goal is mul_SNo_assoc (Im z) (Re w) (Re v) LImzR LRewR LRevR.

Use symmetry.

An exact proof term for the current goal is mul_SNo_distrR (Re z * Im w) (Im z * Re w) (Re v) (SNo_mul_SNo (Re z) (Im w) LRezR LImwR) (SNo_mul_SNo (Im z) (Re w) LImzR LRewR) LRevR.

Use f_equal.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CIm z w Hz Hw.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CIm (mult' z w) v Lzw Hv.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Subgoal 9 Subgoal 10 Main Goal

Theorem. (CSNo_0) The following is provable:

CSNo 0

Proof:

Apply SNo_CSNo to the current goal.

An exact proof term for the current goal is SNo_0.

∎

Try to prove it yourself. Main Goal

Theorem. (CSNo_1) The following is provable:

CSNo 1

Proof:

Apply SNo_CSNo to the current goal.

An exact proof term for the current goal is SNo_1.

∎

Try to prove it yourself. Main Goal

Theorem. (mul_CSNo_oneL) The following is provable:

∀z, CSNo z → 1 ⨯ z = z

Proof:

Let z be given.

Assume Hz.

We prove the intermediate claim L1z: CSNo (mult' 1 z).

An exact proof term for the current goal is CSNo_mul_CSNo 1 z CSNo_1 Hz.

We prove the intermediate claim LRezR: SNo (Re z).

An exact proof term for the current goal is CSNo_ReR z Hz.

We prove the intermediate claim LImzR: SNo (Im z).

An exact proof term for the current goal is CSNo_ImR z Hz.

Apply CSNo_ReIm_split (mult' 1 z) z L1z Hz to the current goal.

We will prove Re (mult' 1 z) = Re z.

Use transitivity with Re 1 * Re z + - (Im 1 * Im z), and Re z + 0.

An exact proof term for the current goal is mul_CSNo_CRe 1 z CSNo_1 Hz.

Use f_equal.

We will prove Re 1 * Re z = Re z.

rewrite the current goal using SNo_pair_0 1 (from right to left).

We will prove Re (pa 1 0) * Re z = Re z.

Apply CSNo_Re2 1 0 SNo_1 SNo_0 (λU V ⇒ V * Re z = Re z) to the current goal.

We will prove 1 * Re z = Re z.

An exact proof term for the current goal is mul_SNo_oneL (Re z) LRezR.

We will prove - (Im 1 * Im z) = 0.

rewrite the current goal using minus_SNo_0 (from right to left) at position 2.

We will prove - (Im 1 * Im z) = - 0.

Use f_equal.

rewrite the current goal using SNo_pair_0 1 (from right to left).

We will prove Im (pa 1 0) * Im z = 0.

Use transitivity with and 0 * Im z.

Use f_equal.

An exact proof term for the current goal is CSNo_Im2 1 0 SNo_1 SNo_0.

An exact proof term for the current goal is mul_SNo_zeroL (Im z) LImzR.

Use transitivity with and 0 + Re z.

An exact proof term for the current goal is add_SNo_com (Re z) 0 LRezR SNo_0.

An exact proof term for the current goal is add_SNo_0L (Re z) LRezR.

We will prove Im (mult' 1 z) = Im z.

Use transitivity with Re 1 * Im z + Im 1 * Re z, and Im z + 0.

An exact proof term for the current goal is mul_CSNo_CIm 1 z CSNo_1 Hz.

Use f_equal.

We will prove Re 1 * Im z = Im z.

rewrite the current goal using SNo_pair_0 1 (from right to left).

We will prove Re (pa 1 0) * Im z = Im z.

Apply CSNo_Re2 1 0 SNo_1 SNo_0 (λU V ⇒ V * Im z = Im z) to the current goal.

We will prove 1 * Im z = Im z.

An exact proof term for the current goal is mul_SNo_oneL (Im z) LImzR.

We will prove Im 1 * Re z = 0.

Use transitivity with and 0 * Re z.

Use f_equal.

rewrite the current goal using SNo_pair_0 1 (from right to left).

An exact proof term for the current goal is CSNo_Im2 1 0 SNo_1 SNo_0.

An exact proof term for the current goal is mul_SNo_zeroL (Re z) LRezR.

Use transitivity with and 0 + Im z.

An exact proof term for the current goal is add_SNo_com (Im z) 0 LImzR SNo_0.

An exact proof term for the current goal is add_SNo_0L (Im z) LImzR.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Main Goal

Theorem. (mul_CSNo_distrL) The following is provable:

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

Proof:

Let z, w and v be given.

Assume Hz Hw Hv.

We prove the intermediate claim Lwv: CSNo (plus' w v).

An exact proof term for the current goal is CSNo_add_CSNo w v Hw Hv.

We prove the intermediate claim Lzw: CSNo (mult' z w).

An exact proof term for the current goal is CSNo_mul_CSNo z w Hz Hw.

We prove the intermediate claim Lzv: CSNo (mult' z v).

An exact proof term for the current goal is CSNo_mul_CSNo z v Hz Hv.

We prove the intermediate claim Lzwv: CSNo (mult' z (plus' w v)).

An exact proof term for the current goal is CSNo_mul_CSNo z (plus' w v) Hz Lwv.

We prove the intermediate claim Lzwzv: CSNo (plus' (mult' z w) (mult' z v)).

An exact proof term for the current goal is CSNo_add_CSNo (mult' z w) (mult' z v) Lzw Lzv.

We prove the intermediate claim LRezR: SNo (Re z).

An exact proof term for the current goal is CSNo_ReR z Hz.

We prove the intermediate claim LRewR: SNo (Re w).

An exact proof term for the current goal is CSNo_ReR w Hw.

We prove the intermediate claim LRevR: SNo (Re v).

An exact proof term for the current goal is CSNo_ReR v Hv.

We prove the intermediate claim LImzR: SNo (Im z).

An exact proof term for the current goal is CSNo_ImR z Hz.

We prove the intermediate claim LImwR: SNo (Im w).

An exact proof term for the current goal is CSNo_ImR w Hw.

We prove the intermediate claim LImvR: SNo (Im v).

An exact proof term for the current goal is CSNo_ImR v Hv.

Apply CSNo_ReIm_split (mult' z (plus' w v)) (plus' (mult' z w) (mult' z v)) Lzwv Lzwzv to the current goal.

We will prove Re (mult' z (plus' w v)) = Re (plus' (mult' z w) (mult' z v)).

Use transitivity with Re z * Re (plus' w v) + - Im z * Im (plus' w v), (Re z * Re w + Re z * Re v) + (- Im z * Im w + - Im z * Im v), (Re z * Re w + - (Im z * Im w)) + (Re z * Re v + - (Im z * Im v)), and Re (mult' z w) + Re (mult' z v).

An exact proof term for the current goal is mul_CSNo_CRe z (plus' w v) Hz Lwv.

Use f_equal.

We will prove Re z * Re (plus' w v) = Re z * Re w + Re z * Re v.

Apply mul_SNo_distrL (Re z) (Re w) (Re v) LRezR LRewR LRevR (λU V ⇒ Re z * Re (plus' w v) = U) to the current goal.

We will prove Re z * Re (plus' w v) = Re z * (Re w + Re v).

Use f_equal.

An exact proof term for the current goal is add_CSNo_CRe w v Hw Hv.

We will prove - Im z * Im (plus' w v) = - Im z * Im w + - Im z * Im v.

Use transitivity with - Im z * (Im w + Im v), (- Im z) * (Im w + Im v), and (- Im z) * Im w + (- Im z) * Im v.

Use f_equal.

An exact proof term for the current goal is add_CSNo_CIm w v Hw Hv.

Use symmetry.

An exact proof term for the current goal is mul_SNo_minus_distrL (Im z) (Im w + Im v) LImzR (SNo_add_SNo (Im w) (Im v) LImwR LImvR).

An exact proof term for the current goal is mul_SNo_distrL (- Im z) (Im w) (Im v) (SNo_minus_SNo (Im z) LImzR) LImwR LImvR.

Use f_equal.

An exact proof term for the current goal is mul_SNo_minus_distrL (Im z) (Im w) LImzR LImwR.

An exact proof term for the current goal is mul_SNo_minus_distrL (Im z) (Im v) LImzR LImvR.

Apply add_SNo_com_4_inner_mid to the current goal.

An exact proof term for the current goal is SNo_mul_SNo (Re z) (Re w) LRezR LRewR.

An exact proof term for the current goal is SNo_mul_SNo (Re z) (Re v) LRezR LRevR.

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is SNo_mul_SNo (Im z) (Im w) LImzR LImwR.

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is SNo_mul_SNo (Im z) (Im v) LImzR LImvR.

Use f_equal.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CRe z w Hz Hw.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CRe z v Hz Hv.

Use symmetry.

An exact proof term for the current goal is add_CSNo_CRe (mult' z w) (mult' z v) Lzw Lzv.

We will prove Im (mult' z (plus' w v)) = Im (plus' (mult' z w) (mult' z v)).

Use transitivity with Re z * Im (plus' w v) + Im z * Re (plus' w v), (Re z * Im w + Re z * Im v) + (Im z * Re w + Im z * Re v), (Re z * Im w + Im z * Re w) + (Re z * Im v + Im z * Re v), and Im (mult' z w) + Im (mult' z v).

An exact proof term for the current goal is mul_CSNo_CIm z (plus' w v) Hz Lwv.

Use f_equal.

We will prove Re z * Im (plus' w v) = Re z * Im w + Re z * Im v.

Apply mul_SNo_distrL (Re z) (Im w) (Im v) LRezR LImwR LImvR (λU V ⇒ Re z * Im (plus' w v) = U) to the current goal.

We will prove Re z * Im (plus' w v) = Re z * (Im w + Im v).

Use f_equal.

An exact proof term for the current goal is add_CSNo_CIm w v Hw Hv.

We will prove Im z * Re (plus' w v) = Im z * Re w + Im z * Re v.

Use transitivity with and Im z * (Re w + Re v).

Use f_equal.

An exact proof term for the current goal is add_CSNo_CRe w v Hw Hv.

An exact proof term for the current goal is mul_SNo_distrL (Im z) (Re w) (Re v) LImzR LRewR LRevR.

Apply add_SNo_com_4_inner_mid to the current goal.

An exact proof term for the current goal is SNo_mul_SNo (Re z) (Im w) LRezR LImwR.

An exact proof term for the current goal is SNo_mul_SNo (Re z) (Im v) LRezR LImvR.

An exact proof term for the current goal is SNo_mul_SNo (Im z) (Re w) LImzR LRewR.

An exact proof term for the current goal is SNo_mul_SNo (Im z) (Re v) LImzR LRevR.

Use f_equal.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CIm z w Hz Hw.

Use symmetry.

An exact proof term for the current goal is mul_CSNo_CIm z v Hz Hv.

Use symmetry.

An exact proof term for the current goal is add_CSNo_CIm (mult' z w) (mult' z v) Lzw Lzv.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Subgoal 9 Subgoal 10 Subgoal 11 Main Goal

Theorem. (mul_SNo_mul_CSNo) The following is provable:

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

Proof:

Let x and y be given.

Assume Hx Hy.

Use transitivity with Re x * Re y, and pa (Re x * Re y) 0.

rewrite the current goal using SNo_Re x Hx (from left to right).

rewrite the current goal using SNo_Re y Hy (from left to right).

Use reflexivity.

Use symmetry.

An exact proof term for the current goal is SNo_pair_0 (Re x * Re y).

We will prove pa (Re x * Re y) 0 = pa (Re x * Re y + - Im x * Im y) (Re x * Im y + Im x * Re y).

Use f_equal.

We will prove Re x * Re y = Re x * Re y + - Im x * Im y.

rewrite the current goal using SNo_Im x Hx (from left to right).

rewrite the current goal using mul_SNo_zeroL (Im y) (CSNo_ImR y (SNo_CSNo y Hy)) (from left to right).

We will prove Re x * Re y = Re x * Re y + - 0.

rewrite the current goal using minus_SNo_0 (from left to right).

Use symmetry.

We will prove Re x * Re y + 0 = Re x * Re y.

An exact proof term for the current goal is add_SNo_0R (Re x * Re y) (SNo_mul_SNo (Re x) (Re y) (CSNo_ReR x (SNo_CSNo x Hx)) (CSNo_ReR y (SNo_CSNo y Hy))).

We will prove 0 = Re x * Im y + Im x * Re y.

rewrite the current goal using SNo_Im x Hx (from left to right).

rewrite the current goal using SNo_Im y Hy (from left to right).

rewrite the current goal using mul_SNo_zeroL (Re y) (CSNo_ReR y (SNo_CSNo y Hy)) (from left to right).

rewrite the current goal using mul_SNo_zeroR (Re x) (CSNo_ReR x (SNo_CSNo x Hx)) (from left to right).

Use symmetry.

An exact proof term for the current goal is add_SNo_0R 0 SNo_0.

∎

Try to prove it yourself. Main Goal

Theorem. (Complex_i_sqr) The following is provable:

i ⨯ i = :-: 1

Proof:

We prove the intermediate claim Lii: CSNo (i ⨯ i).

An exact proof term for the current goal is CSNo_mul_CSNo i i CSNo_Complex_i CSNo_Complex_i.

We prove the intermediate claim Lm1: CSNo (:-: 1).

An exact proof term for the current goal is CSNo_minus_CSNo 1 CSNo_1.

Apply CSNo_ReIm_split (i ⨯ i) (:-: 1) Lii Lm1 to the current goal.

We will prove Re (i ⨯ i) = Re (:-: 1).

rewrite the current goal using mul_CSNo_CRe i i CSNo_Complex_i CSNo_Complex_i (from left to right).

rewrite the current goal using minus_CSNo_CRe 1 CSNo_1 (from left to right).

We will prove Re i * Re i + - Im i * Im i = - Re 1.

rewrite the current goal using Re_i (from left to right).

rewrite the current goal using Im_i (from left to right).

rewrite the current goal using Re_1 (from left to right).

We will prove 0 * 0 + - 1 * 1 = - 1.

rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).

rewrite the current goal using mul_SNo_oneL 1 SNo_1 (from left to right).

We will prove 0 + - 1 = - 1.

An exact proof term for the current goal is add_SNo_0L (- 1) (SNo_minus_SNo 1 SNo_1).

We will prove Im (i ⨯ i) = Im (:-: 1).

rewrite the current goal using mul_CSNo_CIm i i CSNo_Complex_i CSNo_Complex_i (from left to right).

rewrite the current goal using minus_CSNo_CIm 1 CSNo_1 (from left to right).

We will prove Re i * Im i + Im i * Re i = - Im 1.

rewrite the current goal using Re_i (from left to right).

rewrite the current goal using Im_i (from left to right).

rewrite the current goal using Im_1 (from left to right).

We will prove 0 * 1 + 1 * 0 = - 0.

rewrite the current goal using minus_SNo_0 (from left to right).

rewrite the current goal using mul_SNo_zeroL 1 SNo_1 (from left to right).

rewrite the current goal using mul_SNo_zeroR 1 SNo_1 (from left to right).

We will prove 0 + 0 = 0.

An exact proof term for the current goal is add_SNo_0L 0 SNo_0.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Main Goal

Theorem. (CSNo_relative_recip) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

Let u be given.

Assume Hu.

Assume Hur: (Re z * Re z + Im z * Im z) * u = 1.

We will prove z ⨯ (u ⨯ Re z + :-: i ⨯ u ⨯ Im z) = 1.

We prove the intermediate claim LRezR: SNo (Re z).

An exact proof term for the current goal is CSNo_ReR z Hz.

We prove the intermediate claim LImzR: SNo (Im z).

An exact proof term for the current goal is CSNo_ImR z Hz.

We will prove z ⨯ (u ⨯ Re z + :-: i ⨯ u ⨯ Im z) = 1.

rewrite the current goal using mul_SNo_mul_CSNo u (Re z) Hu LRezR (from right to left).

rewrite the current goal using mul_SNo_mul_CSNo u (Im z) Hu LImzR (from right to left).

We will prove z ⨯ (u * Re z + :-: i ⨯ u * Im z) = 1.

We prove the intermediate claim LuRez: SNo (u * Re z).

An exact proof term for the current goal is SNo_mul_SNo u (Re z) ?? ??.

We prove the intermediate claim LuRez': CSNo (u * Re z).

Apply SNo_CSNo to the current goal.

An exact proof term for the current goal is LuRez.

We prove the intermediate claim LuImz: SNo (u * Im z).

An exact proof term for the current goal is SNo_mul_SNo u (Im z) ?? ??.

We prove the intermediate claim LuImz': CSNo (u * Im z).

Apply SNo_CSNo to the current goal.

An exact proof term for the current goal is LuImz.

We prove the intermediate claim LiuImz: CSNo (i ⨯ u * Im z).

Apply CSNo_mul_CSNo to the current goal.

An exact proof term for the current goal is CSNo_Complex_i.

An exact proof term for the current goal is LuImz'.

We prove the intermediate claim LmiuImz: CSNo (:-: i ⨯ u * Im z).

Apply CSNo_minus_CSNo to the current goal.

An exact proof term for the current goal is LiuImz.

We prove the intermediate claim L1: CSNo (u * Re z + :-: i ⨯ u * Im z).

Apply CSNo_add_CSNo to the current goal.

We will prove CSNo (u * Re z).

An exact proof term for the current goal is LuRez'.

We will prove CSNo (:-: i ⨯ u * Im z).

An exact proof term for the current goal is LmiuImz.

We prove the intermediate claim LRezRez: SNo (Re z * Re z).

An exact proof term for the current goal is SNo_mul_SNo (Re z) (Re z) ?? ??.

We prove the intermediate claim LImzImz: SNo (Im z * Im z).

An exact proof term for the current goal is SNo_mul_SNo (Im z) (Im z) ?? ??.

Apply CSNo_ReIm_split (z ⨯ (u * Re z + :-: i ⨯ u * Im z)) 1 (CSNo_mul_CSNo z (u * Re z + :-: i ⨯ u * Im z) Hz L1) CSNo_1 to the current goal.

We will prove Re (z ⨯ (u * Re z + :-: i ⨯ u * Im z)) = Re 1.

rewrite the current goal using Re_1 (from left to right).

rewrite the current goal using mul_CSNo_CRe z (u * Re z + :-: i ⨯ u * Im z) Hz L1 (from left to right).

We will prove Re z * Re (u * Re z + :-: i ⨯ u * Im z) + - Im z * Im (u * Re z + :-: i ⨯ u * Im z) = 1.

rewrite the current goal using add_CSNo_CRe (u * Re z) (:-: i ⨯ u * Im z) LuRez' LmiuImz (from left to right).

rewrite the current goal using add_CSNo_CIm (u * Re z) (:-: i ⨯ u * Im z) LuRez' LmiuImz (from left to right).

We will prove Re z * (Re (u * Re z) + Re (:-: i ⨯ u * Im z)) + - Im z * (Im (u * Re z) + Im (:-: i ⨯ u * Im z)) = 1.

rewrite the current goal using minus_CSNo_CRe (i ⨯ u * Im z) LiuImz (from left to right).

rewrite the current goal using minus_CSNo_CIm (i ⨯ u * Im z) LiuImz (from left to right).

rewrite the current goal using SNo_Re (u * Re z) LuRez (from left to right).

rewrite the current goal using SNo_Im (u * Re z) LuRez (from left to right).

We will prove Re z * (u * Re z + - Re (i ⨯ u * Im z)) + - Im z * (0 + - Im (i ⨯ u * Im z)) = 1.

rewrite the current goal using mul_CSNo_CRe i (u * Im z) CSNo_Complex_i LuImz' (from left to right).

We will prove Re z * (u * Re z + - (Re i * Re (u * Im z) + - Im i * Im (u * Im z))) + - Im z * (0 + - Im (i ⨯ u * Im z)) = 1.

rewrite the current goal using mul_CSNo_CIm i (u * Im z) CSNo_Complex_i LuImz' (from left to right).

We will prove Re z * (u * Re z + - (Re i * Re (u * Im z) + - Im i * Im (u * Im z))) + - Im z * (0 + - (Re i * Im (u * Im z) + Im i * Re (u * Im z))) = 1.

rewrite the current goal using Re_i (from left to right).

rewrite the current goal using Im_i (from left to right).

We will prove Re z * (u * Re z + - (0 * Re (u * Im z) + - 1 * Im (u * Im z))) + - Im z * (0 + - (0 * Im (u * Im z) + 1 * Re (u * Im z))) = 1.

rewrite the current goal using SNo_Re (u * Im z) LuImz (from left to right).

rewrite the current goal using SNo_Im (u * Im z) LuImz (from left to right).

We will prove Re z * (u * Re z + - (0 * (u * Im z) + - 1 * 0)) + - Im z * (0 + - (0 * 0 + 1 * (u * Im z))) = 1.

rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from left to right).

rewrite the current goal using mul_SNo_zeroL (u * Im z) LuImz (from left to right).

rewrite the current goal using mul_SNo_zeroR 1 SNo_1 (from left to right).

We will prove Re z * (u * Re z + - (0 + - 0)) + - Im z * (0 + - (0 + 1 * (u * Im z))) = 1.

rewrite the current goal using minus_SNo_0 (from left to right).

rewrite the current goal using add_SNo_0L 0 SNo_0 (from left to right).

rewrite the current goal using minus_SNo_0 (from left to right).

rewrite the current goal using add_SNo_0R (u * Re z) LuRez (from left to right).

We will prove Re z * (u * Re z) + - Im z * (0 + - (0 + 1 * (u * Im z))) = 1.

rewrite the current goal using mul_SNo_oneL (u * Im z) LuImz (from left to right).

We will prove Re z * (u * Re z) + - Im z * (0 + - (0 + (u * Im z))) = 1.

rewrite the current goal using add_SNo_0L (u * Im z) LuImz (from left to right).

rewrite the current goal using add_SNo_0L (- u * Im z) (SNo_minus_SNo (u * Im z) LuImz) (from left to right).

We will prove Re z * (u * Re z) + - Im z * (- (u * Im z)) = 1.

rewrite the current goal using mul_SNo_minus_distrR (Im z) (- u * Im z) LImzR (SNo_minus_SNo (u * Im z) LuImz) (from right to left).

rewrite the current goal using minus_SNo_invol (u * Im z) LuImz (from left to right).

We will prove Re z * (u * Re z) + Im z * (u * Im z) = 1.

rewrite the current goal using mul_SNo_com_3_0_1 (Re z) u (Re z) ?? ?? ?? (from left to right).

rewrite the current goal using mul_SNo_com_3_0_1 (Im z) u (Im z) ?? ?? ?? (from left to right).

We will prove u * (Re z * Re z) + u * (Im z * Im z) = 1.

rewrite the current goal using mul_SNo_com u (Re z * Re z) ?? ?? (from left to right).

rewrite the current goal using mul_SNo_com u (Im z * Im z) ?? ?? (from left to right).

rewrite the current goal using mul_SNo_distrR (Re z * Re z) (Im z * Im z) u ?? ?? ?? (from right to left).

An exact proof term for the current goal is Hur.

We will prove Im (z ⨯ (u * Re z + :-: i ⨯ u * Im z)) = Im 1.

rewrite the current goal using mul_CSNo_CIm z (u * Re z + :-: i ⨯ u * Im z) Hz L1 (from left to right).

rewrite the current goal using Im_1 (from left to right).

We will prove Re z * Im (u * Re z + :-: i ⨯ u * Im z) + Im z * Re (u * Re z + :-: i ⨯ u * Im z) = 0.

rewrite the current goal using add_CSNo_CRe (u * Re z) (:-: i ⨯ u * Im z) LuRez' LmiuImz (from left to right).

rewrite the current goal using add_CSNo_CIm (u * Re z) (:-: i ⨯ u * Im z) LuRez' LmiuImz (from left to right).

We will prove Re z * (Im (u * Re z) + Im (:-: i ⨯ u * Im z)) + Im z * (Re (u * Re z) + Re (:-: i ⨯ u * Im z)) = 0.

rewrite the current goal using minus_CSNo_CRe (i ⨯ u * Im z) LiuImz (from left to right).

rewrite the current goal using minus_CSNo_CIm (i ⨯ u * Im z) LiuImz (from left to right).

We will prove Re z * (Im (u * Re z) + - Im (i ⨯ u * Im z)) + Im z * (Re (u * Re z) + - Re (i ⨯ u * Im z)) = 0.

rewrite the current goal using SNo_Re (u * Re z) LuRez (from left to right).

rewrite the current goal using SNo_Im (u * Re z) LuRez (from left to right).

We will prove Re z * (0 + - Im (i ⨯ u * Im z)) + Im z * ((u * Re z) + - Re (i ⨯ u * Im z)) = 0.

rewrite the current goal using mul_CSNo_CRe i (u * Im z) CSNo_Complex_i LuImz' (from left to right).

We will prove Re z * (0 + - Im (i ⨯ u * Im z)) + Im z * ((u * Re z) + - (Re i * Re (u * Im z) + - Im i * Im (u * Im z))) = 0.

rewrite the current goal using mul_CSNo_CIm i (u * Im z) CSNo_Complex_i LuImz' (from left to right).

We will prove Re z * (0 + - (Re i * Im (u * Im z) + Im i * Re (u * Im z))) + Im z * ((u * Re z) + - (Re i * Re (u * Im z) + - Im i * Im (u * Im z))) = 0.

rewrite the current goal using Re_i (from left to right).

rewrite the current goal using Im_i (from left to right).

We will prove Re z * (0 + - (0 * Im (u * Im z) + 1 * Re (u * Im z))) + Im z * ((u * Re z) + - (0 * Re (u * Im z) + - 1 * Im (u * Im z))) = 0.

rewrite the current goal using SNo_Re (u * Im z) LuImz (from left to right).

rewrite the current goal using SNo_Im (u * Im z) LuImz (from left to right).

We will prove Re z * (0 + - (0 * 0 + 1 * (u * Im z))) + Im z * ((u * Re z) + - (0 * (u * Im z) + - 1 * 0)) = 0.

rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).

rewrite the current goal using mul_SNo_zeroL (u * Im z) ?? (from left to right).

rewrite the current goal using mul_SNo_zeroR 1 SNo_1 (from left to right).

rewrite the current goal using mul_SNo_oneL (u * Im z) ?? (from left to right).

We will prove Re z * (0 + - (0 + u * Im z)) + Im z * ((u * Re z) + - (0 + - 0)) = 0.

rewrite the current goal using minus_SNo_0 (from left to right).

rewrite the current goal using add_SNo_0L 0 SNo_0 (from left to right).

rewrite the current goal using minus_SNo_0 (from left to right).

rewrite the current goal using add_SNo_0R (u * Re z) ?? (from left to right).

rewrite the current goal using add_SNo_0L (u * Im z) ?? (from left to right).

We will prove Re z * (0 + - (u * Im z)) + Im z * (u * Re z) = 0.

rewrite the current goal using add_SNo_0L (- (u * Im z)) (SNo_minus_SNo (u * Im z) ??) (from left to right).

We will prove Re z * (- (u * Im z)) + Im z * (u * Re z) = 0.

rewrite the current goal using mul_SNo_minus_distrR (Re z) (u * Im z) ?? ?? (from left to right).

We will prove - Re z * u * Im z + Im z * u * Re z = 0.

rewrite the current goal using mul_SNo_com_3_0_1 (Re z) u (Im z) ?? ?? ?? (from left to right).

rewrite the current goal using mul_SNo_com_3_0_1 (Im z) u (Re z) ?? ?? ?? (from left to right).

We will prove - u * Re z * Im z + u * Im z * Re z = 0.

rewrite the current goal using mul_SNo_com (Re z) (Im z) ?? ?? (from left to right).

We will prove - u * Im z * Re z + u * Im z * Re z = 0.

An exact proof term for the current goal is add_SNo_minus_SNo_linv (u * Im z * Re z) (SNo_mul_SNo_3 u (Im z) (Re z) ?? ?? ??).

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Subgoal 9 Subgoal 10 Subgoal 11 Main Goal

End of Section ComplexSNo

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.

Theorem. (complex_I) The following is provable:

∀x y ∈ real, pa x y ∈ complex

Proof:

Let x be given.

Assume Hx.

Let y be given.

Assume Hy.

We will prove pa x y ∈ complex.

rewrite the current goal using tuple_2_0_eq x y (from right to left).

rewrite the current goal using tuple_2_1_eq x y (from right to left) at position 2.

We will prove pa ((x,y) 0) ((x,y) 1) ∈ complex.

Apply ReplI (real ⨯ real) (λu ⇒ pa (u 0) (u 1)) to the current goal.

We will prove (x,y) ∈ real ⨯ real.

An exact proof term for the current goal is tuple_2_setprod real real x Hx y Hy.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_E) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

Let p be given.

Assume Hp.

Apply ReplE_impred (real ⨯ real) (λu ⇒ pa (u 0) (u 1)) z Hz to the current goal.

Let u be given.

Assume Hu: u ∈ real ⨯ real.

Assume Hzu: z = pa (u 0) (u 1).

An exact proof term for the current goal is Hp (u 0) (ap0_Sigma real (λ_ ⇒ real) u Hu) (u 1) (ap1_Sigma real (λ_ ⇒ real) u Hu) Hzu.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_CSNo) The following is provable:

∀z ∈ complex, CSNo z

Proof:

Let z be given.

Assume Hz.

Apply complex_E z Hz to the current goal.

Let x be given.

Assume Hx.

Let y be given.

Assume Hy.

Assume Hzxy: z = pa x y.

We will prove CSNo z.

rewrite the current goal using Hzxy (from left to right).

Apply CSNo_I to the current goal.

An exact proof term for the current goal is real_SNo x Hx.

An exact proof term for the current goal is real_SNo y Hy.

∎

Try to prove it yourself. Main Goal

Theorem. (real_complex) The following is provable:

real ⊆ complex

Proof:

Let x be given.

Assume Hx: x ∈ real.

We will prove x ∈ complex.

rewrite the current goal using SNo_pair_0 x (from right to left).

We will prove pa x 0 ∈ complex.

Apply complex_I to the current goal.

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is real_0.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_0) The following is provable:

0 ∈ complex

Proof:

An exact proof term for the current goal is real_complex 0 real_0.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_1) The following is provable:

1 ∈ complex

Proof:

An exact proof term for the current goal is real_complex 1 real_1.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_i) The following is provable:

i ∈ complex

Proof:

We will prove pa 0 1 ∈ complex.

Apply complex_I to the current goal.

An exact proof term for the current goal is real_0.

An exact proof term for the current goal is real_1.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_Re_eq) The following is provable:

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

Proof:

Let x be given.

Assume Hx.

Let y be given.

Assume Hy.

An exact proof term for the current goal is CSNo_Re2 x y (real_SNo x Hx) (real_SNo y Hy).

∎

Try to prove it yourself. Main Goal

Theorem. (complex_Im_eq) The following is provable:

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

Proof:

Let x be given.

Assume Hx.

Let y be given.

Assume Hy.

An exact proof term for the current goal is CSNo_Im2 x y (real_SNo x Hx) (real_SNo y Hy).

∎

Try to prove it yourself. Main Goal

Theorem. (complex_Re_real) The following is provable:

∀z ∈ complex, Re z ∈ real

Proof:

Let z be given.

Assume Hz.

Apply complex_E z Hz to the current goal.

Let x be given.

Assume Hx.

Let y be given.

Assume Hy Hzxy.

rewrite the current goal using Hzxy (from left to right).

We will prove Re (pa x y) ∈ real.

rewrite the current goal using complex_Re_eq x Hx y Hy (from left to right).

We will prove x ∈ real.

An exact proof term for the current goal is Hx.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_Im_real) The following is provable:

∀z ∈ complex, Im z ∈ real

Proof:

Let z be given.

Assume Hz.

Apply complex_E z Hz to the current goal.

Let x be given.

Assume Hx.

Let y be given.

Assume Hy Hzxy.

rewrite the current goal using Hzxy (from left to right).

We will prove Im (pa x y) ∈ real.

rewrite the current goal using complex_Im_eq x Hx y Hy (from left to right).

We will prove y ∈ real.

An exact proof term for the current goal is Hy.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_ReIm_split) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

Let w be given.

Assume Hw.

An exact proof term for the current goal is CSNo_ReIm_split z w (complex_CSNo z Hz) (complex_CSNo w Hw).

∎

Try to prove it yourself. Main Goal

Theorem. (complex_minus_CSNo) The following is provable:

∀z ∈ complex, - z ∈ complex

Proof:

Let z be given.

Assume Hz.

We will prove pa (minus_SNo (Re z)) (minus_SNo (Im z)) ∈ complex.

Apply complex_I to the current goal.

Apply real_minus_SNo to the current goal.

An exact proof term for the current goal is complex_Re_real z Hz.

Apply real_minus_SNo to the current goal.

An exact proof term for the current goal is complex_Im_real z Hz.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_add_CSNo) The following is provable:

∀z w ∈ complex, z + w ∈ complex

Proof:

Let z be given.

Assume Hz.

Let w be given.

Assume Hw.

We will prove pa (add_SNo (Re z) (Re w)) (add_SNo (Im z) (Im w)) ∈ complex.

Apply complex_I to the current goal.

Apply real_add_SNo to the current goal.

An exact proof term for the current goal is complex_Re_real z Hz.

An exact proof term for the current goal is complex_Re_real w Hw.

Apply real_add_SNo to the current goal.

An exact proof term for the current goal is complex_Im_real z Hz.

An exact proof term for the current goal is complex_Im_real w Hw.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_mul_CSNo) The following is provable:

∀z w ∈ complex, z * w ∈ complex

Proof:

Let z be given.

Assume Hz.

Let w be given.

Assume Hw.

We will prove pa (add_SNo (mul_SNo (Re z) (Re w)) (minus_SNo (mul_SNo (Im z) (Im w)))) (add_SNo (mul_SNo (Re z) (Im w)) (mul_SNo (Im z) (Re w))) ∈ complex.

We prove the intermediate claim Lz0: Re z ∈ real.

An exact proof term for the current goal is complex_Re_real z Hz.

We prove the intermediate claim Lz1: Im z ∈ real.

An exact proof term for the current goal is complex_Im_real z Hz.

We prove the intermediate claim Lw0: Re w ∈ real.

An exact proof term for the current goal is complex_Re_real w Hw.

We prove the intermediate claim Lw1: Im w ∈ real.

An exact proof term for the current goal is complex_Im_real w Hw.

Apply complex_I to the current goal.

Apply real_add_SNo to the current goal.

Apply real_mul_SNo to the current goal.

An exact proof term for the current goal is ??.

Apply real_minus_SNo to the current goal.

Apply real_mul_SNo to the current goal.

An exact proof term for the current goal is ??.

Apply real_add_SNo to the current goal.

Apply real_mul_SNo to the current goal.

An exact proof term for the current goal is ??.

Apply real_mul_SNo to the current goal.

An exact proof term for the current goal is ??.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Main Goal

Theorem. (real_Re_eq) The following is provable:

∀x ∈ real, Re x = x

Proof:

Let x be given.

Assume Hx.

rewrite the current goal using SNo_pair_0 x (from right to left) at position 1.

An exact proof term for the current goal is complex_Re_eq x Hx 0 real_0.

∎

Try to prove it yourself. Main Goal

Theorem. (real_Im_eq) The following is provable:

∀x ∈ real, Im x = 0

Proof:

Let x be given.

Assume Hx.

rewrite the current goal using SNo_pair_0 x (from right to left).

An exact proof term for the current goal is complex_Im_eq x Hx 0 real_0.

∎

Try to prove it yourself. Main Goal

Theorem. (mul_i_real_eq) The following is provable:

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

Proof:

Let x be given.

Assume Hx.

We will prove pa (add_SNo (mul_SNo (Re (pa 0 1)) (Re x)) (minus_SNo (mul_SNo (Im (pa 0 1)) (Im x)))) (add_SNo (mul_SNo (Re (pa 0 1)) (Im x)) (mul_SNo (Im (pa 0 1)) (Re x))) = pa 0 x.

rewrite the current goal using real_Re_eq x Hx (from left to right).

rewrite the current goal using real_Im_eq x Hx (from left to right).

rewrite the current goal using complex_Re_eq 0 real_0 1 real_1 (from left to right).

rewrite the current goal using complex_Im_eq 0 real_0 1 real_1 (from left to right).

We will prove pa (add_SNo (mul_SNo 0 x) (minus_SNo (mul_SNo 1 0))) (add_SNo (mul_SNo 0 0) (mul_SNo 1 x)) = pa 0 x.

rewrite the current goal using mul_SNo_zeroL x (real_SNo x Hx) (from left to right).

rewrite the current goal using mul_SNo_zeroR 1 SNo_1 (from left to right).

rewrite the current goal using minus_SNo_0 (from left to right).

rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).

rewrite the current goal using mul_SNo_oneL x (real_SNo x Hx) (from left to right).

We will prove pa (add_SNo 0 0) (add_SNo 0 x) = pa 0 x.

rewrite the current goal using add_SNo_0L 0 SNo_0 (from left to right).

rewrite the current goal using add_SNo_0L x (real_SNo x Hx) (from left to right).

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (real_Re_i_eq) The following is provable:

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

Proof:

Let x be given.

Assume Hx.

rewrite the current goal using mul_i_real_eq x Hx (from left to right).

We will prove Re (pa 0 x) = 0.

An exact proof term for the current goal is complex_Re_eq 0 real_0 x Hx.

∎

Try to prove it yourself. Main Goal

Theorem. (real_Im_i_eq) The following is provable:

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

Proof:

Let x be given.

Assume Hx.

rewrite the current goal using mul_i_real_eq x Hx (from left to right).

We will prove Im (pa 0 x) = x.

An exact proof term for the current goal is complex_Im_eq 0 real_0 x Hx.

∎

Try to prove it yourself. Main Goal

Theorem. (complex_eta) The following is provable:

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

Proof:

Let z be given.

Assume Hz.

Apply complex_E z Hz to the current goal.

Let x be given.

Assume Hx.

Let y be given.

Assume Hy Hzxy.

rewrite the current goal using Hzxy (from left to right).

rewrite the current goal using complex_Re_eq x Hx y Hy (from left to right).

rewrite the current goal using complex_Im_eq x Hx y Hy (from left to right).

We will prove pa x y = x + i * y.

We will prove pa x y = pa (add_SNo (Re x) (Re (i * y))) (add_SNo (Im x) (Im (i * y))).

rewrite the current goal using real_Re_eq x Hx (from left to right).

rewrite the current goal using real_Im_eq x Hx (from left to right).

rewrite the current goal using real_Re_i_eq y Hy (from left to right).

rewrite the current goal using real_Im_i_eq y Hy (from left to right).

We will prove pa x y = pa (add_SNo x 0) (add_SNo 0 y).

rewrite the current goal using add_SNo_0R x (real_SNo x Hx) (from left to right).

rewrite the current goal using add_SNo_0L y (real_SNo y Hy) (from left to right).

Use reflexivity.

∎

Try to prove it yourself. Main Goal

Theorem. (nonzero_complex_recip_ex) The following is provable:

∀z ∈ complex, z ≠ 0 → ∃w ∈ complex, z * w = 1

Proof:

Let z be given.

Assume Hz Hznz.

Set x to be the term Re z.

Set y to be the term Im z.

Set r to be the term add_SNo (mul_SNo x x) (mul_SNo y y).

We prove the intermediate claim Lx: x ∈ real.

An exact proof term for the current goal is complex_Re_real z Hz.

We prove the intermediate claim Ly: y ∈ real.

An exact proof term for the current goal is complex_Im_real z Hz.

We prove the intermediate claim Lxx: mul_SNo x x ∈ real.

An exact proof term for the current goal is real_mul_SNo x ?? x ??.

We prove the intermediate claim Lxx': SNo (mul_SNo x x).

Apply real_SNo to the current goal.

An exact proof term for the current goal is Lxx.

We prove the intermediate claim Lyy: mul_SNo y y ∈ real.

An exact proof term for the current goal is real_mul_SNo y ?? y ??.

We prove the intermediate claim Lyy': SNo (mul_SNo y y).

Apply real_SNo to the current goal.

An exact proof term for the current goal is Lyy.

We prove the intermediate claim Lr: r ∈ real.

An exact proof term for the current goal is real_add_SNo (mul_SNo x x) ?? (mul_SNo y y) ??.

We prove the intermediate claim Lr': SNo r.

Apply real_SNo to the current goal.

An exact proof term for the current goal is Lr.

We prove the intermediate claim Lrnz: r ≠ 0.

Assume H1: r = 0.

Apply Hznz to the current goal.

We will prove z = 0.

Apply CSNo_ReIm_split z 0 (complex_CSNo z Hz) CSNo_0 to the current goal.

We will prove Re z = Re 0.

rewrite the current goal using Re_0 (from left to right).

We will prove x = 0.

Apply SNo_zero_or_sqr_pos x (real_SNo x Lx) to the current goal.

Assume H2: x = 0.

An exact proof term for the current goal is H2.

Assume H2: 0 < mul_SNo x x.

We will prove False.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

rewrite the current goal using H1 (from right to left) at position 2.

We will prove 0 < r.

Apply SNoLtLe_tra 0 (mul_SNo x x) r SNo_0 ?? ?? H2 to the current goal.

We will prove mul_SNo x x ≤ r.

rewrite the current goal using add_SNo_0R (mul_SNo x x) ?? (from right to left) at position 1.

We will prove add_SNo (mul_SNo x x) 0 ≤ r.

Apply add_SNo_Le2 (mul_SNo x x) 0 (mul_SNo y y) ?? SNo_0 ?? to the current goal.

We will prove 0 ≤ mul_SNo y y.

Apply SNo_sqr_nonneg y (real_SNo y Ly) to the current goal.

We will prove Im z = Im 0.

rewrite the current goal using Im_0 (from left to right).

We will prove y = 0.

Apply SNo_zero_or_sqr_pos y (real_SNo y Ly) to the current goal.

Assume H2: y = 0.

An exact proof term for the current goal is H2.

Assume H2: 0 < mul_SNo y y.

We will prove False.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

rewrite the current goal using H1 (from right to left) at position 2.

We will prove 0 < r.

Apply SNoLtLe_tra 0 (mul_SNo y y) r SNo_0 ?? ?? H2 to the current goal.

We will prove mul_SNo y y ≤ r.

rewrite the current goal using add_SNo_0L (mul_SNo y y) ?? (from right to left) at position 1.

We will prove add_SNo 0 (mul_SNo y y) ≤ r.

Apply add_SNo_Le1 0 (mul_SNo y y) (mul_SNo x x) SNo_0 ?? ?? to the current goal.

We will prove 0 ≤ mul_SNo x x.

Apply SNo_sqr_nonneg x (real_SNo x Lx) to the current goal.

Apply nonzero_real_recip_ex r Lr Lrnz to the current goal.

Let u be given.

Assume H.

Apply H to the current goal.

Assume Hu: u ∈ real.

Assume Hu2: mul_SNo r u = 1.

We use (u * x + - i * u * y) to witness the existential quantifier.

Apply andI to the current goal.

Apply complex_add_CSNo to the current goal.

Apply complex_mul_CSNo to the current goal.

Apply real_complex to the current goal.

An exact proof term for the current goal is Hu.

Apply real_complex to the current goal.

An exact proof term for the current goal is ??.

Apply complex_minus_CSNo to the current goal.

Apply complex_mul_CSNo to the current goal.

An exact proof term for the current goal is complex_i.

Apply complex_mul_CSNo to the current goal.

Apply real_complex to the current goal.

An exact proof term for the current goal is Hu.

Apply real_complex to the current goal.

An exact proof term for the current goal is ??.

Apply CSNo_relative_recip z (complex_CSNo z Hz) u (real_SNo u Hu) Hu2 to the current goal.

∎

Try to prove it yourself. Subgoal 1 Subgoal 2 Subgoal 3 Subgoal 4 Subgoal 5 Subgoal 6 Subgoal 7 Subgoal 8 Subgoal 9 Main Goal

Theorem. (complex_real_set_eq) The following is provable:

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

Proof:

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ real.

Apply SepI to the current goal.

An exact proof term for the current goal is real_complex x Hx.

An exact proof term for the current goal is real_Re_eq x Hx.

Let z be given.

Assume Hz: z ∈ {z ∈ complex|Re z = z}.

Apply SepE complex (λz ⇒ Re z = z) z Hz to the current goal.

Assume Hz1: z ∈ complex.

Assume Hz2: Re z = z.

We will prove z ∈ real.

rewrite the current goal using Hz2 (from right to left).

An exact proof term for the current goal is complex_Re_real z Hz1.

∎

Try to prove it yourself. Main Goal

End of Section Complex

Complex Surreal Numbers and Complex Numbers

From Parts 1 to 8

Complex Surreal Numbers