Let seq be given.
Assume Hseq: sequence_on seq R.
Assume HabC: ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < eps.
We prove the intermediate claim H1pair: 1 ∈ R ∧ Rlt 0 1.
Apply andI to the current goal.
An exact proof term for the current goal is real_1.
An exact proof term for the current goal is Rlt_0_1.
Apply (HabC 1 H1pair) to the current goal.
Let N0 be given.
Assume HN0pair.
We prove the intermediate claim HN0omega: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < 1) HN0pair).
We prove the intermediate claim Htail1: ∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < 1.
An exact proof term for the current goal is (andER (N0 ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < 1) HN0pair).
We prove the intermediate claim Hx0R: apply_fun seq N0 ∈ R.
An exact proof term for the current goal is (Hseq N0 HN0omega).
Set u to be the term add_SNo 1 (apply_fun seq N0).
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (apply_fun seq N0) Hx0R).
Set A to be the term {x ∈ R|∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rle x (apply_fun seq n)}.
We prove the intermediate claim HAinR: ∀x : set, x ∈ A → x ∈ R.
Let x be given.
Assume HxA: x ∈ A.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rle x0 (apply_fun seq n)) x HxA).
We prove the intermediate claim HAnen: ∃a0 : set, a0 ∈ A.
Set a0 to be the term add_SNo (minus_SNo 1) (apply_fun seq N0).
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo 1) (real_minus_SNo 1 real_1) (apply_fun seq N0) Hx0R).
We use a0 to witness the existential quantifier.
Apply (SepI R (λx0 : set ⇒ ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rle x0 (apply_fun seq n)) a0 Ha0R) to the current goal.
We use N0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN0omega.
Let n be given.
Assume HnO: n ∈ ω.
Assume HN0subn: N0 ⊆ n.
We prove the intermediate claim Habslt1: abs_SNo (add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq N0))) < 1.
An exact proof term for the current goal is (Htail1 n N0 HnO HN0omega HN0subn (Subq_ref N0)).
We prove the intermediate claim HnR: apply_fun seq n ∈ R.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim HnS: SNo (apply_fun seq n).
An exact proof term for the current goal is (real_SNo (apply_fun seq n) HnR).
We prove the intermediate claim Hx0S: SNo (apply_fun seq N0).
An exact proof term for the current goal is (real_SNo (apply_fun seq N0) Hx0R).
We prove the intermediate claim HmS: SNo (minus_SNo (apply_fun seq N0)).
An exact proof term for the current goal is (SNo_minus_SNo (apply_fun seq N0) Hx0S).
Set t to be the term add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq N0)).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (SNo_add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq N0)) HnS HmS).
We prove the intermediate claim Hneglt1: minus_SNo t < 1.
An exact proof term for the current goal is (abs_SNo_lt_imp_neg_lt t 1 HtS SNo_1 SNoLt_0_1 Habslt1).
We prove the intermediate claim Hm1lt: minus_SNo 1 < t.
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim HmmtS: SNo (minus_SNo (minus_SNo t)).
An exact proof term for the current goal is (SNo_minus_SNo (minus_SNo t) HmtS).
We prove the intermediate claim Hinv1: add_SNo (minus_SNo (minus_SNo t)) (minus_SNo t) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv (minus_SNo t) HmtS).
We prove the intermediate claim Hinv2: add_SNo t (minus_SNo t) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv t HtS).
We prove the intermediate claim Hnegneg: minus_SNo (minus_SNo t) = t.
We prove the intermediate claim Heq: add_SNo (minus_SNo (minus_SNo t)) (minus_SNo t) = add_SNo t (minus_SNo t).
rewrite the current goal using Hinv1 (from left to right).
rewrite the current goal using Hinv2 (from left to right).
Use reflexivity.
An exact proof term for the current goal is (add_SNo_cancel_R (minus_SNo (minus_SNo t)) (minus_SNo t) t HmmtS HmtS HtS Heq).
We prove the intermediate claim Hm1lt2: minus_SNo 1 < minus_SNo (minus_SNo t).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo t) 1 HmtS SNo_1 Hneglt1).
rewrite the current goal using Hnegneg (from right to left).
An exact proof term for the current goal is Hm1lt2.
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim Htlt: add_SNo (minus_SNo 1) (apply_fun seq N0) < apply_fun seq n.
An exact proof term for the current goal is (add_SNo_minus_Lt2 (apply_fun seq n) (apply_fun seq N0) (minus_SNo 1) HnS Hx0S Hm1S Hm1lt).
An exact proof term for the current goal is (Rlt_implies_Rle a0 (apply_fun seq n) (RltI a0 (apply_fun seq n) Ha0R HnR Htlt)).
We prove the intermediate claim HtailLeU: ∀n : set, n ∈ ω → N0 ⊆ n → Rle (apply_fun seq n) u.
Let n be given.
Assume HnO: n ∈ ω.
Assume HN0subn: N0 ⊆ n.
We prove the intermediate claim Habslt1: abs_SNo (add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq N0))) < 1.
An exact proof term for the current goal is (Htail1 n N0 HnO HN0omega HN0subn (Subq_ref N0)).
We prove the intermediate claim HnR: apply_fun seq n ∈ R.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim HnS: SNo (apply_fun seq n).
An exact proof term for the current goal is (real_SNo (apply_fun seq n) HnR).
We prove the intermediate claim Hx0S: SNo (apply_fun seq N0).
An exact proof term for the current goal is (real_SNo (apply_fun seq N0) Hx0R).
We prove the intermediate claim HmS: SNo (minus_SNo (apply_fun seq N0)).
An exact proof term for the current goal is (SNo_minus_SNo (apply_fun seq N0) Hx0S).
Set t to be the term add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq N0)).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (SNo_add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq N0)) HnS HmS).
We prove the intermediate claim Htlt1: t < 1.
An exact proof term for the current goal is (abs_SNo_lt_imp_lt t 1 HtS SNo_1 SNoLt_0_1 Habslt1).
We prove the intermediate claim Htltu: apply_fun seq n < u.
An exact proof term for the current goal is (add_SNo_minus_Lt1 (apply_fun seq n) (apply_fun seq N0) 1 HnS Hx0S SNo_1 Htlt1).
We prove the intermediate claim HxRlt: Rlt (apply_fun seq n) u.
An exact proof term for the current goal is (RltI (apply_fun seq n) u HnR HuR Htltu).
An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun seq n) u HxRlt).
We prove the intermediate claim HubExists: ∃u0 : set, u0 ∈ R ∧ ∀x : set, x ∈ A → x ∈ R → Rle x u0.
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HuR.
Let x be given.
Assume HxA: x ∈ A.
Assume HxR: x ∈ R.
We prove the intermediate claim Hxprop: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rle x (apply_fun seq n).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rle x0 (apply_fun seq n)) x HxA).
Apply Hxprop to the current goal.
Let N be given.
Assume HNpair2.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → Rle x (apply_fun seq n)) HNpair2).
We prove the intermediate claim HNtail: ∀n : set, n ∈ ω → N ⊆ n → Rle x (apply_fun seq n).
An exact proof term for the current goal is (andER (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → Rle x (apply_fun seq n)) HNpair2).
Set n0 to be the term ordsucc (N ∪ N0).
We prove the intermediate claim HmaxO: N ∪ N0 ∈ ω.
An exact proof term for the current goal is (omega_binunion N N0 HNomega HN0omega).
We prove the intermediate claim Hn0O: n0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc (N ∪ N0) HmaxO).
We prove the intermediate claim HNsubn0: N ⊆ n0.
Let t be given.
Assume Ht: t ∈ N.
We prove the intermediate claim Htmax: t ∈ (N ∪ N0).
An exact proof term for the current goal is (binunionI1 N N0 t Ht).
An exact proof term for the current goal is (ordsuccI1 (N ∪ N0) t Htmax).
We prove the intermediate claim HN0subn0: N0 ⊆ n0.
Let t be given.
Assume Ht: t ∈ N0.
We prove the intermediate claim Htmax: t ∈ (N ∪ N0).
An exact proof term for the current goal is (binunionI2 N N0 t Ht).
An exact proof term for the current goal is (ordsuccI1 (N ∪ N0) t Htmax).
We prove the intermediate claim Hxlen0: Rle x (apply_fun seq n0).
An exact proof term for the current goal is (HNtail n0 Hn0O HNsubn0).
We prove the intermediate claim Hn0leu: Rle (apply_fun seq n0) u.
An exact proof term for the current goal is (HtailLeU n0 Hn0O HN0subn0).
An exact proof term for the current goal is (Rle_tra x (apply_fun seq n0) u Hxlen0 Hn0leu).
Apply (R_lub_exists A HAnen HAinR HubExists) to the current goal.
Let l be given.
Assume Hlub: R_lub A l.
We use l to witness the existential quantifier.
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (R_lub_in_R A l Hlub).
We will prove converges_to R R_standard_topology seq l.
We will prove topology_on R R_standard_topology ∧ sequence_on seq R ∧ l ∈ R ∧ ∀U : set, U ∈ R_standard_topology → l ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
An exact proof term for the current goal is Hseq.
An exact proof term for the current goal is HlR.
Let U be given.
Assume HU: U ∈ R_standard_topology.
Assume HlU: l ∈ U.
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b ∈ R_standard_basis, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ R_standard_basis, x0 ∈ b ∧ b ⊆ U0) U HU).
Apply (HUprop l HlU) to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (b ∈ R_standard_basis) (l ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hlbsub: l ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ R_standard_basis) (l ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hlb: l ∈ b.
An exact proof term for the current goal is (andEL (l ∈ b) (b ⊆ U) Hlbsub).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (l ∈ b) (b ⊆ U) Hlbsub).
We prove the intermediate claim Hexa: ∃a ∈ R, b ∈ {open_interval a c|c ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 c|c ∈ R}) b HbB).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (b ∈ {open_interval a c|c ∈ R}) Hapair).
We prove the intermediate claim Hbfam: b ∈ {open_interval a c|c ∈ R}.
An exact proof term for the current goal is (andER (a ∈ R) (b ∈ {open_interval a c|c ∈ R}) Hapair).
We prove the intermediate claim Hexc: ∃c ∈ R, b = open_interval a c.
An exact proof term for the current goal is (ReplE R (λc0 : set ⇒ open_interval a c0) b Hbfam).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpair.
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (b = open_interval a c) Hcpair).
We prove the intermediate claim Hbeq: b = open_interval a c.
An exact proof term for the current goal is (andER (c ∈ R) (b = open_interval a c) Hcpair).
We prove the intermediate claim HlInt: l ∈ open_interval a c.
rewrite the current goal using Hbeq (from right to left) at position 1.
An exact proof term for the current goal is Hlb.
We prove the intermediate claim Hltac: Rlt a l ∧ Rlt l c.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 c) l HlInt).
We prove the intermediate claim Hlta: Rlt a l.
An exact proof term for the current goal is (andEL (Rlt a l) (Rlt l c) Hltac).
We prove the intermediate claim Hltlc: Rlt l c.
An exact proof term for the current goal is (andER (Rlt a l) (Rlt l c) Hltac).
We prove the intermediate claim Hlubcore: l ∈ R ∧ ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l) (∀u0 : set, u0 ∈ R → (∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 u0) → Rle l u0) Hlub).
We prove the intermediate claim HubA: ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l.
An exact proof term for the current goal is (andER (l ∈ R) (∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l) Hlubcore).
We prove the intermediate claim HexLower: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt a (apply_fun seq n).
We prove the intermediate claim HaR2: a ∈ R.
An exact proof term for the current goal is HaR.
We prove the intermediate claim HlR2: l ∈ R.
An exact proof term for the current goal is HlR.
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR2).
We prove the intermediate claim HlS: SNo l.
An exact proof term for the current goal is (real_SNo l HlR2).
We prove the intermediate claim HaltlS: a < l.
An exact proof term for the current goal is (RltE_lt a l Hlta).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim HdiffR: add_SNo l (minus_SNo a) ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR2 (minus_SNo a) (real_minus_SNo a HaR2)).
We prove the intermediate claim H0ltdS: 0 < add_SNo (minus_SNo a) l.
We prove the intermediate claim H0lt: add_SNo (minus_SNo a) a < add_SNo (minus_SNo a) l.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo a) a l HmaS HaS HlS HaltlS).
rewrite the current goal using (add_SNo_minus_SNo_linv a HaS) (from right to left) at position 1.
An exact proof term for the current goal is H0lt.
We prove the intermediate claim H0ltdS2: 0 < add_SNo l (minus_SNo a).
We prove the intermediate claim Hcom: add_SNo (minus_SNo a) l = add_SNo l (minus_SNo a).
An exact proof term for the current goal is (add_SNo_com (minus_SNo a) l HmaS HlS).
rewrite the current goal using Hcom (from right to left).
An exact proof term for the current goal is H0ltdS.
We prove the intermediate claim Hdpos: Rlt 0 (add_SNo l (minus_SNo a)).
An exact proof term for the current goal is (RltI 0 (add_SNo l (minus_SNo a)) real_0 HdiffR H0ltdS2).
We prove the intermediate claim Hexeps: ∃Neps ∈ ω, eps_ Neps < add_SNo l (minus_SNo a).
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid (add_SNo l (minus_SNo a)) HdiffR Hdpos).
Apply Hexeps to the current goal.
Let Neps be given.
Assume HNepspair.
We prove the intermediate claim HNepsO: Neps ∈ ω.
An exact proof term for the current goal is (andEL (Neps ∈ ω) (eps_ Neps < add_SNo l (minus_SNo a)) HNepspair).
We prove the intermediate claim Hepslt: eps_ Neps < add_SNo l (minus_SNo a).
An exact proof term for the current goal is (andER (Neps ∈ ω) (eps_ Neps < add_SNo l (minus_SNo a)) HNepspair).
We prove the intermediate claim HepsR: eps_ Neps ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ Neps) (SNo_eps_SNoS_omega Neps HNepsO)).
We prove the intermediate claim HepsposS: 0 < eps_ Neps.
An exact proof term for the current goal is (SNo_eps_pos Neps HNepsO).
We prove the intermediate claim HepsposR: Rlt 0 (eps_ Neps).
An exact proof term for the current goal is (RltI 0 (eps_ Neps) real_0 HepsR HepsposS).
We prove the intermediate claim HepsS: SNo (eps_ Neps).
An exact proof term for the current goal is (real_SNo (eps_ Neps) HepsR).
We prove the intermediate claim Hu0R: add_SNo l (minus_SNo (eps_ Neps)) ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR2 (minus_SNo (eps_ Neps)) (real_minus_SNo (eps_ Neps) HepsR)).
We prove the intermediate claim Hsumlt1: add_SNo (eps_ Neps) a < l.
An exact proof term for the current goal is (add_SNo_minus_Lt2 l a (eps_ Neps) HlS HaS HepsS Hepslt).
We prove the intermediate claim Hsumlt2: add_SNo a (eps_ Neps) < l.
rewrite the current goal using (add_SNo_com a (eps_ Neps) HaS HepsS) (from left to right).
An exact proof term for the current goal is Hsumlt1.
We prove the intermediate claim Haltu0S: a < add_SNo l (minus_SNo (eps_ Neps)).
An exact proof term for the current goal is (add_SNo_minus_Lt2b l (eps_ Neps) a HlS HepsS HaS Hsumlt2).
We prove the intermediate claim Haltu0R: Rlt a (add_SNo l (minus_SNo (eps_ Neps))).
An exact proof term for the current goal is (RltI a (add_SNo l (minus_SNo (eps_ Neps))) HaR2 Hu0R Haltu0S).
We prove the intermediate claim HexAbove: ∃x0 : set, x0 ∈ A ∧ x0 ∈ R ∧ Rlt (add_SNo l (minus_SNo (eps_ Neps))) x0.
An exact proof term for the current goal is (R_lub_approx_from_below A l (eps_ Neps) Hlub HepsR HepsposR).
Apply HexAbove to the current goal.
Let x0 be given.
Assume Hx0pack.
We prove the intermediate claim Hx0pair: x0 ∈ A ∧ x0 ∈ R.
An exact proof term for the current goal is (andEL (x0 ∈ A ∧ x0 ∈ R) (Rlt (add_SNo l (minus_SNo (eps_ Neps))) x0) Hx0pack).
We prove the intermediate claim Hltu0x0: Rlt (add_SNo l (minus_SNo (eps_ Neps))) x0.
An exact proof term for the current goal is (andER (x0 ∈ A ∧ x0 ∈ R) (Rlt (add_SNo l (minus_SNo (eps_ Neps))) x0) Hx0pack).
We prove the intermediate claim Hx0A: x0 ∈ A.
An exact proof term for the current goal is (andEL (x0 ∈ A) (x0 ∈ R) Hx0pair).
We prove the intermediate claim Hx0R: x0 ∈ R.
An exact proof term for the current goal is (andER (x0 ∈ A) (x0 ∈ R) Hx0pair).
We prove the intermediate claim Haltax0: Rlt a x0.
An exact proof term for the current goal is (Rlt_tra a (add_SNo l (minus_SNo (eps_ Neps))) x0 Haltu0R Hltu0x0).
We prove the intermediate claim Hx0prop: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rle x0 (apply_fun seq n).
An exact proof term for the current goal is (SepE2 R (λx1 : set ⇒ ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rle x1 (apply_fun seq n)) x0 Hx0A).
Apply Hx0prop to the current goal.
Let N be given.
Assume HNpair3.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → Rle x0 (apply_fun seq n)) HNpair3).
Let n be given.
Assume HnO: n ∈ ω.
Assume HNsubn: N ⊆ n.
We prove the intermediate claim Hx0len: Rle x0 (apply_fun seq n).
An exact proof term for the current goal is (andER (N ∈ ω) (∀n0 : set, n0 ∈ ω → N ⊆ n0 → Rle x0 (apply_fun seq n0)) HNpair3 n HnO HNsubn).
An exact proof term for the current goal is (Rlt_Rle_tra a x0 (apply_fun seq n) Haltax0 Hx0len).
We prove the intermediate claim HexUpper: ∃Nhi : set, Nhi ∈ ω ∧ ∀n : set, n ∈ ω → Nhi ⊆ n → Rlt (apply_fun seq n) c.
We prove the intermediate claim HlR2: l ∈ R.
An exact proof term for the current goal is HlR.
We prove the intermediate claim HcR2: c ∈ R.
An exact proof term for the current goal is HcR.
We prove the intermediate claim HlS: SNo l.
An exact proof term for the current goal is (real_SNo l HlR2).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR2).
Set gap to be the term add_SNo c (minus_SNo l).
We prove the intermediate claim HgapR: gap ∈ R.
An exact proof term for the current goal is (real_add_SNo c HcR2 (minus_SNo l) (real_minus_SNo l HlR2)).
We prove the intermediate claim HmlS: SNo (minus_SNo l).
An exact proof term for the current goal is (SNo_minus_SNo l HlS).
We prove the intermediate claim H0lt_gapS: 0 < add_SNo (minus_SNo l) c.
We prove the intermediate claim HltS: l < c.
An exact proof term for the current goal is (RltE_lt l c Hltlc).
We prove the intermediate claim H0lt: add_SNo (minus_SNo l) l < add_SNo (minus_SNo l) c.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo l) l c HmlS HlS HcS HltS).
rewrite the current goal using (add_SNo_minus_SNo_linv l HlS) (from right to left) at position 1.
An exact proof term for the current goal is H0lt.
We prove the intermediate claim H0lt_gapS2: 0 < gap.
rewrite the current goal using (add_SNo_com (minus_SNo l) c HmlS HcS) (from right to left) at position 1.
An exact proof term for the current goal is H0lt_gapS.
We prove the intermediate claim HgapPos: Rlt 0 gap.
An exact proof term for the current goal is (RltI 0 gap real_0 HgapR H0lt_gapS2).
We prove the intermediate claim Hexd: ∃Nd ∈ ω, eps_ Nd < gap.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid gap HgapR HgapPos).
Apply Hexd to the current goal.
Let Nd be given.
Assume HNdPair.
We prove the intermediate claim HNdO: Nd ∈ ω.
An exact proof term for the current goal is (andEL (Nd ∈ ω) (eps_ Nd < gap) HNdPair).
We prove the intermediate claim HdltGapS: eps_ Nd < gap.
An exact proof term for the current goal is (andER (Nd ∈ ω) (eps_ Nd < gap) HNdPair).
Set d to be the term eps_ Nd.
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (SNoS_omega_real d (SNo_eps_SNoS_omega Nd HNdO)).
We prove the intermediate claim HdposS: 0 < d.
An exact proof term for the current goal is (SNo_eps_pos Nd HNdO).
We prove the intermediate claim Hdpos: Rlt 0 d.
An exact proof term for the current goal is (RltI 0 d real_0 HdR HdposS).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
We prove the intermediate claim HmdR: minus_SNo d ∈ R.
An exact proof term for the current goal is (real_minus_SNo d HdR).
We prove the intermediate claim HmdS: SNo (minus_SNo d).
An exact proof term for the current goal is (SNo_minus_SNo d HdS).
We prove the intermediate claim HcdR: add_SNo c (minus_SNo d) ∈ R.
An exact proof term for the current goal is (real_add_SNo c HcR2 (minus_SNo d) HmdR).
We prove the intermediate claim HdltGapR: Rlt d gap.
An exact proof term for the current goal is (RltI d gap HdR HgapR HdltGapS).
We prove the intermediate claim HdltGapS2: d < gap.
An exact proof term for the current goal is (RltE_lt d gap HdltGapR).
We prove the intermediate claim Hdl_lt_c: add_SNo d l < c.
An exact proof term for the current goal is (add_SNo_minus_Lt2 c l d HcS HlS HdS HdltGapS2).
We prove the intermediate claim Hld_lt_c: add_SNo l d < c.
rewrite the current goal using (add_SNo_com d l HdS HlS) (from right to left) at position 1.
An exact proof term for the current goal is Hdl_lt_c.
We prove the intermediate claim Hlt_l_cdS: l < add_SNo c (minus_SNo d).
An exact proof term for the current goal is (add_SNo_minus_Lt2b c d l HcS HdS HlS Hld_lt_c).
We prove the intermediate claim Hlt_l_cd: Rlt l (add_SNo c (minus_SNo d)).
An exact proof term for the current goal is (RltI l (add_SNo c (minus_SNo d)) HlR2 HcdR Hlt_l_cdS).
We prove the intermediate claim HexN0: ∃N0 : set, N0 ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < d.
An exact proof term for the current goal is (HabC d (andI (d ∈ R) (Rlt 0 d) HdR Hdpos)).
Apply HexN0 to the current goal.
Let N0 be given.
Assume HN0pair.
We prove the intermediate claim HN0omega2: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < d) HN0pair).
We prove the intermediate claim HN0tail: ∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < d.
An exact proof term for the current goal is (andER (N0 ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < d) HN0pair).
We prove the intermediate claim Hx0R2: apply_fun seq N0 ∈ R.
An exact proof term for the current goal is (Hseq N0 HN0omega2).
We use N0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < d) HN0pair).
Let n be given.
Assume HnO: n ∈ ω.
Assume HN0subn: N0 ⊆ n.
We will prove Rlt (apply_fun seq n) c.
We prove the intermediate claim HnR: apply_fun seq n ∈ R.
An exact proof term for the current goal is (Hseq n HnO).
Apply xm (Rlt (apply_fun seq n) c) to the current goal.
Assume Hlt: Rlt (apply_fun seq n) c.
An exact proof term for the current goal is Hlt.
Assume Hnlt: ¬ (Rlt (apply_fun seq n) c).
We prove the intermediate claim HcLeN: Rle c (apply_fun seq n).
An exact proof term for the current goal is (RleI c (apply_fun seq n) HcR2 HnR Hnlt).
We prove the intermediate claim HcdA: add_SNo c (minus_SNo d) ∈ A.
Apply (SepI R (λx0 : set ⇒ ∃N : set, N ∈ ω ∧ ∀n0 : set, n0 ∈ ω → N ⊆ n0 → Rle x0 (apply_fun seq n0)) (add_SNo c (minus_SNo d)) HcdR) to the current goal.
We use N0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN0omega2.
Let m be given.
Assume HmO: m ∈ ω.
Assume HN0subm: N0 ⊆ m.
We prove the intermediate claim Habmn: abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < d.
An exact proof term for the current goal is (HN0tail m n HmO HnO HN0subm HN0subn).
We prove the intermediate claim HmR: apply_fun seq m ∈ R.
An exact proof term for the current goal is (Hseq m HmO).
We prove the intermediate claim HmS: SNo (apply_fun seq m).
An exact proof term for the current goal is (real_SNo (apply_fun seq m) HmR).
We prove the intermediate claim HnS: SNo (apply_fun seq n).
An exact proof term for the current goal is (real_SNo (apply_fun seq n) HnR).
We prove the intermediate claim HabsSwap: abs_SNo (add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq m))) = abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))).
An exact proof term for the current goal is (abs_SNo_dist_swap (apply_fun seq n) (apply_fun seq m) HnS HmS).
We prove the intermediate claim Habnm: abs_SNo (add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq m))) < d.
rewrite the current goal using HabsSwap (from left to right).
An exact proof term for the current goal is Habmn.
We prove the intermediate claim HtS: SNo (add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq m))).
An exact proof term for the current goal is (SNo_add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq m)) HnS (SNo_minus_SNo (apply_fun seq m) HmS)).
We prove the intermediate claim Hnm_lt_d: add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq m)) < d.
An exact proof term for the current goal is (abs_SNo_lt_imp_lt (add_SNo (apply_fun seq n) (minus_SNo (apply_fun seq m))) d HtS HdS HdposS Habnm).
We prove the intermediate claim Hn_lt_dm: apply_fun seq n < add_SNo d (apply_fun seq m).
An exact proof term for the current goal is (add_SNo_minus_Lt1 (apply_fun seq n) (apply_fun seq m) d HnS HmS HdS Hnm_lt_d).
We prove the intermediate claim Hn_lt_md: apply_fun seq n < add_SNo (apply_fun seq m) d.
rewrite the current goal using (add_SNo_com d (apply_fun seq m) HdS HmS) (from right to left) at position 1.
An exact proof term for the current goal is Hn_lt_dm.
We prove the intermediate claim Hnmd_lt_m: add_SNo (apply_fun seq n) (minus_SNo d) < apply_fun seq m.
An exact proof term for the current goal is (add_SNo_minus_Lt1b (apply_fun seq n) d (apply_fun seq m) HnS HdS HmS Hn_lt_md).
We prove the intermediate claim HnmdR: add_SNo (apply_fun seq n) (minus_SNo d) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun seq n) HnR (minus_SNo d) HmdR).
We prove the intermediate claim Hnmd_lt_mR: Rlt (add_SNo (apply_fun seq n) (minus_SNo d)) (apply_fun seq m).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun seq n) (minus_SNo d)) (apply_fun seq m) HnmdR HmR Hnmd_lt_m).
We prove the intermediate claim HcdLeNmd: Rle (add_SNo c (minus_SNo d)) (add_SNo (apply_fun seq n) (minus_SNo d)).
We prove the intermediate claim Hleft: Rle (add_SNo (minus_SNo d) c) (add_SNo (minus_SNo d) (apply_fun seq n)).
An exact proof term for the current goal is (Rle_add_SNo_2 (minus_SNo d) c (apply_fun seq n) HmdR HcR2 HnR HcLeN).
rewrite the current goal using (add_SNo_com (minus_SNo d) c HmdS HcS) (from right to left) at position 1.
rewrite the current goal using (add_SNo_com (minus_SNo d) (apply_fun seq n) HmdS HnS) (from right to left) at position 1.
An exact proof term for the current goal is Hleft.
We prove the intermediate claim Hcdltm: Rlt (add_SNo c (minus_SNo d)) (apply_fun seq m).
An exact proof term for the current goal is (Rle_Rlt_tra (add_SNo c (minus_SNo d)) (add_SNo (apply_fun seq n) (minus_SNo d)) (apply_fun seq m) HcdLeNmd Hnmd_lt_mR).
An exact proof term for the current goal is (Rlt_implies_Rle (add_SNo c (minus_SNo d)) (apply_fun seq m) Hcdltm).
We prove the intermediate claim HcdLeL: Rle (add_SNo c (minus_SNo d)) l.
An exact proof term for the current goal is (HubA (add_SNo c (minus_SNo d)) HcdA HcdR).
We prove the intermediate claim Hnlt2: ¬ (Rlt l (add_SNo c (minus_SNo d))).
An exact proof term for the current goal is (RleE_nlt (add_SNo c (minus_SNo d)) l HcdLeL).
An exact proof term for the current goal is (FalseE (Hnlt2 Hlt_l_cd) (Rlt (apply_fun seq n) c)).
Apply HexLower to the current goal.
Let Nlow be given.
Assume HNlowpair.
Apply HexUpper to the current goal.
Let Nhi be given.
Assume HNhipair.
Set N to be the term ordsucc (Nlow ∪ Nhi).
We use N to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hmax: Nlow ∪ Nhi ∈ ω.
An exact proof term for the current goal is (omega_binunion Nlow Nhi (andEL (Nlow ∈ ω) (∀n : set, n ∈ ω → Nlow ⊆ n → Rlt a (apply_fun seq n)) HNlowpair) (andEL (Nhi ∈ ω) (∀n : set, n ∈ ω → Nhi ⊆ n → Rlt (apply_fun seq n) c) HNhipair)).
An exact proof term for the current goal is (omega_ordsucc (Nlow ∪ Nhi) Hmax).
Let n be given.
Assume HnO: n ∈ ω.
Assume HNsub: N ⊆ n.
We will prove apply_fun seq n ∈ U.
We prove the intermediate claim HNlowSubn: Nlow ⊆ n.
Let t be given.
Assume Ht: t ∈ Nlow.
We prove the intermediate claim HtN: t ∈ N.
We prove the intermediate claim Htmax: t ∈ (Nlow ∪ Nhi).
An exact proof term for the current goal is (binunionI1 Nlow Nhi t Ht).
An exact proof term for the current goal is (ordsuccI1 (Nlow ∪ Nhi) t Htmax).
An exact proof term for the current goal is (HNsub t HtN).
We prove the intermediate claim HNhiSubn: Nhi ⊆ n.
Let t be given.
Assume Ht: t ∈ Nhi.
We prove the intermediate claim HtN: t ∈ N.
We prove the intermediate claim Htmax: t ∈ (Nlow ∪ Nhi).
An exact proof term for the current goal is (binunionI2 Nlow Nhi t Ht).
An exact proof term for the current goal is (ordsuccI1 (Nlow ∪ Nhi) t Htmax).
An exact proof term for the current goal is (HNsub t HtN).
We prove the intermediate claim HltA: Rlt a (apply_fun seq n).
An exact proof term for the current goal is ((andER (Nlow ∈ ω) (∀n0 : set, n0 ∈ ω → Nlow ⊆ n0 → Rlt a (apply_fun seq n0)) HNlowpair) n HnO HNlowSubn).
We prove the intermediate claim HltC: Rlt (apply_fun seq n) c.
An exact proof term for the current goal is ((andER (Nhi ∈ ω) (∀n0 : set, n0 ∈ ω → Nhi ⊆ n0 → Rlt (apply_fun seq n0) c) HNhipair) n HnO HNhiSubn).
We prove the intermediate claim HnR: apply_fun seq n ∈ R.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim Hnb: apply_fun seq n ∈ open_interval a c.
We prove the intermediate claim HdefInt: open_interval a c = {x ∈ R|Rlt a x ∧ Rlt x c}.
Use reflexivity.
rewrite the current goal using HdefInt (from left to right).
Apply (SepI R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 c) (apply_fun seq n) HnR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HltA.
An exact proof term for the current goal is HltC.
We prove the intermediate claim Hnb2: apply_fun seq n ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is Hnb.
An exact proof term for the current goal is (HbsubU (apply_fun seq n) Hnb2).
∎