Let x be given.
Assume Hx: x ∈ closure_of R R_C_topology ex17_17_interval_A.
We will prove x ∈ ex17_17_interval_A_closure_C.
Set A to be the term ex17_17_interval_A.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ∀U : set, U ∈ R_C_topology → x0 ∈ U → U ∩ A ≠ Empty) x Hx).
We prove the intermediate claim Hxcl: ∀U : set, U ∈ R_C_topology → x ∈ U → U ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ∀U : set, U ∈ R_C_topology → x0 ∈ U → U ∩ A ≠ Empty) x Hx).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Hs2R: sqrt2 ∈ R.
An exact proof term for the current goal is sqrt2_in_R.
We prove the intermediate claim Hs2S: SNo sqrt2.
An exact proof term for the current goal is (real_SNo sqrt2 Hs2R).
We prove the intermediate claim HBasisC: basis_on R rational_halfopen_intervals_basis.
An exact proof term for the current goal is (andEL (basis_on R rational_halfopen_intervals_basis) (generated_topology R rational_halfopen_intervals_basis ≠ R_lower_limit_topology) ex13_8b_halfopen_rational_basis_topology).
We prove the intermediate claim H0lex: 0 ≤ x.
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (0 ≤ x)) to the current goal.
Assume Hxlt0: x < 0.
Apply FalseE to the current goal.
We prove the intermediate claim Hxlt0R: Rlt x 0.
An exact proof term for the current goal is (RltI x 0 HxR real_0 Hxlt0).
Apply (rational_dense_between_reals x 0 HxR real_0 Hxlt0R) to the current goal.
Let q2 be given.
Assume Hq2pair.
Apply Hq2pair to the current goal.
Assume Hq2Q: q2 ∈ rational_numbers.
Assume Hq2prop: Rlt x q2 ∧ Rlt q2 0.
We prove the intermediate claim Hxltq2: Rlt x q2.
An exact proof term for the current goal is (andEL (Rlt x q2) (Rlt q2 0) Hq2prop).
We prove the intermediate claim Hq2lt0: Rlt q2 0.
An exact proof term for the current goal is (andER (Rlt x q2) (Rlt q2 0) Hq2prop).
We prove the intermediate claim Hq2R: q2 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q2 Hq2Q).
Set a0 to be the term add_SNo x (minus_SNo 1).
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR (minus_SNo 1) (real_minus_SNo 1 real_1)).
We prove the intermediate claim Ha0ltx: Rlt a0 x.
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (real_SNo (minus_SNo 1) Hm1R).
We prove the intermediate claim Ha0Def: a0 = add_SNo x (minus_SNo 1).
Use reflexivity.
We prove the intermediate claim Hx0: add_SNo x 0 = x.
An exact proof term for the current goal is (add_SNo_0R x HxS).
We prove the intermediate claim Hlt: add_SNo x (minus_SNo 1) < add_SNo x 0.
An exact proof term for the current goal is (add_SNo_Lt2 x (minus_SNo 1) 0 HxS Hm1S SNo_0 minus_1_lt_0).
We prove the intermediate claim Ha0ltxS: a0 < x.
rewrite the current goal using Ha0Def (from left to right).
rewrite the current goal using Hx0 (from right to left) at position 2.
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (RltI a0 x Ha0R HxR Ha0ltxS).
Apply (rational_dense_between_reals a0 x Ha0R HxR Ha0ltx) to the current goal.
Let q1 be given.
Assume Hq1pair.
Apply Hq1pair to the current goal.
Assume Hq1Q: q1 ∈ rational_numbers.
Assume Hq1prop: Rlt a0 q1 ∧ Rlt q1 x.
We prove the intermediate claim Hq1ltx: Rlt q1 x.
An exact proof term for the current goal is (andER (Rlt a0 q1) (Rlt q1 x) Hq1prop).
We prove the intermediate claim Hq1R: q1 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q1 Hq1Q).
Set U to be the term halfopen_interval_left q1 q2.
We prove the intermediate claim HUinB: U ∈ rational_halfopen_intervals_basis.
We will prove U ∈ rational_halfopen_intervals_basis.
We prove the intermediate claim HUfam: U ∈ {halfopen_interval_left q1 qq|qq ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ halfopen_interval_left q1 qq) q2 Hq2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) q1 U Hq1Q HUfam).
We prove the intermediate claim HUopen: U ∈ R_C_topology.
An exact proof term for the current goal is (generated_topology_contains_basis R rational_halfopen_intervals_basis HBasisC U HUinB).
We prove the intermediate claim Hnxq1: ¬ (Rlt x q1).
An exact proof term for the current goal is (not_Rlt_sym q1 x Hq1ltx).
We prove the intermediate claim HxU: x ∈ U.
We prove the intermediate claim Hconj: ¬ (Rlt x q1) ∧ Rlt x q2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxq1.
An exact proof term for the current goal is Hxltq2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) x HxR Hconj).
We prove the intermediate claim Hne: U ∩ A ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ A = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ A.
We will prove y ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U A y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 U A y Hy).
We prove the intermediate claim HyUprop: ¬ (Rlt y q1) ∧ Rlt y q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) y HyU).
We prove the intermediate claim Hyltq2: Rlt y q2.
An exact proof term for the current goal is (andER (¬ (Rlt y q1)) (Rlt y q2) HyUprop).
We prove the intermediate claim HyAprop: Rlt 0 y ∧ Rlt y sqrt2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) y HyA).
We prove the intermediate claim H0lty: Rlt 0 y.
An exact proof term for the current goal is (andEL (Rlt 0 y) (Rlt y sqrt2) HyAprop).
We prove the intermediate claim H0ltq2: Rlt 0 q2.
An exact proof term for the current goal is (Rlt_tra 0 y q2 H0lty Hyltq2).
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) (Rlt_tra 0 q2 0 H0ltq2 Hq2lt0)).
An exact proof term for the current goal is (Hne Hempty).
Assume Heq: x = 0.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
Assume H0ltx: 0 < x.
An exact proof term for the current goal is (SNoLtLe 0 x H0ltx).
We prove the intermediate claim HxleS2: x ≤ sqrt2.
Apply (SNoLt_trichotomy_or_impred sqrt2 x Hs2S HxS (x ≤ sqrt2)) to the current goal.
Assume Hs2ltx: sqrt2 < x.
Apply FalseE to the current goal.
We prove the intermediate claim Hs2ltxR: Rlt sqrt2 x.
An exact proof term for the current goal is (RltI sqrt2 x Hs2R HxR Hs2ltx).
Apply (rational_dense_between_reals sqrt2 x Hs2R HxR Hs2ltxR) to the current goal.
Let q1 be given.
Assume Hq1pair.
Apply Hq1pair to the current goal.
Assume Hq1Q: q1 ∈ rational_numbers.
Assume Hq1prop: Rlt sqrt2 q1 ∧ Rlt q1 x.
We prove the intermediate claim Hs2ltq1: Rlt sqrt2 q1.
An exact proof term for the current goal is (andEL (Rlt sqrt2 q1) (Rlt q1 x) Hq1prop).
We prove the intermediate claim Hq1ltx: Rlt q1 x.
An exact proof term for the current goal is (andER (Rlt sqrt2 q1) (Rlt q1 x) Hq1prop).
We prove the intermediate claim Hq1R: q1 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q1 Hq1Q).
Set x1 to be the term add_SNo x 1.
We prove the intermediate claim Hx1R: x1 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
We prove the intermediate claim Hxltx1: x < x1.
We prove the intermediate claim Hlt0: add_SNo x 0 < add_SNo x 1.
An exact proof term for the current goal is (add_SNo_Lt2 x 0 1 HxS SNo_0 SNo_1 SNoLt_0_1).
We prove the intermediate claim Hx0: add_SNo x 0 = x.
An exact proof term for the current goal is (add_SNo_0R x HxS).
We prove the intermediate claim Hx1Def: x1 = add_SNo x 1.
Use reflexivity.
rewrite the current goal using Hx0 (from right to left) at position 1.
rewrite the current goal using Hx1Def (from left to right).
An exact proof term for the current goal is Hlt0.
We prove the intermediate claim Hxltx1R: Rlt x x1.
An exact proof term for the current goal is (RltI x x1 HxR Hx1R Hxltx1).
Apply (rational_dense_between_reals x x1 HxR Hx1R Hxltx1R) to the current goal.
Let q2 be given.
Assume Hq2pair.
Apply Hq2pair to the current goal.
Assume Hq2Q: q2 ∈ rational_numbers.
Assume Hq2prop: Rlt x q2 ∧ Rlt q2 x1.
We prove the intermediate claim Hxltq2: Rlt x q2.
An exact proof term for the current goal is (andEL (Rlt x q2) (Rlt q2 x1) Hq2prop).
We prove the intermediate claim Hq2R: q2 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q2 Hq2Q).
Set U to be the term halfopen_interval_left q1 q2.
We prove the intermediate claim HUinB: U ∈ rational_halfopen_intervals_basis.
We will prove U ∈ rational_halfopen_intervals_basis.
We prove the intermediate claim HUfam: U ∈ {halfopen_interval_left q1 qq|qq ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ halfopen_interval_left q1 qq) q2 Hq2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) q1 U Hq1Q HUfam).
We prove the intermediate claim HUopen: U ∈ R_C_topology.
An exact proof term for the current goal is (generated_topology_contains_basis R rational_halfopen_intervals_basis HBasisC U HUinB).
We prove the intermediate claim Hnxq1: ¬ (Rlt x q1).
An exact proof term for the current goal is (not_Rlt_sym q1 x Hq1ltx).
We prove the intermediate claim HxU: x ∈ U.
We prove the intermediate claim Hconj: ¬ (Rlt x q1) ∧ Rlt x q2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxq1.
An exact proof term for the current goal is Hxltq2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) x HxR Hconj).
We prove the intermediate claim Hne: U ∩ A ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ A = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ A.
We will prove y ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U A y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 U A y Hy).
We prove the intermediate claim HyUprop: ¬ (Rlt y q1) ∧ Rlt y q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) y HyU).
We prove the intermediate claim Hnyq1: ¬ (Rlt y q1).
An exact proof term for the current goal is (andEL (¬ (Rlt y q1)) (Rlt y q2) HyUprop).
We prove the intermediate claim HyAprop: Rlt 0 y ∧ Rlt y sqrt2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) y HyA).
We prove the intermediate claim Hylts2: Rlt y sqrt2.
An exact proof term for the current goal is (andER (Rlt 0 y) (Rlt y sqrt2) HyAprop).
We prove the intermediate claim Hyltoq1: Rlt y q1.
An exact proof term for the current goal is (Rlt_tra y sqrt2 q1 Hylts2 Hs2ltq1).
An exact proof term for the current goal is (Hnyq1 Hyltoq1).
An exact proof term for the current goal is (Hne Hempty).
Assume Heq: sqrt2 = x.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is (SNoLe_ref sqrt2).
Assume HxltS2: x < sqrt2.
An exact proof term for the current goal is (SNoLtLe x sqrt2 HxltS2).
We will prove x ∈ ex17_17_interval_A_closure_C.
An exact proof term for the current goal is (SepI R (λz : set ⇒ 0 ≤ z ∧ z ≤ sqrt2) x HxR (andI (0 ≤ x) (x ≤ sqrt2) H0lex HxleS2)).
∎