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.
(*** $I sig/Part1.mgs ***)
(*** $I sig/Part2.mgs ***)
(*** $I sig/Part3.mgs ***)
(*** $I sig/Part4.mgs ***)
(*** $I sig/Part5.mgs ***)
(*** $I sig/Part6.mgs ***)
(*** Part 7 ***)
L13
Definition. We define int to be ω ∪ {- n|n ∈ ω} of type set.
In Proofgold the corresponding term root is 90ee85... and object id is 331669...
L15
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:
Proof not loaded.
L29
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:
Proof not loaded.
L58
Theorem. (int_SNo)
∀x ∈ int, SNo x
In Proofgold the corresponding term root is 19fdd2... and proposition id is 6089ec...
Proof:
Proof not loaded.
L66
Theorem. (Subq_omega_int)
ω ⊆ int
In Proofgold the corresponding term root is 405dda... and proposition id is b1bb2b...
Proof:
Proof not loaded.
L73
Theorem. (int_minus_SNo_omega)
∀n ∈ ω, - n ∈ int
In Proofgold the corresponding term root is 869503... and proposition id is 3a2593...
Proof:
Proof not loaded.
L81
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:
Proof not loaded.
L137
Theorem. (int_add_SNo)
∀x y ∈ int, x + y ∈ int
In Proofgold the corresponding term root is d66975... and proposition id is 1036d9...
Proof:
Proof not loaded.
L166
Theorem. (int_minus_SNo)
∀x ∈ int, - x ∈ int
In Proofgold the corresponding term root is 00e714... and proposition id is b2c591...
Proof:
Proof not loaded.
L175
Theorem. (int_mul_SNo)
∀x y ∈ int, x * y ∈ int
In Proofgold the corresponding term root is a7bc92... and proposition id is f40564...
Proof:
Proof not loaded.
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.
L254
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...
L255
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:
Proof not loaded.
L260
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:
Proof not loaded.
L265
Theorem. (abs_SNo_0)
abs_SNo 0 = 0
In Proofgold the corresponding term root is c0c559... and proposition id is 35a655...
Proof:
Proof not loaded.
L269
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:
Proof not loaded.
L275
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:
Proof not loaded.
L285
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:
Proof not loaded.
L293
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:
Proof not loaded.
L301
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:
Proof not loaded.
L333
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:
Proof not loaded.
L351
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:
Proof not loaded.
L436
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:
Proof not loaded.
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.
L470
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...
L472
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...
L473
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:
Proof not loaded.
L494
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:
Proof not loaded.
L513
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:
Proof not loaded.
L534
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:
Proof not loaded.
L726
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:
Proof not loaded.
L796
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:
Proof not loaded.
L942
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:
Proof not loaded.
L1010
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:
Proof not loaded.
L1025
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:
Proof not loaded.
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.
L1053
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:
Proof not loaded.
L1077
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...
L1079
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:
Proof not loaded.
L1104
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:
Proof not loaded.
L1115
Theorem. (omega_diadic_rational_p)
∀m ∈ ω, diadic_rational_p m
In Proofgold the corresponding term root is 40b048... and proposition id is c250b0...
Proof:
Proof not loaded.
L1120
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:
Proof not loaded.
L1132
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:
Proof not loaded.
L1158
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:
Proof not loaded.
L1200
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:
Proof not loaded.
L1278
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:
Proof not loaded.
L1483
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:
Proof not loaded.
L1496
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:
Proof not loaded.
End of Section DiadicRationals