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.
Definition. We define int to be ω ∪ {- n|n ∈ ω} of type set.
In Proofgold the corresponding term root is 90ee85... and object id is 331669...
Theorem. (int_SNo_cases)
∀p : set → prop, (∀n ∈ ω, p n) → (∀n ∈ ω, p (- n)) → ∀x ∈ int, p x
In Proofgold the corresponding term root is 60107a... and proposition id is 14278d...
Proof:
Let p be given.
Assume Hp1 Hp2.
Let x be given.
Assume Hx.
We will prove p x.
Apply binunionE ω {- n|n ∈ ω} x Hx to the current goal.
Assume Hx: x ∈ ω.
An exact proof term for the current goal is Hp1 x Hx.
Assume Hx.
Apply ReplE_impred ω minus_SNo x Hx to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hxn: x = - n.
rewrite the current goal using Hxn (from left to right).
An exact proof term for the current goal is Hp2 n Hn.
∎
Theorem. (int_3_cases)
∀n ∈ int, ∀p : prop, (∀m ∈ ω, n = - ordsucc m → p) → (n = 0 → p) → (∀m ∈ ω, n = ordsucc m → p) → p
In Proofgold the corresponding term root is 67b16d... and proposition id is 5c24db...
Proof:
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Let p be given.
Assume Hneg H0 Hpos.
We prove the intermediate claim L1: ∀k, nat_p k → m = ordsucc k → p.
Let k be given.
Assume Hk HmSk.
An exact proof term for the current goal is Hpos k (nat_p_omega k Hk) HmSk.
An exact proof term for the current goal is nat_inv_impred (λk ⇒ m = k → p) H0 L1 m (omega_nat_p m Hm) (λq H ⇒ H).
Let m be given.
Assume Hm: m ∈ ω.
Let p be given.
Assume Hneg: ∀k ∈ ω, - m = - ordsucc k → p.
Assume H0: - m = 0 → p.
Assume Hpos: ∀k ∈ ω, - m = ordsucc k → p.
We prove the intermediate claim L2: m = 0 → p.
Assume Hm0.
Apply H0 to the current goal.
rewrite the current goal using Hm0 (from left to right).
An exact proof term for the current goal is minus_SNo_0.
We prove the intermediate claim L3: ∀k, nat_p k → m = ordsucc k → p.
Let k be given.
Assume Hk HmSk.
Apply Hneg k (nat_p_omega k Hk) to the current goal.
We will prove - m = - ordsucc k.
Use f_equal.
An exact proof term for the current goal is HmSk.
Apply nat_inv_impred (λk ⇒ m = k → p) L2 L3 m (omega_nat_p m Hm) (λq H ⇒ H) to the current goal.
∎
Theorem. (int_SNo)
∀x ∈ int, SNo x
In Proofgold the corresponding term root is 19fdd2... and proposition id is 6089ec...
Proof:
Apply int_SNo_cases to the current goal.
An exact proof term for the current goal is omega_SNo.
Let n be given.
Assume Hn.
We will prove SNo (- n).
Apply SNo_minus_SNo to the current goal.
We will prove SNo n.
An exact proof term for the current goal is omega_SNo n Hn.
∎
Theorem. (Subq_omega_int)
ω ⊆ int
In Proofgold the corresponding term root is 405dda... and proposition id is b1bb2b...
Proof:
Let n be given.
Assume Hn.
We will prove n ∈ ω ∪ {- k|k ∈ ω}.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is Hn.
∎
Theorem. (int_minus_SNo_omega)
∀n ∈ ω, - n ∈ int
In Proofgold the corresponding term root is 869503... and proposition id is 3a2593...
Proof:
Let n be given.
Assume Hn.
We will prove - n ∈ ω ∪ {- k|k ∈ ω}.
Apply binunionI2 to the current goal.
We will prove - n ∈ {- k|k ∈ ω}.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn.
∎
Theorem. (int_add_SNo_lem)
∀n ∈ ω, ∀m, nat_p m → - n + m ∈ int
In Proofgold the corresponding term root is 8f0047... and proposition id is aab9d5...
Proof:
Let n be given.
Assume Hn.
We prove the intermediate claim Lnn: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Lno: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Lnn.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is ordinal_SNo n Lno.
Apply nat_ind to the current goal.
We will prove - n + 0 ∈ int.
rewrite the current goal using add_SNo_0R (- n) (SNo_minus_SNo n LnS) (from left to right).
We will prove - n ∈ int.
Apply int_minus_SNo_omega to the current goal.
An exact proof term for the current goal is Hn.
Let m be given.
Assume Hm: nat_p m.
Assume IHm: - n + m ∈ int.
We prove the intermediate claim Lmo: ordinal m.
An exact proof term for the current goal is nat_p_ordinal m Hm.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is ordinal_SNo m Lmo.
We will prove - n + ordsucc m ∈ int.
rewrite the current goal using ordinal_ordsucc_SNo_eq m Lmo (from left to right).
We will prove - n + (1 + m) ∈ int.
rewrite the current goal using add_SNo_com_3_0_1 (- n) 1 m (SNo_minus_SNo n LnS) SNo_1 LmS (from left to right).
We will prove 1 + (- n + m) ∈ int.
We prove the intermediate claim L1: ∀k ∈ ω, - n + m = k → 1 + (- n + m) ∈ int.
Let k be given.
Assume Hk He.
rewrite the current goal using He (from left to right).
We will prove 1 + k ∈ int.
rewrite the current goal using ordinal_ordsucc_SNo_eq k (nat_p_ordinal k (omega_nat_p k Hk)) (from right to left).
We will prove ordsucc k ∈ int.
Apply Subq_omega_int to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hk.
We prove the intermediate claim L2: ∀k ∈ ω, - n + m = - k → 1 + (- n + m) ∈ int.
Let k be given.
Assume Hk He.
rewrite the current goal using He (from left to right).
We will prove 1 + - k ∈ int.
Apply nat_inv k (omega_nat_p k Hk) to the current goal.
Assume H1: k = 0.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using add_SNo_0R 1 SNo_1 (from left to right).
We will prove 1 ∈ int.
Apply Subq_omega_int to the current goal.
We will prove 1 ∈ ω.
An exact proof term for the current goal is nat_p_omega 1 nat_1.
Assume H1.
Apply H1 to the current goal.
Let k' be given.
Assume H1.
Apply H1 to the current goal.
Assume H1: nat_p k'.
Assume H2: k = ordsucc k'.
rewrite the current goal using H2 (from left to right).
We will prove 1 + - (ordsucc k') ∈ int.
rewrite the current goal using ordinal_ordsucc_SNo_eq k' (nat_p_ordinal k' H1) (from left to right).
We will prove 1 + - (1 + k') ∈ int.
rewrite the current goal using minus_add_SNo_distr 1 k' SNo_1 (ordinal_SNo k' (nat_p_ordinal k' H1)) (from left to right).
We will prove 1 + - 1 + - k' ∈ int.
rewrite the current goal using add_SNo_minus_L2' 1 (- k') SNo_1 (SNo_minus_SNo k' (ordinal_SNo k' (nat_p_ordinal k' H1))) (from left to right).
We will prove - k' ∈ int.
Apply int_minus_SNo_omega to the current goal.
An exact proof term for the current goal is nat_p_omega k' H1.
Apply int_SNo_cases (λx ⇒ - n + m = x → 1 + (- n + m) ∈ int) L1 L2 (- n + m) IHm to the current goal.
Use reflexivity.
∎
Theorem. (int_add_SNo)
∀x y ∈ int, x + y ∈ int
In Proofgold the corresponding term root is d66975... and proposition id is 1036d9...
Proof:
Apply int_SNo_cases to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Apply Subq_omega_int to the current goal.
We will prove n + m ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega n Hn m Hm.
Let m be given.
Assume Hm: m ∈ ω.
We will prove n + - m ∈ int.
rewrite the current goal using add_SNo_com n (- m) (ordinal_SNo n (nat_p_ordinal n (omega_nat_p n Hn))) (SNo_minus_SNo m (ordinal_SNo m (nat_p_ordinal m (omega_nat_p m Hm)))) (from left to right).
We will prove - m + n ∈ int.
An exact proof term for the current goal is int_add_SNo_lem m Hm n (omega_nat_p n Hn).
Let n be given.
Assume Hn: n ∈ ω.
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
We will prove - n + m ∈ int.
An exact proof term for the current goal is int_add_SNo_lem n Hn m (omega_nat_p m Hm).
Let m be given.
Assume Hm: m ∈ ω.
We will prove - n + - m ∈ int.
We prove the intermediate claim Ln: SNo n.
An exact proof term for the current goal is ordinal_SNo n (nat_p_ordinal n (omega_nat_p n Hn)).
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is ordinal_SNo m (nat_p_ordinal m (omega_nat_p m Hm)).
rewrite the current goal using minus_add_SNo_distr n m Ln Lm (from right to left).
Apply int_minus_SNo_omega to the current goal.
We will prove n + m ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega n Hn m Hm.
∎
Theorem. (int_minus_SNo)
∀x ∈ int, - x ∈ int
In Proofgold the corresponding term root is 00e714... and proposition id is b2c591...
Proof:
Apply int_SNo_cases to the current goal.
Let n be given.
Assume Hn.
We will prove - n ∈ int.
Apply int_minus_SNo_omega to the current goal.
An exact proof term for the current goal is Hn.
Let n be given.
Assume Hn.
We will prove - - n ∈ int.
rewrite the current goal using minus_SNo_invol n (ordinal_SNo n (nat_p_ordinal n (omega_nat_p n Hn))) (from left to right).
We will prove n ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is Hn.
∎
Theorem. (int_mul_SNo)
∀x y ∈ int, x * y ∈ int
In Proofgold the corresponding term root is a7bc92... and proposition id is f40564...
Proof:
Apply int_SNo_cases to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
We prove the intermediate claim Lnn: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Lno: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Lnn.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is ordinal_SNo n Lno.
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Apply Subq_omega_int to the current goal.
We will prove n * m ∈ ω.
An exact proof term for the current goal is mul_SNo_In_omega n Hn m Hm.
Let m be given.
Assume Hm: m ∈ ω.
We prove the intermediate claim Lmn: nat_p m.
An exact proof term for the current goal is omega_nat_p m Hm.
We prove the intermediate claim Lmo: ordinal m.
An exact proof term for the current goal is nat_p_ordinal m Lmn.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is ordinal_SNo m Lmo.
We will prove n * (- m) ∈ int.
rewrite the current goal using mul_SNo_com n (- m) LnS (SNo_minus_SNo m LmS) (from left to right).
We will prove (- m) * n ∈ int.
rewrite the current goal using mul_SNo_minus_distrL m n LmS LnS (from left to right).
We will prove - (m * n) ∈ int.
Apply int_minus_SNo to the current goal.
We will prove m * n ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is mul_SNo_In_omega m Hm n Hn.
Let n be given.
Assume Hn: n ∈ ω.
We prove the intermediate claim Lnn: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Lno: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Lnn.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is ordinal_SNo n Lno.
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
We prove the intermediate claim Lmn: nat_p m.
An exact proof term for the current goal is omega_nat_p m Hm.
We prove the intermediate claim Lmo: ordinal m.
An exact proof term for the current goal is nat_p_ordinal m Lmn.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is ordinal_SNo m Lmo.
We will prove (- n) * m ∈ int.
rewrite the current goal using mul_SNo_minus_distrL n m LnS LmS (from left to right).
We will prove - (n * m) ∈ int.
Apply int_minus_SNo to the current goal.
We will prove n * m ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is mul_SNo_In_omega n Hn m Hm.
Let m be given.
Assume Hm: m ∈ ω.
We prove the intermediate claim Lmn: nat_p m.
An exact proof term for the current goal is omega_nat_p m Hm.
We prove the intermediate claim Lmo: ordinal m.
An exact proof term for the current goal is nat_p_ordinal m Lmn.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is ordinal_SNo m Lmo.
We will prove (- n) * (- m) ∈ int.
rewrite the current goal using mul_SNo_minus_distrL n (- m) LnS (SNo_minus_SNo m LmS) (from left to right).
We will prove - (n * (- m)) ∈ int.
rewrite the current goal using mul_SNo_com n (- m) LnS (SNo_minus_SNo m LmS) (from left to right).
We will prove - ((- m) * n) ∈ int.
rewrite the current goal using mul_SNo_minus_distrL m n LmS LnS (from left to right).
We will prove - - (m * n) ∈ int.
rewrite the current goal using minus_SNo_invol (m * n) (SNo_mul_SNo m n LmS LnS) (from left to right).
We will prove m * n ∈ int.
Apply Subq_omega_int to the current goal.
We will prove m * n ∈ ω.
An exact proof term for the current goal is mul_SNo_In_omega m Hm n Hn.
∎
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.
In Proofgold the corresponding term root is 34f6dc... and object id is 2990e5...
Theorem. (nonneg_abs_SNo)
∀x, 0 ≤ x → abs_SNo x = x
In Proofgold the corresponding term root is 330ed1... and proposition id is 1ed323...
Proof:
Let x be given.
Assume Hx.
An exact proof term for the current goal is If_i_1 (0 ≤ x) x (- x) Hx.
∎
Theorem. (not_nonneg_abs_SNo)
∀x, ¬ (0 ≤ x) → abs_SNo x = - x
In Proofgold the corresponding term root is bc755d... and proposition id is b29f70...
Proof:
Let x be given.
Assume Hx.
An exact proof term for the current goal is If_i_0 (0 ≤ x) x (- x) Hx.
∎
Theorem. (abs_SNo_0)
abs_SNo 0 = 0
In Proofgold the corresponding term root is c0c559... and proposition id is 35a655...
Proof:
Apply nonneg_abs_SNo to the current goal.
We will prove 0 ≤ 0.
Apply SNoLe_ref to the current goal.
∎
Theorem. (pos_abs_SNo)
∀x, 0 < x → abs_SNo x = x
In Proofgold the corresponding term root is 32e626... and proposition id is 88568f...
Proof:
Let x be given.
Assume Hx.
Apply nonneg_abs_SNo to the current goal.
We will prove 0 ≤ x.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hx.
∎
Theorem. (neg_abs_SNo)
∀x, SNo x → x < 0 → abs_SNo x = - x
In Proofgold the corresponding term root is d1245a... and proposition id is f858cb...
Proof:
Let x be given.
Assume Hx1 Hx2.
Apply not_nonneg_abs_SNo to the current goal.
Assume H1: 0 ≤ x.
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
An exact proof term for the current goal is SNoLtLe_tra x 0 x Hx1 SNo_0 Hx1 Hx2 H1.
∎
Theorem. (SNo_abs_SNo)
∀x, SNo x → SNo (abs_SNo x)
In Proofgold the corresponding term root is 7266a7... and proposition id is 1c9c46...
Proof:
Let x be given.
Assume Hx.
Apply xm (0 ≤ x) to the current goal.
Assume H1.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
An exact proof term for the current goal is Hx.
Assume H1.
rewrite the current goal using not_nonneg_abs_SNo x H1 (from left to right).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
∎
Theorem. (abs_SNo_Lev)
∀x, SNo x → SNoLev (abs_SNo x) = SNoLev x
In Proofgold the corresponding term root is fe5907... and proposition id is 24d266...
Proof:
Let x be given.
Assume Hx.
Apply xm (0 ≤ x) to the current goal.
Assume H1.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
Use reflexivity.
Assume H1.
rewrite the current goal using not_nonneg_abs_SNo x H1 (from left to right).
Apply minus_SNo_Lev to the current goal.
An exact proof term for the current goal is Hx.
∎
Theorem. (abs_SNo_minus)
∀x, SNo x → abs_SNo (- x) = abs_SNo x
In Proofgold the corresponding term root is 977106... and proposition id is 2c0d4c...
Proof:
Let x be given.
Assume Hx.
Apply SNoLtLe_or x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using neg_abs_SNo x Hx H1 (from left to right).
We will prove abs_SNo (- x) = - x.
We prove the intermediate claim L1: 0 ≤ - x.
Apply SNoLtLe to the current goal.
We will prove 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1.
An exact proof term for the current goal is nonneg_abs_SNo (- x) L1.
Assume H1: 0 ≤ x.
Apply SNoLtLe_or (- x) 0 (SNo_minus_SNo x Hx) SNo_0 to the current goal.
Assume H2: - x < 0.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
rewrite the current goal using neg_abs_SNo (- x) (SNo_minus_SNo x Hx) H2 (from left to right).
We will prove - - x = x.
An exact proof term for the current goal is minus_SNo_invol x Hx.
Assume H2: 0 ≤ - x.
We prove the intermediate claim L2: x = 0.
Apply SNoLe_antisym x 0 Hx SNo_0 to the current goal.
We will prove x ≤ 0.
rewrite the current goal using minus_SNo_0 (from right to left).
rewrite the current goal using minus_SNo_invol x Hx (from right to left).
We will prove - - x ≤ - 0.
Apply minus_SNo_Le_contra 0 (- x) SNo_0 (SNo_minus_SNo x Hx) to the current goal.
We will prove 0 ≤ - x.
An exact proof term for the current goal is H2.
We will prove 0 ≤ x.
An exact proof term for the current goal is H1.
rewrite the current goal using L2 (from left to right).
Use f_equal.
An exact proof term for the current goal is minus_SNo_0.
∎
Theorem. (abs_SNo_dist_swap)
∀x y, SNo x → SNo y → abs_SNo (x + - y) = abs_SNo (y + - x)
In Proofgold the corresponding term root is 73d709... and proposition id is fd708c...
Proof:
Let x and y be given.
Assume Hx Hy.
We prove the intermediate claim Lmx: SNo (- x).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
We prove the intermediate claim Lmy: SNo (- y).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Lymx: SNo (y + - x).
An exact proof term for the current goal is SNo_add_SNo y (- x) Hy Lmx.
Use transitivity with and abs_SNo (- (y + - x)).
Use f_equal.
We will prove x + - y = - (y + - x).
rewrite the current goal using minus_add_SNo_distr y (- x) Hy Lmx (from left to right).
We will prove x + - y = - y + - - x.
rewrite the current goal using minus_SNo_invol x Hx (from left to right).
We will prove x + - y = - y + x.
An exact proof term for the current goal is add_SNo_com x (- y) Hx Lmy.
An exact proof term for the current goal is abs_SNo_minus (y + - x) Lymx.
∎
Theorem. (SNo_triangle)
∀x y, SNo x → SNo y → abs_SNo (x + y) ≤ abs_SNo x + abs_SNo y
In Proofgold the corresponding term root is f7ed3b... and proposition id is db0357...
Proof:
Let x and y be given.
Assume Hx Hy.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim Lmx: SNo (- x).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
We prove the intermediate claim Lmy: SNo (- y).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hy.
Apply SNoLtLe_or x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using neg_abs_SNo x Hx H1 (from left to right).
Apply SNoLtLe_or y 0 Hy SNo_0 to the current goal.
Assume H2: y < 0.
rewrite the current goal using neg_abs_SNo y Hy H2 (from left to right).
We will prove abs_SNo (x + y) ≤ - x + - y.
We prove the intermediate claim L1: x + y < 0.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).
We will prove x + y < 0 + 0.
An exact proof term for the current goal is add_SNo_Lt3 x y 0 0 Hx Hy SNo_0 SNo_0 H1 H2.
rewrite the current goal using neg_abs_SNo (x + y) Lxy L1 (from left to right).
We will prove - (x + y) ≤ - x + - y.
rewrite the current goal using minus_add_SNo_distr x y Hx Hy (from left to right).
Apply SNoLe_ref to the current goal.
Assume H2: 0 ≤ y.
rewrite the current goal using nonneg_abs_SNo y H2 (from left to right).
We will prove abs_SNo (x + y) ≤ - x + y.
Apply xm (0 ≤ x + y) to the current goal.
Assume H3.
rewrite the current goal using nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove x + y ≤ - x + y.
Apply add_SNo_Le1 x y (- x) Hx Hy Lmx to the current goal.
We will prove x ≤ - x.
Apply SNoLtLe to the current goal.
We will prove x < - x.
Apply SNoLt_tra x 0 (- x) Hx SNo_0 Lmx H1 to the current goal.
We will prove 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1.
Assume H3.
rewrite the current goal using not_nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove - (x + y) ≤ - x + y.
rewrite the current goal using minus_add_SNo_distr x y Hx Hy (from left to right).
We will prove - x + - y ≤ - x + y.
Apply add_SNo_Le2 (- x) (- y) y Lmx Lmy Hy to the current goal.
We will prove - y ≤ y.
We prove the intermediate claim L2: - y ≤ 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is minus_SNo_Le_contra 0 y SNo_0 Hy H2.
An exact proof term for the current goal is SNoLe_tra (- y) 0 y Lmy SNo_0 Hy L2 H2.
Assume H1: 0 ≤ x.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
Apply SNoLtLe_or y 0 Hy SNo_0 to the current goal.
Assume H2: y < 0.
rewrite the current goal using neg_abs_SNo y Hy H2 (from left to right).
We will prove abs_SNo (x + y) ≤ x + - y.
Apply xm (0 ≤ x + y) to the current goal.
Assume H3.
rewrite the current goal using nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove x + y ≤ x + - y.
Apply add_SNo_Le2 x y (- y) Hx Hy Lmy to the current goal.
We will prove y ≤ - y.
Apply SNoLtLe to the current goal.
We will prove y < - y.
Apply SNoLt_tra y 0 (- y) Hy SNo_0 Lmy H2 to the current goal.
We will prove 0 < - y.
Apply minus_SNo_Lt_contra2 y 0 Hy SNo_0 to the current goal.
We will prove y < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H2.
Assume H3.
rewrite the current goal using not_nonneg_abs_SNo (x + y) H3 (from left to right).
We will prove - (x + y) ≤ x + - y.
rewrite the current goal using minus_add_SNo_distr x y Hx Hy (from left to right).
We will prove - x + - y ≤ x + - y.
Apply add_SNo_Le1 (- x) (- y) x Lmx Lmy Hx to the current goal.
We will prove - x ≤ x.
We prove the intermediate claim L3: - x ≤ 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is minus_SNo_Le_contra 0 x SNo_0 Hx H1.
An exact proof term for the current goal is SNoLe_tra (- x) 0 x Lmx SNo_0 Hx L3 H1.
Assume H2: 0 ≤ y.
rewrite the current goal using nonneg_abs_SNo y H2 (from left to right).
We will prove abs_SNo (x + y) ≤ x + y.
We prove the intermediate claim L1: 0 ≤ x + y.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).
We will prove 0 + 0 ≤ x + y.
An exact proof term for the current goal is add_SNo_Le3 0 0 x y SNo_0 SNo_0 Hx Hy H1 H2.
rewrite the current goal using nonneg_abs_SNo (x + y) L1 (from left to right).
Apply SNoLe_ref to the current goal.
∎
Theorem. (SNo_triangle2)
∀x y z, SNo x → SNo y → SNo z → abs_SNo (x + - z) ≤ abs_SNo (x + - y) + abs_SNo (y + - z)
In Proofgold the corresponding term root is d54ddd... and proposition id is 8a76af...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
We prove the intermediate claim Lmy: SNo (- y).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Lmz: SNo (- z).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hz.
We prove the intermediate claim L1: x + - z = (x + - y) + (y + - z).
rewrite the current goal using add_SNo_assoc x (- y) (y + - z) Hx Lmy (SNo_add_SNo y (- z) Hy Lmz) (from right to left).
We will prove x + - z = x + (- y + y + - z).
Use f_equal.
Use symmetry.
An exact proof term for the current goal is add_SNo_minus_L2 y (- z) Hy Lmz.
rewrite the current goal using L1 (from left to right).
Apply SNo_triangle to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Lmy.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Lmz.
∎
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.
In Proofgold the corresponding term root is 9570d4... and object id is 0e9f0e...
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.
In Proofgold the corresponding term root is 5eb8d7... and object id is 144946...
Theorem. (minus_SNo_max_min)
∀X y, (∀x ∈ X, SNo x) → SNo_max_of X y → SNo_min_of {- x|x ∈ X} (- y)
In Proofgold the corresponding term root is 2403cf... and proposition id is f6c519...
Proof:
Let X and y be given.
Assume HX H1.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1a: y ∈ X.
Assume H1b: SNo y.
Assume H1c: ∀z ∈ X, SNo z → z ≤ y.
We will prove - y ∈ {- x|x ∈ X} ∧ SNo (- y) ∧ (∀z ∈ {- x|x ∈ X}, SNo z → - y ≤ z).
Apply and3I to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is H1a.
An exact proof term for the current goal is SNo_minus_SNo y H1b.
Let z be given.
Assume Hz1: z ∈ {- x|x ∈ X}.
Assume Hz2: SNo z.
Apply ReplE_impred X (λx ⇒ - x) z Hz1 to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hze: z = - x.
rewrite the current goal using Hze (from left to right).
We will prove - y ≤ - x.
Apply minus_SNo_Le_contra x y (HX x Hx) H1b to the current goal.
We will prove x ≤ y.
An exact proof term for the current goal is H1c x Hx (HX x Hx).
∎
Theorem. (minus_SNo_max_min')
∀X y, (∀x ∈ X, SNo x) → SNo_max_of {- x|x ∈ X} y → SNo_min_of X (- y)
In Proofgold the corresponding term root is 544581... and proposition id is b07737...
Proof:
Let X and y be given.
Assume HX H1.
We prove the intermediate claim L1: {- z|z ∈ {- x|x ∈ X}} = X.
Apply Repl_invol_eq SNo minus_SNo to the current goal.
We will prove ∀x, SNo x → - - x = x.
An exact proof term for the current goal is minus_SNo_invol.
We will prove ∀x ∈ X, SNo x.
An exact proof term for the current goal is HX.
We prove the intermediate claim L2: ∀z ∈ {- x|x ∈ X}, SNo z.
Let z be given.
Assume Hz.
Apply ReplE_impred X (λx ⇒ - x) z Hz to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hzx: z = - x.
rewrite the current goal using Hzx (from left to right).
Apply SNo_minus_SNo to the current goal.
We will prove SNo x.
An exact proof term for the current goal is HX x Hx.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is minus_SNo_max_min {- x|x ∈ X} y L2 H1.
∎
Theorem. (minus_SNo_min_max)
∀X y, (∀x ∈ X, SNo x) → SNo_min_of X y → SNo_max_of {- x|x ∈ X} (- y)
In Proofgold the corresponding term root is d435c2... and proposition id is fbf599...
Proof:
Let X and y be given.
Assume HX H1.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1a: y ∈ X.
Assume H1b: SNo y.
Assume H1c: ∀z ∈ X, SNo z → y ≤ z.
We will prove - y ∈ {- x|x ∈ X} ∧ SNo (- y) ∧ (∀z ∈ {- x|x ∈ X}, SNo z → z ≤ - y).
Apply and3I to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is H1a.
An exact proof term for the current goal is SNo_minus_SNo y H1b.
Let z be given.
Assume Hz1: z ∈ {- x|x ∈ X}.
Assume Hz2: SNo z.
Apply ReplE_impred X (λx ⇒ - x) z Hz1 to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hze: z = - x.
rewrite the current goal using Hze (from left to right).
We will prove - x ≤ - y.
Apply minus_SNo_Le_contra y x H1b (HX x Hx) to the current goal.
We will prove y ≤ x.
An exact proof term for the current goal is H1c x Hx (HX x Hx).
∎
Theorem. (double_SNo_max_1)
∀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
In Proofgold the corresponding term root is 3155e8... and proposition id is d66034...
Proof:
Let x and y be given.
Assume Hx Hy.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Assume Hy1: y ∈ SNoL x.
Assume Hy2: SNo y.
Assume Hy3: ∀w ∈ SNoL x, SNo w → w ≤ y.
Apply SNoL_E x Hx y Hy1 to the current goal.
Assume Hy1a.
Assume Hy1b: SNoLev y ∈ SNoLev x.
Assume Hy1c: y < x.
Apply SNoLev_ind to the current goal.
Let z be given.
Assume Hz: SNo z.
Assume IH: ∀w ∈ SNoS_ (SNoLev z), x < w → y + w < x + x → ∃u ∈ SNoR w, y + u = x + x.
Assume H1: x < z.
Assume H2: y + z < x + x.
We will prove ∃w ∈ SNoR z, y + w = x + x.
We prove the intermediate claim Lxx: SNo (x + x).
An exact proof term for the current goal is SNo_add_SNo x x Hx Hx.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy2 Hz.
We prove the intermediate claim L1: ∀w ∈ SNoR y, w + z ≤ x + x → False.
Let w be given.
Assume Hw.
Assume H3: w + z ≤ x + x.
Apply SNoR_E y Hy2 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: y < w.
Apply SNoLt_irref (x + x) to the current goal.
We will prove x + x < x + x.
Apply SNoLtLe_tra (x + x) (w + z) (x + x) Lxx (SNo_add_SNo w z Hw1 Hz) Lxx to the current goal.
We will prove x + x < w + z.
Apply add_SNo_Lt3b x x w z Hx Hx Hw1 Hz to the current goal.
We will prove x ≤ w.
Apply SNoLtLe_or w x Hw1 Hx to the current goal.
Assume H4: w < x.
We prove the intermediate claim L1a: w ∈ SNoL x.
Apply SNoL_I x Hx w Hw1 to the current goal.
We will prove SNoLev w ∈ SNoLev x.
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) (SNoLev y) Hy1b (SNoLev w) Hw2.
We will prove w < x.
An exact proof term for the current goal is H4.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
Apply SNoLtLe_tra y w y Hy2 Hw1 Hy2 Hw3 to the current goal.
We will prove w ≤ y.
An exact proof term for the current goal is Hy3 w L1a Hw1.
Assume H4: x ≤ w.
An exact proof term for the current goal is H4.
We will prove x < z.
An exact proof term for the current goal is H1.
We will prove w + z ≤ x + x.
An exact proof term for the current goal is H3.
We prove the intermediate claim L2: ∀w ∈ SNoL x, y + z ≤ w + x → False.
Let w be given.
Assume Hw.
Assume H3: y + z ≤ w + x.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: w < x.
Apply SNoLt_irref (w + x) to the current goal.
We will prove w + x < w + x.
Apply SNoLtLe_tra (w + x) (w + z) (w + x) (SNo_add_SNo w x Hw1 Hx) (SNo_add_SNo w z Hw1 Hz) (SNo_add_SNo w x Hw1 Hx) to the current goal.
We will prove w + x < w + z.
Apply add_SNo_Lt2 w x z Hw1 Hx Hz to the current goal.
We will prove x < z.
An exact proof term for the current goal is H1.
We will prove w + z ≤ w + x.
Apply SNoLe_tra (w + z) (y + z) (w + x) (SNo_add_SNo w z Hw1 Hz) Lyz (SNo_add_SNo w x Hw1 Hx) to the current goal.
We will prove w + z ≤ y + z.
Apply add_SNo_Le1 w z y Hw1 Hz Hy2 to the current goal.
We will prove w ≤ y.
An exact proof term for the current goal is Hy3 w Hw Hw1.
We will prove y + z ≤ w + x.
An exact proof term for the current goal is H3.
We prove the intermediate claim L3: ∀w ∈ SNoR z, y + w < x + x → ∃w ∈ SNoR z, y + w = x + x.
Let w be given.
Assume Hw: w ∈ SNoR z.
Assume H4: y + w < x + x.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2.
Assume Hw3: z < w.
We prove the intermediate claim LIH: ∃u ∈ SNoR w, y + u = x + x.
Apply IH w (SNoR_SNoS_ z w Hw) to the current goal.
We will prove x < w.
An exact proof term for the current goal is SNoLt_tra x z w Hx Hz Hw1 H1 Hw3.
We will prove y + w < x + x.
An exact proof term for the current goal is H4.
Apply LIH to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu1: u ∈ SNoR w.
Assume Hu2: y + u = x + x.
Apply SNoR_E w Hw1 u Hu1 to the current goal.
Assume Hu1a Hu1b Hu1c.
We use u to witness the existential quantifier.
Apply andI to the current goal.
We will prove u ∈ SNoR z.
Apply SNoR_I z Hz u Hu1a to the current goal.
We will prove SNoLev u ∈ SNoLev z.
An exact proof term for the current goal is ordinal_TransSet (SNoLev z) (SNoLev_ordinal z Hz) (SNoLev w) Hw2 (SNoLev u) Hu1b.
We will prove z < u.
An exact proof term for the current goal is SNoLt_tra z w u Hz Hw1 Hu1a Hw3 Hu1c.
An exact proof term for the current goal is Hu2.
Apply SNoLt_SNoL_or_SNoR_impred (y + z) (x + x) Lyz Lxx H2 to the current goal.
Let u be given.
Assume Hu1: u ∈ SNoL (x + x).
Assume Hu2: u ∈ SNoR (y + z).
Apply SNoL_E (x + x) Lxx u Hu1 to the current goal.
Assume Hu1a: SNo u.
Assume Hu1b.
Assume Hu1c: u < x + x.
Apply add_SNo_SNoR_interpolate y z Hy2 Hz u Hu2 to the current goal.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR y.
Assume H4: w + z ≤ u.
Apply SNoR_E y Hy2 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2.
Assume Hw3: y < w.
We will prove False.
Apply L1 w Hw to the current goal.
We will prove w + z ≤ x + x.
Apply SNoLtLe to the current goal.
We will prove w + z < x + x.
Apply SNoLeLt_tra (w + z) u (x + x) (SNo_add_SNo w z Hw1 Hz) Hu1a Lxx H4 to the current goal.
We will prove u < x + x.
An exact proof term for the current goal is Hu1c.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR z.
Assume H4: y + w ≤ u.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2.
Assume Hw3: z < w.
Apply L3 w Hw to the current goal.
We will prove y + w < x + x.
Apply SNoLeLt_tra (y + w) u (x + x) (SNo_add_SNo y w Hy2 Hw1) Hu1a Lxx H4 to the current goal.
We will prove u < x + x.
An exact proof term for the current goal is Hu1c.
Assume H3: y + z ∈ SNoL (x + x).
We will prove False.
Apply add_SNo_SNoL_interpolate x x Hx Hx (y + z) H3 to the current goal.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoL x.
Assume H4: y + z ≤ w + x.
An exact proof term for the current goal is L2 w Hw H4.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoL x.
Assume H4: y + z ≤ x + w.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply L2 w Hw to the current goal.
We will prove y + z ≤ w + x.
rewrite the current goal using add_SNo_com w x Hw1 Hx (from left to right).
We will prove y + z ≤ x + w.
An exact proof term for the current goal is H4.
Assume H3: x + x ∈ SNoR (y + z).
Apply add_SNo_SNoR_interpolate y z Hy2 Hz (x + x) H3 to the current goal.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR y.
Assume H4: w + z ≤ x + x.
We will prove False.
An exact proof term for the current goal is L1 w Hw H4.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR z.
Assume H4: y + w ≤ x + x.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev z.
Assume Hw3: z < w.
Apply SNoLtLe_or (y + w) (x + x) (SNo_add_SNo y w Hy2 Hw1) Lxx to the current goal.
Assume H5: y + w < x + x.
We will prove ∃w ∈ SNoR z, y + w = x + x.
Apply L3 w Hw to the current goal.
We will prove y + w < x + x.
An exact proof term for the current goal is H5.
Assume H5: x + x ≤ y + w.
We will prove ∃w ∈ SNoR z, y + w = x + x.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw.
Apply SNoLe_antisym (y + w) (x + x) (SNo_add_SNo y w Hy2 Hw1) Lxx to the current goal.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
∎
Theorem. (double_SNo_min_1)
∀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
In Proofgold the corresponding term root is fa7d8b... and proposition id is 084f04...
Proof:
Let x and y be given.
Assume Hx Hy.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Assume Hy1: y ∈ SNoR x.
Assume Hy2: SNo y.
Assume Hy3: ∀w ∈ SNoR x, SNo w → y ≤ w.
Apply SNoR_E x Hx y Hy1 to the current goal.
Assume Hy1a.
Assume Hy1b: SNoLev y ∈ SNoLev x.
Assume Hy1c: x < y.
Let z be given.
Assume Hz: SNo z.
Assume H1: z < x.
Assume H2: x + x < y + z.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate claim Lmy: SNo (- y).
An exact proof term for the current goal is SNo_minus_SNo y Hy2.
We prove the intermediate claim Lmz: SNo (- z).
An exact proof term for the current goal is SNo_minus_SNo z Hz.
We prove the intermediate claim Lxx: SNo (x + x).
An exact proof term for the current goal is SNo_add_SNo x x Hx Hx.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy2 Hz.
We prove the intermediate claim L1: SNo_max_of (SNoL (- x)) (- y).
rewrite the current goal using SNoL_minus_SNoR x Hx (from left to right).
We will prove SNo_max_of {- w|w ∈ SNoR x} (- y).
Apply minus_SNo_min_max to the current goal.
We will prove ∀w ∈ SNoR x, SNo w.
Let w be given.
Assume Hw.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 _ _.
An exact proof term for the current goal is Hw1.
We will prove SNo_min_of (SNoR x) y.
An exact proof term for the current goal is Hy.
We prove the intermediate claim L2: - x < - z.
An exact proof term for the current goal is minus_SNo_Lt_contra z x Hz Hx H1.
We prove the intermediate claim L3: - y + - z < - x + - x.
rewrite the current goal using minus_add_SNo_distr y z Hy2 Hz (from right to left).
rewrite the current goal using minus_add_SNo_distr x x Hx Hx (from right to left).
An exact proof term for the current goal is minus_SNo_Lt_contra (x + x) (y + z) Lxx Lyz H2.
Apply double_SNo_max_1 (- x) (- y) Lmx L1 (- z) Lmz L2 L3 to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR (- z).
rewrite the current goal using minus_add_SNo_distr x x Hx Hx (from right to left).
Assume H3: - y + w = - (x + x).
Apply SNoR_E (- z) Lmz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev (- z).
Assume Hw3: - z < w.
We prove the intermediate claim Lmw: SNo (- w).
An exact proof term for the current goal is SNo_minus_SNo w Hw1.
We use (- w) to witness the existential quantifier.
Apply andI to the current goal.
We will prove - w ∈ SNoL z.
rewrite the current goal using minus_SNo_invol z Hz (from right to left).
We will prove - w ∈ SNoL (- - z).
rewrite the current goal using SNoL_minus_SNoR (- z) Lmz (from left to right).
We will prove - w ∈ {- w|w ∈ SNoR (- z)}.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hw.
We will prove y + - w = x + x.
rewrite the current goal using minus_SNo_invol (x + x) Lxx (from right to left).
We will prove y + - w = - - (x + x).
rewrite the current goal using H3 (from right to left).
We will prove y + - w = - (- y + w).
rewrite the current goal using minus_add_SNo_distr (- y) w Lmy Hw1 (from left to right).
We will prove y + - w = - - y + - w.
rewrite the current goal using minus_SNo_invol y Hy2 (from left to right).
Use reflexivity.
∎
Theorem. (finite_max_exists)
∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_max_of X x
In Proofgold the corresponding term root is 182021... and proposition id is 9baa0b...
Proof:
We prove the intermediate claim L1: ∀n, nat_p n → ∀X, (∀x ∈ X, SNo x) → equip X (ordsucc n) → ∃x, SNo_max_of X x.
Apply nat_ind to the current goal.
Let X be given.
Assume HX.
Assume H1: equip X 1.
Apply equip_sym X 1 H1 to the current goal.
Let f be given.
Assume Hf: bij 1 X f.
Apply bijE 1 X f Hf to the current goal.
Assume Hf1 Hf2 Hf3.
We use f 0 to witness the existential quantifier.
We will prove SNo_max_of X (f 0).
We will prove f 0 ∈ X ∧ SNo (f 0) ∧ ∀y ∈ X, SNo y → y ≤ f 0.
We prove the intermediate claim Lf0X: f 0 ∈ X.
An exact proof term for the current goal is Hf1 0 In_0_1.
Apply and3I to the current goal.
We will prove f 0 ∈ X.
An exact proof term for the current goal is Lf0X.
An exact proof term for the current goal is HX (f 0) Lf0X.
Let y be given.
Assume Hy: y ∈ X.
Assume Hy2: SNo y.
Apply Hf3 y Hy to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ 1.
Assume Hyi: f i = y.
We will prove y ≤ f 0.
rewrite the current goal using Hyi (from right to left).
Apply cases_1 i Hi to the current goal.
We will prove f 0 ≤ f 0.
Apply SNoLe_ref to the current goal.
Let n be given.
Assume Hn.
Assume IHn: ∀X, (∀x ∈ X, SNo x) → equip X (ordsucc n) → ∃x, SNo_max_of X x.
Let X be given.
Assume HX.
Assume H1: equip X (ordsucc (ordsucc n)).
Apply equip_sym X (ordsucc (ordsucc n)) H1 to the current goal.
Let f be given.
Assume Hf: bij (ordsucc (ordsucc n)) X f.
Apply bijE (ordsucc (ordsucc n)) X f Hf to the current goal.
Assume Hf1 Hf2 Hf3.
Set X' to be the term {f i|i ∈ ordsucc n}.
We prove the intermediate claim LX'1: X' ⊆ X.
Let w be given.
Assume Hw: w ∈ X'.
Apply ReplE_impred (ordsucc n) f w Hw to the current goal.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Assume Hwi: w = f i.
rewrite the current goal using Hwi (from left to right).
We will prove f i ∈ X.
Apply Hf1 i to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We prove the intermediate claim LX'2: equip X' (ordsucc n).
Apply equip_sym to the current goal.
We will prove ∃f : set → set, bij (ordsucc n) X' f.
We use f to witness the existential quantifier.
Apply bijI to the current goal.
Let i be given.
Assume Hi: i ∈ ordsucc n.
We will prove f i ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hi.
Let i be given.
Assume Hi.
Let j be given.
Assume Hj.
Assume Hij: f i = f j.
Apply Hf2 to the current goal.
We will prove i ∈ ordsucc (ordsucc n).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We will prove j ∈ ordsucc (ordsucc n).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hj.
An exact proof term for the current goal is Hij.
Let w be given.
Assume Hw: w ∈ X'.
Apply ReplE_impred (ordsucc n) f w Hw to the current goal.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Assume Hwi: w = f i.
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi.
Use symmetry.
An exact proof term for the current goal is Hwi.
Apply IHn X' (λx' Hx' ⇒ HX x' (LX'1 x' Hx')) LX'2 to the current goal.
Let z be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hz1: z ∈ X'.
Assume Hz2: SNo z.
Assume Hz3: ∀y ∈ X', SNo y → y ≤ z.
We prove the intermediate claim Lfn1: f (ordsucc n) ∈ X.
Apply Hf1 (ordsucc n) to the current goal.
Apply ordsuccI2 to the current goal.
We prove the intermediate claim Lfn1': SNo (f (ordsucc n)).
Apply HX (f (ordsucc n)) Lfn1 to the current goal.
Apply SNoLtLe_or z (f (ordsucc n)) Hz2 Lfn1' to the current goal.
Assume H2: z < f (ordsucc n).
We use (f (ordsucc n)) to witness the existential quantifier.
We will prove f (ordsucc n) ∈ X ∧ SNo (f (ordsucc n)) ∧ ∀y ∈ X, SNo y → y ≤ f (ordsucc n).
Apply and3I to the current goal.
An exact proof term for the current goal is Lfn1.
An exact proof term for the current goal is Lfn1'.
Let y be given.
Assume Hy Hy2.
Apply Hf3 y Hy to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ ordsucc (ordsucc n).
Assume Hyi: f i = y.
Apply ordsuccE (ordsucc n) i Hi to the current goal.
Assume H3: i ∈ ordsucc n.
We will prove y ≤ f (ordsucc n).
Apply SNoLe_tra y z (f (ordsucc n)) Hy2 Hz2 Lfn1' to the current goal.
We will prove y ≤ z.
Apply Hz3 y to the current goal.
We will prove y ∈ X'.
rewrite the current goal using Hyi (from right to left).
We will prove f i ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is Hy2.
We will prove z ≤ f (ordsucc n).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H2.
Assume H3: i = ordsucc n.
rewrite the current goal using Hyi (from right to left).
rewrite the current goal using H3 (from left to right).
We will prove f (ordsucc n) ≤ f (ordsucc n).
Apply SNoLe_ref to the current goal.
Assume H2: f (ordsucc n) ≤ z.
We use z to witness the existential quantifier.
We will prove z ∈ X ∧ SNo z ∧ ∀y ∈ X, SNo y → y ≤ z.
Apply and3I to the current goal.
An exact proof term for the current goal is LX'1 z Hz1.
An exact proof term for the current goal is Hz2.
Let y be given.
Assume Hy Hy2.
Apply Hf3 y Hy to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ ordsucc (ordsucc n).
Assume Hyi: f i = y.
Apply ordsuccE (ordsucc n) i Hi to the current goal.
Assume H3: i ∈ ordsucc n.
We will prove y ≤ z.
Apply Hz3 y to the current goal.
We will prove y ∈ X'.
rewrite the current goal using Hyi (from right to left).
We will prove f i ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is Hy2.
Assume H3: i = ordsucc n.
rewrite the current goal using Hyi (from right to left).
rewrite the current goal using H3 (from left to right).
We will prove f (ordsucc n) ≤ z.
An exact proof term for the current goal is H2.
Let X be given.
Assume HX.
Assume H1: finite X.
Apply H1 to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω.
Apply nat_inv n (omega_nat_p n Hn) to the current goal.
Assume Hn0: n = 0.
rewrite the current goal using Hn0 (from left to right).
Assume H2: equip X 0.
Assume H3: X ≠ 0.
We will prove False.
Apply H2 to the current goal.
Let f be given.
Assume Hf: bij X 0 f.
Apply bijE X 0 f Hf to the current goal.
Assume Hf1 _ _.
Apply H3 to the current goal.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx.
Apply EmptyE (f x) to the current goal.
An exact proof term for the current goal is Hf1 x Hx.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: nat_p m.
Assume Hnm: n = ordsucc m.
rewrite the current goal using Hnm (from left to right).
Assume H2: equip X (ordsucc m).
Assume _.
An exact proof term for the current goal is L1 m Hm X HX H2.
∎
Theorem. (finite_min_exists)
∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_min_of X x
In Proofgold the corresponding term root is efc9f1... and proposition id is 25808a...
Proof:
Let X be given.
Assume HX: ∀x ∈ X, SNo x.
Assume H1: finite X.
Assume H2: X ≠ 0.
Set X' to be the term {- x|x ∈ X}.
We prove the intermediate claim L1: ∀z ∈ X', SNo z.
Let z be given.
Assume Hz.
Apply ReplE_impred X (λx ⇒ - x) z Hz to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hzx: z = - x.
rewrite the current goal using Hzx (from left to right).
Apply SNo_minus_SNo to the current goal.
We will prove SNo x.
An exact proof term for the current goal is HX x Hx.
We prove the intermediate claim L2: finite X'.
Apply H1 to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω.
Assume H3: equip X n.
We will prove ∃n ∈ ω, equip X' n.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
We will prove equip X' n.
Apply equip_tra X' X n to the current goal.
We will prove equip X' X.
Apply equip_sym to the current goal.
We will prove equip X X'.
We will prove ∃f : set → set, bij X X' f.
We use minus_SNo to witness the existential quantifier.
Apply bijI to the current goal.
Let x be given.
Assume Hx: x ∈ X.
We will prove - x ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
Assume Hxx': - x = - x'.
We will prove x = x'.
Use transitivity with - - x, and - - x'.
Use symmetry.
An exact proof term for the current goal is minus_SNo_invol x (HX x Hx).
Use f_equal.
An exact proof term for the current goal is Hxx'.
An exact proof term for the current goal is minus_SNo_invol x' (HX x' Hx').
Let w be given.
Assume Hw: w ∈ X'.
Apply ReplE_impred X (λx ⇒ - x) w Hw to the current goal.
Let x be given.
Assume Hx.
Assume Hwx: w = - x.
We will prove ∃u ∈ X, - u = w.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx.
Use symmetry.
An exact proof term for the current goal is Hwx.
We will prove equip X n.
An exact proof term for the current goal is H3.
We prove the intermediate claim L3: X' ≠ 0.
Assume H1: X' = 0.
Apply H2 to the current goal.
We will prove X = 0.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Apply EmptyE (- x) to the current goal.
We will prove - x ∈ 0.
rewrite the current goal using H1 (from right to left).
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx.
Apply finite_max_exists X' L1 L2 L3 to the current goal.
Let y be given.
Assume Hy: SNo_max_of X' y.
We use (- y) to witness the existential quantifier.
We will prove SNo_min_of X (- y).
An exact proof term for the current goal is minus_SNo_max_min' X y HX Hy.
∎
Theorem. (SNoS_omega_SNoL_max_exists)
∀x ∈ SNoS_ ω, SNoL x = 0 ∨ ∃y, SNo_max_of (SNoL x) y
In Proofgold the corresponding term root is 4539ed... and proposition id is faaae1...
Proof:
Let x be given.
Assume Hx.
Apply xm (SNoL x = 0) to the current goal.
Assume H1: SNoL x = 0.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
Assume H1: SNoL x ≠ 0.
Apply orIR to the current goal.
We prove the intermediate claim L1: ∀y ∈ SNoL x, SNo y.
Let y be given.
Assume Hy.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume _ _ Hx3 _.
Apply SNoL_E x Hx3 y Hy to the current goal.
Assume H _ _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is finite_max_exists (SNoL x) L1 (SNoS_omega_SNoL_finite x Hx) H1.
∎
Theorem. (SNoS_omega_SNoR_min_exists)
∀x ∈ SNoS_ ω, SNoR x = 0 ∨ ∃y, SNo_min_of (SNoR x) y
In Proofgold the corresponding term root is b0aa0c... and proposition id is baaae8...
Proof:
Let x be given.
Assume Hx.
Apply xm (SNoR x = 0) to the current goal.
Assume H1: SNoR x = 0.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
Assume H1: SNoR x ≠ 0.
Apply orIR to the current goal.
We prove the intermediate claim L1: ∀y ∈ SNoR x, SNo y.
Let y be given.
Assume Hy.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume _ _ Hx3 _.
Apply SNoR_E x Hx3 y Hy to the current goal.
Assume H _ _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is finite_min_exists (SNoR x) L1 (SNoS_omega_SNoR_finite x Hx) H1.
∎
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.
Theorem. (nonneg_diadic_rational_p_SNoS_omega)
∀k ∈ ω, ∀n, nat_p n → eps_ k * n ∈ SNoS_ ω
In Proofgold the corresponding term root is 9323b5... and proposition id is d9b318...
Proof:
Let k be given.
Assume Hk.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
We prove the intermediate claim Lek2: eps_ k ∈ SNoS_ ω.
An exact proof term for the current goal is SNo_eps_SNoS_omega k Hk.
Apply nat_ind to the current goal.
We will prove eps_ k * 0 ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_zeroR (eps_ k) Lek (from left to right).
We will prove 0 ∈ SNoS_ ω.
An exact proof term for the current goal is omega_SNoS_omega 0 (nat_p_omega 0 nat_0).
Let n be given.
Assume Hn.
Assume IHn: eps_ k * n ∈ SNoS_ ω.
We will prove eps_ k * ordsucc n ∈ SNoS_ ω.
rewrite the current goal using add_SNo_1_ordsucc n (nat_p_omega n Hn) (from right to left).
We will prove eps_ k * (n + 1) ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_distrL (eps_ k) n 1 Lek (omega_SNo n (nat_p_omega n Hn)) (omega_SNo 1 (nat_p_omega 1 nat_1)) (from left to right).
We will prove eps_ k * n + eps_ k * 1 ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_oneR (eps_ k) Lek (from left to right).
We will prove eps_ k * n + eps_ k ∈ SNoS_ ω.
Apply add_SNo_SNoS_omega to the current goal.
An exact proof term for the current goal is IHn.
An exact proof term for the current goal is SNo_eps_SNoS_omega k Hk.
∎
Definition. We define diadic_rational_p to be λx ⇒ ∃k ∈ ω, ∃m ∈ int, x = eps_ k * m of type set → prop.
In Proofgold the corresponding term root is a02ca9... and object id is 25bca1...
Theorem. (diadic_rational_p_SNoS_omega)
∀x, diadic_rational_p x → x ∈ SNoS_ ω
In Proofgold the corresponding term root is b7e7af... and proposition id is 3dea67...
Proof:
Let x be given.
Assume H.
Apply H to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hxkm: x = eps_ k * m.
rewrite the current goal using Hxkm (from left to right).
We will prove eps_ k * m ∈ SNoS_ ω.
We prove the intermediate claim L1: ∀n ∈ ω, eps_ k * n ∈ SNoS_ ω.
Let n be given.
Assume Hn: n ∈ ω.
We will prove eps_ k * n ∈ SNoS_ ω.
An exact proof term for the current goal is nonneg_diadic_rational_p_SNoS_omega k Hk n (omega_nat_p n Hn).
We prove the intermediate claim L2: ∀n ∈ ω, eps_ k * (- n) ∈ SNoS_ ω.
Let n be given.
Assume Hn: n ∈ ω.
We will prove eps_ k * (- n) ∈ SNoS_ ω.
rewrite the current goal using mul_SNo_minus_distrR (eps_ k) n (SNo_eps_ k Hk) (omega_SNo n Hn) (from left to right).
Apply minus_SNo_SNoS_omega to the current goal.
An exact proof term for the current goal is nonneg_diadic_rational_p_SNoS_omega k Hk n (omega_nat_p n Hn).
An exact proof term for the current goal is int_SNo_cases (λm ⇒ eps_ k * m ∈ SNoS_ ω) L1 L2 m Hm.
∎
Theorem. (int_diadic_rational_p)
∀m ∈ int, diadic_rational_p m
In Proofgold the corresponding term root is 88ce9c... and proposition id is 8a4cf7...
Proof:
Let m be given.
Assume Hm.
We will prove ∃k ∈ ω, ∃m' ∈ int, m = eps_ k * m'.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is nat_p_omega 0 nat_0.
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm.
We will prove m = eps_ 0 * m.
rewrite the current goal using eps_0_1 (from left to right).
Use symmetry.
An exact proof term for the current goal is mul_SNo_oneL m (int_SNo m Hm).
∎
Theorem. (omega_diadic_rational_p)
∀m ∈ ω, diadic_rational_p m
In Proofgold the corresponding term root is 40b048... and proposition id is c250b0...
Proof:
Let m be given.
Assume Hm.
Apply int_diadic_rational_p to the current goal.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is Hm.
∎
Theorem. (eps_diadic_rational_p)
∀k ∈ ω, diadic_rational_p (eps_ k)
In Proofgold the corresponding term root is d306dc... and proposition id is cc1098...
Proof:
Let k be given.
Assume Hk.
We will prove ∃k' ∈ ω, ∃m ∈ int, eps_ k = eps_ k' * m.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is nat_p_omega 1 nat_1.
We will prove eps_ k = eps_ k * 1.
Use symmetry.
An exact proof term for the current goal is mul_SNo_oneR (eps_ k) (SNo_eps_ k Hk).
∎
Theorem. (minus_SNo_diadic_rational_p)
∀x, diadic_rational_p x → diadic_rational_p (- x)
In Proofgold the corresponding term root is bb6f7d... and proposition id is bc4825...
Proof:
Let x be given.
Assume H.
Apply H to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hxkm: x = eps_ k * m.
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim Lekm: SNo (eps_ k * m).
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) m Lek Lm.
We will prove ∃k' ∈ ω, ∃m' ∈ int, - x = eps_ k' * m'.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
We use (- m) to witness the existential quantifier.
Apply andI to the current goal.
Apply int_minus_SNo to the current goal.
An exact proof term for the current goal is Hm.
We will prove - x = eps_ k * (- m).
rewrite the current goal using mul_SNo_minus_distrR (eps_ k) m (SNo_eps_ k Hk) Lm (from left to right).
We will prove - x = - eps_ k * m.
Use f_equal.
An exact proof term for the current goal is Hxkm.
∎
Theorem. (mul_SNo_diadic_rational_p)
∀x y, diadic_rational_p x → diadic_rational_p y → diadic_rational_p (x * y)
In Proofgold the corresponding term root is ed6a37... and proposition id is e4ff6e...
Proof:
Let x and y be given.
Assume Hx.
Apply Hx to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hxkm: x = eps_ k * m.
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim Lekm: SNo (eps_ k * m).
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) m Lek Lm.
Assume Hy.
Apply Hy to the current goal.
Let l be given.
Assume H.
Apply H to the current goal.
Assume Hl: l ∈ ω.
We prove the intermediate claim Lel: SNo (eps_ l).
An exact proof term for the current goal is SNo_eps_ l Hl.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ int.
We prove the intermediate claim Ln: SNo n.
An exact proof term for the current goal is int_SNo n Hn.
We prove the intermediate claim Leln: SNo (eps_ l * n).
An exact proof term for the current goal is SNo_mul_SNo (eps_ l) n Lel Ln.
Assume Hyln: y = eps_ l * n.
We will prove ∃k' ∈ ω, ∃m' ∈ int, x * y = eps_ k' * m'.
We use (k + l) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is add_SNo_In_omega k Hk l Hl.
We use (m * n) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is int_mul_SNo m Hm n Hn.
We will prove x * y = eps_ (k + l) * (m * n).
rewrite the current goal using mul_SNo_eps_eps_add_SNo k Hk l Hl (from right to left).
We will prove x * y = (eps_ k * eps_ l) * (m * n).
rewrite the current goal using mul_SNo_com_4_inner_mid (eps_ k) (eps_ l) m n Lek Lel Lm Ln (from left to right).
We will prove x * y = (eps_ k * m) * (eps_ l * n).
Use f_equal.
An exact proof term for the current goal is Hxkm.
An exact proof term for the current goal is Hyln.
∎
Theorem. (add_SNo_diadic_rational_p)
∀x y, diadic_rational_p x → diadic_rational_p y → diadic_rational_p (x + y)
In Proofgold the corresponding term root is bd7ab2... and proposition id is 4e6254...
Proof:
Let x and y be given.
Assume Hx.
Apply Hx to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hxkm: x = eps_ k * m.
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim Lekm: SNo (eps_ k * m).
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) m Lek Lm.
Assume Hy.
Apply Hy to the current goal.
Let l be given.
Assume H.
Apply H to the current goal.
Assume Hl: l ∈ ω.
We prove the intermediate claim Lel: SNo (eps_ l).
An exact proof term for the current goal is SNo_eps_ l Hl.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ int.
Assume Hyln: y = eps_ l * n.
We prove the intermediate claim Ln: SNo n.
An exact proof term for the current goal is int_SNo n Hn.
We prove the intermediate claim Leln: SNo (eps_ l * n).
An exact proof term for the current goal is SNo_mul_SNo (eps_ l) n Lel Ln.
We will prove ∃k' ∈ ω, ∃m' ∈ int, x + y = eps_ k' * m'.
We use (k + l) to witness the existential quantifier.
Apply andI to the current goal.
We will prove k + l ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k Hk l Hl.
We use (2 ^ l * m + 2 ^ k * n) to witness the existential quantifier.
We prove the intermediate claim L2l: 2 ^ l ∈ int.
Apply Subq_omega_int to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 l (omega_nat_p l Hl).
We prove the intermediate claim L2lm: 2 ^ l * m ∈ int.
Apply int_mul_SNo to the current goal.
An exact proof term for the current goal is L2l.
An exact proof term for the current goal is Hm.
We prove the intermediate claim L2k: 2 ^ k ∈ int.
Apply Subq_omega_int to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 k (omega_nat_p k Hk).
We prove the intermediate claim L2kn: 2 ^ k * n ∈ int.
Apply int_mul_SNo to the current goal.
An exact proof term for the current goal is L2k.
An exact proof term for the current goal is Hn.
Apply andI to the current goal.
We will prove 2 ^ l * m + 2 ^ k * n ∈ int.
Apply int_add_SNo to the current goal.
An exact proof term for the current goal is L2lm.
An exact proof term for the current goal is L2kn.
We will prove x + y = eps_ (k + l) * (2 ^ l * m + 2 ^ k * n).
rewrite the current goal using mul_SNo_eps_eps_add_SNo k Hk l Hl (from right to left).
We will prove x + y = (eps_ k * eps_ l) * (2 ^ l * m + 2 ^ k * n).
rewrite the current goal using mul_SNo_distrL (eps_ k * eps_ l) (2 ^ l * m) (2 ^ k * n) (SNo_mul_SNo (eps_ k) (eps_ l) Lek Lel) (int_SNo (2 ^ l * m) L2lm) (int_SNo (2 ^ k * n) L2kn) (from left to right).
We will prove x + y = (eps_ k * eps_ l) * 2 ^ l * m + (eps_ k * eps_ l) * 2 ^ k * n.
Use f_equal.
We will prove x = (eps_ k * eps_ l) * 2 ^ l * m.
rewrite the current goal using mul_SNo_assoc (eps_ k) (eps_ l) (2 ^ l * m) Lek Lel (int_SNo (2 ^ l * m) L2lm) (from right to left).
We will prove x = eps_ k * eps_ l * 2 ^ l * m.
rewrite the current goal using mul_SNo_assoc (eps_ l) (2 ^ l) m Lel (int_SNo (2 ^ l) L2l) (int_SNo m Hm) (from left to right).
We will prove x = eps_ k * (eps_ l * 2 ^ l) * m.
rewrite the current goal using mul_SNo_eps_power_2 l (omega_nat_p l Hl) (from left to right).
We will prove x = eps_ k * 1 * m.
rewrite the current goal using mul_SNo_oneL m (int_SNo m Hm) (from left to right).
We will prove x = eps_ k * m.
An exact proof term for the current goal is Hxkm.
We will prove y = (eps_ k * eps_ l) * (2 ^ k * n).
rewrite the current goal using mul_SNo_com_4_inner_mid (eps_ k) (eps_ l) (2 ^ k) n Lek Lel (int_SNo (2 ^ k) L2k) (int_SNo n Hn) (from left to right).
We will prove y = (eps_ k * 2 ^ k) * (eps_ l * n).
rewrite the current goal using mul_SNo_eps_power_2 k (omega_nat_p k Hk) (from left to right).
We will prove y = 1 * (eps_ l * n).
rewrite the current goal using mul_SNo_oneL (eps_ l * n) Leln (from left to right).
An exact proof term for the current goal is Hyln.
∎
Theorem. (SNoS_omega_diadic_rational_p_lem)
∀n, nat_p n → ∀x, SNo x → SNoLev x = n → diadic_rational_p x
In Proofgold the corresponding term root is 85a5ea... and proposition id is bf97d9...
Proof:
Apply nat_complete_ind to the current goal.
Let n be given.
Assume Hn.
Assume IH: ∀m ∈ n, ∀x, SNo x → SNoLev x = m → diadic_rational_p x.
Let x be given.
Assume Hx: SNo x.
Assume Hxn: SNoLev x = n.
We will prove diadic_rational_p x.
Apply dneg to the current goal.
Assume HC: ¬ diadic_rational_p x.
We will prove False.
We prove the intermediate claim LxSo: x ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal x (SNoLev x) to the current goal.
We will prove SNoLev x ∈ ω.
rewrite the current goal using Hxn (from left to right).
An exact proof term for the current goal is nat_p_omega n Hn.
We will prove SNo_ (SNoLev x) x.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hx.
We prove the intermediate claim L1: ∃y, SNo_max_of (SNoL x) y.
Apply SNoS_omega_SNoL_max_exists x LxSo to the current goal.
Assume H1: SNoL x = 0.
We prove the intermediate claim L1a: ordinal (- x).
Apply SNo_max_ordinal (- x) (SNo_minus_SNo x Hx) to the current goal.
Let w be given.
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
Assume Hw: w ∈ SNoS_ (SNoLev x).
We will prove w < - x.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) w Hw to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
Apply SNoLt_trichotomy_or_impred w (- x) ?? (SNo_minus_SNo x Hx) to the current goal.
Assume H2: w < - x.
An exact proof term for the current goal is H2.
Assume H2: w = - x.
We will prove False.
Apply In_irref (SNoLev w) to the current goal.
rewrite the current goal using H2 (from left to right) at position 2.
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is ??.
Assume H2: - x < w.
We will prove False.
Apply EmptyE (- w) to the current goal.
We will prove - w ∈ 0.
rewrite the current goal using H1 (from right to left).
We will prove - w ∈ SNoL x.
Apply SNoL_I x Hx (- w) (SNo_minus_SNo w ??) to the current goal.
We will prove SNoLev (- w) ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev w ?? (from left to right).
An exact proof term for the current goal is ??.
We will prove - w < x.
An exact proof term for the current goal is minus_SNo_Lt_contra1 x w Hx ?? ??.
We prove the intermediate claim L1b: - x = n.
rewrite the current goal using Hxn (from right to left).
We will prove - x = SNoLev x.
Use symmetry.
rewrite the current goal using minus_SNo_Lev x ?? (from right to left).
An exact proof term for the current goal is ordinal_SNoLev (- x) L1a.
We will prove False.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using minus_SNo_invol x ?? (from right to left).
We will prove diadic_rational_p (- - x).
Apply minus_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (- x).
rewrite the current goal using L1b (from left to right).
We will prove diadic_rational_p n.
Apply omega_diadic_rational_p to the current goal.
An exact proof term for the current goal is nat_p_omega n Hn.
Assume H1.
An exact proof term for the current goal is H1.
We prove the intermediate claim L2: ∃z, SNo_min_of (SNoR x) z.
Apply SNoS_omega_SNoR_min_exists x LxSo to the current goal.
Assume H1: SNoR x = 0.
We prove the intermediate claim L2a: ordinal x.
Apply SNo_max_ordinal x Hx to the current goal.
Let w be given.
Assume Hw: w ∈ SNoS_ (SNoLev x).
We will prove w < x.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x ??) w Hw to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
Apply SNoLt_trichotomy_or_impred w x ?? ?? to the current goal.
Assume H2: w < x.
An exact proof term for the current goal is H2.
Assume H2: w = x.
We will prove False.
Apply In_irref (SNoLev x) to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is ??.
Assume H2: x < w.
We will prove False.
Apply EmptyE w to the current goal.
We will prove w ∈ 0.
rewrite the current goal using H1 (from right to left).
We will prove w ∈ SNoR x.
Apply SNoR_I x ?? w ?? ?? ?? to the current goal.
We prove the intermediate claim L2b: x = n.
rewrite the current goal using Hxn (from right to left).
We will prove x = SNoLev x.
Use symmetry.
An exact proof term for the current goal is ordinal_SNoLev x L2a.
We will prove False.
Apply HC to the current goal.
We will prove diadic_rational_p x.
Apply omega_diadic_rational_p to the current goal.
We will prove x ∈ ω.
rewrite the current goal using L2b (from left to right).
An exact proof term for the current goal is nat_p_omega n Hn.
Assume H1.
An exact proof term for the current goal is H1.
Apply L1 to the current goal.
Let y be given.
Assume Hy: SNo_max_of (SNoL x) y.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Assume Hy1: y ∈ SNoL x.
Assume Hy2: SNo y.
Assume Hy3: ∀w ∈ SNoL x, SNo w → w ≤ y.
Apply SNoL_E x Hx y Hy1 to the current goal.
Assume _ Hy1b Hy1c.
Apply L2 to the current goal.
Let z be given.
Assume Hz: SNo_min_of (SNoR x) z.
Apply Hz to the current goal.
Assume H.
Apply H to the current goal.
Assume Hz1: z ∈ SNoR x.
Assume Hz2: SNo z.
Assume Hz3: ∀w ∈ SNoR x, SNo w → z ≤ w.
Apply SNoR_E x Hx z Hz1 to the current goal.
Assume _ Hz1b Hz1c.
We prove the intermediate claim Lxx: SNo (x + x).
An exact proof term for the current goal is SNo_add_SNo x x Hx Hx.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy2 Hz2.
We prove the intermediate claim Ldry: diadic_rational_p y.
Apply IH (SNoLev y) to the current goal.
We will prove SNoLev y ∈ n.
rewrite the current goal using Hxn (from right to left).
We will prove SNoLev y ∈ SNoLev x.
An exact proof term for the current goal is Hy1b.
We will prove SNo y.
An exact proof term for the current goal is Hy2.
We will prove SNoLev y = SNoLev y.
Use reflexivity.
We prove the intermediate claim Ldrz: diadic_rational_p z.
Apply IH (SNoLev z) to the current goal.
We will prove SNoLev z ∈ n.
rewrite the current goal using Hxn (from right to left).
We will prove SNoLev z ∈ SNoLev x.
An exact proof term for the current goal is Hz1b.
We will prove SNo z.
An exact proof term for the current goal is Hz2.
We will prove SNoLev z = SNoLev z.
Use reflexivity.
Apply SNoLt_trichotomy_or_impred (x + x) (y + z) Lxx Lyz to the current goal.
rewrite the current goal using add_SNo_com y z Hy2 Hz2 (from left to right).
Assume H1: x + x < z + y.
Apply double_SNo_min_1 x z Hx Hz y Hy2 Hy1c H1 to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoL y.
Assume H2: z + w = x + x.
Apply SNoL_E y Hy2 w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Ldrw: diadic_rational_p w.
Apply IH (SNoLev w) to the current goal.
We will prove SNoLev w ∈ n.
Apply ordinal_TransSet n (nat_p_ordinal n Hn) (SNoLev y) to the current goal.
We will prove SNoLev y ∈ n.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hy1b.
We will prove SNoLev w ∈ SNoLev y.
An exact proof term for the current goal is Hw2.
We will prove SNo w.
An exact proof term for the current goal is Hw1.
We will prove SNoLev w = SNoLev w.
Use reflexivity.
We prove the intermediate claim Lxe: x = eps_ 1 * (z + w).
Apply double_eps_1 x z w Hx Hz2 Hw1 to the current goal.
Use symmetry.
An exact proof term for the current goal is H2.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using Lxe (from left to right).
Apply mul_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (eps_ 1).
An exact proof term for the current goal is eps_diadic_rational_p 1 (nat_p_omega 1 nat_1).
We will prove diadic_rational_p (z + w).
Apply add_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p z.
An exact proof term for the current goal is Ldrz.
We will prove diadic_rational_p w.
An exact proof term for the current goal is Ldrw.
Assume H1: x + x = y + z.
We prove the intermediate claim Lxe: x = eps_ 1 * (y + z).
An exact proof term for the current goal is double_eps_1 x y z Hx Hy2 Hz2 H1.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using Lxe (from left to right).
Apply mul_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (eps_ 1).
An exact proof term for the current goal is eps_diadic_rational_p 1 (nat_p_omega 1 nat_1).
We will prove diadic_rational_p (y + z).
Apply add_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p y.
An exact proof term for the current goal is Ldry.
We will prove diadic_rational_p z.
An exact proof term for the current goal is Ldrz.
Assume H1: y + z < x + x.
Apply double_SNo_max_1 x y Hx Hy z Hz2 Hz1c H1 to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR z.
Assume H2: y + w = x + x.
Apply SNoR_E z Hz2 w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Ldrw: diadic_rational_p w.
Apply IH (SNoLev w) to the current goal.
We will prove SNoLev w ∈ n.
Apply ordinal_TransSet n (nat_p_ordinal n Hn) (SNoLev z) to the current goal.
We will prove SNoLev z ∈ n.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hz1b.
We will prove SNoLev w ∈ SNoLev z.
An exact proof term for the current goal is Hw2.
We will prove SNo w.
An exact proof term for the current goal is Hw1.
We will prove SNoLev w = SNoLev w.
Use reflexivity.
We prove the intermediate claim Lxe: x = eps_ 1 * (y + w).
Apply double_eps_1 x y w Hx Hy2 Hw1 to the current goal.
Use symmetry.
An exact proof term for the current goal is H2.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using Lxe (from left to right).
Apply mul_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (eps_ 1).
An exact proof term for the current goal is eps_diadic_rational_p 1 (nat_p_omega 1 nat_1).
We will prove diadic_rational_p (y + w).
Apply add_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p y.
An exact proof term for the current goal is Ldry.
We will prove diadic_rational_p w.
An exact proof term for the current goal is Ldrw.
∎
Theorem. (SNoS_omega_diadic_rational_p)
∀x ∈ SNoS_ ω, diadic_rational_p x
In Proofgold the corresponding term root is a9c764... and proposition id is 963bd5...
Proof:
Let x be given.
Assume Hx: x ∈ SNoS_ ω.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume Hx1: SNoLev x ∈ ω.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
Apply SNoS_omega_diadic_rational_p_lem (SNoLev x) to the current goal.
We will prove nat_p (SNoLev x).
An exact proof term for the current goal is omega_nat_p (SNoLev x) Hx1.
We will prove SNo x.
An exact proof term for the current goal is Hx3.
We will prove SNoLev x = SNoLev x.
Use reflexivity.
∎
Theorem. (mul_SNo_SNoS_omega)
∀x y ∈ SNoS_ ω, x * y ∈ SNoS_ ω
In Proofgold the corresponding term root is d17aa1... and proposition id is 768371...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Apply diadic_rational_p_SNoS_omega to the current goal.
Apply mul_SNo_diadic_rational_p to the current goal.
Apply SNoS_omega_diadic_rational_p to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoS_omega_diadic_rational_p to the current goal.
An exact proof term for the current goal is Hy.
∎
End of Section DiadicRationals