Let x be given.
Assume Hx: x ∈ closure_of R R_lower_limit_topology ex17_17_interval_B.
We will prove x ∈ ex17_17_interval_B_closure_lower.
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_lower_limit_topology → x0 ∈ U → U ∩ ex17_17_interval_B ≠ Empty) x Hx).
We prove the intermediate claim Hxcl: ∀U : set, U ∈ R_lower_limit_topology → x ∈ U → U ∩ ex17_17_interval_B ≠ Empty.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ∀U : set, U ∈ R_lower_limit_topology → x0 ∈ U → U ∩ ex17_17_interval_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 H3S: SNo 3.
An exact proof term for the current goal is (real_SNo 3 real_3).
We prove the intermediate claim HnotxltS2: ¬ (x < sqrt2).
Assume HxltS2: x < sqrt2.
Apply FalseE to the current goal.
We prove the intermediate claim HxRltS2: Rlt x sqrt2.
An exact proof term for the current goal is (RltI x sqrt2 HxR Hs2R HxltS2).
Set U to be the term halfopen_interval_left x sqrt2.
We prove the intermediate claim HUopen: U ∈ R_lower_limit_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x sqrt2 HxR Hs2R).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (halfopen_interval_left_leftmem x sqrt2 HxRltS2).
We prove the intermediate claim Hne: U ∩ ex17_17_interval_B ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ ex17_17_interval_B = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ ex17_17_interval_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 ex17_17_interval_B y Hy).
We prove the intermediate claim HyB: y ∈ ex17_17_interval_B.
An exact proof term for the current goal is (binintersectE2 U ex17_17_interval_B y Hy).
We prove the intermediate claim HyUprop: ¬ (Rlt y x) ∧ Rlt y sqrt2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z x) ∧ Rlt z sqrt2) y HyU).
We prove the intermediate claim HyltS2: Rlt y sqrt2.
An exact proof term for the current goal is (andER (¬ (Rlt y x)) (Rlt y sqrt2) 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 Hs2ltS2: Rlt sqrt2 sqrt2.
An exact proof term for the current goal is (Rlt_tra sqrt2 y sqrt2 Hs2lty HyltS2).
An exact proof term for the current goal is ((not_Rlt_refl sqrt2 Hs2R) Hs2ltS2).
An exact proof term for the current goal is (Hne Hempty).
We prove the intermediate claim Hs2lex: sqrt2 ≤ x.
Apply (SNoLt_trichotomy_or_impred x sqrt2 HxS Hs2S (sqrt2 ≤ x)) to the current goal.
Assume Hlt: x < sqrt2.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotxltS2 Hlt).
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 b0 to be the term add_SNo x 1.
We prove the intermediate claim Hb0R: b0 ∈ R.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (real_add_SNo 3 real_3 1 real_1).
We prove the intermediate claim HxInStd: x ∈ open_interval (add_SNo x (minus_SNo 1)) b0.
An exact proof term for the current goal is (real_in_open_interval_minus1_plus1 x HxR).
We prove the intermediate claim HxStdProp: Rlt (add_SNo x (minus_SNo 1)) x ∧ Rlt x b0.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt (add_SNo x (minus_SNo 1)) z ∧ Rlt z b0) x HxInStd).
We prove the intermediate claim Hxb0: Rlt x b0.
An exact proof term for the current goal is (andER (Rlt (add_SNo x (minus_SNo 1)) x) (Rlt x b0) HxStdProp).
Set U to be the term halfopen_interval_left x b0.
We prove the intermediate claim HUopen: U ∈ R_lower_limit_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x b0 HxR Hb0R).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (halfopen_interval_left_leftmem x b0 Hxb0).
We prove the intermediate claim Hne: U ∩ ex17_17_interval_B ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ ex17_17_interval_B = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ ex17_17_interval_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 ex17_17_interval_B y Hy).
We prove the intermediate claim HyB: y ∈ ex17_17_interval_B.
An exact proof term for the current goal is (binintersectE2 U ex17_17_interval_B y Hy).
We prove the intermediate claim HyUprop: ¬ (Rlt y x) ∧ Rlt y b0.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z x) ∧ Rlt z b0) y HyU).
We prove the intermediate claim Hnyx: ¬ (Rlt y x).
An exact proof term for the current goal is (andEL (¬ (Rlt y x)) (Rlt y b0) 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 Hyltx: Rlt y x.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hylt3.
An exact proof term for the current goal is (Hnyx Hyltx).
An exact proof term for the current goal is (Hne Hempty).
Assume Hgt: 3 < x.
Apply FalseE to the current goal.
Set b0 to be the term add_SNo x 1.
We prove the intermediate claim Hb0R: b0 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
We prove the intermediate claim HxInStd: x ∈ open_interval (add_SNo x (minus_SNo 1)) b0.
An exact proof term for the current goal is (real_in_open_interval_minus1_plus1 x HxR).
We prove the intermediate claim HxStdProp: Rlt (add_SNo x (minus_SNo 1)) x ∧ Rlt x b0.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt (add_SNo x (minus_SNo 1)) z ∧ Rlt z b0) x HxInStd).
We prove the intermediate claim Hxb0: Rlt x b0.
An exact proof term for the current goal is (andER (Rlt (add_SNo x (minus_SNo 1)) x) (Rlt x b0) HxStdProp).
Set U to be the term halfopen_interval_left x b0.
We prove the intermediate claim HUopen: U ∈ R_lower_limit_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x b0 HxR Hb0R).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (halfopen_interval_left_leftmem x b0 Hxb0).
We prove the intermediate claim Hne: U ∩ ex17_17_interval_B ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ ex17_17_interval_B = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ ex17_17_interval_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 ex17_17_interval_B y Hy).
We prove the intermediate claim HyB: y ∈ ex17_17_interval_B.
An exact proof term for the current goal is (binintersectE2 U ex17_17_interval_B y Hy).
We prove the intermediate claim HyUprop: ¬ (Rlt y x) ∧ Rlt y b0.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z x) ∧ Rlt z b0) y HyU).
We prove the intermediate claim Hnyx: ¬ (Rlt y x).
An exact proof term for the current goal is (andEL (¬ (Rlt y x)) (Rlt y b0) 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 HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt sqrt2 z ∧ Rlt z 3) y HyB).
We prove the intermediate claim Hylt3R: 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 HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Hylt3: y < 3.
An exact proof term for the current goal is (RltE_lt y 3 Hylt3R).
We prove the intermediate claim H3ltx: 3 < x.
An exact proof term for the current goal is Hgt.
We prove the intermediate claim Hyltx: y < x.
An exact proof term for the current goal is (SNoLt_tra y 3 x HyS H3S HxS Hylt3 H3ltx).
We prove the intermediate claim Hyltrx: Rlt y x.
An exact proof term for the current goal is (RltI y x HyR HxR Hyltx).
An exact proof term for the current goal is (Hnyx Hyltrx).
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)).
∎