Let x be given.
Assume Hx: x ∈ ex17_17_interval_A_closure_lower.
We will prove x ∈ closure_of R R_lower_limit_topology ex17_17_interval_A.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ 0 ≤ z ∧ z < sqrt2) x Hx).
We prove the intermediate claim HxProp: 0 ≤ x ∧ x < sqrt2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ 0 ≤ z ∧ z < sqrt2) x Hx).
We prove the intermediate claim H0lex: 0 ≤ x.
An exact proof term for the current goal is (andEL (0 ≤ x) (x < sqrt2) HxProp).
We prove the intermediate claim HxltS2: x < sqrt2.
An exact proof term for the current goal is (andER (0 ≤ x) (x < sqrt2) 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 Hcl: ∀U : set, U ∈ R_lower_limit_topology → x ∈ U → U ∩ ex17_17_interval_A ≠ Empty.
Let U be given.
Assume HU: U ∈ R_lower_limit_topology.
Assume HxU: x ∈ U.
We will prove U ∩ ex17_17_interval_A ≠ Empty.
We prove the intermediate claim Hcases: 0 < x ∨ 0 = x.
An exact proof term for the current goal is (SNoLeE 0 x SNo_0 HxS H0lex).
Apply Hcases to the current goal.
Assume H0ltx: 0 < x.
Set A to be the term ex17_17_interval_A.
We prove the intermediate claim H0ltxR: Rlt 0 x.
An exact proof term for the current goal is (RltI 0 x real_0 HxR H0ltx).
We prove the intermediate claim HxltS2R: Rlt x sqrt2.
An exact proof term for the current goal is (RltI x sqrt2 HxR Hs2R HxltS2).
We prove the intermediate claim Hxconj: Rlt 0 x ∧ Rlt x sqrt2.
Apply andI to the current goal.
An exact proof term for the current goal is H0ltxR.
An exact proof term for the current goal is HxltS2R.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) x HxR Hxconj).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxUA: x ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A x HxU HxA).
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 HxUA.
An exact proof term for the current goal is (EmptyE x HxEmp).
Assume H0eqx: 0 = x.
Set A to be the term ex17_17_interval_A.
We prove the intermediate claim H0U: 0 ∈ U.
rewrite the current goal using H0eqx (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, 0 ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (Hneigh 0 H0U).
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: 0 ∈ b ∧ b ⊆ U.
We prove the intermediate claim H0b: 0 ∈ b.
An exact proof term for the current goal is (andEL (0 ∈ b) (b ⊆ U) Hbcore).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (0 ∈ 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 H0Inb: 0 ∈ halfopen_interval_left a bb.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is H0b.
We prove the intermediate claim H0bprop: ¬ (Rlt 0 a) ∧ Rlt 0 bb.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a) ∧ Rlt z bb) 0 H0Inb).
We prove the intermediate claim Hnot0a: ¬ (Rlt 0 a).
An exact proof term for the current goal is (andEL (¬ (Rlt 0 a)) (Rlt 0 bb) H0bprop).
We prove the intermediate claim H0ltbb: Rlt 0 bb.
An exact proof term for the current goal is (andER (¬ (Rlt 0 a)) (Rlt 0 bb) H0bprop).
We prove the intermediate claim HbbS: SNo bb.
An exact proof term for the current goal is (real_SNo bb HbbR).
Apply (SNoLt_trichotomy_or_impred bb sqrt2 HbbS Hs2S (U ∩ A ≠ Empty)) to the current goal.
Assume HbbLtS2: bb < sqrt2.
We prove the intermediate claim HbbLtS2R: Rlt bb sqrt2.
An exact proof term for the current goal is (RltI bb sqrt2 HbbR Hs2R HbbLtS2).
Apply (rational_dense_between_reals 0 bb real_0 HbbR H0ltbb) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt 0 q ∧ Rlt q bb.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 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 0 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 HqltS2: Rlt q sqrt2.
An exact proof term for the current goal is (Rlt_tra q bb sqrt2 Hqltbb HbbLtS2R).
We prove the intermediate claim Hnotqa: ¬ (Rlt q a).
Assume Hqa: Rlt q a.
We prove the intermediate claim H0a: Rlt 0 a.
An exact proof term for the current goal is (Rlt_tra 0 q a H0ltq Hqa).
An exact proof term for the current goal is (Hnot0a H0a).
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 HqInA: q ∈ A.
We prove the intermediate claim HqconjA: Rlt 0 q ∧ Rlt q sqrt2.
Apply andI to the current goal.
An exact proof term for the current goal is H0ltq.
An exact proof term for the current goal is HqltS2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) q HqR HqconjA).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUA: q ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A q HqInU HqInA).
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 HqUA.
An exact proof term for the current goal is (EmptyE q HqEmp).
Assume HbbEqS2: bb = sqrt2.
Apply (rational_dense_between_reals 0 bb real_0 HbbR H0ltbb) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt 0 q ∧ Rlt q bb.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 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 0 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 HqltS2: Rlt q sqrt2.
rewrite the current goal using HbbEqS2 (from right to left).
An exact proof term for the current goal is Hqltbb.
We prove the intermediate claim Hnotqa: ¬ (Rlt q a).
Assume Hqa: Rlt q a.
We prove the intermediate claim H0a: Rlt 0 a.
An exact proof term for the current goal is (Rlt_tra 0 q a H0ltq Hqa).
An exact proof term for the current goal is (Hnot0a H0a).
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 HqInA: q ∈ A.
We prove the intermediate claim HqconjA: Rlt 0 q ∧ Rlt q sqrt2.
Apply andI to the current goal.
An exact proof term for the current goal is H0ltq.
An exact proof term for the current goal is HqltS2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) q HqR HqconjA).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUA: q ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A q HqInU HqInA).
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 HqUA.
An exact proof term for the current goal is (EmptyE q HqEmp).
Assume Hs2Ltbb: sqrt2 < bb.
We prove the intermediate claim Hs2LtbbR: Rlt sqrt2 bb.
An exact proof term for the current goal is (RltI sqrt2 bb Hs2R HbbR Hs2Ltbb).
We prove the intermediate claim H0ltS2R: Rlt 0 sqrt2.
An exact proof term for the current goal is (RltI 0 sqrt2 real_0 Hs2R SNoLt_0_sqrt2).
Apply (rational_dense_between_reals 0 sqrt2 real_0 Hs2R H0ltS2R) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt 0 q ∧ Rlt q sqrt2.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 q) (Rlt q sqrt2) Hqprop).
We prove the intermediate claim HqltS2: Rlt q sqrt2.
An exact proof term for the current goal is (andER (Rlt 0 q) (Rlt q sqrt2) 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.
An exact proof term for the current goal is (Rlt_tra q sqrt2 bb HqltS2 Hs2LtbbR).
We prove the intermediate claim Hnotqa: ¬ (Rlt q a).
Assume Hqa: Rlt q a.
We prove the intermediate claim H0a: Rlt 0 a.
An exact proof term for the current goal is (Rlt_tra 0 q a H0ltq Hqa).
An exact proof term for the current goal is (Hnot0a H0a).
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 HqInA: q ∈ A.
We prove the intermediate claim HqconjA: Rlt 0 q ∧ Rlt q sqrt2.
Apply andI to the current goal.
An exact proof term for the current goal is H0ltq.
An exact proof term for the current goal is HqltS2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) q HqR HqconjA).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUA: q ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A q HqInU HqInA).
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 HqUA.
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_A ≠ Empty) x HxR Hcl).
∎