Let x be given.
Assume Hx: x ∈ closure_of R R_C_topology ex17_17_interval_B.
We will prove x ∈ ex17_17_interval_B_closure_lower.
Set B to be the term ex17_17_interval_B.
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 ∩ B ≠ Empty) x Hx).
We prove the intermediate claim Hxcl: ∀U : set, U ∈ R_C_topology → x ∈ U → U ∩ B ≠ Empty.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ∀U : set, U ∈ R_C_topology → x0 ∈ U → U ∩ B ≠ 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 H3R: 3 ∈ R.
An exact proof term for the current goal is real_3.
We prove the intermediate claim H3S: SNo 3.
An exact proof term for the current goal is (real_SNo 3 H3R).
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 Hs2lex: sqrt2 ≤ x.
Apply (SNoLt_trichotomy_or_impred x sqrt2 HxS Hs2S (sqrt2 ≤ x)) to the current goal.
Assume HxltS2: x < sqrt2.
Apply FalseE to the current goal.
We prove the intermediate claim HxltS2R: Rlt x sqrt2.
An exact proof term for the current goal is (RltI x sqrt2 HxR Hs2R HxltS2).
Apply (rational_dense_between_reals x sqrt2 HxR Hs2R HxltS2R) 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 sqrt2.
We prove the intermediate claim Hxltq2: Rlt x q2.
An exact proof term for the current goal is (andEL (Rlt x q2) (Rlt q2 sqrt2) Hq2prop).
We prove the intermediate claim Hq2ltS2: Rlt q2 sqrt2.
An exact proof term for the current goal is (andER (Rlt x q2) (Rlt q2 sqrt2) 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 ∩ B ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ B = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ B.
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 B y Hy).
We prove the intermediate claim HyB: y ∈ B.
An exact proof term for the current goal is (binintersectE2 U B 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 HyBprop: Rlt sqrt2 y ∧ Rlt y 3.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt sqrt2 z ∧ Rlt z 3) y HyB).
We prove the intermediate claim Hs2lty: Rlt sqrt2 y.
An exact proof term for the current goal is (andEL (Rlt sqrt2 y) (Rlt y 3) HyBprop).
We prove the intermediate claim Hs2ltq2: Rlt sqrt2 q2.
An exact proof term for the current goal is (Rlt_tra sqrt2 y q2 Hs2lty Hyltq2).
An exact proof term for the current goal is ((not_Rlt_refl sqrt2 Hs2R) (Rlt_tra sqrt2 q2 sqrt2 Hs2ltq2 Hq2ltS2)).
An exact proof term for the current goal is (Hne Hempty).
Assume Heq: x = sqrt2.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SNoLe_ref sqrt2).
Assume Hgt: sqrt2 < x.
An exact proof term for the current goal is (SNoLtLe sqrt2 x Hgt).
We prove the intermediate claim Hxlt3: x < 3.
Apply (SNoLt_trichotomy_or_impred x 3 HxS H3S (x < 3)) to the current goal.
Assume Hlt: x < 3.
An exact proof term for the current goal is Hlt.
Assume Heq: x = 3.
Apply FalseE to the current goal.
Set x1 to be the term add_SNo 3 1.
We prove the intermediate claim Hx1R: x1 ∈ R.
An exact proof term for the current goal is (real_add_SNo 3 real_3 1 real_1).
We prove the intermediate claim H3ltx1: 3 < x1.
We prove the intermediate claim Hlt0: add_SNo 3 0 < add_SNo 3 1.
An exact proof term for the current goal is (add_SNo_Lt2 3 0 1 H3S SNo_0 SNo_1 SNoLt_0_1).
We prove the intermediate claim Hlt1: 3 < add_SNo 3 1.
rewrite the current goal using (add_SNo_0R 3 H3S) (from right to left) at position 1.
An exact proof term for the current goal is Hlt0.
We prove the intermediate claim Hx1Def: x1 = add_SNo 3 1.
Use reflexivity.
rewrite the current goal using Hx1Def (from right to left).
An exact proof term for the current goal is Hlt1.
We prove the intermediate claim H3ltx1R: Rlt 3 x1.
An exact proof term for the current goal is (RltI 3 x1 H3R Hx1R H3ltx1).
Apply (rational_dense_between_reals 3 x1 H3R Hx1R H3ltx1R) to the current goal.
Let q2 be given.
Assume Hq2pair.
Apply Hq2pair to the current goal.
Assume Hq2Q: q2 ∈ rational_numbers.
Assume Hq2prop: Rlt 3 q2 ∧ Rlt q2 x1.
We prove the intermediate claim H3ltq2: Rlt 3 q2.
An exact proof term for the current goal is (andEL (Rlt 3 q2) (Rlt q2 x1) Hq2prop).
Set q1 to be the term 3.
We prove the intermediate claim Hq1Def: q1 = 3.
Use reflexivity.
We prove the intermediate claim Hq1Q: q1 ∈ rational_numbers.
rewrite the current goal using Hq1Def (from left to right).
An exact proof term for the current goal is three_in_rational_numbers.
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 HxU: x ∈ U.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hnot33: ¬ (Rlt 3 3).
An exact proof term for the current goal is (not_Rlt_refl 3 H3R).
We prove the intermediate claim Hnot3q1: ¬ (Rlt 3 q1).
rewrite the current goal using Hq1Def (from left to right).
An exact proof term for the current goal is Hnot33.
We prove the intermediate claim Hconj: ¬ (Rlt 3 q1) ∧ Rlt 3 q2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnot3q1.
An exact proof term for the current goal is H3ltq2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) 3 H3R Hconj).
We prove the intermediate claim Hne: U ∩ B ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ B = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ B.
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 B y Hy).
We prove the intermediate claim HyB: y ∈ B.
An exact proof term for the current goal is (binintersectE2 U B 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 Hny3: ¬ (Rlt y 3).
rewrite the current goal using Hq1Def (from right to left).
An exact proof term for the current goal is (andEL (¬ (Rlt y q1)) (Rlt y q2) HyUprop).
We prove the intermediate claim HyBprop: Rlt sqrt2 y ∧ Rlt y 3.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt sqrt2 z ∧ Rlt z 3) y HyB).
We prove the intermediate claim Hylt3: Rlt y 3.
An exact proof term for the current goal is (andER (Rlt sqrt2 y) (Rlt y 3) HyBprop).
An exact proof term for the current goal is (Hny3 Hylt3).
An exact proof term for the current goal is (Hne Hempty).
Assume Hgt: 3 < x.
Apply FalseE to the current goal.
We prove the intermediate claim HgtR: Rlt 3 x.
An exact proof term for the current goal is (RltI 3 x H3R HxR Hgt).
Apply (rational_dense_between_reals 3 x H3R HxR HgtR) to the current goal.
Let q1 be given.
Assume Hq1pair.
Apply Hq1pair to the current goal.
Assume Hq1Q: q1 ∈ rational_numbers.
Assume Hq1prop: Rlt 3 q1 ∧ Rlt q1 x.
We prove the intermediate claim H3ltq1: Rlt 3 q1.
An exact proof term for the current goal is (andEL (Rlt 3 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 3 q1) (Rlt q1 x) Hq1prop).
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 ∩ B ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ B = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ B.
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 B y Hy).
We prove the intermediate claim HyB: y ∈ B.
An exact proof term for the current goal is (binintersectE2 U B 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 HyBprop: Rlt sqrt2 y ∧ Rlt y 3.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt sqrt2 z ∧ Rlt z 3) y HyB).
We prove the intermediate claim Hylt3: Rlt y 3.
An exact proof term for the current goal is (andER (Rlt sqrt2 y) (Rlt y 3) HyBprop).
We prove the intermediate claim Hyltq1: Rlt y q1.
An exact proof term for the current goal is (Rlt_tra y 3 q1 Hylt3 H3ltq1).
An exact proof term for the current goal is (Hnyq1 Hyltq1).
An exact proof term for the current goal is (Hne Hempty).
We will prove x ∈ ex17_17_interval_B_closure_lower.
An exact proof term for the current goal is (SepI R (λz : set ⇒ sqrt2 ≤ z ∧ z < 3) x HxR (andI (sqrt2 ≤ x) (x < 3) Hs2lex Hxlt3)).
∎