Let a, b, c, d and y be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Assume HdR: d ∈ R.
Assume HyK: y ∈ K_set.
Assume Hyab: y ∈ open_interval a b.
Assume Hycd: y ∈ open_interval c d.
We will prove ∃z : set, z ∈ (open_interval a b ∩ open_interval c d) ∧ z ∉ K_set.
Set I to be the term open_interval a b ∩ open_interval c d.
We prove the intermediate claim HabB: open_interval a b ∈ R_standard_basis.
We prove the intermediate claim Habfam: open_interval a b ∈ {open_interval a bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb0 : set ⇒ open_interval a bb0) b HbR).
An exact proof term for the current goal is (famunionI R (λaa0 : set ⇒ {open_interval aa0 bb|bb ∈ R}) a (open_interval a b) HaR Habfam).
We prove the intermediate claim HcdB: open_interval c d ∈ R_standard_basis.
We prove the intermediate claim Hcdfam: open_interval c d ∈ {open_interval c dd|dd ∈ R}.
An exact proof term for the current goal is (ReplI R (λdd0 : set ⇒ open_interval c dd0) d HdR).
An exact proof term for the current goal is (famunionI R (λcc0 : set ⇒ {open_interval cc0 dd|dd ∈ R}) c (open_interval c d) HcR Hcdfam).
We prove the intermediate claim Hexb3: ∃b3 ∈ R_standard_basis, y ∈ b3 ∧ b3 ⊆ I.
An exact proof term for the current goal is (basis_on_refine R R_standard_basis R_standard_basis_is_basis_local (open_interval a b) HabB (open_interval c d) HcdB y Hyab Hycd).
Apply Hexb3 to the current goal.
Let b3 be given.
Assume Hb3pair.
We prove the intermediate claim Hb3B: b3 ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (b3 ∈ R_standard_basis) (y ∈ b3 ∧ b3 ⊆ I) Hb3pair).
We prove the intermediate claim Hb3rest: y ∈ b3 ∧ b3 ⊆ I.
An exact proof term for the current goal is (andER (b3 ∈ R_standard_basis) (y ∈ b3 ∧ b3 ⊆ I) Hb3pair).
We prove the intermediate claim Hyb3: y ∈ b3.
An exact proof term for the current goal is (andEL (y ∈ b3) (b3 ⊆ I) Hb3rest).
We prove the intermediate claim Hb3subI: b3 ⊆ I.
An exact proof term for the current goal is (andER (y ∈ b3) (b3 ⊆ I) Hb3rest).
We prove the intermediate claim Hexe: ∃e ∈ R, b3 ∈ {open_interval e f|f ∈ R}.
An exact proof term for the current goal is (famunionE R (λe0 : set ⇒ {open_interval e0 f|f ∈ R}) b3 Hb3B).
Apply Hexe to the current goal.
Let e be given.
Assume Hepair.
We prove the intermediate claim HeR: e ∈ R.
An exact proof term for the current goal is (andEL (e ∈ R) (b3 ∈ {open_interval e f|f ∈ R}) Hepair).
We prove the intermediate claim Hb3fam: b3 ∈ {open_interval e f|f ∈ R}.
An exact proof term for the current goal is (andER (e ∈ R) (b3 ∈ {open_interval e f|f ∈ R}) Hepair).
We prove the intermediate claim Hexf: ∃f ∈ R, b3 = open_interval e f.
An exact proof term for the current goal is (ReplE R (λf0 : set ⇒ open_interval e f0) b3 Hb3fam).
Apply Hexf to the current goal.
Let f be given.
Assume Hfpair.
We prove the intermediate claim HfR: f ∈ R.
An exact proof term for the current goal is (andEL (f ∈ R) (b3 = open_interval e f) Hfpair).
We prove the intermediate claim Hb3eq: b3 = open_interval e f.
An exact proof term for the current goal is (andER (f ∈ R) (b3 = open_interval e f) Hfpair).
We prove the intermediate claim Hyef: y ∈ open_interval e f.
rewrite the current goal using Hb3eq (from right to left).
An exact proof term for the current goal is Hyb3.
We prove the intermediate claim Hexz: ∃z : set, z ∈ open_interval e f ∧ z ∉ K_set.
We prove the intermediate claim HyR0: y ∈ R.
An exact proof term for the current goal is (K_set_Subq_R y HyK).
We prove the intermediate claim Hypos: Rlt 0 y.
Apply (ReplE_impred (ω ∖ {0}) (λn : set ⇒ inv_nat n) y HyK (Rlt 0 y)) to the current goal.
Let n be given.
Assume HnIn: n ∈ ω ∖ {0}.
Assume Hyeq: y = inv_nat n.
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is (inv_nat_pos n HnIn).
We prove the intermediate claim HyefProp: Rlt e y ∧ Rlt y f.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt e x0 ∧ Rlt x0 f) y Hyef).
We prove the intermediate claim HyltF: Rlt y f.
An exact proof term for the current goal is (andER (Rlt e y) (Rlt y f) HyefProp).
We prove the intermediate claim HeltY: Rlt e y.
An exact proof term for the current goal is (andEL (Rlt e y) (Rlt y f) HyefProp).
Set J to be the term open_interval y f.
We prove the intermediate claim HinfJ: infinite J.
We will prove infinite J.
Assume HfinJ: finite J.
We prove the intermediate claim Hexq: ∃q ∈ rational_numbers, Rlt y q ∧ Rlt q f.
An exact proof term for the current goal is (rational_dense_between_reals y f HyR0 HfR HyltF).
Apply Hexq to the current goal.
Let q be given.
Assume Hqpair.
We prove the intermediate claim HqQ: q ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q ∈ rational_numbers) (Rlt y q ∧ Rlt q f) Hqpair).
We prove the intermediate claim Hqrest: Rlt y q ∧ Rlt q f.
An exact proof term for the current goal is (andER (q ∈ rational_numbers) (Rlt y q ∧ Rlt q f) Hqpair).
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 HqJ: q ∈ J.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt y x0 ∧ Rlt x0 f) q HqR Hqrest).
We prove the intermediate claim HJne: J ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty J q HqJ).
We prove the intermediate claim HAllSNo: ∀t ∈ J, SNo t.
Let t be given.
Assume HtJ: t ∈ J.
An exact proof term for the current goal is (real_SNo t (SepE1 R (λx0 : set ⇒ Rlt y x0 ∧ Rlt x0 f) t HtJ)).
We prove the intermediate claim Hexm: ∃m : set, SNo_max_of J m.
An exact proof term for the current goal is (finite_max_exists J (λt HtJ ⇒ HAllSNo t HtJ) HfinJ HJne).
Apply Hexm to the current goal.
Let m be given.
Assume Hmmax: SNo_max_of J m.
We prove the intermediate claim Hmconj1: m ∈ J ∧ SNo m.
An exact proof term for the current goal is (andEL (m ∈ J ∧ SNo m) (∀t ∈ J, SNo t → t ≤ m) Hmmax).
We prove the intermediate claim HmJ: m ∈ J.
An exact proof term for the current goal is (andEL (m ∈ J) (SNo m) Hmconj1).
We prove the intermediate claim HmS: SNo m.
An exact proof term for the current goal is (andER (m ∈ J) (SNo m) Hmconj1).
We prove the intermediate claim Hmmaxprop: ∀t ∈ J, SNo t → t ≤ m.
An exact proof term for the current goal is (andER (m ∈ J ∧ SNo m) (∀t ∈ J, SNo t → t ≤ m) Hmmax).
We prove the intermediate claim HmR: m ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt y x0 ∧ Rlt x0 f) m HmJ).
We prove the intermediate claim HmProp: Rlt y m ∧ Rlt m f.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt y x0 ∧ Rlt x0 f) m HmJ).
We prove the intermediate claim HmltF: Rlt m f.
An exact proof term for the current goal is (andER (Rlt y m) (Rlt m f) HmProp).
We prove the intermediate claim Hexq2: ∃q2 ∈ rational_numbers, Rlt m q2 ∧ Rlt q2 f.
An exact proof term for the current goal is (rational_dense_between_reals m f HmR HfR HmltF).
Apply Hexq2 to the current goal.
Let q2 be given.
Assume Hq2pair.
We prove the intermediate claim Hq2Q: q2 ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q2 ∈ rational_numbers) (Rlt m q2 ∧ Rlt q2 f) Hq2pair).
We prove the intermediate claim Hq2rest: Rlt m q2 ∧ Rlt q2 f.
An exact proof term for the current goal is (andER (q2 ∈ rational_numbers) (Rlt m q2 ∧ Rlt q2 f) Hq2pair).
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 Hmq2: Rlt m q2.
An exact proof term for the current goal is (andEL (Rlt m q2) (Rlt q2 f) Hq2rest).
We prove the intermediate claim Hq2ltF: Rlt q2 f.
An exact proof term for the current goal is (andER (Rlt m q2) (Rlt q2 f) Hq2rest).
We prove the intermediate claim Hylm: Rlt y m.
An exact proof term for the current goal is (andEL (Rlt y m) (Rlt m f) HmProp).
We prove the intermediate claim Hylq2: Rlt y q2.
An exact proof term for the current goal is (Rlt_tra y m q2 Hylm Hmq2).
We prove the intermediate claim Hq2J: q2 ∈ J.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt y x0 ∧ Rlt x0 f) q2 Hq2R (andI (Rlt y q2) (Rlt q2 f) Hylq2 Hq2ltF)).
We prove the intermediate claim Hq2S: SNo q2.
An exact proof term for the current goal is (real_SNo q2 Hq2R).
We prove the intermediate claim Hq2le: q2 ≤ m.
An exact proof term for the current goal is (Hmmaxprop q2 Hq2J Hq2S).
We prove the intermediate claim Hmq2lt: m < q2.
An exact proof term for the current goal is (RltE_lt m q2 Hmq2).
We prove the intermediate claim HmLtM: m < m.
An exact proof term for the current goal is (SNoLtLe_tra m q2 m HmS Hq2S HmS Hmq2lt Hq2le).
An exact proof term for the current goal is ((SNoLt_irref m) HmLtM).
Set F to be the term K_set ∩ J.
Set V to be the term {t ∈ R|Rlt y t}.
We prove the intermediate claim HVfin: finite (K_set ∩ V).
An exact proof term for the current goal is (K_set_above_positive_bound_finite y HyR0 Hypos).
We prove the intermediate claim HFsub: F ⊆ (K_set ∩ V).
Let t be given.
Assume HtF: t ∈ F.
We prove the intermediate claim HtK: t ∈ K_set.
An exact proof term for the current goal is (binintersectE1 K_set J t HtF).
We prove the intermediate claim HtJ: t ∈ J.
An exact proof term for the current goal is (binintersectE2 K_set J t HtF).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt y x0 ∧ Rlt x0 f) t HtJ).
We prove the intermediate claim HtProp: Rlt y t ∧ Rlt t f.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt y x0 ∧ Rlt x0 f) t HtJ).
We prove the intermediate claim HyltT: Rlt y t.
An exact proof term for the current goal is (andEL (Rlt y t) (Rlt t f) HtProp).
We prove the intermediate claim HtV: t ∈ V.
An exact proof term for the current goal is (SepI R (λt0 : set ⇒ Rlt y t0) t HtR HyltT).
An exact proof term for the current goal is (binintersectI K_set V t HtK HtV).
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (Subq_finite (K_set ∩ V) HVfin F HFsub).
We prove the intermediate claim Hexw: ∃z : set, z ∈ J ∖ F.
An exact proof term for the current goal is (infinite_setminus_finite_nonempty J F HinfJ HFfin).
Apply Hexw to the current goal.
Let z be given.
Assume HzJF: z ∈ J ∖ F.
We prove the intermediate claim HzJ: z ∈ J.
An exact proof term for the current goal is (setminusE1 J F z HzJF).
We prove the intermediate claim HznotF: z ∉ F.
An exact proof term for the current goal is (setminusE2 J F z HzJF).
We prove the intermediate claim HzR: z ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt y x0 ∧ Rlt x0 f) z HzJ).
We prove the intermediate claim HzProp: Rlt y z ∧ Rlt z f.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt y x0 ∧ Rlt x0 f) z HzJ).
We prove the intermediate claim HyltZ: Rlt y z.
An exact proof term for the current goal is (andEL (Rlt y z) (Rlt z f) HzProp).
We prove the intermediate claim HzltF: Rlt z f.
An exact proof term for the current goal is (andER (Rlt y z) (Rlt z f) HzProp).
We prove the intermediate claim HznotK: z ∉ K_set.
Assume HzK: z ∈ K_set.
We prove the intermediate claim HzF: z ∈ F.
An exact proof term for the current goal is (binintersectI K_set J z HzK HzJ).
An exact proof term for the current goal is (HznotF HzF).
We prove the intermediate claim Helz: Rlt e z.
An exact proof term for the current goal is (Rlt_tra e y z HeltY HyltZ).
We use z to witness the existential quantifier.
Apply andI to the current goal.
We will prove z ∈ open_interval e f.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt e x0 ∧ Rlt x0 f) z HzR (andI (Rlt e z) (Rlt z f) Helz HzltF)).
An exact proof term for the current goal is HznotK.
Apply Hexz to the current goal.
Let z be given.
Assume Hzpair.
We prove the intermediate claim Hzef: z ∈ open_interval e f.
An exact proof term for the current goal is (andEL (z ∈ open_interval e f) (z ∉ K_set) Hzpair).
We prove the intermediate claim HznotK: z ∉ K_set.
An exact proof term for the current goal is (andER (z ∈ open_interval e f) (z ∉ K_set) Hzpair).
We prove the intermediate claim Hzb3: z ∈ b3.
rewrite the current goal using Hb3eq (from left to right).
An exact proof term for the current goal is Hzef.
We prove the intermediate claim HzI: z ∈ I.
An exact proof term for the current goal is (Hb3subI z Hzb3).
We use z to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HzI.
An exact proof term for the current goal is HznotK.
∎