Let x be given.
Assume Hx: x ∈ ex17_17_interval_B_closure_lower.
We will prove x ∈ closure_of R R_lower_limit_topology 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_lower_limit_topology → x ∈ U → U ∩ ex17_17_interval_B ≠ Empty.
Let U be given.
Assume HU: U ∈ R_lower_limit_topology.
Assume HxU: x ∈ U.
We will prove U ∩ ex17_17_interval_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.
Set B to be the term ex17_17_interval_B.
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.
Set B to be the term ex17_17_interval_B.
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 ∈ R_lower_limit_basis, z ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀z ∈ U0, ∃b ∈ R_lower_limit_basis, z ∈ b ∧ b ⊆ U0) U HU).
We prove the intermediate claim Hexb: ∃b ∈ R_lower_limit_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 ∈ R_lower_limit_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 Hexa: ∃a ∈ R, b ∈ {halfopen_interval_left a bb|bb ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_left a0 bb|bb ∈ R}) b HbB).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
Apply Hapair to the current goal.
Assume HaR: a ∈ R.
Assume HbFam: b ∈ {halfopen_interval_left a bb|bb ∈ R}.
We prove the intermediate claim Hexbb: ∃bb ∈ R, b = halfopen_interval_left a bb.
An exact proof term for the current goal is (ReplE R (λbb0 : set ⇒ halfopen_interval_left a bb0) b HbFam).
Apply Hexbb to the current goal.
Let bb be given.
Assume Hbbpair.
Apply Hbbpair to the current goal.
Assume HbbR: bb ∈ R.
Assume Hbeq: b = halfopen_interval_left a bb.
We prove the intermediate claim Hs2Inb: sqrt2 ∈ halfopen_interval_left a bb.
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 a) ∧ Rlt sqrt2 bb.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a) ∧ Rlt z bb) sqrt2 Hs2Inb).
We prove the intermediate claim Hnots2a: ¬ (Rlt sqrt2 a).
An exact proof term for the current goal is (andEL (¬ (Rlt sqrt2 a)) (Rlt sqrt2 bb) Hs2bprop).
We prove the intermediate claim Hs2ltbb: Rlt sqrt2 bb.
An exact proof term for the current goal is (andER (¬ (Rlt sqrt2 a)) (Rlt sqrt2 bb) Hs2bprop).
We prove the intermediate claim HbbS: SNo bb.
An exact proof term for the current goal is (real_SNo bb HbbR).
We prove the intermediate claim Hs2lt3R: Rlt sqrt2 3.
rewrite the current goal using Hs2eqx (from left to right).
An exact proof term for the current goal is (RltI x 3 HxR H3R Hxlt3).
Apply (SNoLt_trichotomy_or_impred bb 3 HbbS H3S (U ∩ B ≠ Empty)) to the current goal.
Assume HbbLt3: bb < 3.
We prove the intermediate claim HbbLt3R: Rlt bb 3.
An exact proof term for the current goal is (RltI bb 3 HbbR H3R HbbLt3).
Apply (rational_dense_between_reals sqrt2 bb Hs2R HbbR Hs2ltbb) 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 bb.
We prove the intermediate claim Hs2ltq: Rlt sqrt2 q.
An exact proof term for the current goal is (andEL (Rlt sqrt2 q) (Rlt q bb) Hqprop).
We prove the intermediate claim Hqltbb: Rlt q bb.
An exact proof term for the current goal is (andER (Rlt sqrt2 q) (Rlt q bb) 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 Hqlt3: Rlt q 3.
An exact proof term for the current goal is (Rlt_tra q bb 3 Hqltbb HbbLt3R).
We prove the intermediate claim Hnotqa: ¬ (Rlt q a).
Assume Hqa: Rlt q a.
We prove the intermediate claim Hs2a: Rlt sqrt2 a.
An exact proof term for the current goal is (Rlt_tra sqrt2 q a Hs2ltq Hqa).
An exact proof term for the current goal is (Hnots2a Hs2a).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hqconj: ¬ (Rlt q a) ∧ Rlt q bb.
Apply andI to the current goal.
An exact proof term for the current goal is Hnotqa.
An exact proof term for the current goal is Hqltbb.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a) ∧ Rlt z bb) q HqR Hqconj).
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 HqInB: q ∈ B.
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.
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 HbbEq3: bb = 3.
Apply (rational_dense_between_reals sqrt2 3 Hs2R H3R Hs2lt3R) 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 Hqltbb: Rlt q bb.
rewrite the current goal using HbbEq3 (from left to right).
An exact proof term for the current goal is Hqlt3.
We prove the intermediate claim Hnotqa: ¬ (Rlt q a).
Assume Hqa: Rlt q a.
We prove the intermediate claim Hs2a: Rlt sqrt2 a.
An exact proof term for the current goal is (Rlt_tra sqrt2 q a Hs2ltq Hqa).
An exact proof term for the current goal is (Hnots2a Hs2a).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hqconj: ¬ (Rlt q a) ∧ Rlt q bb.
Apply andI to the current goal.
An exact proof term for the current goal is Hnotqa.
An exact proof term for the current goal is Hqltbb.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a) ∧ Rlt z bb) q HqR Hqconj).
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 HqInB: q ∈ B.
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.
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 H3Ltbb: 3 < bb.
Apply (rational_dense_between_reals sqrt2 3 Hs2R H3R Hs2lt3R) 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 H3LtbbR: Rlt 3 bb.
An exact proof term for the current goal is (RltI 3 bb H3R HbbR H3Ltbb).
We prove the intermediate claim Hqltbb: Rlt q bb.
An exact proof term for the current goal is (Rlt_tra q 3 bb Hqlt3 H3LtbbR).
We prove the intermediate claim Hnotqa: ¬ (Rlt q a).
Assume Hqa: Rlt q a.
We prove the intermediate claim Hs2a: Rlt sqrt2 a.
An exact proof term for the current goal is (Rlt_tra sqrt2 q a Hs2ltq Hqa).
An exact proof term for the current goal is (Hnots2a Hs2a).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hqconj: ¬ (Rlt q a) ∧ Rlt q bb.
Apply andI to the current goal.
An exact proof term for the current goal is Hnotqa.
An exact proof term for the current goal is Hqltbb.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a) ∧ Rlt z bb) q HqR Hqconj).
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 HqInB: q ∈ B.
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.
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_lower_limit_topology → x0 ∈ U → U ∩ ex17_17_interval_B ≠ Empty) x HxR Hcl).
∎