Let x be given.
Assume Hx: x ∈ closure_of R R_lower_limit_topology ex17_17_interval_A.
We will prove x ∈ ex17_17_interval_A_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_A ≠ Empty) x Hx).
We prove the intermediate claim Hxcl: ∀U : set, U ∈ R_lower_limit_topology → x ∈ U → U ∩ ex17_17_interval_A ≠ 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_A ≠ 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 Hnotxlt0: ¬ (x < 0).
Assume Hxlt0: x < 0.
Apply FalseE to the current goal.
We prove the intermediate claim HxRlt0: Rlt x 0.
An exact proof term for the current goal is (RltI x 0 HxR real_0 Hxlt0).
Set U to be the term halfopen_interval_left x 0.
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 0 HxR real_0).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (halfopen_interval_left_leftmem x 0 HxRlt0).
We prove the intermediate claim Hne: U ∩ ex17_17_interval_A ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ ex17_17_interval_A = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ ex17_17_interval_A.
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_A y Hy).
We prove the intermediate claim HyA: y ∈ ex17_17_interval_A.
An exact proof term for the current goal is (binintersectE2 U ex17_17_interval_A y Hy).
We prove the intermediate claim HyUprop: ¬ (Rlt y x) ∧ Rlt y 0.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z x) ∧ Rlt z 0) y HyU).
We prove the intermediate claim Hylt0: Rlt y 0.
An exact proof term for the current goal is (andER (¬ (Rlt y x)) (Rlt y 0) HyUprop).
We prove the intermediate claim HyAprop: Rlt 0 y ∧ Rlt y sqrt2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) y HyA).
We prove the intermediate claim H0lty: Rlt 0 y.
An exact proof term for the current goal is (andEL (Rlt 0 y) (Rlt y sqrt2) HyAprop).
We prove the intermediate claim H00: Rlt 0 0.
An exact proof term for the current goal is (Rlt_tra 0 y 0 H0lty Hylt0).
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) H00).
An exact proof term for the current goal is (Hne Hempty).
We prove the intermediate claim H0lex: 0 ≤ x.
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (0 ≤ x)) to the current goal.
Assume Hxlt0: x < 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnotxlt0 Hxlt0).
Assume Hx0: x = 0.
rewrite the current goal using Hx0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
Assume H0ltx: 0 < x.
An exact proof term for the current goal is (SNoLtLe 0 x H0ltx).
We prove the intermediate claim HxltS2: x < sqrt2.
Apply (SNoLt_trichotomy_or_impred x sqrt2 HxS Hs2S (x < sqrt2)) to the current goal.
Assume Hlt: x < sqrt2.
An exact proof term for the current goal is Hlt.
Assume Heq: x = sqrt2.
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 sqrt2 Hs2R 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_A ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ ex17_17_interval_A = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ ex17_17_interval_A.
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_A y Hy).
We prove the intermediate claim HyA: y ∈ ex17_17_interval_A.
An exact proof term for the current goal is (binintersectE2 U ex17_17_interval_A 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 HyAprop: Rlt 0 y ∧ Rlt y sqrt2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) y HyA).
We prove the intermediate claim HyltS2: Rlt y sqrt2.
An exact proof term for the current goal is (andER (Rlt 0 y) (Rlt y sqrt2) HyAprop).
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 HyltS2.
An exact proof term for the current goal is (Hnyx Hyltx).
An exact proof term for the current goal is (Hne Hempty).
Assume Hgt: sqrt2 < 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_A ≠ Empty.
An exact proof term for the current goal is (Hxcl U HUopen HxU).
We prove the intermediate claim Hempty: U ∩ ex17_17_interval_A = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ ex17_17_interval_A.
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_A y Hy).
We prove the intermediate claim HyA: y ∈ ex17_17_interval_A.
An exact proof term for the current goal is (binintersectE2 U ex17_17_interval_A 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 HyAprop: Rlt 0 y ∧ Rlt y sqrt2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) y HyA).
We prove the intermediate claim HyltS2R: Rlt y sqrt2.
An exact proof term for the current goal is (andER (Rlt 0 y) (Rlt y sqrt2) HyAprop).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y (SepE1 R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) y HyA)).
We prove the intermediate claim HyltS2: y < sqrt2.
An exact proof term for the current goal is (RltE_lt y sqrt2 HyltS2R).
We prove the intermediate claim Hyltx: y < x.
An exact proof term for the current goal is (SNoLt_tra y sqrt2 x HyS Hs2S HxS HyltS2 Hgt).
We prove the intermediate claim Hyltrx: Rlt y x.
An exact proof term for the current goal is (RltI y x (SepE1 R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) y HyA) 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_A_closure_lower.
An exact proof term for the current goal is (SepI R (λz : set ⇒ 0 ≤ z ∧ z < sqrt2) x HxR (andI (0 ≤ x) (x < sqrt2) H0lex HxltS2)).
∎