ioodvbdlimc2lem - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ioodvbdlimc2lem		Structured version Visualization version GIF version

Theorem ioodvbdlimc2lem 44165

Description: Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.)

**Hypotheses**
Ref	Expression
ioodvbdlimc2lem.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
ioodvbdlimc2lem.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
ioodvbdlimc2lem.altb	⊢ (𝜑 → 𝐴 < 𝐵)
ioodvbdlimc2lem.f	⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
ioodvbdlimc2lem.dmdv	⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
ioodvbdlimc2lem.dvbd	⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
ioodvbdlimc2lem.y	⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
ioodvbdlimc2lem.m	⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1)
ioodvbdlimc2lem.s	⊢ 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗))))
ioodvbdlimc2lem.r	⊢ 𝑅 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐵 − (1 / 𝑗)))
ioodvbdlimc2lem.n	⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
ioodvbdlimc2lem.ch	⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)))

**Assertion**
Ref	Expression
ioodvbdlimc2lem	⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐵))

Distinct variable groups: 𝐴,𝑗,𝑥,𝑧,𝑦 𝐵,𝑗,𝑥,𝑧,𝑦 𝑗,𝐹,𝑥,𝑧,𝑦 𝑗,𝑀,𝑥,𝑦 𝑗,𝑁,𝑧 𝑅,𝑗,𝑥,𝑦 𝑥,𝑆,𝑗,𝑦,𝑧 𝑥,𝑌 𝜑,𝑥,𝑗,𝑧,𝑦 Allowed substitution hints: 𝜒(𝑥,𝑦,𝑧,𝑗) 𝑅(𝑧) 𝑀(𝑧) 𝑁(𝑥,𝑦) 𝑌(𝑦,𝑧,𝑗)

Proof of Theorem ioodvbdlimc2lem Dummy variables 𝑏 𝑘 ℎ 𝑖 𝑙 𝑤 𝑚 𝑐 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uzssz 12784	. . . . . 6 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
2		zssre 12506	. . . . . 6 ⊢ ℤ ⊆ ℝ
3	1, 2	sstri 3953	. . . . 5 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (ℤ_≥‘𝑀) ⊆ ℝ)
5		ioodvbdlimc2lem.m	. . . . . . 7 ⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1)
6		ioodvbdlimc2lem.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
7		ioodvbdlimc2lem.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
8	6, 7	resubcld 11583	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
9		ioodvbdlimc2lem.altb	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
10	7, 6	posdifd 11742	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
11	9, 10	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
12	11	gt0ne0d 11719	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0)
13	8, 12	rereccld 11982	. . . . . . . . 9 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ)
14		0red 11158	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
15	8, 11	recgt0d 12089	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (1 / (𝐵 − 𝐴)))
16	14, 13, 15	ltled 11303	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (1 / (𝐵 − 𝐴)))
17		flge0nn0 13725	. . . . . . . . 9 ⊢ (((1 / (𝐵 − 𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐵 − 𝐴))) → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀)
18	13, 16, 17	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀)
19		peano2nn0 12453	. . . . . . . 8 ⊢ ((⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀ → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℕ₀)
20	18, 19	syl 17	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℕ₀)
21	5, 20	eqeltrid 2842	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
22	21	nn0zd 12525	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
23		eqid 2736	. . . . . 6 ⊢ (ℤ_≥‘𝑀) = (ℤ_≥‘𝑀)
24	23	uzsup 13768	. . . . 5 ⊢ (𝑀 ∈ ℤ → sup((ℤ_≥‘𝑀), ℝ^*, < ) = +∞)
25	22, 24	syl 17	. . . 4 ⊢ (𝜑 → sup((ℤ_≥‘𝑀), ℝ^*, < ) = +∞)
26		ioodvbdlimc2lem.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
27	26	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
28	7	rexrd 11205	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
29	28	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ^*)
30	6	rexrd 11205	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
31	30	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ^*)
32	6	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ)
33		eluzelre 12774	. . . . . . . . . 10 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑗 ∈ ℝ)
34	33	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℝ)
35		0red 11158	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 ∈ ℝ)
36		0red 11158	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 0 ∈ ℝ)
37		1red 11156	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 1 ∈ ℝ)
38	36, 37	readdcld 11184	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → (0 + 1) ∈ ℝ)
39	38	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ∈ ℝ)
40	36	ltp1d 12085	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 0 < (0 + 1))
41	40	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 < (0 + 1))
42		eluzel2 12768	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
43	42	zred 12607	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℝ)
44	43	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
45	13	flcld 13703	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℤ)
46	45	zred 12607	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℝ)
47		1red 11156	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℝ)
48	18	nn0ge0d 12476	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ≤ (⌊‘(1 / (𝐵 − 𝐴))))
49	14, 46, 47, 48	leadd1dd 11769	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + 1) ≤ ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
50	49, 5	breqtrrdi 5147	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 + 1) ≤ 𝑀)
51	50	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ≤ 𝑀)
52		eluzle 12776	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑗)
53	52	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑗)
54	39, 44, 34, 51, 53	letrd 11312	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ≤ 𝑗)
55	35, 39, 34, 41, 54	ltletrd 11315	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑗)
56	55	gt0ne0d 11719	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ≠ 0)
57	34, 56	rereccld 11982	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ∈ ℝ)
58	32, 57	resubcld 11583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑗)) ∈ ℝ)
59	7	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
60	21	nn0red 12474	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
61	14, 47	readdcld 11184	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + 1) ∈ ℝ)
62	46, 47	readdcld 11184	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℝ)
63	14	ltp1d 12085	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (0 + 1))
64	14, 61, 62, 63, 49	ltletrd 11315	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
65	64, 5	breqtrrdi 5147	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝑀)
66	65	gt0ne0d 11719	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≠ 0)
67	60, 66	rereccld 11982	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 𝑀) ∈ ℝ)
68	67	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑀) ∈ ℝ)
69	32, 68	resubcld 11583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑀)) ∈ ℝ)
70	5	eqcomi 2745	. . . . . . . . . . . . 13 ⊢ ((⌊‘(1 / (𝐵 − 𝐴))) + 1) = 𝑀
71	70	oveq2i 7368	. . . . . . . . . . . 12 ⊢ (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) = (1 / 𝑀)
72	71, 67	eqeltrid 2842	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) ∈ ℝ)
73	13, 15	elrpd 12954	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ⁺)
74	62, 64	elrpd 12954	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℝ⁺)
75		1rp 12919	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ⁺
76	75	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ⁺)
77		fllelt 13702	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) ∈ ℝ → ((⌊‘(1 / (𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
78	13, 77	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
79	78	simprd 496	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
80	73, 74, 76, 79	ltdiv2dd 43518	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) < (1 / (1 / (𝐵 − 𝐴))))
81	8	recnd 11183	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ)
82	81, 12	recrecd 11928	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / (1 / (𝐵 − 𝐴))) = (𝐵 − 𝐴))
83	80, 82	breqtrd 5131	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) < (𝐵 − 𝐴))
84	72, 8, 6, 83	ltsub2dd 11768	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) < (𝐵 − (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))))
85	6	recnd 11183	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
86	7	recnd 11183	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
87	85, 86	nncand 11517	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) = 𝐴)
88	71	oveq2i 7368	. . . . . . . . . . 11 ⊢ (𝐵 − (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) = (𝐵 − (1 / 𝑀))
89	88	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) = (𝐵 − (1 / 𝑀)))
90	84, 87, 89	3brtr3d 5136	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 < (𝐵 − (1 / 𝑀)))
91	90	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 < (𝐵 − (1 / 𝑀)))
92	60, 65	elrpd 12954	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
93	92	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ⁺)
94	34, 55	elrpd 12954	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℝ⁺)
95		1red 11156	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 1 ∈ ℝ)
96		0le1 11678	. . . . . . . . . . 11 ⊢ 0 ≤ 1
97	96	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 ≤ 1)
98	93, 94, 95, 97, 53	lediv2ad 12979	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀))
99	57, 68, 32, 98	lesub2dd 11772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑀)) ≤ (𝐵 − (1 / 𝑗)))
100	59, 69, 58, 91, 99	ltletrd 11315	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 < (𝐵 − (1 / 𝑗)))
101	94	rpreccld 12967	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ∈ ℝ⁺)
102	32, 101	ltsubrpd 12989	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑗)) < 𝐵)
103	29, 31, 58, 100, 102	eliood 43726	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵))
104	27, 103	ffvelcdmd 7036	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘(𝐵 − (1 / 𝑗))) ∈ ℝ)
105		ioodvbdlimc2lem.s	. . . . 5 ⊢ 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗))))
106	104, 105	fmptd 7062	. . . 4 ⊢ (𝜑 → 𝑆:(ℤ_≥‘𝑀)⟶ℝ)
107		ioodvbdlimc2lem.dmdv	. . . . . 6 ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
108		ioodvbdlimc2lem.dvbd	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
109	7, 6, 9, 26, 107, 108	dvbdfbdioo 44161	. . . . 5 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏)
110	60	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ)
111		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ (ℤ_≥‘𝑀))
112	105	fvmpt2 6959	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (ℤ_≥‘𝑀) ∧ (𝐹‘(𝐵 − (1 / 𝑗))) ∈ ℝ) → (𝑆‘𝑗) = (𝐹‘(𝐵 − (1 / 𝑗))))
113	111, 104, 112	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑆‘𝑗) = (𝐹‘(𝐵 − (1 / 𝑗))))
114	113	fveq2d 6846	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))))
115	114	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))))
116		simplr 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏)
117	103	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵))
118		2fveq3 6847	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐵 − (1 / 𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))))
119	118	breq1d 5115	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐵 − (1 / 𝑗)) → ((abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏))
120	119	rspccva 3580	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 ∧ (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏)
121	116, 117, 120	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏)
122	115, 121	eqbrtrd 5127	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) ≤ 𝑏)
123	122	a1d 25	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
124	123	ralrimiva 3143	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
125		breq1 5108	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑀 → (𝑘 ≤ 𝑗 ↔ 𝑀 ≤ 𝑗))
126	125	imbi1d 341	. . . . . . . . . 10 ⊢ (𝑘 = 𝑀 → ((𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
127	126	ralbidv 3174	. . . . . . . . 9 ⊢ (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
128	127	rspcev 3581	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
129	110, 124, 128	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
130	129	ex 413	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
131	130	reximdv 3167	. . . . 5 ⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
132	109, 131	mpd 15	. . . 4 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
133	4, 25, 106, 132	limsupre 43872	. . 3 ⊢ (𝜑 → (lim sup‘𝑆) ∈ ℝ)
134	133	recnd 11183	. 2 ⊢ (𝜑 → (lim sup‘𝑆) ∈ ℂ)
135		eluzelre 12774	. . . . . . . . 9 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑗 ∈ ℝ)
136	135	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑗 ∈ ℝ)
137		0red 11158	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 ∈ ℝ)
138	45	peano2zd 12610	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℤ)
139	5, 138	eqeltrid 2842	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
140	139	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ∈ ℤ)
141	140	zred 12607	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ∈ ℝ)
142	141	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ∈ ℝ)
143	65	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < 𝑀)
144		ioodvbdlimc2lem.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
145		ioodvbdlimc2lem.y	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
146		ioomidp 43742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
147	7, 6, 9, 146	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
148		ne0i 4294	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
149	147, 148	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴(,)𝐵) ≠ ∅)
150		ioossre 13325	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴(,)𝐵) ⊆ ℝ
151	150	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
152		dvfre 25315	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
153	26, 151, 152	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
154	107	feq2d 6654	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
155	153, 154	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
156	155	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
157	156	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
158	157	abscld 15321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
159		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥)))
160		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
161	149, 158, 108, 159, 160	suprnmpt 43381	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )))
162	161	simpld 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ)
163	145, 162	eqeltrid 2842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑌 ∈ ℝ)
164	163	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑌 ∈ ℝ)
165		rpre 12923	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
166	165	rehalfcld 12400	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ)
167	166	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
168	165	recnd 11183	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
169	168	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
170		2cnd 12231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℂ)
171		rpne0 12931	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
172	171	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
173		2ne0 12257	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
174	173	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ≠ 0)
175	169, 170, 172, 174	divne0d 11947	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ≠ 0)
176	164, 167, 175	redivcld 11983	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
177	176	flcld 13703	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
178	177	peano2zd 12610	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
179	178, 140	ifcld 4532	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
180	144, 179	eqeltrid 2842	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ ℤ)
181	180	zred 12607	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ ℝ)
182	181	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑁 ∈ ℝ)
183	178	zred 12607	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
184		max1 13104	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
185	141, 183, 184	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
186	185, 144	breqtrrdi 5147	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ≤ 𝑁)
187	186	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ≤ 𝑁)
188		eluzle 12776	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑁 ≤ 𝑗)
189	188	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑁 ≤ 𝑗)
190	142, 182, 136, 187, 189	letrd 11312	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ≤ 𝑗)
191	137, 142, 136, 143, 190	ltletrd 11315	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < 𝑗)
192	191	gt0ne0d 11719	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑗 ≠ 0)
193	136, 192	rereccld 11982	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (1 / 𝑗) ∈ ℝ)
194	136, 191	recgt0d 12089	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < (1 / 𝑗))
195	193, 194	elrpd 12954	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (1 / 𝑗) ∈ ℝ⁺)
196	195	adantr 481	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈ ℝ⁺)
197		ioodvbdlimc2lem.ch	. . . . . . . . 9 ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)))
198	197	biimpi 215	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)))
199		simp-5l 783	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → 𝜑)
200	198, 199	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝜑)
201	200, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
202	198	simplrd 768	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑧 ∈ (𝐴(,)𝐵))
203	201, 202	ffvelcdmd 7036	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝐹‘𝑧) ∈ ℝ)
204	203	recnd 11183	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝐹‘𝑧) ∈ ℂ)
205	200, 106	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑆:(ℤ_≥‘𝑀)⟶ℝ)
206		simp-5r 784	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → 𝑥 ∈ ℝ⁺)
207	198, 206	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑥 ∈ ℝ⁺)
208		eluz2 12769	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
209	140, 180, 186, 208	syl3anbrc 1343	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ (ℤ_≥‘𝑀))
210	200, 207, 209	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑁 ∈ (ℤ_≥‘𝑀))
211		uzss 12786	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
212	210, 211	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
213		simp-4r 782	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ_≥‘𝑁))
214	198, 213	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑗 ∈ (ℤ_≥‘𝑁))
215	212, 214	sseldd 3945	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑗 ∈ (ℤ_≥‘𝑀))
216	205, 215	ffvelcdmd 7036	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
217	216	recnd 11183	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ)
218	200, 134	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → (lim sup‘𝑆) ∈ ℂ)
219	204, 217, 218	npncand 11536	. . . . . . . . . . . 12 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) = ((𝐹‘𝑧) − (lim sup‘𝑆)))
220	219	eqcomd 2742	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹‘𝑧) − (lim sup‘𝑆)) = (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))))
221	220	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))))
222	203, 216	resubcld 11583	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℝ)
223	200, 133	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (lim sup‘𝑆) ∈ ℝ)
224	216, 223	resubcld 11583	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℝ)
225	222, 224	readdcld 11184	. . . . . . . . . . . . 13 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ)
226	225	recnd 11183	. . . . . . . . . . . 12 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℂ)
227	226	abscld 15321	. . . . . . . . . . 11 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
228	222	recnd 11183	. . . . . . . . . . . . 13 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℂ)
229	228	abscld 15321	. . . . . . . . . . . 12 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ∈ ℝ)
230	224	recnd 11183	. . . . . . . . . . . . 13 ⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℂ)
231	230	abscld 15321	. . . . . . . . . . . 12 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ)
232	229, 231	readdcld 11184	. . . . . . . . . . 11 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
233	207	rpred 12957	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑥 ∈ ℝ)
234	228, 230	abstrid 15341	. . . . . . . . . . 11 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))))
235	233	rehalfcld 12400	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑥 / 2) ∈ ℝ)
236	200, 215, 113	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑆‘𝑗) = (𝐹‘(𝐵 − (1 / 𝑗))))
237	236	oveq2d 7373	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) = ((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗)))))
238	237	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) = (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))))
239	238, 229	eqeltrrd 2839	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ∈ ℝ)
240	200, 163	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑌 ∈ ℝ)
241	150, 202	sselid 3942	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑧 ∈ ℝ)
242	200, 215, 58	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝐵 − (1 / 𝑗)) ∈ ℝ)
243	241, 242	resubcld 11583	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) ∈ ℝ)
244	240, 243	remulcld 11185	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ∈ ℝ)
245	200, 7	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝐴 ∈ ℝ)
246	200, 6	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝐵 ∈ ℝ)
247	200, 107	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
248	161	simprd 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
249	145	breq2i 5113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
250	249	ralbii 3096	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
251	248, 250	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
252	200, 251	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
253		2fveq3 6847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥)))
254	253	breq1d 5115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌))
255	254	cbvralvw 3225	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
256	252, 255	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌)
257	200, 215, 103	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵))
258	242	rexrd 11205	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝐵 − (1 / 𝑗)) ∈ ℝ^*)
259	200, 30	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝐵 ∈ ℝ^*)
260	3, 215	sselid 3942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → 𝑗 ∈ ℝ)
261	200, 215, 56	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → 𝑗 ≠ 0)
262	260, 261	rereccld 11982	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (1 / 𝑗) ∈ ℝ)
263	246, 241	resubcld 11583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝐵 − 𝑧) ∈ ℝ)
264	241, 246	resubcld 11583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (𝑧 − 𝐵) ∈ ℝ)
265	264	recnd 11183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑧 − 𝐵) ∈ ℂ)
266	265	abscld 15321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (abs‘(𝑧 − 𝐵)) ∈ ℝ)
267	263	leabsd 15299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝐵 − 𝑧) ≤ (abs‘(𝐵 − 𝑧)))
268	200, 85	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝐵 ∈ ℂ)
269	241	recnd 11183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑧 ∈ ℂ)
270	268, 269	abssubd 15338	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (abs‘(𝐵 − 𝑧)) = (abs‘(𝑧 − 𝐵)))
271	267, 270	breqtrd 5131	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝐵 − 𝑧) ≤ (abs‘(𝑧 − 𝐵)))
272	198	simprd 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (abs‘(𝑧 − 𝐵)) < (1 / 𝑗))
273	263, 266, 262, 271, 272	lelttrd 11313	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝐵 − 𝑧) < (1 / 𝑗))
274	246, 241, 262, 273	ltsub23d 11760	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝐵 − (1 / 𝑗)) < 𝑧)
275	200, 28	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐴 ∈ ℝ^*)
276		iooltub 43738	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 < 𝐵)
277	275, 259, 202, 276	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑧 < 𝐵)
278	258, 259, 241, 274, 277	eliood 43726	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑧 ∈ ((𝐵 − (1 / 𝑗))(,)𝐵))
279	245, 246, 201, 247, 240, 256, 257, 278	dvbdfbdioolem1 44159	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ∧ (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝐵 − 𝐴))))
280	279	simpld 495	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))))
281	200, 215, 57	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (1 / 𝑗) ∈ ℝ)
282	240, 281	remulcld 11185	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ)
283	155, 147	ffvelcdmd 7036	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ)
284	283	recnd 11183	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ)
285	284	abscld 15321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ)
286	284	absge0d 15329	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≤ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
287		2fveq3 6847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
288	145	eqcomi 2745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌
289	288	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌)
290	287, 289	breq12d 5118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌))
291	290	rspcva 3579	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
292	147, 248, 291	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
293	14, 285, 163, 286, 292	letrd 11312	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ≤ 𝑌)
294	200, 293	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 0 ≤ 𝑌)
295	281	recnd 11183	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (1 / 𝑗) ∈ ℂ)
296		sub31 43514	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (1 / 𝑗) ∈ ℂ) → (𝑧 − (𝐵 − (1 / 𝑗))) = ((1 / 𝑗) − (𝐵 − 𝑧)))
297	269, 268, 295, 296	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) = ((1 / 𝑗) − (𝐵 − 𝑧)))
298	241, 246	posdifd 11742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (𝑧 < 𝐵 ↔ 0 < (𝐵 − 𝑧)))
299	277, 298	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 0 < (𝐵 − 𝑧))
300	263, 299	elrpd 12954	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝐵 − 𝑧) ∈ ℝ⁺)
301	281, 300	ltsubrpd 12989	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ((1 / 𝑗) − (𝐵 − 𝑧)) < (1 / 𝑗))
302	297, 301	eqbrtrd 5127	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) < (1 / 𝑗))
303	243, 281, 302	ltled 11303	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) ≤ (1 / 𝑗))
304	243, 281, 240, 294, 303	lemul2ad 12095	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ≤ (𝑌 · (1 / 𝑗)))
305	282	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
306	235	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑥 / 2) ∈ ℝ)
307		oveq1 7364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗)))
308	295	mul02d 11353	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (0 · (1 / 𝑗)) = 0)
309	307, 308	sylan9eqr 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0)
310	207	rphalfcld 12969	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑥 / 2) ∈ ℝ⁺)
311	310	rpgt0d 12960	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → 0 < (𝑥 / 2))
312	311	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → 0 < (𝑥 / 2))
313	309, 312	eqbrtrd 5127	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2))
314	305, 306, 313	ltled 11303	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
315	240	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ)
316	294	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌)
317		neqne 2951	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑌 = 0 → 𝑌 ≠ 0)
318	317	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0)
319	315, 316, 318	ne0gt0d 11292	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌)
320	282	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
321	3, 210	sselid 3942	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑁 ∈ ℝ)
322		0red 11158	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 0 ∈ ℝ)
323	200, 207, 141	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 𝑀 ∈ ℝ)
324	200, 65	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 0 < 𝑀)
325	200, 207, 186	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 𝑀 ≤ 𝑁)
326	322, 323, 321, 324, 325	ltletrd 11315	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 0 < 𝑁)
327	326	gt0ne0d 11719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑁 ≠ 0)
328	321, 327	rereccld 11982	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (1 / 𝑁) ∈ ℝ)
329	240, 328	remulcld 11185	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ)
330	329	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ)
331	235	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ)
332	281	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ)
333	328	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ)
334	240	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ)
335	294	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌)
336	321, 326	elrpd 12954	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑁 ∈ ℝ⁺)
337	200, 215, 94	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑗 ∈ ℝ⁺)
338		1red 11156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 1 ∈ ℝ)
339	96	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 0 ≤ 1)
340	214, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑁 ≤ 𝑗)
341	336, 337, 338, 339, 340	lediv2ad 12979	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁))
342	341	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁))
343	332, 333, 334, 335, 342	lemul2ad 12095	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁)))
344	233	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 𝑥 ∈ ℂ)
345		2cnd 12231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 2 ∈ ℂ)
346	207	rpne0d 12962	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 𝑥 ≠ 0)
347	173	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 2 ≠ 0)
348	344, 345, 346, 347	divne0d 11947	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → (𝑥 / 2) ≠ 0)
349	240, 235, 348	redivcld 11983	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ)
350	349	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
351		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌)
352	311	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2))
353	334, 331, 351, 352	divgt0d 12090	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2)))
354	350, 353	elrpd 12954	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ⁺)
355	354	rprecred 12968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ)
356	336	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈ ℝ⁺)
357		1red 11156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ)
358	96	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1)
359	349	flcld 13703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
360	359	peano2zd 12610	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
361	360	zred 12607	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
362	200, 139	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → 𝑀 ∈ ℤ)
363	360, 362	ifcld 4532	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
364	144, 363	eqeltrid 2842	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 𝑁 ∈ ℤ)
365	364	zred 12607	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑁 ∈ ℝ)
366		flltp1 13705	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
367	349, 366	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
368	200, 60	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑀 ∈ ℝ)
369		max2 13106	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
370	368, 361, 369	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
371	370, 144	breqtrrdi 5147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁)
372	349, 361, 365, 367, 371	ltletrd 11315	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁)
373	349, 321, 372	ltled 11303	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
374	373	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
375	354, 356, 357, 358, 374	lediv2ad 12979	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2))))
376	333, 355, 334, 335, 375	lemul2ad 12095	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
377	334	recnd 11183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ)
378	350	recnd 11183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ)
379	353	gt0ne0d 11719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0)
380	377, 378, 379	divrecd 11934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
381	331	recnd 11183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ)
382	351	gt0ne0d 11719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0)
383	348	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0)
384	377, 381, 382, 383	ddcand 11951	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2))
385	380, 384	eqtr3d 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2))
386	376, 385	breqtrd 5131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2))
387	320, 330, 331, 343, 386	letrd 11312	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
388	319, 387	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
389	314, 388	pm2.61dan 811	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
390	244, 282, 235, 304, 389	letrd 11312	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ≤ (𝑥 / 2))
391	239, 244, 235, 280, 390	letrd 11312	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑥 / 2))
392	238, 391	eqbrtrd 5127	. . . . . . . . . . . . 13 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ≤ (𝑥 / 2))
393		simpllr 774	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
394	198, 393	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
395	229, 231, 235, 235, 392, 394	leltaddd 11777	. . . . . . . . . . . 12 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2)))
396	344	2halvesd 12399	. . . . . . . . . . . 12 ⊢ (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
397	395, 396	breqtrd 5131	. . . . . . . . . . 11 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥)
398	227, 232, 233, 234, 397	lelttrd 11313	. . . . . . . . . 10 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥)
399	221, 398	eqbrtrd 5127	. . . . . . . . 9 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
400	197, 399	sylbir 234	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
401	400	adantrl 714	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗))) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
402	401	ex 413	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
403	402	ralrimiva 3143	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
404		brimralrspcev 5166	. . . . 5 ⊢ (((1 / 𝑗) ∈ ℝ⁺ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
405	196, 403, 404	syl2anc 584	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
406		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → 𝑏 ≤ 𝑁)
407	406	iftrued 4494	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑁)
408		uzid 12778	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ_≥‘𝑁))
409	180, 408	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ (ℤ_≥‘𝑁))
410	409	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → 𝑁 ∈ (ℤ_≥‘𝑁))
411	407, 410	eqeltrd 2838	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
412	411	adantlr 713	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
413		iffalse 4495	. . . . . . . . . 10 ⊢ (¬ 𝑏 ≤ 𝑁 → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏)
414	413	adantl 482	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏)
415	180	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ∈ ℤ)
416		simplr 767	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ ℤ)
417	415	zred 12607	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ∈ ℝ)
418	416	zred 12607	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ ℝ)
419		simpr 485	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → ¬ 𝑏 ≤ 𝑁)
420	417, 418	ltnled 11302	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑁))
421	419, 420	mpbird 256	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 < 𝑏)
422	417, 418, 421	ltled 11303	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ≤ 𝑏)
423		eluz2 12769	. . . . . . . . . 10 ⊢ (𝑏 ∈ (ℤ_≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ≤ 𝑏))
424	415, 416, 422, 423	syl3anbrc 1343	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ (ℤ_≥‘𝑁))
425	414, 424	eqeltrd 2838	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
426	412, 425	pm2.61dan 811	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
427	426	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
428		simpr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
429		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
430	180	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
431	430, 429	ifcld 4532	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ)
432	429	zred 12607	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
433	430	zred 12607	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℝ)
434		max1 13104	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))
435	432, 433, 434	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))
436		eluz2 12769	. . . . . . . . . 10 ⊢ (if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
437	429, 431, 435, 436	syl3anbrc 1343	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏))
438	437	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏))
439		fveq2 6842	. . . . . . . . . . 11 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑐) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
440	439	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ))
441	439	fvoveq1d 7379	. . . . . . . . . . 11 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
442	441	breq1d 5115	. . . . . . . . . 10 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
443	440, 442	anbi12d 631	. . . . . . . . 9 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))))
444	443	rspccva 3580	. . . . . . . 8 ⊢ ((∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏)) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
445	428, 438, 444	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
446	445	simprd 496	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))
447		fveq2 6842	. . . . . . . . 9 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑗) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
448	447	fvoveq1d 7379	. . . . . . . 8 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
449	448	breq1d 5115	. . . . . . 7 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
450	449	rspcev 3581	. . . . . 6 ⊢ ((if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁) ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
451	427, 446, 450	syl2anc 584	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
452		ax-resscn 11108	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
453	452	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℝ ⊆ ℂ)
454	26, 453	fssd 6686	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ)
455		dvcn 25285	. . . . . . . . . . . . . 14 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
456	453, 454, 151, 107, 455	syl31anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
457		cncfcdm 24261	. . . . . . . . . . . . 13 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
458	453, 456, 457	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
459	26, 458	mpbird 256	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
460		ioodvbdlimc2lem.r	. . . . . . . . . . . 12 ⊢ 𝑅 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐵 − (1 / 𝑗)))
461	103, 460	fmptd 7062	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅:(ℤ_≥‘𝑀)⟶(𝐴(,)𝐵))
462		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))
463		climrel 15374	. . . . . . . . . . . . 13 ⊢ Rel ⇝
464	463	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Rel ⇝ )
465		fvex 6855	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑀) ∈ V
466	465	mptex 7173	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵) ∈ V
467	466	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵) ∈ V)
468		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵))
469		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑚) → 𝐵 = 𝐵)
470		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ (ℤ_≥‘𝑀))
471	6	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ)
472	468, 469, 470, 471	fvmptd 6955	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑚) = 𝐵)
473	23, 22, 467, 85, 472	climconst 15425	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵) ⇝ 𝐵)
474	465	mptex 7173	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐵 − (1 / 𝑗))) ∈ V
475	460, 474	eqeltri 2834	. . . . . . . . . . . . . . 15 ⊢ 𝑅 ∈ V
476	475	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ V)
477		1cnd 11150	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
478		elnnnn0b 12457	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ₀ ∧ 0 < 𝑀))
479	21, 65, 478	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
480		divcnvg 43858	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0)
481	477, 479, 480	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0)
482		eqidd 2737	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵))
483		eqidd 2737	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → 𝐵 = 𝐵)
484		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ (ℤ_≥‘𝑀))
485	6	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ)
486	482, 483, 484, 485	fvmptd 6955	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑖) = 𝐵)
487	486, 485	eqeltrd 2838	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑖) ∈ ℝ)
488	487	recnd 11183	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑖) ∈ ℂ)
489		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)))
490		oveq2 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖))
491	490	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖))
492	3, 484	sselid 3942	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℝ)
493		0red 11158	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 ∈ ℝ)
494	60	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
495	65	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑀)
496		eluzle 12776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑖)
497	496	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑖)
498	493, 494, 492, 495, 497	ltletrd 11315	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑖)
499	498	gt0ne0d 11719	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ≠ 0)
500	492, 499	rereccld 11982	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑖) ∈ ℝ)
501	489, 491, 484, 500	fvmptd 6955	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖))
502	492	recnd 11183	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℂ)
503	502, 499	reccld 11924	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑖) ∈ ℂ)
504	501, 503	eqeltrd 2838	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ)
505	490	oveq2d 7373	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (𝐵 − (1 / 𝑗)) = (𝐵 − (1 / 𝑖)))
506		ovex 7390	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 − (1 / 𝑖)) ∈ V
507	505, 460, 506	fvmpt 6948	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (ℤ_≥‘𝑀) → (𝑅‘𝑖) = (𝐵 − (1 / 𝑖)))
508	507	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑖) = (𝐵 − (1 / 𝑖)))
509	486, 501	oveq12d 7375	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑖) − ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐵 − (1 / 𝑖)))
510	508, 509	eqtr4d 2779	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑖) = (((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑖) − ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)))
511	23, 22, 473, 476, 481, 488, 504, 510	climsub 15516	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ⇝ (𝐵 − 0))
512	85	subid1d 11501	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 0) = 𝐵)
513	511, 512	breqtrd 5131	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ⇝ 𝐵)
514		releldm 5899	. . . . . . . . . . . 12 ⊢ ((Rel ⇝ ∧ 𝑅 ⇝ 𝐵) → 𝑅 ∈ dom ⇝ )
515	464, 513, 514	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ dom ⇝ )
516		fveq2 6842	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → (ℤ_≥‘𝑙) = (ℤ_≥‘𝑘))
517		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = 𝑘 → (𝑅‘𝑙) = (𝑅‘𝑘))
518	517	oveq2d 7373	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 𝑘 → ((𝑅‘ℎ) − (𝑅‘𝑙)) = ((𝑅‘ℎ) − (𝑅‘𝑘)))
519	518	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑘 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) = (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))))
520	519	breq1d 5115	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
521	516, 520	raleqbidv 3319	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → (∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
522	521	cbvrabv 3417	. . . . . . . . . . . . 13 ⊢ {𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
523		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = 𝑖 → (𝑅‘ℎ) = (𝑅‘𝑖))
524	523	fvoveq1d 7379	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑖 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) = (abs‘((𝑅‘𝑖) − (𝑅‘𝑘))))
525	524	breq1d 5115	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑖 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
526	525	cbvralvw 3225	. . . . . . . . . . . . . . 15 ⊢ (∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
527	526	rgenw 3068	. . . . . . . . . . . . . 14 ⊢ ∀𝑘 ∈ (ℤ_≥‘𝑀)(∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
528		rabbi 3432	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ (ℤ_≥‘𝑀)(∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))) ↔ {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))})
529	527, 528	mpbi 229	. . . . . . . . . . . . 13 ⊢ {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
530	522, 529	eqtri 2764	. . . . . . . . . . . 12 ⊢ {𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
531	530	infeq1i 9414	. . . . . . . . . . 11 ⊢ inf({𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < ) = inf({𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
532	7, 6, 9, 459, 107, 108, 22, 461, 462, 515, 531	ioodvbdlimc1lem1 44162	. . . . . . . . . 10 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) ⇝ (lim sup‘(𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))))
533	460	fvmpt2 6959	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (ℤ_≥‘𝑀) ∧ (𝐵 − (1 / 𝑗)) ∈ ℝ) → (𝑅‘𝑗) = (𝐵 − (1 / 𝑗)))
534	111, 58, 533	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑗) = (𝐵 − (1 / 𝑗)))
535	534	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑗)) = (𝑅‘𝑗))
536	535	fveq2d 6846	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘(𝐵 − (1 / 𝑗))) = (𝐹‘(𝑅‘𝑗)))
537	536	mpteq2dva 5205	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗)))) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))
538	105, 537	eqtrid 2788	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))
539	538	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))))
540	532, 538, 539	3brtr4d 5137	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⇝ (lim sup‘𝑆))
541	465	mptex 7173	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗)))) ∈ V
542	105, 541	eqeltri 2834	. . . . . . . . . . 11 ⊢ 𝑆 ∈ V
543	542	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ V)
544		eqidd 2737	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ℤ) → (𝑆‘𝑐) = (𝑆‘𝑐))
545	543, 544	clim 15376	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))))
546	540, 545	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)))
547	546	simprd 496	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))
548	547	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))
549		simpr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
550	549	rphalfcld 12969	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
551		breq2 5109	. . . . . . . . 9 ⊢ (𝑎 = (𝑥 / 2) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
552	551	anbi2d 629	. . . . . . . 8 ⊢ (𝑎 = (𝑥 / 2) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
553	552	rexralbidv 3214	. . . . . . 7 ⊢ (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
554	553	rspccva 3580	. . . . . 6 ⊢ ((∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ⁺) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
555	548, 550, 554	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
556	451, 555	r19.29a 3159	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
557	405, 556	r19.29a 3159	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
558	557	ralrimiva 3143	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
559		ioosscn 13326	. . . 4 ⊢ (𝐴(,)𝐵) ⊆ ℂ
560	559	a1i 11	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
561	454, 560, 85	ellimc3 25243	. 2 ⊢ (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐵) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))))
562	134, 558, 561	mpbir2and 711	1 ⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 {crab 3407 Vcvv 3445 ⊆ wss 3910 ∅c0 4282 ifcif 4486 class class class wbr 5105 ↦ cmpt 5188 dom cdm 5633 ran crn 5634 Rel wrel 5638 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 supcsup 9376 infcinf 9377 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 · cmul 11056 +∞cpnf 11186 ℝ^*cxr 11188 < clt 11189 ≤ cle 11190 − cmin 11385 / cdiv 11812 ℕcn 12153 2c2 12208 ℕ₀cn0 12413 ℤcz 12499 ℤ_≥cuz 12763 ℝ⁺crp 12915 (,)cioo 13264 ⌊cfl 13695 abscabs 15119 lim supclsp 15352 ⇝ cli 15366 –cn→ccncf 24239 lim_ℂ climc 25226 D cdv 25227

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129 ax-addf 11130 ax-mulf 11131

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-supp 8093 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-2o 8413 df-er 8648 df-map 8767 df-pm 8768 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9306 df-fi 9347 df-sup 9378 df-inf 9379 df-oi 9446 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-5 12219 df-6 12220 df-7 12221 df-8 12222 df-9 12223 df-n0 12414 df-z 12500 df-dec 12619 df-uz 12764 df-q 12874 df-rp 12916 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13268 df-ico 13270 df-icc 13271 df-fz 13425 df-fzo 13568 df-fl 13697 df-seq 13907 df-exp 13968 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-limsup 15353 df-clim 15370 df-rlim 15371 df-struct 17019 df-sets 17036 df-slot 17054 df-ndx 17066 df-base 17084 df-ress 17113 df-plusg 17146 df-mulr 17147 df-starv 17148 df-sca 17149 df-vsca 17150 df-ip 17151 df-tset 17152 df-ple 17153 df-ds 17155 df-unif 17156 df-hom 17157 df-cco 17158 df-rest 17304 df-topn 17305 df-0g 17323 df-gsum 17324 df-topgen 17325 df-pt 17326 df-prds 17329 df-xrs 17384 df-qtop 17389 df-imas 17390 df-xps 17392 df-mre 17466 df-mrc 17467 df-acs 17469 df-mgm 18497 df-sgrp 18546 df-mnd 18557 df-submnd 18602 df-mulg 18873 df-cntz 19097 df-cmn 19564 df-psmet 20788 df-xmet 20789 df-met 20790 df-bl 20791 df-mopn 20792 df-fbas 20793 df-fg 20794 df-cnfld 20797 df-top 22243 df-topon 22260 df-topsp 22282 df-bases 22296 df-cld 22370 df-ntr 22371 df-cls 22372 df-nei 22449 df-lp 22487 df-perf 22488 df-cn 22578 df-cnp 22579 df-haus 22666 df-cmp 22738 df-tx 22913 df-hmeo 23106 df-fil 23197 df-fm 23289 df-flim 23290 df-flf 23291 df-xms 23673 df-ms 23674 df-tms 23675 df-cncf 24241 df-limc 25230 df-dv 25231

This theorem is referenced by: ioodvbdlimc2 44166

W3C validator