Let x be given.
Assume Hx: x ∈ ex17_17_interval_B_closure_lower.
We will prove x ∈ closure_of R R_C_topology ex17_17_interval_B.
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 (λz : set ⇒ sqrt2 ≤ z ∧ z < 3) x Hx).
We prove the intermediate claim HxProp: sqrt2 ≤ x ∧ x < 3.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ sqrt2 ≤ z ∧ z < 3) x Hx).
We prove the intermediate claim Hs2lex: sqrt2 ≤ x.
An exact proof term for the current goal is (andEL (sqrt2 ≤ x) (x < 3) HxProp).
We prove the intermediate claim Hxlt3: x < 3.
An exact proof term for the current goal is (andER (sqrt2 ≤ x) (x < 3) HxProp).
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 Hcl: ∀U : set, U ∈ R_C_topology → x ∈ U → U ∩ B ≠ Empty.
Let U be given.
Assume HU: U ∈ R_C_topology.
Assume HxU: x ∈ U.
We will prove U ∩ B ≠ Empty.
We prove the intermediate claim Hcases: sqrt2 < x ∨ sqrt2 = x.
An exact proof term for the current goal is (SNoLeE sqrt2 x Hs2S HxS Hs2lex).
Apply Hcases to the current goal.
Assume Hs2ltx: sqrt2 < x.
We prove the intermediate claim Hs2ltxR: Rlt sqrt2 x.
An exact proof term for the current goal is (RltI sqrt2 x Hs2R HxR Hs2ltx).
We prove the intermediate claim Hxlt3R: Rlt x 3.
An exact proof term for the current goal is (RltI x 3 HxR H3R Hxlt3).
We prove the intermediate claim Hxconj: Rlt sqrt2 x ∧ Rlt x 3.
Apply andI to the current goal.
An exact proof term for the current goal is Hs2ltxR.
An exact proof term for the current goal is Hxlt3R.
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt sqrt2 z ∧ Rlt z 3) x HxR Hxconj).
Assume Hemp: U ∩ B = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxUB: x ∈ U ∩ B.
An exact proof term for the current goal is (binintersectI U B x HxU HxB).
We prove the intermediate claim HxEmp: x ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HxUB.
An exact proof term for the current goal is (EmptyE x HxEmp).
Assume Hs2eqx: sqrt2 = x.
We prove the intermediate claim Hs2U: sqrt2 ∈ U.
rewrite the current goal using Hs2eqx (from left to right).
An exact proof term for the current goal is HxU.
We prove the intermediate claim Hneigh: ∀z ∈ U, ∃b ∈ rational_halfopen_intervals_basis, z ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀z ∈ U0, ∃b ∈ rational_halfopen_intervals_basis, z ∈ b ∧ b ⊆ U0) U HU).
We prove the intermediate claim Hexb: ∃b ∈ rational_halfopen_intervals_basis, sqrt2 ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (Hneigh sqrt2 Hs2U).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
Apply Hbpair to the current goal.
Assume HbB: b ∈ rational_halfopen_intervals_basis.
Assume Hbcore: sqrt2 ∈ b ∧ b ⊆ U.
We prove the intermediate claim Hs2b: sqrt2 ∈ b.
An exact proof term for the current goal is (andEL (sqrt2 ∈ b) (b ⊆ U) Hbcore).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (sqrt2 ∈ b) (b ⊆ U) Hbcore).
We prove the intermediate claim Hexq1: ∃q1 ∈ rational_numbers, b ∈ {halfopen_interval_left q1 q2|q2 ∈ rational_numbers}.
An exact proof term for the current goal is (famunionE rational_numbers (λq1 : set ⇒ {halfopen_interval_left q1 q2|q2 ∈ rational_numbers}) b HbB).
Apply Hexq1 to the current goal.
Let q1 be given.
Assume Hq1pair.
Apply Hq1pair to the current goal.
Assume Hq1Q: q1 ∈ rational_numbers.
Assume HbFam: b ∈ {halfopen_interval_left q1 q2|q2 ∈ rational_numbers}.
We prove the intermediate claim Hexq2: ∃q2 ∈ rational_numbers, b = halfopen_interval_left q1 q2.
An exact proof term for the current goal is (ReplE rational_numbers (λq2 : set ⇒ halfopen_interval_left q1 q2) b HbFam).
Apply Hexq2 to the current goal.
Let q2 be given.
Assume Hq2pair.
Apply Hq2pair to the current goal.
Assume Hq2Q: q2 ∈ rational_numbers.
Assume Hbeq: b = halfopen_interval_left q1 q2.
We prove the intermediate claim Hq1R: q1 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q1 Hq1Q).
We prove the intermediate claim Hq2R: q2 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q2 Hq2Q).
We prove the intermediate claim Hs2Inb: sqrt2 ∈ halfopen_interval_left q1 q2.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hs2b.
We prove the intermediate claim Hs2bprop: ¬ (Rlt sqrt2 q1) ∧ Rlt sqrt2 q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) sqrt2 Hs2Inb).
We prove the intermediate claim Hs2ltq2: Rlt sqrt2 q2.
An exact proof term for the current goal is (andER (¬ (Rlt sqrt2 q1)) (Rlt sqrt2 q2) Hs2bprop).
We prove the intermediate claim Hq1neq: q1 ≠ sqrt2.
Assume Heq: q1 = sqrt2.
Apply FalseE to the current goal.
We prove the intermediate claim Hs2Q: sqrt2 ∈ rational_numbers.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hq1Q.
An exact proof term for the current goal is (sqrt2_not_rational_numbers Hs2Q).
We prove the intermediate claim Hq1S: SNo q1.
An exact proof term for the current goal is (real_SNo q1 Hq1R).
We prove the intermediate claim Hq1ltS2: Rlt q1 sqrt2.
Apply (SNoLt_trichotomy_or_impred q1 sqrt2 Hq1S Hs2S (Rlt q1 sqrt2)) to the current goal.
Assume Hlt: q1 < sqrt2.
An exact proof term for the current goal is (RltI q1 sqrt2 Hq1R Hs2R Hlt).
Assume Heq: q1 = sqrt2.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hq1neq Heq).
Assume Hgt: sqrt2 < q1.
Apply FalseE to the current goal.
We prove the intermediate claim Hs2q1: Rlt sqrt2 q1.
An exact proof term for the current goal is (RltI sqrt2 q1 Hs2R Hq1R Hgt).
An exact proof term for the current goal is ((andEL (¬ (Rlt sqrt2 q1)) (Rlt sqrt2 q2) Hs2bprop) Hs2q1).
Apply (SNoLt_trichotomy_or_impred q2 3 (real_SNo q2 Hq2R) H3S (U ∩ B ≠ Empty)) to the current goal.
Assume Hq2lt3: q2 < 3.
We prove the intermediate claim Hq2lt3R: Rlt q2 3.
An exact proof term for the current goal is (RltI q2 3 Hq2R H3R Hq2lt3).
Apply (rational_dense_between_reals sqrt2 q2 Hs2R Hq2R Hs2ltq2) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt sqrt2 q ∧ Rlt q q2.
We prove the intermediate claim Hs2ltq: Rlt sqrt2 q.
An exact proof term for the current goal is (andEL (Rlt sqrt2 q) (Rlt q q2) Hqprop).
We prove the intermediate claim Hqltq2: Rlt q q2.
An exact proof term for the current goal is (andER (Rlt sqrt2 q) (Rlt q q2) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim HqconjU: ¬ (Rlt q q1) ∧ Rlt q q2.
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_sym q1 q (Rlt_tra q1 sqrt2 q Hq1ltS2 Hs2ltq)).
An exact proof term for the current goal is Hqltq2.
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) q HqR HqconjU).
We prove the intermediate claim HqInU: q ∈ U.
An exact proof term for the current goal is (HbsubU q HqInb).
We prove the intermediate claim Hqlt3: Rlt q 3.
An exact proof term for the current goal is (Rlt_tra q q2 3 Hqltq2 Hq2lt3R).
We prove the intermediate claim HqconjB: Rlt sqrt2 q ∧ Rlt q 3.
Apply andI to the current goal.
An exact proof term for the current goal is Hs2ltq.
An exact proof term for the current goal is Hqlt3.
We prove the intermediate claim HqInB: q ∈ B.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt sqrt2 z ∧ Rlt z 3) q HqR HqconjB).
Assume Hemp: U ∩ B = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUB: q ∈ U ∩ B.
An exact proof term for the current goal is (binintersectI U B q HqInU HqInB).
We prove the intermediate claim HqEmp: q ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HqUB.
An exact proof term for the current goal is (EmptyE q HqEmp).
Assume Hq2eq3: q2 = 3.
Apply (rational_dense_between_reals sqrt2 3 Hs2R H3R (RltI sqrt2 3 Hs2R H3R (SNoLeLt_tra sqrt2 x 3 Hs2S HxS H3S Hs2lex Hxlt3))) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt sqrt2 q ∧ Rlt q 3.
We prove the intermediate claim Hs2ltq: Rlt sqrt2 q.
An exact proof term for the current goal is (andEL (Rlt sqrt2 q) (Rlt q 3) Hqprop).
We prove the intermediate claim Hqlt3: Rlt q 3.
An exact proof term for the current goal is (andER (Rlt sqrt2 q) (Rlt q 3) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim Hqltq2: Rlt q q2.
rewrite the current goal using Hq2eq3 (from left to right).
An exact proof term for the current goal is Hqlt3.
We prove the intermediate claim HqconjU: ¬ (Rlt q q1) ∧ Rlt q q2.
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_sym q1 q (Rlt_tra q1 sqrt2 q Hq1ltS2 Hs2ltq)).
An exact proof term for the current goal is Hqltq2.
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) q HqR HqconjU).
We prove the intermediate claim HqInU: q ∈ U.
An exact proof term for the current goal is (HbsubU q HqInb).
We prove the intermediate claim HqconjB: Rlt sqrt2 q ∧ Rlt q 3.
Apply andI to the current goal.
An exact proof term for the current goal is Hs2ltq.
An exact proof term for the current goal is Hqlt3.
We prove the intermediate claim HqInB: q ∈ B.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt sqrt2 z ∧ Rlt z 3) q HqR HqconjB).
Assume Hemp: U ∩ B = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUB: q ∈ U ∩ B.
An exact proof term for the current goal is (binintersectI U B q HqInU HqInB).
We prove the intermediate claim HqEmp: q ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HqUB.
An exact proof term for the current goal is (EmptyE q HqEmp).
Assume H3ltq2: 3 < q2.
Apply (rational_dense_between_reals sqrt2 3 Hs2R H3R (RltI sqrt2 3 Hs2R H3R (SNoLeLt_tra sqrt2 x 3 Hs2S HxS H3S Hs2lex Hxlt3))) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt sqrt2 q ∧ Rlt q 3.
We prove the intermediate claim Hs2ltq: Rlt sqrt2 q.
An exact proof term for the current goal is (andEL (Rlt sqrt2 q) (Rlt q 3) Hqprop).
We prove the intermediate claim Hqlt3: Rlt q 3.
An exact proof term for the current goal is (andER (Rlt sqrt2 q) (Rlt q 3) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim H3ltq2R: Rlt 3 q2.
An exact proof term for the current goal is (RltI 3 q2 H3R Hq2R H3ltq2).
We prove the intermediate claim Hqltq2: Rlt q q2.
An exact proof term for the current goal is (Rlt_tra q 3 q2 Hqlt3 H3ltq2R).
We prove the intermediate claim HqconjU: ¬ (Rlt q q1) ∧ Rlt q q2.
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_sym q1 q (Rlt_tra q1 sqrt2 q Hq1ltS2 Hs2ltq)).
An exact proof term for the current goal is Hqltq2.
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) q HqR HqconjU).
We prove the intermediate claim HqInU: q ∈ U.
An exact proof term for the current goal is (HbsubU q HqInb).
We prove the intermediate claim HqconjB: Rlt sqrt2 q ∧ Rlt q 3.
Apply andI to the current goal.
An exact proof term for the current goal is Hs2ltq.
An exact proof term for the current goal is Hqlt3.
We prove the intermediate claim HqInB: q ∈ B.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt sqrt2 z ∧ Rlt z 3) q HqR HqconjB).
Assume Hemp: U ∩ B = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUB: q ∈ U ∩ B.
An exact proof term for the current goal is (binintersectI U B q HqInU HqInB).
We prove the intermediate claim HqEmp: q ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HqUB.
An exact proof term for the current goal is (EmptyE q HqEmp).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ∀U : set, U ∈ R_C_topology → x0 ∈ U → U ∩ B ≠ Empty) x HxR Hcl).
∎