Beginning of Section Reals
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 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.
Theorem. (SNoS_omega_drat_intvl)
∀x ∈ SNoS_ ω, ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k
In Proofgold the corresponding term root is d24dbb... and proposition id is eb9878...
Proof:
Proof not loaded.
Theorem. (SNoS_ordsucc_omega_bdd_above)
∀x ∈ SNoS_ (ordsucc ω), x < ω → ∃N ∈ ω, x < N
In Proofgold the corresponding term root is c51d13... and proposition id is 7fd9f0...
Proof:
Proof not loaded.
Theorem. (SNoS_ordsucc_omega_bdd_below)
∀x ∈ SNoS_ (ordsucc ω), - ω < x → ∃N ∈ ω, - N < x
In Proofgold the corresponding term root is d7d14e... and proposition id is 09271c...
Proof:
Proof not loaded.
Theorem. (SNoS_ordsucc_omega_bdd_drat_intvl)
∀x ∈ SNoS_ (ordsucc ω), - ω < x → x < ω → ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k
In Proofgold the corresponding term root is 57512e... and proposition id is 0ae7ab...
Proof:
Proof not loaded.
Definition. We define real to be {x ∈ SNoS_ (ordsucc ω)|x ≠ ω ∧ x ≠ - ω ∧ (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x)} of type set.
In Proofgold the corresponding term root is e26ffa... and object id is 5277ef...
Definition. We define rational to be {x ∈ real|∃m ∈ int, ∃n ∈ ω ∖ {0}, x = m :/: n} of type set.
In Proofgold the corresponding term root is efaf16... and object id is 6ea078...
Theorem. (real_I)
∀x ∈ SNoS_ (ordsucc ω), x ≠ ω → x ≠ - ω → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → x ∈ real
In Proofgold the corresponding term root is b05b9f... and proposition id is 9f45f4...
Proof:
Proof not loaded.
Theorem. (real_E)
∀x ∈ real, ∀p : prop, (SNo x → SNoLev x ∈ ordsucc ω → x ∈ SNoS_ (ordsucc ω) → - ω < x → x < ω → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → p) → p
In Proofgold the corresponding term root is ac0c5d... and proposition id is 447bb9...
Proof:
Proof not loaded.
Theorem. (real_SNo)
∀x ∈ real, SNo x
In Proofgold the corresponding term root is 17c3d6... and proposition id is d4cbb8...
Proof:
Proof not loaded.
Theorem. (real_SNoS_omega_prop)
∀x ∈ real, ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x
In Proofgold the corresponding term root is 6da66c... and proposition id is cb7f5e...
Proof:
Proof not loaded.
Theorem. (SNoS_omega_real)
SNoS_ ω ⊆ real
In Proofgold the corresponding term root is a469c6... and proposition id is d9411b...
Proof:
Proof not loaded.
Theorem. (real_0)
0 ∈ real
In Proofgold the corresponding term root is 53bbc2... and proposition id is 493130...
Proof:
Proof not loaded.
Theorem. (real_1)
1 ∈ real
In Proofgold the corresponding term root is bbf720... and proposition id is 790b4d...
Proof:
Proof not loaded.
Theorem. (SNoLev_In_real_SNoS_omega)
∀x ∈ real, ∀w, SNo w → SNoLev w ∈ SNoLev x → w ∈ SNoS_ ω
In Proofgold the corresponding term root is defc4e... and proposition id is 30df9a...
Proof:
Proof not loaded.
Theorem. (real_SNoCut_SNoS_omega)
∀L R ⊆ SNoS_ ω, SNoCutP L R → L ≠ 0 → R ≠ 0 → (∀w ∈ L, ∃w' ∈ L, w < w') → (∀z ∈ R, ∃z' ∈ R, z' < z) → SNoCut L R ∈ real
In Proofgold the corresponding term root is 9f1398... and proposition id is 49872c...
Proof:
Proof not loaded.
Theorem. (real_SNoCut)
∀L R ⊆ real, SNoCutP L R → L ≠ 0 → R ≠ 0 → (∀w ∈ L, ∃w' ∈ L, w < w') → (∀z ∈ R, ∃z' ∈ R, z' < z) → SNoCut L R ∈ real
In Proofgold the corresponding term root is 6c4b7d... and proposition id is 463b8d...
Proof:
Proof not loaded.
Theorem. (minus_SNo_prereal_1)
∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - - x) < eps_ k) → q = - x)
In Proofgold the corresponding term root is 824b89... and proposition id is 1d4018...
Proof:
Proof not loaded.
Theorem. (minus_SNo_prereal_2)
∀x, SNo x → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < - x ∧ - x < q + eps_ k)
In Proofgold the corresponding term root is 68fe96... and proposition id is 8ce93f...
Proof:
Proof not loaded.
Theorem. (SNo_prereal_incr_lower_pos)
∀x, SNo x → 0 < x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∀k ∈ ω, ∀p : prop, (∀q ∈ SNoS_ ω, 0 < q → q < x → x < q + eps_ k → p) → p
In Proofgold the corresponding term root is 96a462... and proposition id is 947a7e...
Proof:
Proof not loaded.
Theorem. (real_minus_SNo)
∀x ∈ real, - x ∈ real
In Proofgold the corresponding term root is e8e8be... and proposition id is 4b8379...
Proof:
Proof not loaded.
Theorem. (SNo_prereal_incr_lower_approx)
∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∃f ∈ SNoS_ ωω, ∀n ∈ ω, f n < x ∧ x < f n + eps_ n ∧ ∀i ∈ n, f i < f n
In Proofgold the corresponding term root is 29e857... and proposition id is 85c0ef...
Proof:
Proof not loaded.
Theorem. (SNo_prereal_decr_upper_approx)
∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∃g ∈ SNoS_ ωω, ∀n ∈ ω, g n + - eps_ n < x ∧ x < g n ∧ ∀i ∈ n, g n < g i
In Proofgold the corresponding term root is e28afc... and proposition id is 07ed25...
Proof:
Proof not loaded.
Theorem. (SNoCutP_SNoCut_lim)
∀lambda, ordinal lambda → (∀alpha ∈ lambda, ordsucc alpha ∈ lambda) → ∀L R ⊆ SNoS_ lambda, SNoCutP L R → SNoLev (SNoCut L R) ∈ ordsucc lambda
In Proofgold the corresponding term root is 1a37c9... and proposition id is f1520f...
Proof:
Proof not loaded.
Theorem. (SNoCutP_SNoCut_omega)
∀L R ⊆ SNoS_ ω, SNoCutP L R → SNoLev (SNoCut L R) ∈ ordsucc ω
In Proofgold the corresponding term root is d11617... and proposition id is a23f8a...
Proof:
Proof not loaded.
Theorem. (SNo_approx_real_lem)
∀f g ∈ SNoS_ ωω, (∀n m ∈ ω, f n < g m) → ∀p : prop, (SNoCutP {f n|n ∈ ω} {g n|n ∈ ω} → SNo (SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) → SNoLev (SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) ∈ ordsucc ω → SNoCut {f n|n ∈ ω} {g n|n ∈ ω} ∈ SNoS_ (ordsucc ω) → (∀n ∈ ω, f n < SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) → (∀n ∈ ω, SNoCut {f n|n ∈ ω} {g n|n ∈ ω} < g n) → p) → p
In Proofgold the corresponding term root is d275e7... and proposition id is 3ca0b1...
Proof:
Proof not loaded.
Theorem. (SNo_approx_real)
∀x, SNo x → ∀f g ∈ SNoS_ ωω, (∀n ∈ ω, f n < x) → (∀n ∈ ω, x < f n + eps_ n) → (∀n ∈ ω, ∀i ∈ n, f i < f n) → (∀n ∈ ω, x < g n) → (∀n ∈ ω, ∀i ∈ n, g n < g i) → x = SNoCut {f n|n ∈ ω} {g n|n ∈ ω} → x ∈ real
In Proofgold the corresponding term root is 8b24c5... and proposition id is fca80e...
Proof:
Proof not loaded.
Theorem. (SNo_approx_real_rep)
∀x ∈ real, ∀p : prop, (∀f g ∈ SNoS_ ωω, (∀n ∈ ω, f n < x) → (∀n ∈ ω, x < f n + eps_ n) → (∀n ∈ ω, ∀i ∈ n, f i < f n) → (∀n ∈ ω, g n + - eps_ n < x) → (∀n ∈ ω, x < g n) → (∀n ∈ ω, ∀i ∈ n, g n < g i) → SNoCutP {f n|n ∈ ω} {g n|n ∈ ω} → x = SNoCut {f n|n ∈ ω} {g n|n ∈ ω} → p) → p
In Proofgold the corresponding term root is 91befd... and proposition id is a38d26...
Proof:
Proof not loaded.
Theorem. (real_add_SNo)
∀x y ∈ real, x + y ∈ real
In Proofgold the corresponding term root is 695361... and proposition id is 3c841f...
Proof:
Proof not loaded.
Theorem. (SNoS_ordsucc_omega_bdd_eps_pos)
∀x ∈ SNoS_ (ordsucc ω), 0 < x → x < ω → ∃N ∈ ω, eps_ N * x < 1
In Proofgold the corresponding term root is 064957... and proposition id is 9096d4...
Proof:
Proof not loaded.
Theorem. (real_mul_SNo_pos)
∀x y ∈ real, 0 < x → 0 < y → x * y ∈ real
In Proofgold the corresponding term root is dfe1b6... and proposition id is 8ba463...
Proof:
Proof not loaded.
Theorem. (real_mul_SNo)
∀x y ∈ real, x * y ∈ real
In Proofgold the corresponding term root is b48f84... and proposition id is 51dc42...
Proof:
Proof not loaded.
Theorem. (abs_SNo_intvl_bd)
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y < x + z → abs_SNo (y + - x) < z
In Proofgold the corresponding term root is c5bd1c... and proposition id is 31a8bf...
Proof:
Proof not loaded.
Theorem. (nonneg_real_nat_interval)
∀x ∈ real, 0 ≤ x → ∃n ∈ ω, n ≤ x ∧ x < ordsucc n
In Proofgold the corresponding term root is 00f333... and proposition id is a6e1f8...
Proof:
Proof not loaded.
Theorem. (pos_real_left_approx_double)
∀x ∈ real, 0 < x → x ≠ 2 → (∀m ∈ ω, x ≠ eps_ m) → ∃w ∈ SNoL_pos x, x < 2 * w
In Proofgold the corresponding term root is 721fe7... and proposition id is b80017...
Proof:
Proof not loaded.
Theorem. (real_recip_SNo_lem1)
∀x, SNo x → x ∈ real → 0 < x → recip_SNo_pos x ∈ real ∧ ∀k, nat_p k → (SNo_recipaux x recip_SNo_pos k 0 ⊆ real) ∧ (SNo_recipaux x recip_SNo_pos k 1 ⊆ real)
In Proofgold the corresponding term root is 129489... and proposition id is cfc2ec...
Proof:
Proof not loaded.
Theorem. (real_recip_SNo_pos)
∀x ∈ real, 0 < x → recip_SNo_pos x ∈ real
In Proofgold the corresponding term root is 8169ab... and proposition id is 406f08...
Proof:
Proof not loaded.
Theorem. (real_recip_SNo)
∀x ∈ real, recip_SNo x ∈ real
In Proofgold the corresponding term root is 336956... and proposition id is 64deb9...
Proof:
Proof not loaded.
Theorem. (real_div_SNo)
∀x y ∈ real, x :/: y ∈ real
In Proofgold the corresponding term root is 1b354d... and proposition id is 4ff694...
Proof:
Proof not loaded.
Theorem. (sqrt_SNo_nonneg_0inL0)
∀x, SNo x → 0 ≤ x → 0 ∈ SNoLev x → 0 ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 0
In Proofgold the corresponding term root is afb66e... and proposition id is 6bcc63...
Proof:
Proof not loaded.
Theorem. (sqrt_SNo_nonneg_Lnonempty)
∀x, SNo x → 0 ≤ x → 0 ∈ SNoLev x → (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) ≠ 0
In Proofgold the corresponding term root is 1725fa... and proposition id is c1c8c8...
Proof:
Proof not loaded.
Theorem. (sqrt_SNo_nonneg_Rnonempty)
∀x, SNo x → 0 ≤ x → 1 ∈ SNoLev x → (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1) ≠ 0
In Proofgold the corresponding term root is b397c9... and proposition id is 04384e...
Proof:
Proof not loaded.
Theorem. (SNo_sqrtauxset_real)
∀Y Z x, Y ⊆ real → Z ⊆ real → x ∈ real → SNo_sqrtauxset Y Z x ⊆ real
In Proofgold the corresponding term root is 5d5b3c... and proposition id is d040c4...
Proof:
Proof not loaded.
Theorem. (SNo_sqrtauxset_real_nonneg)
∀Y Z x, Y ⊆ {w ∈ real|0 ≤ w} → Z ⊆ {z ∈ real|0 ≤ z} → x ∈ real → 0 ≤ x → SNo_sqrtauxset Y Z x ⊆ {w ∈ real|0 ≤ w}
In Proofgold the corresponding term root is 1c421c... and proposition id is 3226b5...
Proof:
Proof not loaded.
Theorem. (sqrt_SNo_nonneg_SNoS_omega)
∀x ∈ SNoS_ ω, 0 ≤ x → sqrt_SNo_nonneg x ∈ real
In Proofgold the corresponding term root is 6aa091... and proposition id is 85b0b0...
Proof:
Proof not loaded.
Theorem. (sqrt_SNo_nonneg_real)
∀x ∈ real, 0 ≤ x → sqrt_SNo_nonneg x ∈ real
In Proofgold the corresponding term root is 17e0d9... and proposition id is 511860...
Proof:
Proof not loaded.
Theorem. (real_Archimedean)
∀x y ∈ real, 0 < x → 0 ≤ y → ∃n ∈ ω, y ≤ n * x
In Proofgold the corresponding term root is 0b7299... and proposition id is dc4568...
Proof:
Proof not loaded.
Theorem. (real_complete1)
∀a b ∈ realω, (∀n ∈ ω, a n ≤ b n ∧ a n ≤ a (ordsucc n) ∧ b (ordsucc n) ≤ b n) → ∃x ∈ real, ∀n ∈ ω, a n ≤ x ∧ x ≤ b n
In Proofgold the corresponding term root is 05d96d... and proposition id is 96392e...
Proof:
Proof not loaded.
Theorem. (real_complete2)
∀a b ∈ realω, (∀n ∈ ω, a n ≤ b n ∧ a n ≤ a (n + 1) ∧ b (n + 1) ≤ b n) → ∃x ∈ real, ∀n ∈ ω, a n ≤ x ∧ x ≤ b n
In Proofgold the corresponding term root is f33d40... and proposition id is 0d70c4...
Proof:
Proof not loaded.
End of Section Reals