ioodvbdlimc1lem2 - Mathbox for Glauco Siliprandi

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

Theorem ioodvbdlimc1lem2 40147

Description: Limit at the lower 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
ioodvbdlimc1lem2.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
ioodvbdlimc1lem2.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
ioodvbdlimc1lem2.altb	⊢ (𝜑 → 𝐴 < 𝐵)
ioodvbdlimc1lem2.f	⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
ioodvbdlimc1lem2.dmdv	⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
ioodvbdlimc1lem2.dvbd	⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
ioodvbdlimc1lem2.y	⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
ioodvbdlimc1lem2.m	⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1)
ioodvbdlimc1lem2.s	⊢ 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗))))
ioodvbdlimc1lem2.r	⊢ 𝑅 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐴 + (1 / 𝑗)))
ioodvbdlimc1lem2.n	⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
ioodvbdlimc1lem2.ch	⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)))

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

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

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

Step	Hyp	Ref	Expression
1		uzssz 11707	. . . . . 6 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
2		zssre 11384	. . . . . 6 ⊢ ℤ ⊆ ℝ
3	1, 2	sstri 3612	. . . . 5 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (ℤ_≥‘𝑀) ⊆ ℝ)
5		ioodvbdlimc1lem2.m	. . . . . . 7 ⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1)
6		ioodvbdlimc1lem2.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
7		ioodvbdlimc1lem2.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
8	6, 7	resubcld 10458	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
9		ioodvbdlimc1lem2.altb	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
10	7, 6	posdifd 10614	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
11	9, 10	mpbid 222	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
12	11	gt0ne0d 10592	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0)
13	8, 12	rereccld 10852	. . . . . . . . 9 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ)
14		0red 10041	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
15	8, 11	recgt0d 10958	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (1 / (𝐵 − 𝐴)))
16	14, 13, 15	ltled 10185	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (1 / (𝐵 − 𝐴)))
17		flge0nn0 12621	. . . . . . . . 9 ⊢ (((1 / (𝐵 − 𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐵 − 𝐴))) → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀)
18	13, 16, 17	syl2anc 693	. . . . . . . 8 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀)
19		peano2nn0 11333	. . . . . . . 8 ⊢ ((⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀ → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℕ₀)
20	18, 19	syl 17	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℕ₀)
21	5, 20	syl5eqel 2705	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
22	21	nn0zd 11480	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
23		eqid 2622	. . . . . 6 ⊢ (ℤ_≥‘𝑀) = (ℤ_≥‘𝑀)
24	23	uzsup 12662	. . . . 5 ⊢ (𝑀 ∈ ℤ → sup((ℤ_≥‘𝑀), ℝ^*, < ) = +∞)
25	22, 24	syl 17	. . . 4 ⊢ (𝜑 → sup((ℤ_≥‘𝑀), ℝ^*, < ) = +∞)
26		ioodvbdlimc1lem2.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
27	26	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
28	7	rexrd 10089	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
29	28	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ^*)
30	6	rexrd 10089	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
31	30	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ^*)
32	7	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
33		eluzelre 11698	. . . . . . . . . 10 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑗 ∈ ℝ)
34	33	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℝ)
35		0red 10041	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 ∈ ℝ)
36		0red 10041	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 0 ∈ ℝ)
37		1red 10055	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 1 ∈ ℝ)
38	36, 37	readdcld 10069	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → (0 + 1) ∈ ℝ)
39	38	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ∈ ℝ)
40	36	ltp1d 10954	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 0 < (0 + 1))
41	40	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 < (0 + 1))
42		eluzel2 11692	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
43	42	zred 11482	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℝ)
44	43	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
45	13	flcld 12599	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℤ)
46	45	zred 11482	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℝ)
47		1red 10055	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℝ)
48	18	nn0ge0d 11354	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ≤ (⌊‘(1 / (𝐵 − 𝐴))))
49	14, 46, 47, 48	leadd1dd 10641	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + 1) ≤ ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
50	49, 5	syl6breqr 4695	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 + 1) ≤ 𝑀)
51	50	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ≤ 𝑀)
52		eluzle 11700	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑗)
53	52	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑗)
54	39, 44, 34, 51, 53	letrd 10194	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ≤ 𝑗)
55	35, 39, 34, 41, 54	ltletrd 10197	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑗)
56	55	gt0ne0d 10592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ≠ 0)
57	34, 56	rereccld 10852	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ∈ ℝ)
58	32, 57	readdcld 10069	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ ℝ)
59	34, 55	elrpd 11869	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℝ⁺)
60	59	rpreccld 11882	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ∈ ℝ⁺)
61	32, 60	ltaddrpd 11905	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 < (𝐴 + (1 / 𝑗)))
62	21	nn0red 11352	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
63	14, 47	readdcld 10069	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + 1) ∈ ℝ)
64	46, 47	readdcld 10069	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℝ)
65	14	ltp1d 10954	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (0 + 1))
66	14, 63, 64, 65, 49	ltletrd 10197	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
67	66, 5	syl6breqr 4695	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝑀)
68	67	gt0ne0d 10592	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≠ 0)
69	62, 68	rereccld 10852	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 𝑀) ∈ ℝ)
70	69	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑀) ∈ ℝ)
71	32, 70	readdcld 10069	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑀)) ∈ ℝ)
72	6	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ)
73	62, 67	elrpd 11869	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
74	73	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ⁺)
75		1red 10055	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 1 ∈ ℝ)
76		0le1 10551	. . . . . . . . . . 11 ⊢ 0 ≤ 1
77	76	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 ≤ 1)
78	74, 59, 75, 77, 53	lediv2ad 11894	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀))
79	57, 70, 32, 78	leadd2dd 10642	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ≤ (𝐴 + (1 / 𝑀)))
80	5	eqcomi 2631	. . . . . . . . . . . . 13 ⊢ ((⌊‘(1 / (𝐵 − 𝐴))) + 1) = 𝑀
81	80	oveq2i 6661	. . . . . . . . . . . 12 ⊢ (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) = (1 / 𝑀)
82	81, 69	syl5eqel 2705	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) ∈ ℝ)
83	13, 15	elrpd 11869	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ⁺)
84	64, 66	elrpd 11869	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℝ⁺)
85		1rp 11836	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ⁺
86	85	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ⁺)
87		fllelt 12598	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) ∈ ℝ → ((⌊‘(1 / (𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
88	13, 87	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
89	88	simprd 479	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
90	83, 84, 86, 89	ltdiv2dd 39507	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) < (1 / (1 / (𝐵 − 𝐴))))
91	8	recnd 10068	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ)
92	91, 12	recrecd 10798	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / (1 / (𝐵 − 𝐴))) = (𝐵 − 𝐴))
93	90, 92	breqtrd 4679	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) < (𝐵 − 𝐴))
94	82, 8, 7, 93	ltadd2dd 10196	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) < (𝐴 + (𝐵 − 𝐴)))
95	5	oveq2i 6661	. . . . . . . . . . . 12 ⊢ (1 / 𝑀) = (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
96	95	oveq2i 6661	. . . . . . . . . . 11 ⊢ (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
97	96	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))))
98	7	recnd 10068	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
99	6	recnd 10068	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
100	98, 99	pncan3d 10395	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
101	100	eqcomd 2628	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = (𝐴 + (𝐵 − 𝐴)))
102	94, 97, 101	3brtr4d 4685	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 + (1 / 𝑀)) < 𝐵)
103	102	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑀)) < 𝐵)
104	58, 71, 72, 79, 103	lelttrd 10195	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) < 𝐵)
105	29, 31, 58, 61, 104	eliood 39720	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
106	27, 105	ffvelrnd 6360	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
107		ioodvbdlimc1lem2.s	. . . . 5 ⊢ 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗))))
108	106, 107	fmptd 6385	. . . 4 ⊢ (𝜑 → 𝑆:(ℤ_≥‘𝑀)⟶ℝ)
109		ioodvbdlimc1lem2.dmdv	. . . . . 6 ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
110		ioodvbdlimc1lem2.dvbd	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
111	7, 6, 9, 26, 109, 110	dvbdfbdioo 40145	. . . . 5 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏)
112	62	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ)
113		simpr 477	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ (ℤ_≥‘𝑀))
114	107	fvmpt2 6291	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (ℤ_≥‘𝑀) ∧ (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
115	113, 106, 114	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
116	115	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
117	116	adantlr 751	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
118		simplr 792	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏)
119	105	adantlr 751	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
120		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → (𝐹‘𝑥) = (𝐹‘(𝐴 + (1 / 𝑗))))
121	120	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
122	121	breq1d 4663	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → ((abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏))
123	122	rspccva 3308	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 ∧ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
124	118, 119, 123	syl2anc 693	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
125	117, 124	eqbrtrd 4675	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) ≤ 𝑏)
126	125	a1d 25	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
127	126	ralrimiva 2966	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
128		breq1 4656	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑀 → (𝑘 ≤ 𝑗 ↔ 𝑀 ≤ 𝑗))
129	128	imbi1d 331	. . . . . . . . . 10 ⊢ (𝑘 = 𝑀 → ((𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
130	129	ralbidv 2986	. . . . . . . . 9 ⊢ (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
131	130	rspcev 3309	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
132	112, 127, 131	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
133	132	ex 450	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
134	133	reximdv 3016	. . . . 5 ⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
135	111, 134	mpd 15	. . . 4 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
136	4, 25, 108, 135	limsupre 39873	. . 3 ⊢ (𝜑 → (lim sup‘𝑆) ∈ ℝ)
137	136	recnd 10068	. 2 ⊢ (𝜑 → (lim sup‘𝑆) ∈ ℂ)
138		eluzelre 11698	. . . . . . . . 9 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑗 ∈ ℝ)
139	138	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑗 ∈ ℝ)
140		0red 10041	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 ∈ ℝ)
141	45	peano2zd 11485	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℤ)
142	5, 141	syl5eqel 2705	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
143	142	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ∈ ℤ)
144	143	zred 11482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ∈ ℝ)
145	144	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ∈ ℝ)
146	67	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < 𝑀)
147		ioodvbdlimc1lem2.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
148		ioodvbdlimc1lem2.y	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
149		ioomidp 39740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
150	7, 6, 9, 149	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
151		ne0i 3921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴(,)𝐵) ≠ ∅)
153		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴(,)𝐵) ⊆ ℝ
154	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
155		dvfre 23714	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
156	26, 154, 155	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
157	109	feq2d 6031	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
158	156, 157	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
159	158	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
160	159	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
161	160	abscld 14175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
162		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥)))
163		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
164	152, 161, 110, 162, 163	suprnmpt 39355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )))
165	164	simpld 475	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ)
166	148, 165	syl5eqel 2705	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑌 ∈ ℝ)
167	166	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑌 ∈ ℝ)
168		rpre 11839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
169	168	rehalfcld 11279	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ)
170	169	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
171	168	recnd 10068	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
172	171	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
173		2cnd 11093	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℂ)
174		rpne0 11848	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
175	174	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
176		2ne0 11113	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
177	176	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ≠ 0)
178	172, 173, 175, 177	divne0d 10817	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ≠ 0)
179	167, 170, 178	redivcld 10853	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
180	179	flcld 12599	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
181	180	peano2zd 11485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
182	181, 143	ifcld 4131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
183	147, 182	syl5eqel 2705	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ ℤ)
184	183	zred 11482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ ℝ)
185	184	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑁 ∈ ℝ)
186	181	zred 11482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
187		max1 12016	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
188	144, 186, 187	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
189	188, 147	syl6breqr 4695	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ≤ 𝑁)
190	189	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ≤ 𝑁)
191		eluzle 11700	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑁 ≤ 𝑗)
192	191	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑁 ≤ 𝑗)
193	145, 185, 139, 190, 192	letrd 10194	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ≤ 𝑗)
194	140, 145, 139, 146, 193	ltletrd 10197	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < 𝑗)
195	194	gt0ne0d 10592	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑗 ≠ 0)
196	139, 195	rereccld 10852	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (1 / 𝑗) ∈ ℝ)
197	139, 194	recgt0d 10958	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < (1 / 𝑗))
198	196, 197	elrpd 11869	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (1 / 𝑗) ∈ ℝ⁺)
199	198	adantr 481	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈ ℝ⁺)
200		ioodvbdlimc1lem2.ch	. . . . . . . . 9 ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)))
201	200	biimpi 206	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)))
202		simp-5l 808	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝜑)
203	201, 202	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝜑)
204	203, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
205	201	simplrd 793	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑧 ∈ (𝐴(,)𝐵))
206	204, 205	ffvelrnd 6360	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝐹‘𝑧) ∈ ℝ)
207	206	recnd 10068	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝐹‘𝑧) ∈ ℂ)
208	203, 108	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑆:(ℤ_≥‘𝑀)⟶ℝ)
209		simp-5r 809	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝑥 ∈ ℝ⁺)
210	201, 209	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑥 ∈ ℝ⁺)
211		eluz2 11693	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
212	143, 183, 189, 211	syl3anbrc 1246	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ (ℤ_≥‘𝑀))
213	203, 210, 212	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑁 ∈ (ℤ_≥‘𝑀))
214		uzss 11708	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
215	213, 214	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
216		simp-4r 807	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ_≥‘𝑁))
217	201, 216	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑗 ∈ (ℤ_≥‘𝑁))
218	215, 217	sseldd 3604	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑗 ∈ (ℤ_≥‘𝑀))
219	208, 218	ffvelrnd 6360	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
220	219	recnd 10068	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ)
221	203, 137	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → (lim sup‘𝑆) ∈ ℂ)
222	207, 220, 221	npncand 10416	. . . . . . . . . . . 12 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) = ((𝐹‘𝑧) − (lim sup‘𝑆)))
223	222	eqcomd 2628	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹‘𝑧) − (lim sup‘𝑆)) = (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))))
224	223	fveq2d 6195	. . . . . . . . . 10 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))))
225	206, 219	resubcld 10458	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℝ)
226	203, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (lim sup‘𝑆) ∈ ℝ)
227	219, 226	resubcld 10458	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℝ)
228	225, 227	readdcld 10069	. . . . . . . . . . . . 13 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ)
229	228	recnd 10068	. . . . . . . . . . . 12 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℂ)
230	229	abscld 14175	. . . . . . . . . . 11 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
231	225	recnd 10068	. . . . . . . . . . . . 13 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℂ)
232	231	abscld 14175	. . . . . . . . . . . 12 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ∈ ℝ)
233	227	recnd 10068	. . . . . . . . . . . . 13 ⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℂ)
234	233	abscld 14175	. . . . . . . . . . . 12 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ)
235	232, 234	readdcld 10069	. . . . . . . . . . 11 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
236	210	rpred 11872	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑥 ∈ ℝ)
237	231, 233	abstrid 14195	. . . . . . . . . . 11 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))))
238	236	rehalfcld 11279	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑥 / 2) ∈ ℝ)
239	207, 220	abssubd 14192	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) = (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))))
240	203, 218, 115	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
241	240	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ((𝑆‘𝑗) − (𝐹‘𝑧)) = ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)))
242	241	fveq2d 6195	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))) = (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))))
243	203, 218, 106	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
244	243, 206	resubcld 10458	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)) ∈ ℝ)
245	244	recnd 10068	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)) ∈ ℂ)
246	245	abscld 14175	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ∈ ℝ)
247	203, 166	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑌 ∈ ℝ)
248	203, 218, 58	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝐴 + (1 / 𝑗)) ∈ ℝ)
249	153, 205	sseldi 3601	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑧 ∈ ℝ)
250	248, 249	resubcld 10458	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ∈ ℝ)
251	247, 250	remulcld 10070	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∈ ℝ)
252	203, 7	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝐴 ∈ ℝ)
253	203, 6	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝐵 ∈ ℝ)
254	203, 109	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
255	164	simprd 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
256	148	breq2i 4661	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
257	256	ralbii 2980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
258	255, 257	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
259	203, 258	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
260		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑥 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑥))
261	260	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥)))
262	261	breq1d 4663	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌))
263	262	cbvralv 3171	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
264	259, 263	sylibr 224	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌)
265	249	rexrd 10089	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑧 ∈ ℝ^*)
266	203, 30	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐵 ∈ ℝ^*)
267	249, 252	resubcld 10458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑧 − 𝐴) ∈ ℝ)
268	267	recnd 10068	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (𝑧 − 𝐴) ∈ ℂ)
269	268	abscld 14175	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (abs‘(𝑧 − 𝐴)) ∈ ℝ)
270	3, 218	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑗 ∈ ℝ)
271	203, 218, 56	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑗 ≠ 0)
272	270, 271	rereccld 10852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (1 / 𝑗) ∈ ℝ)
273	267	leabsd 14153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑧 − 𝐴) ≤ (abs‘(𝑧 − 𝐴)))
274	201	simprd 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))
275	267, 269, 272, 273, 274	lelttrd 10195	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝑧 − 𝐴) < (1 / 𝑗))
276	249, 252, 272	ltsubadd2d 10625	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ((𝑧 − 𝐴) < (1 / 𝑗) ↔ 𝑧 < (𝐴 + (1 / 𝑗))))
277	275, 276	mpbid 222	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑧 < (𝐴 + (1 / 𝑗)))
278	203, 218, 104	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝐴 + (1 / 𝑗)) < 𝐵)
279	265, 266, 248, 277, 278	eliood 39720	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝐴 + (1 / 𝑗)) ∈ (𝑧(,)𝐵))
280	252, 253, 204, 254, 247, 264, 205, 279	dvbdfbdioolem1 40143	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ((abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∧ (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · (𝐵 − 𝐴))))
281	280	simpld 475	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)))
282	203, 218, 57	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (1 / 𝑗) ∈ ℝ)
283	247, 282	remulcld 10070	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ)
284	158, 150	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ)
285	284	recnd 10068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ)
286	285	abscld 14175	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ)
287	285	absge0d 14183	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 ≤ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
288		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))
289	288	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
290	148	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌
291	290	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌)
292	289, 291	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌))
293	292	rspcva 3307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
294	150, 255, 293	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
295	14, 286, 166, 287, 294	letrd 10194	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≤ 𝑌)
296	203, 295	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 0 ≤ 𝑌)
297	203, 28	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝐴 ∈ ℝ^*)
298		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑧)
299	297, 266, 205, 298	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 𝐴 < 𝑧)
300	252, 249, 248, 299	ltsub2dd 10640	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < ((𝐴 + (1 / 𝑗)) − 𝐴))
301	203, 98	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 𝐴 ∈ ℂ)
302	282	recnd 10068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (1 / 𝑗) ∈ ℂ)
303	301, 302	pncan2d 10394	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝐴) = (1 / 𝑗))
304	300, 303	breqtrd 4679	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < (1 / 𝑗))
305	250, 272, 304	ltled 10185	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ≤ (1 / 𝑗))
306	250, 272, 247, 296, 305	lemul2ad 10964	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑌 · (1 / 𝑗)))
307	283	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
308	238	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑥 / 2) ∈ ℝ)
309		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗)))
310	302	mul02d 10234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (0 · (1 / 𝑗)) = 0)
311	309, 310	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0)
312	210	rphalfcld 11884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (𝑥 / 2) ∈ ℝ⁺)
313	312	rpgt0d 11875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 0 < (𝑥 / 2))
314	313	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑌 = 0) → 0 < (𝑥 / 2))
315	311, 314	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2))
316	307, 308, 315	ltled 10185	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
317	247	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ)
318	296	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌)
319		neqne 2802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑌 = 0 → 𝑌 ≠ 0)
320	319	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0)
321	317, 318, 320	ne0gt0d 10174	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌)
322	283	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
323	3, 213	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ∈ ℝ)
324		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 0 ∈ ℝ)
325	203, 210, 144	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑀 ∈ ℝ)
326	203, 67	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 0 < 𝑀)
327	203, 210, 189	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑀 ≤ 𝑁)
328	324, 325, 323, 326, 327	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 0 < 𝑁)
329	328	gt0ne0d 10592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ≠ 0)
330	323, 329	rereccld 10852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (1 / 𝑁) ∈ ℝ)
331	247, 330	remulcld 10070	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ)
332	331	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ)
333	238	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ)
334	282	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ)
335	330	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ)
336	247	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ)
337	296	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌)
338	323, 328	elrpd 11869	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ∈ ℝ⁺)
339	203, 218, 59	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑗 ∈ ℝ⁺)
340		1red 10055	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 1 ∈ ℝ)
341	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 0 ≤ 1)
342	217, 191	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ≤ 𝑗)
343	338, 339, 340, 341, 342	lediv2ad 11894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁))
344	343	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁))
345	334, 335, 336, 337, 344	lemul2ad 10964	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁)))
346	236	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑥 ∈ ℂ)
347		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 2 ∈ ℂ)
348	210	rpne0d 11877	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑥 ≠ 0)
349	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 2 ≠ 0)
350	346, 347, 348, 349	divne0d 10817	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑥 / 2) ≠ 0)
351	247, 238, 350	redivcld 10853	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ)
352	351	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
353		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌)
354	313	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2))
355	336, 333, 353, 354	divgt0d 10959	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2)))
356	352, 355	elrpd 11869	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ⁺)
357	356	rprecred 11883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ)
358	338	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈ ℝ⁺)
359		1red 10055	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ)
360	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1)
361	351	flcld 12599	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
362	361	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
363	362	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
364	203, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜒 → 𝑀 ∈ ℤ)
365	362, 364	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
366	147, 365	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑁 ∈ ℤ)
367	366	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 𝑁 ∈ ℝ)
368		flltp1 12601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
369	351, 368	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
370	203, 62	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → 𝑀 ∈ ℝ)
371		max2 12018	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
372	370, 363, 371	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
373	372, 147	syl6breqr 4695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁)
374	351, 363, 367, 369, 373	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁)
375	351, 323, 374	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
376	375	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
377	356, 358, 359, 360, 376	lediv2ad 11894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2))))
378	335, 357, 336, 337, 377	lemul2ad 10964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
379	336	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ)
380	352	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ)
381	355	gt0ne0d 10592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0)
382	379, 380, 381	divrecd 10804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
383	333	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ)
384	353	gt0ne0d 10592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0)
385	350	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0)
386	379, 383, 384, 385	ddcand 10821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2))
387	382, 386	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2))
388	378, 387	breqtrd 4679	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2))
389	322, 332, 333, 345, 388	letrd 10194	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
390	321, 389	syldan 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
391	316, 390	pm2.61dan 832	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
392	251, 283, 238, 306, 391	letrd 10194	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑥 / 2))
393	246, 251, 238, 281, 392	letrd 10194	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑥 / 2))
394	242, 393	eqbrtrd 4675	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))) ≤ (𝑥 / 2))
395	239, 394	eqbrtrd 4675	. . . . . . . . . . . . 13 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ≤ (𝑥 / 2))
396		simpllr 799	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
397	201, 396	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
398	232, 234, 238, 238, 395, 397	leltaddd 10649	. . . . . . . . . . . 12 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2)))
399	346	2halvesd 11278	. . . . . . . . . . . 12 ⊢ (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
400	398, 399	breqtrd 4679	. . . . . . . . . . 11 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥)
401	230, 235, 236, 237, 400	lelttrd 10195	. . . . . . . . . 10 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥)
402	224, 401	eqbrtrd 4675	. . . . . . . . 9 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
403	200, 402	sylbir 225	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
404	403	adantrl 752	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
405	404	ex 450	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
406	405	ralrimiva 2966	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
407		breq2 4657	. . . . . . . . 9 ⊢ (𝑦 = (1 / 𝑗) → ((abs‘(𝑧 − 𝐴)) < 𝑦 ↔ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)))
408	407	anbi2d 740	. . . . . . . 8 ⊢ (𝑦 = (1 / 𝑗) → ((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) ↔ (𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))))
409	408	imbi1d 331	. . . . . . 7 ⊢ (𝑦 = (1 / 𝑗) → (((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) ↔ ((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)))
410	409	ralbidv 2986	. . . . . 6 ⊢ (𝑦 = (1 / 𝑗) → (∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) ↔ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)))
411	410	rspcev 3309	. . . . 5 ⊢ (((1 / 𝑗) ∈ ℝ⁺ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
412	199, 406, 411	syl2anc 693	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
413		simpr 477	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → 𝑏 ≤ 𝑁)
414	413	iftrued 4094	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑁)
415		uzid 11702	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ_≥‘𝑁))
416	183, 415	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ (ℤ_≥‘𝑁))
417	416	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → 𝑁 ∈ (ℤ_≥‘𝑁))
418	414, 417	eqeltrd 2701	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
419	418	adantlr 751	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
420		iffalse 4095	. . . . . . . . . 10 ⊢ (¬ 𝑏 ≤ 𝑁 → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏)
421	420	adantl 482	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏)
422	183	ad2antrr 762	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ∈ ℤ)
423		simplr 792	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ ℤ)
424	422	zred 11482	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ∈ ℝ)
425	423	zred 11482	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ ℝ)
426		simpr 477	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → ¬ 𝑏 ≤ 𝑁)
427	424, 425	ltnled 10184	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑁))
428	426, 427	mpbird 247	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 < 𝑏)
429	424, 425, 428	ltled 10185	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ≤ 𝑏)
430		eluz2 11693	. . . . . . . . . 10 ⊢ (𝑏 ∈ (ℤ_≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ≤ 𝑏))
431	422, 423, 429, 430	syl3anbrc 1246	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ (ℤ_≥‘𝑁))
432	421, 431	eqeltrd 2701	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
433	419, 432	pm2.61dan 832	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
434	433	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
435		simpr 477	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
436		simpr 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
437	183	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
438	437, 436	ifcld 4131	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ)
439	436	zred 11482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
440	437	zred 11482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℝ)
441		max1 12016	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))
442	439, 440, 441	syl2anc 693	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))
443		eluz2 11693	. . . . . . . . . 10 ⊢ (if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
444	436, 438, 442, 443	syl3anbrc 1246	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏))
445	444	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏))
446		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑐) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
447	446	eleq1d 2686	. . . . . . . . . 10 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ))
448	446	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑐) − (lim sup‘𝑆)) = ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))
449	448	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
450	449	breq1d 4663	. . . . . . . . . 10 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
451	447, 450	anbi12d 747	. . . . . . . . 9 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))))
452	451	rspccva 3308	. . . . . . . 8 ⊢ ((∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏)) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
453	435, 445, 452	syl2anc 693	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
454	453	simprd 479	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))
455		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑗) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
456	455	oveq1d 6665	. . . . . . . . 9 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑗) − (lim sup‘𝑆)) = ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))
457	456	fveq2d 6195	. . . . . . . 8 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
458	457	breq1d 4663	. . . . . . 7 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
459	458	rspcev 3309	. . . . . 6 ⊢ ((if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁) ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
460	434, 454, 459	syl2anc 693	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
461		ax-resscn 9993	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
462	461	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℝ ⊆ ℂ)
463	26, 462	fssd 6057	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ)
464		dvcn 23684	. . . . . . . . . . . . . 14 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
465	462, 463, 154, 109, 464	syl31anc 1329	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
466		cncffvrn 22701	. . . . . . . . . . . . 13 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
467	462, 465, 466	syl2anc 693	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
468	26, 467	mpbird 247	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
469		ioodvbdlimc1lem2.r	. . . . . . . . . . . 12 ⊢ 𝑅 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐴 + (1 / 𝑗)))
470	105, 469	fmptd 6385	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅:(ℤ_≥‘𝑀)⟶(𝐴(,)𝐵))
471		eqid 2622	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))
472		climrel 14223	. . . . . . . . . . . . 13 ⊢ Rel ⇝
473	472	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Rel ⇝ )
474		fvex 6201	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑀) ∈ V
475	474	mptex 6486	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) ∈ V
476	475	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) ∈ V)
477		eqidd 2623	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴))
478		eqidd 2623	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑚) → 𝐴 = 𝐴)
479		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ (ℤ_≥‘𝑀))
480	7	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
481	477, 478, 479, 480	fvmptd 6288	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑚) = 𝐴)
482	23, 142, 476, 98, 481	climconst 14274	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) ⇝ 𝐴)
483	474	mptex 6486	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐴 + (1 / 𝑗))) ∈ V
484	469, 483	eqeltri 2697	. . . . . . . . . . . . . . 15 ⊢ 𝑅 ∈ V
485	484	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ V)
486		1cnd 10056	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
487		elnnnn0b 11337	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ₀ ∧ 0 < 𝑀))
488	21, 67, 487	sylanbrc 698	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
489		divcnvg 39859	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0)
490	486, 488, 489	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0)
491		eqidd 2623	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴))
492		eqidd 2623	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → 𝐴 = 𝐴)
493		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ (ℤ_≥‘𝑀))
494	7	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
495	491, 492, 493, 494	fvmptd 6288	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) = 𝐴)
496	98	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℂ)
497	495, 496	eqeltrd 2701	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) ∈ ℂ)
498		eqidd 2623	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)))
499		oveq2 6658	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖))
500	499	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖))
501	3, 493	sseldi 3601	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℝ)
502		0red 10041	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 ∈ ℝ)
503	62	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
504	67	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑀)
505		eluzle 11700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑖)
506	505	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑖)
507	502, 503, 501, 504, 506	ltletrd 10197	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑖)
508	507	gt0ne0d 10592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ≠ 0)
509	501, 508	rereccld 10852	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑖) ∈ ℝ)
510	498, 500, 493, 509	fvmptd 6288	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖))
511	501	recnd 10068	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℂ)
512	511, 508	reccld 10794	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑖) ∈ ℂ)
513	510, 512	eqeltrd 2701	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ)
514	469	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑅 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐴 + (1 / 𝑗))))
515	499	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
516	515	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
517	494, 509	readdcld 10069	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑖)) ∈ ℝ)
518	514, 516, 493, 517	fvmptd 6288	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑖) = (𝐴 + (1 / 𝑖)))
519	495, 510	oveq12d 6668	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐴 + (1 / 𝑖)))
520	518, 519	eqtr4d 2659	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑖) = (((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)))
521	23, 142, 482, 485, 490, 497, 513, 520	climadd 14362	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ⇝ (𝐴 + 0))
522	98	addid1d 10236	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 + 0) = 𝐴)
523	521, 522	breqtrd 4679	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ⇝ 𝐴)
524		releldm 5358	. . . . . . . . . . . 12 ⊢ ((Rel ⇝ ∧ 𝑅 ⇝ 𝐴) → 𝑅 ∈ dom ⇝ )
525	473, 523, 524	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ dom ⇝ )
526		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → (ℤ_≥‘𝑙) = (ℤ_≥‘𝑘))
527		fveq2 6191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = 𝑘 → (𝑅‘𝑙) = (𝑅‘𝑘))
528	527	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 𝑘 → ((𝑅‘ℎ) − (𝑅‘𝑙)) = ((𝑅‘ℎ) − (𝑅‘𝑘)))
529	528	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑘 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) = (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))))
530	529	breq1d 4663	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
531	526, 530	raleqbidv 3152	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → (∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
532	531	cbvrabv 3199	. . . . . . . . . . . . 13 ⊢ {𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
533		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = 𝑖 → (𝑅‘ℎ) = (𝑅‘𝑖))
534	533	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = 𝑖 → ((𝑅‘ℎ) − (𝑅‘𝑘)) = ((𝑅‘𝑖) − (𝑅‘𝑘)))
535	534	fveq2d 6195	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑖 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) = (abs‘((𝑅‘𝑖) − (𝑅‘𝑘))))
536	535	breq1d 4663	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑖 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
537	536	cbvralv 3171	. . . . . . . . . . . . . . 15 ⊢ (∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
538	537	rgenw 2924	. . . . . . . . . . . . . 14 ⊢ ∀𝑘 ∈ (ℤ_≥‘𝑀)(∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
539		rabbi 3120	. . . . . . . . . . . . . 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))})
540	538, 539	mpbi 220	. . . . . . . . . . . . 13 ⊢ {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
541	532, 540	eqtri 2644	. . . . . . . . . . . 12 ⊢ {𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
542	541	infeq1i 8384	. . . . . . . . . . 11 ⊢ inf({𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < ) = inf({𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
543	7, 6, 9, 468, 109, 110, 22, 470, 471, 525, 542	ioodvbdlimc1lem1 40146	. . . . . . . . . 10 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) ⇝ (lim sup‘(𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))))
544	469	fvmpt2 6291	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (ℤ_≥‘𝑀) ∧ (𝐴 + (1 / 𝑗)) ∈ ℝ) → (𝑅‘𝑗) = (𝐴 + (1 / 𝑗)))
545	113, 58, 544	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑗) = (𝐴 + (1 / 𝑗)))
546	545	eqcomd 2628	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) = (𝑅‘𝑗))
547	546	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) = (𝐹‘(𝑅‘𝑗)))
548	547	mpteq2dva 4744	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))
549	107, 548	syl5eq 2668	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))
550	549	fveq2d 6195	. . . . . . . . . 10 ⊢ (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))))
551	543, 549, 550	3brtr4d 4685	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⇝ (lim sup‘𝑆))
552	474	mptex 6486	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) ∈ V
553	107, 552	eqeltri 2697	. . . . . . . . . . 11 ⊢ 𝑆 ∈ V
554	553	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ V)
555		eqidd 2623	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ℤ) → (𝑆‘𝑐) = (𝑆‘𝑐))
556	554, 555	clim 14225	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))))
557	551, 556	mpbid 222	. . . . . . . 8 ⊢ (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)))
558	557	simprd 479	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))
559	558	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))
560		simpr 477	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
561	560	rphalfcld 11884	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
562		breq2 4657	. . . . . . . . 9 ⊢ (𝑎 = (𝑥 / 2) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
563	562	anbi2d 740	. . . . . . . 8 ⊢ (𝑎 = (𝑥 / 2) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
564	563	rexralbidv 3058	. . . . . . 7 ⊢ (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
565	564	rspccva 3308	. . . . . 6 ⊢ ((∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ⁺) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
566	559, 561, 565	syl2anc 693	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
567	460, 566	r19.29a 3078	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
568	412, 567	r19.29a 3078	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
569	568	ralrimiva 2966	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
570		ioosscn 39716	. . . 4 ⊢ (𝐴(,)𝐵) ⊆ ℂ
571	570	a1i 11	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
572	463, 571, 98	ellimc3 23643	. 2 ⊢ (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐴) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))))
573	137, 569, 572	mpbir2and 957	1 ⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 {crab 2916 Vcvv 3200 ⊆ wss 3574 ∅c0 3915 ifcif 4086 class class class wbr 4653 ↦ cmpt 4729 dom cdm 5114 ran crn 5115 Rel wrel 5119 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 supcsup 8346 infcinf 8347 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 +∞cpnf 10071 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 (,)cioo 12175 ⌊cfl 12591 abscabs 13974 lim supclsp 14201 ⇝ cli 14215 –cn→ccncf 22679 lim_ℂ climc 23626 D cdv 23627

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631

This theorem is referenced by: ioodvbdlimc1 40148

W3C validator