Beginning of Section SurrealSqrt
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Notation. We use < as an infix operator with priority 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.
(*** $I sig/Part1.mgs ***)
(*** $I sig/Part2.mgs ***)
(*** $I sig/Part3.mgs ***)
(*** $I sig/Part4.mgs ***)
(*** $I sig/Part5.mgs ***)
(*** $I sig/Part6.mgs ***)
(*** $I sig/Part7.mgs ***)
(*** $I sig/Part8.mgs ***)
(*** Part 9 ***)
L21
Definition. We define SNoL_nonneg to be λx ⇒ {w ∈ SNoL x|0 ≤ w} of type set → set.
In Proofgold the corresponding term root is 426e35... and object id is 1ec1d7...
L23
Theorem. (SNoL_nonneg_0)
SNoL_nonneg 0 = 0
In Proofgold the corresponding term root is ab6dce... and proposition id is 67aa58...
Proof:
Proof not loaded.
L29
Theorem. (SNoL_nonneg_1)
SNoL_nonneg 1 = 1
In Proofgold the corresponding term root is 74d4e8... and proposition id is e3fc28...
Proof:
Proof not loaded.
L43
Definition. We define SNo_sqrtauxset to be λY Z x ⇒ ⋃y ∈ Y{(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z} of type set → set → set → set.
In Proofgold the corresponding term root is 211c64... and object id is 3fc62b...
L45
Theorem. (SNo_sqrtauxset_I)
∀Y Z x, ∀y ∈ Y, ∀z ∈ Z, 0 < y + z → (x + y * z) :/: (y + z) ∈ SNo_sqrtauxset Y Z x
In Proofgold the corresponding term root is 4b16a1... and proposition id is c09ca4...
Proof:
Proof not loaded.
L55
Theorem. (SNo_sqrtauxset_E)
∀Y Z x, ∀u ∈ SNo_sqrtauxset Y Z x, ∀p : prop, (∀y ∈ Y, ∀z ∈ Z, 0 < y + z → u = (x + y * z) :/: (y + z) → p) → p
In Proofgold the corresponding term root is 0bec9e... and proposition id is b7810c...
Proof:
Proof not loaded.
L69
Theorem. (SNo_sqrtauxset_0)
∀Z x, SNo_sqrtauxset 0 Z x = 0
In Proofgold the corresponding term root is 2d39ce... and proposition id is db93fb...
Proof:
Proof not loaded.
L77
Theorem. (SNo_sqrtauxset_0')
∀Y x, SNo_sqrtauxset Y 0 x = 0
In Proofgold the corresponding term root is b0f585... and proposition id is d57918...
Proof:
Proof not loaded.
L86
Definition. We define SNo_sqrtaux to be λx g ⇒ nat_primrec ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x}) (λk p ⇒ (p 0 ∪ SNo_sqrtauxset (p 0) (p 1) x,p 1 ∪ SNo_sqrtauxset (p 0) (p 0) x ∪ SNo_sqrtauxset (p 1) (p 1) x)) of type set → (set → set) → set → set.
In Proofgold the corresponding term root is e233df... and object id is 2ebc89...
L93
Theorem. (SNo_sqrtaux_0)
∀x, ∀g : set → set, SNo_sqrtaux x g 0 = ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x})
In Proofgold the corresponding term root is d46ed0... and proposition id is 182e5e...
Proof:
Proof not loaded.
L101
Theorem. (SNo_sqrtaux_S)
∀x, ∀g : set → set, ∀n, nat_p n → SNo_sqrtaux x g (ordsucc n) = (SNo_sqrtaux x g n 0 ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 1) x,SNo_sqrtaux x g n 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 1) (SNo_sqrtaux x g n 1) x)
In Proofgold the corresponding term root is bb0dd8... and proposition id is 7223d6...
Proof:
Proof not loaded.
L115
Theorem. (SNo_sqrtaux_mon_lem)
∀x, ∀g : set → set, ∀m, nat_p m → ∀n, nat_p n → SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (add_nat m n) 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (add_nat m n) 1
In Proofgold the corresponding term root is be3c0c... and proposition id is 75cbc1...
Proof:
Proof not loaded.
L157
Theorem. (SNo_sqrtaux_mon)
∀x, ∀g : set → set, ∀m, nat_p m → ∀n, nat_p n → m ⊆ n → SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g n 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g n 1
In Proofgold the corresponding term root is 53a992... and proposition id is f80eb0...
Proof:
Proof not loaded.
L171
Theorem. (SNo_sqrtaux_ext)
∀x, SNo x → ∀g h : set → set, (∀x' ∈ SNoS_ (SNoLev x), g x' = h x') → ∀k, nat_p k → SNo_sqrtaux x g k = SNo_sqrtaux x h k
In Proofgold the corresponding term root is 9e623f... and proposition id is 88e0ac...
Proof:
Proof not loaded.
Beginning of Section sqrt_SNo_nonneg
L212
Let G : set → (set → set) → set ≝ λx g ⇒ SNoCut (⋃k ∈ ωSNo_sqrtaux x g k 0) (⋃k ∈ ωSNo_sqrtaux x g k 1)
L214
Definition. We define sqrt_SNo_nonneg to be SNo_rec_i G of type set → set.
In Proofgold the corresponding term root is 71d152... and object id is 20211a...
L216
Theorem. (sqrt_SNo_nonneg_eq)
∀x, SNo x → sqrt_SNo_nonneg x = G x sqrt_SNo_nonneg
In Proofgold the corresponding term root is 63c3e8... and proposition id is edc75b...
Proof:
Proof not loaded.
L241
Theorem. (sqrt_SNo_nonneg_prop1a)
∀x, SNo x → 0 ≤ x → (∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w) → ∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)
In Proofgold the corresponding term root is 111bf5... and proposition id is 44bfa1...
Proof:
Proof not loaded.
L679
Theorem. (sqrt_SNo_nonneg_prop1b)
∀x, SNo x → 0 ≤ x → (∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)) → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1)
In Proofgold the corresponding term root is 79d32b... and proposition id is 3a96af...
Proof:
Proof not loaded.
L748
Theorem. (sqrt_SNo_nonneg_prop1c)
∀x, SNo x → 0 ≤ x → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1) → (∀z ∈ (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1), ∀p : prop, (SNo z → 0 ≤ z → x < z * z → p) → p) → 0 ≤ G x sqrt_SNo_nonneg
In Proofgold the corresponding term root is afcc07... and proposition id is abe562...
Proof:
Proof not loaded.
L784
Theorem. (sqrt_SNo_nonneg_prop1d)
∀x, SNo x → 0 ≤ x → (∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w) → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1) → 0 ≤ G x sqrt_SNo_nonneg → G x sqrt_SNo_nonneg * G x sqrt_SNo_nonneg < x → False
In Proofgold the corresponding term root is 9308b8... and proposition id is 9979dd...
Proof:
Proof not loaded.
L1067
Theorem. (sqrt_SNo_nonneg_prop1e)
∀x, SNo x → 0 ≤ x → (∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w) → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1) → 0 ≤ G x sqrt_SNo_nonneg → x < G x sqrt_SNo_nonneg * G x sqrt_SNo_nonneg → False
In Proofgold the corresponding term root is bd498d... and proposition id is c07c4e...
Proof:
Proof not loaded.
L1451
Theorem. (sqrt_SNo_nonneg_prop1)
∀x, SNo x → 0 ≤ x → SNo (sqrt_SNo_nonneg x) ∧ 0 ≤ sqrt_SNo_nonneg x ∧ sqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x
In Proofgold the corresponding term root is db6879... and proposition id is b09b96...
Proof:
Proof not loaded.
End of Section sqrt_SNo_nonneg
L1534
Theorem. (SNo_sqrtaux_0_1_prop)
∀x, SNo x → 0 ≤ x → ∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)
In Proofgold the corresponding term root is 955f65... and proposition id is a2bb45...
Proof:
Proof not loaded.
L1545
Theorem. (SNo_sqrtaux_0_prop)
∀x, SNo x → 0 ≤ x → ∀k, nat_p k → ∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x
In Proofgold the corresponding term root is abda0d... and proposition id is 8db9d4...
Proof:
Proof not loaded.
L1554
Theorem. (SNo_sqrtaux_1_prop)
∀x, SNo x → 0 ≤ x → ∀k, nat_p k → ∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y
In Proofgold the corresponding term root is d59bfa... and proposition id is 95a41e...
Proof:
Proof not loaded.
L1563
Theorem. (SNo_sqrt_SNo_SNoCutP)
∀x, SNo x → 0 ≤ x → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1)
In Proofgold the corresponding term root is 33c123... and proposition id is d04ad9...
Proof:
Proof not loaded.
L1571
Theorem. (SNo_sqrt_SNo_nonneg)
∀x, SNo x → 0 ≤ x → SNo (sqrt_SNo_nonneg x)
In Proofgold the corresponding term root is 016da2... and proposition id is c5c4da...
Proof:
Proof not loaded.
L1577
Theorem. (sqrt_SNo_nonneg_nonneg)
∀x, SNo x → 0 ≤ x → 0 ≤ sqrt_SNo_nonneg x
In Proofgold the corresponding term root is 40638f... and proposition id is 6c1cd0...
Proof:
Proof not loaded.
L1583
Theorem. (sqrt_SNo_nonneg_sqr)
∀x, SNo x → 0 ≤ x → sqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x
In Proofgold the corresponding term root is c79d06... and proposition id is 15814c...
Proof:
Proof not loaded.
L1589
Theorem. (sqrt_SNo_nonneg_0)
sqrt_SNo_nonneg 0 = 0
In Proofgold the corresponding term root is 0afb2a... and proposition id is c6b1a7...
Proof:
Proof not loaded.
L1669
Theorem. (sqrt_SNo_nonneg_1)
sqrt_SNo_nonneg 1 = 1
In Proofgold the corresponding term root is 1801e5... and proposition id is d5a6d5...
Proof:
Proof not loaded.
End of Section SurrealSqrt