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.

(*** $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 ***)

(*** $I sig/Part9.mgs ***)

(*** Part 10 ***)

L22

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.

L50

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.

L97

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.

L118

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.

L256

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

L258

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

L260

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.

L276

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.

L319

Theorem. (real_SNo)

∀x ∈ real, SNo x

In Proofgold the corresponding term root is 17c3d6... and proposition id is d4cbb8...

Proof:
Proof not loaded.

L324

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.

L329

Theorem. (SNoS_omega_real)

SNoS_ ω ⊆ real

In Proofgold the corresponding term root is a469c6... and proposition id is d9411b...

Proof:
Proof not loaded.

L420

Theorem. (real_0)

0 ∈ real

In Proofgold the corresponding term root is 53bbc2... and proposition id is 493130...

Proof:
Proof not loaded.

L424

Theorem. (real_1)

1 ∈ real

In Proofgold the corresponding term root is bbf720... and proposition id is 790b4d...

Proof:
Proof not loaded.

L428

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.

L445

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.

L694

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.

L1091

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.

L1117

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.

L1147

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.

L1233

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.

L1260

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.

L1476

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.

L1539

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.

L1605

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.

L1610

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.

L1711

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.

L1928

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.

L2111

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.

L2587

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.

L2638

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.

L4004

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.

L4062

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.

L4080

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.

L4159

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.

L4524

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.

L5268

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.

L5274

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.

L5300

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.

L5308

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.

L5336

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.

L5354

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.

L5428

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.

L5455

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.

L5526

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.

L5950

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.

L6366

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.

L6466

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.

L6899

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