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 38822

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 11583	. . . . . 6 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
2		zssre 11261	. . . . . 6 ⊢ ℤ ⊆ ℝ
3	1, 2	sstri 3577	. . . . 5 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (ℤ_≥‘𝑀) ⊆ ℝ)
5		ioodvbdlimc1lem2.m	. . . . . . 7 ⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1)
6		ioodvbdlimc1lem2.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
7		ioodvbdlimc1lem2.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
8	6, 7	resubcld 10337	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
9		ioodvbdlimc1lem2.altb	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
10	7, 6	posdifd 10493	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
11	9, 10	mpbid 221	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
12	11	gt0ne0d 10471	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0)
13	8, 12	rereccld 10731	. . . . . . . . 9 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ)
14		0red 9920	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
15	8, 11	recgt0d 10837	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (1 / (𝐵 − 𝐴)))
16	14, 13, 15	ltled 10064	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (1 / (𝐵 − 𝐴)))
17		flge0nn0 12483	. . . . . . . . 9 ⊢ (((1 / (𝐵 − 𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐵 − 𝐴))) → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀)
18	13, 16, 17	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀)
19		peano2nn0 11210	. . . . . . . 8 ⊢ ((⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀ → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℕ₀)
20	18, 19	syl 17	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℕ₀)
21	5, 20	syl5eqel 2692	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
22	21	nn0zd 11356	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
23		eqid 2610	. . . . . 6 ⊢ (ℤ_≥‘𝑀) = (ℤ_≥‘𝑀)
24	23	uzsup 12524	. . . . 5 ⊢ (𝑀 ∈ ℤ → sup((ℤ_≥‘𝑀), ℝ^*, < ) = +∞)
25	22, 24	syl 17	. . . 4 ⊢ (𝜑 → sup((ℤ_≥‘𝑀), ℝ^*, < ) = +∞)
26		ioodvbdlimc1lem2.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
27	26	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
28	7	rexrd 9968	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
29	28	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ^*)
30	6	rexrd 9968	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
31	30	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ^*)
32	7	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
33		eluzelre 11574	. . . . . . . . . 10 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑗 ∈ ℝ)
34	33	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℝ)
35		0red 9920	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 ∈ ℝ)
36		0red 9920	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 0 ∈ ℝ)
37		1red 9934	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 1 ∈ ℝ)
38	36, 37	readdcld 9948	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → (0 + 1) ∈ ℝ)
39	38	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ∈ ℝ)
40	36	ltp1d 10833	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 0 < (0 + 1))
41	40	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 < (0 + 1))
42		eluzel2 11568	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
43	42	zred 11358	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℝ)
44	43	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
45	13	flcld 12461	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℤ)
46	45	zred 11358	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℝ)
47		1red 9934	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℝ)
48	18	nn0ge0d 11231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ≤ (⌊‘(1 / (𝐵 − 𝐴))))
49	14, 46, 47, 48	leadd1dd 10520	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + 1) ≤ ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
50	49, 5	syl6breqr 4625	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 + 1) ≤ 𝑀)
51	50	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ≤ 𝑀)
52		eluzle 11576	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑗)
53	52	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑗)
54	39, 44, 34, 51, 53	letrd 10073	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ≤ 𝑗)
55	35, 39, 34, 41, 54	ltletrd 10076	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑗)
56	55	gt0ne0d 10471	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ≠ 0)
57	34, 56	rereccld 10731	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ∈ ℝ)
58	32, 57	readdcld 9948	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ ℝ)
59	34, 55	elrpd 11745	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℝ⁺)
60	59	rpreccld 11758	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ∈ ℝ⁺)
61	32, 60	ltaddrpd 11781	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 < (𝐴 + (1 / 𝑗)))
62	21	nn0red 11229	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
63	14, 47	readdcld 9948	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + 1) ∈ ℝ)
64	46, 47	readdcld 9948	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℝ)
65	14	ltp1d 10833	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (0 + 1))
66	14, 63, 64, 65, 49	ltletrd 10076	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
67	66, 5	syl6breqr 4625	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝑀)
68	67	gt0ne0d 10471	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≠ 0)
69	62, 68	rereccld 10731	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 𝑀) ∈ ℝ)
70	69	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑀) ∈ ℝ)
71	32, 70	readdcld 9948	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑀)) ∈ ℝ)
72	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ)
73	62, 67	elrpd 11745	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
74	73	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ⁺)
75		1red 9934	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 1 ∈ ℝ)
76		0le1 10430	. . . . . . . . . . 11 ⊢ 0 ≤ 1
77	76	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 ≤ 1)
78	74, 59, 75, 77, 53	lediv2ad 11770	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀))
79	57, 70, 32, 78	leadd2dd 10521	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ≤ (𝐴 + (1 / 𝑀)))
80	5	eqcomi 2619	. . . . . . . . . . . . 13 ⊢ ((⌊‘(1 / (𝐵 − 𝐴))) + 1) = 𝑀
81	80	oveq2i 6560	. . . . . . . . . . . 12 ⊢ (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) = (1 / 𝑀)
82	81, 69	syl5eqel 2692	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) ∈ ℝ)
83	13, 15	elrpd 11745	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ⁺)
84	64, 66	elrpd 11745	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℝ⁺)
85		1rp 11712	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ⁺
86	85	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ⁺)
87		fllelt 12460	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) ∈ ℝ → ((⌊‘(1 / (𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
88	13, 87	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
89	88	simprd 478	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
90	83, 84, 86, 89	ltdiv2dd 38448	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) < (1 / (1 / (𝐵 − 𝐴))))
91	8	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ)
92	91, 12	recrecd 10677	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / (1 / (𝐵 − 𝐴))) = (𝐵 − 𝐴))
93	90, 92	breqtrd 4609	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) < (𝐵 − 𝐴))
94	82, 8, 7, 93	ltadd2dd 10075	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) < (𝐴 + (𝐵 − 𝐴)))
95	5	oveq2i 6560	. . . . . . . . . . . 12 ⊢ (1 / 𝑀) = (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
96	95	oveq2i 6560	. . . . . . . . . . 11 ⊢ (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
97	96	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))))
98	7	recnd 9947	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
99	6	recnd 9947	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
100	98, 99	pncan3d 10274	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
101	100	eqcomd 2616	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = (𝐴 + (𝐵 − 𝐴)))
102	94, 97, 101	3brtr4d 4615	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 + (1 / 𝑀)) < 𝐵)
103	102	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑀)) < 𝐵)
104	58, 71, 72, 79, 103	lelttrd 10074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) < 𝐵)
105	29, 31, 58, 61, 104	eliood 38567	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
106	27, 105	ffvelrnd 6268	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
107		ioodvbdlimc1lem2.s	. . . . 5 ⊢ 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗))))
108	106, 107	fmptd 6292	. . . 4 ⊢ (𝜑 → 𝑆:(ℤ_≥‘𝑀)⟶ℝ)
109		ioodvbdlimc1lem2.dmdv	. . . . . 6 ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
110		ioodvbdlimc1lem2.dvbd	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
111	7, 6, 9, 26, 109, 110	dvbdfbdioo 38820	. . . . 5 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏)
112	62	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ)
113		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ (ℤ_≥‘𝑀))
114	107	fvmpt2 6200	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (ℤ_≥‘𝑀) ∧ (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
115	113, 106, 114	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
116	115	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
117	116	adantlr 747	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
118		simplr 788	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏)
119	105	adantlr 747	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
120		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → (𝐹‘𝑥) = (𝐹‘(𝐴 + (1 / 𝑗))))
121	120	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
122	121	breq1d 4593	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → ((abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏))
123	122	rspccva 3281	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 ∧ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
124	118, 119, 123	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
125	117, 124	eqbrtrd 4605	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) ≤ 𝑏)
126	125	a1d 25	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
127	126	ralrimiva 2949	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
128		breq1 4586	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑀 → (𝑘 ≤ 𝑗 ↔ 𝑀 ≤ 𝑗))
129	128	imbi1d 330	. . . . . . . . . 10 ⊢ (𝑘 = 𝑀 → ((𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
130	129	ralbidv 2969	. . . . . . . . 9 ⊢ (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
131	130	rspcev 3282	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
132	112, 127, 131	syl2anc 691	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
133	132	ex 449	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
134	133	reximdv 2999	. . . . 5 ⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
135	111, 134	mpd 15	. . . 4 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
136	4, 25, 108, 135	limsupre 38708	. . 3 ⊢ (𝜑 → (lim sup‘𝑆) ∈ ℝ)
137	136	recnd 9947	. 2 ⊢ (𝜑 → (lim sup‘𝑆) ∈ ℂ)
138		eluzelre 11574	. . . . . . . . 9 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑗 ∈ ℝ)
139	138	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑗 ∈ ℝ)
140		0red 9920	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 ∈ ℝ)
141	45	peano2zd 11361	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℤ)
142	5, 141	syl5eqel 2692	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
143	142	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ∈ ℤ)
144	143	zred 11358	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ∈ ℝ)
145	144	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ∈ ℝ)
146	67	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < 𝑀)
147		ioodvbdlimc1lem2.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
148		ioodvbdlimc1lem2.y	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
149		ioomidp 38587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
150	7, 6, 9, 149	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
151		ne0i 3880	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴(,)𝐵) ≠ ∅)
153		ioossre 12106	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴(,)𝐵) ⊆ ℝ
154	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
155		dvfre 23520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
156	26, 154, 155	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
157	109	feq2d 5944	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
158	156, 157	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
159	158	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
160	159	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
161	160	abscld 14023	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
162		eqid 2610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥)))
163		eqid 2610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
164	152, 161, 110, 162, 163	suprnmpt 38350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )))
165	164	simpld 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ)
166	148, 165	syl5eqel 2692	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑌 ∈ ℝ)
167	166	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑌 ∈ ℝ)
168		rpre 11715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
169	168	rehalfcld 11156	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ)
170	169	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
171	168	recnd 9947	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
172	171	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
173		2cnd 10970	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℂ)
174		rpne0 11724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
175	174	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
176		2ne0 10990	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
177	176	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ≠ 0)
178	172, 173, 175, 177	divne0d 10696	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ≠ 0)
179	167, 170, 178	redivcld 10732	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
180	179	flcld 12461	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
181	180	peano2zd 11361	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
182	181, 143	ifcld 4081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
183	147, 182	syl5eqel 2692	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ ℤ)
184	183	zred 11358	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ ℝ)
185	184	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑁 ∈ ℝ)
186	181	zred 11358	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
187		max1 11890	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
188	144, 186, 187	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
189	188, 147	syl6breqr 4625	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ≤ 𝑁)
190	189	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ≤ 𝑁)
191		eluzle 11576	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑁 ≤ 𝑗)
192	191	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑁 ≤ 𝑗)
193	145, 185, 139, 190, 192	letrd 10073	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ≤ 𝑗)
194	140, 145, 139, 146, 193	ltletrd 10076	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < 𝑗)
195	194	gt0ne0d 10471	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑗 ≠ 0)
196	139, 195	rereccld 10731	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (1 / 𝑗) ∈ ℝ)
197	139, 194	recgt0d 10837	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < (1 / 𝑗))
198	196, 197	elrpd 11745	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (1 / 𝑗) ∈ ℝ⁺)
199	198	adantr 480	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈ ℝ⁺)
200		ioodvbdlimc1lem2.ch	. . . . . . . . 9 ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)))
201	200	biimpi 205	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)))
202		simp-5l 804	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝜑)
203	201, 202	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝜑)
204	203, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
205	201	simplrd 789	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑧 ∈ (𝐴(,)𝐵))
206	204, 205	ffvelrnd 6268	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝐹‘𝑧) ∈ ℝ)
207	206	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝐹‘𝑧) ∈ ℂ)
208	203, 108	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑆:(ℤ_≥‘𝑀)⟶ℝ)
209		simp-5r 805	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝑥 ∈ ℝ⁺)
210	201, 209	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑥 ∈ ℝ⁺)
211		eluz2 11569	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
212	143, 183, 189, 211	syl3anbrc 1239	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ (ℤ_≥‘𝑀))
213	203, 210, 212	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑁 ∈ (ℤ_≥‘𝑀))
214		uzss 11584	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
215	213, 214	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
216		simp-4r 803	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ_≥‘𝑁))
217	201, 216	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑗 ∈ (ℤ_≥‘𝑁))
218	215, 217	sseldd 3569	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑗 ∈ (ℤ_≥‘𝑀))
219	208, 218	ffvelrnd 6268	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
220	219	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ)
221	203, 137	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → (lim sup‘𝑆) ∈ ℂ)
222	207, 220, 221	npncand 10295	. . . . . . . . . . . 12 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) = ((𝐹‘𝑧) − (lim sup‘𝑆)))
223	222	eqcomd 2616	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹‘𝑧) − (lim sup‘𝑆)) = (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))))
224	223	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))))
225	206, 219	resubcld 10337	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℝ)
226	203, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (lim sup‘𝑆) ∈ ℝ)
227	219, 226	resubcld 10337	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℝ)
228	225, 227	readdcld 9948	. . . . . . . . . . . . 13 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ)
229	228	recnd 9947	. . . . . . . . . . . 12 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℂ)
230	229	abscld 14023	. . . . . . . . . . 11 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
231	225	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℂ)
232	231	abscld 14023	. . . . . . . . . . . 12 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ∈ ℝ)
233	227	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℂ)
234	233	abscld 14023	. . . . . . . . . . . 12 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ)
235	232, 234	readdcld 9948	. . . . . . . . . . 11 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
236	210	rpred 11748	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑥 ∈ ℝ)
237	231, 233	abstrid 14043	. . . . . . . . . . 11 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))))
238	236	rehalfcld 11156	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑥 / 2) ∈ ℝ)
239	207, 220	abssubd 14040	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) = (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))))
240	203, 218, 115	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
241	240	oveq1d 6564	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ((𝑆‘𝑗) − (𝐹‘𝑧)) = ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)))
242	241	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))) = (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))))
243	203, 218, 106	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
244	243, 206	resubcld 10337	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)) ∈ ℝ)
245	244	recnd 9947	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)) ∈ ℂ)
246	245	abscld 14023	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ∈ ℝ)
247	203, 166	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑌 ∈ ℝ)
248	203, 218, 58	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝐴 + (1 / 𝑗)) ∈ ℝ)
249	153, 205	sseldi 3566	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑧 ∈ ℝ)
250	248, 249	resubcld 10337	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ∈ ℝ)
251	247, 250	remulcld 9949	. . . . . . . . . . . . . . . 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 478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
256	148	breq2i 4591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
257	256	ralbii 2963	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
258	255, 257	sylibr 223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
259	203, 258	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
260		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑥 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑥))
261	260	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥)))
262	261	breq1d 4593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌))
263	262	cbvralv 3147	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
264	259, 263	sylibr 223	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌)
265	249	rexrd 9968	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑧 ∈ ℝ^*)
266	203, 30	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐵 ∈ ℝ^*)
267	249, 252	resubcld 10337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑧 − 𝐴) ∈ ℝ)
268	267	recnd 9947	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (𝑧 − 𝐴) ∈ ℂ)
269	268	abscld 14023	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (abs‘(𝑧 − 𝐴)) ∈ ℝ)
270	3, 218	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑗 ∈ ℝ)
271	203, 218, 56	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑗 ≠ 0)
272	270, 271	rereccld 10731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (1 / 𝑗) ∈ ℝ)
273	267	leabsd 14001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑧 − 𝐴) ≤ (abs‘(𝑧 − 𝐴)))
274	201	simprd 478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))
275	267, 269, 272, 273, 274	lelttrd 10074	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝑧 − 𝐴) < (1 / 𝑗))
276	249, 252, 272	ltsubadd2d 10504	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ((𝑧 − 𝐴) < (1 / 𝑗) ↔ 𝑧 < (𝐴 + (1 / 𝑗))))
277	275, 276	mpbid 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑧 < (𝐴 + (1 / 𝑗)))
278	203, 218, 104	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝐴 + (1 / 𝑗)) < 𝐵)
279	265, 266, 248, 277, 278	eliood 38567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝐴 + (1 / 𝑗)) ∈ (𝑧(,)𝐵))
280	252, 253, 204, 254, 247, 264, 205, 279	dvbdfbdioolem1 38818	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ((abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∧ (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · (𝐵 − 𝐴))))
281	280	simpld 474	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)))
282	203, 218, 57	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (1 / 𝑗) ∈ ℝ)
283	247, 282	remulcld 9949	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ)
284	158, 150	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ)
285	284	recnd 9947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ)
286	285	abscld 14023	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ)
287	285	absge0d 14031	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 ≤ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
288		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))
289	288	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
290	148	eqcomi 2619	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌
291	290	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌)
292	289, 291	breq12d 4596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌))
293	292	rspcva 3280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
294	150, 255, 293	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
295	14, 286, 166, 287, 294	letrd 10073	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≤ 𝑌)
296	203, 295	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 0 ≤ 𝑌)
297	203, 28	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝐴 ∈ ℝ^*)
298		ioogtlb 38564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑧)
299	297, 266, 205, 298	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 𝐴 < 𝑧)
300	252, 249, 248, 299	ltsub2dd 10519	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < ((𝐴 + (1 / 𝑗)) − 𝐴))
301	203, 98	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 𝐴 ∈ ℂ)
302	282	recnd 9947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (1 / 𝑗) ∈ ℂ)
303	301, 302	pncan2d 10273	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝐴) = (1 / 𝑗))
304	300, 303	breqtrd 4609	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < (1 / 𝑗))
305	250, 272, 304	ltled 10064	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ≤ (1 / 𝑗))
306	250, 272, 247, 296, 305	lemul2ad 10843	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑌 · (1 / 𝑗)))
307	283	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
308	238	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑥 / 2) ∈ ℝ)
309		oveq1 6556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗)))
310	302	mul02d 10113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (0 · (1 / 𝑗)) = 0)
311	309, 310	sylan9eqr 2666	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0)
312	210	rphalfcld 11760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (𝑥 / 2) ∈ ℝ⁺)
313	312	rpgt0d 11751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 0 < (𝑥 / 2))
314	313	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑌 = 0) → 0 < (𝑥 / 2))
315	311, 314	eqbrtrd 4605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2))
316	307, 308, 315	ltled 10064	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
317	247	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ)
318	296	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌)
319		neqne 2790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑌 = 0 → 𝑌 ≠ 0)
320	319	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0)
321	317, 318, 320	ne0gt0d 10053	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌)
322	283	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
323	3, 213	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ∈ ℝ)
324		0red 9920	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 0 ∈ ℝ)
325	203, 210, 144	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑀 ∈ ℝ)
326	203, 67	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 0 < 𝑀)
327	203, 210, 189	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑀 ≤ 𝑁)
328	324, 325, 323, 326, 327	ltletrd 10076	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 0 < 𝑁)
329	328	gt0ne0d 10471	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ≠ 0)
330	323, 329	rereccld 10731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (1 / 𝑁) ∈ ℝ)
331	247, 330	remulcld 9949	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ)
332	331	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ)
333	238	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ)
334	282	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ)
335	330	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ)
336	247	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ)
337	296	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌)
338	323, 328	elrpd 11745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ∈ ℝ⁺)
339	203, 218, 59	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑗 ∈ ℝ⁺)
340		1red 9934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 1 ∈ ℝ)
341	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 0 ≤ 1)
342	217, 191	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ≤ 𝑗)
343	338, 339, 340, 341, 342	lediv2ad 11770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁))
344	343	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁))
345	334, 335, 336, 337, 344	lemul2ad 10843	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁)))
346	236	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑥 ∈ ℂ)
347		2cnd 10970	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 2 ∈ ℂ)
348	210	rpne0d 11753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑥 ≠ 0)
349	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 2 ≠ 0)
350	346, 347, 348, 349	divne0d 10696	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑥 / 2) ≠ 0)
351	247, 238, 350	redivcld 10732	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ)
352	351	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
353		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌)
354	313	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2))
355	336, 333, 353, 354	divgt0d 10838	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2)))
356	352, 355	elrpd 11745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ⁺)
357	356	rprecred 11759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ)
358	338	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈ ℝ⁺)
359		1red 9934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ)
360	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1)
361	351	flcld 12461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
362	361	peano2zd 11361	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
363	362	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
364	203, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜒 → 𝑀 ∈ ℤ)
365	362, 364	ifcld 4081	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
366	147, 365	syl5eqel 2692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑁 ∈ ℤ)
367	366	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 𝑁 ∈ ℝ)
368		flltp1 12463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
369	351, 368	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
370	203, 62	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → 𝑀 ∈ ℝ)
371		max2 11892	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
372	370, 363, 371	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
373	372, 147	syl6breqr 4625	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁)
374	351, 363, 367, 369, 373	ltletrd 10076	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁)
375	351, 323, 374	ltled 10064	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
376	375	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
377	356, 358, 359, 360, 376	lediv2ad 11770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2))))
378	335, 357, 336, 337, 377	lemul2ad 10843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
379	336	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ)
380	352	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ)
381	355	gt0ne0d 10471	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0)
382	379, 380, 381	divrecd 10683	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
383	333	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ)
384	353	gt0ne0d 10471	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0)
385	350	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0)
386	379, 383, 384, 385	ddcand 10700	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2))
387	382, 386	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2))
388	378, 387	breqtrd 4609	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2))
389	322, 332, 333, 345, 388	letrd 10073	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
390	321, 389	syldan 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
391	316, 390	pm2.61dan 828	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
392	251, 283, 238, 306, 391	letrd 10073	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑥 / 2))
393	246, 251, 238, 281, 392	letrd 10073	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑥 / 2))
394	242, 393	eqbrtrd 4605	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))) ≤ (𝑥 / 2))
395	239, 394	eqbrtrd 4605	. . . . . . . . . . . . 13 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ≤ (𝑥 / 2))
396		simpllr 795	. . . . . . . . . . . . . 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 10528	. . . . . . . . . . . 12 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2)))
399	346	2halvesd 11155	. . . . . . . . . . . 12 ⊢ (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
400	398, 399	breqtrd 4609	. . . . . . . . . . 11 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥)
401	230, 235, 236, 237, 400	lelttrd 10074	. . . . . . . . . 10 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥)
402	224, 401	eqbrtrd 4605	. . . . . . . . 9 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
403	200, 402	sylbir 224	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
404	403	adantrl 748	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
405	404	ex 449	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
406	405	ralrimiva 2949	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
407		breq2 4587	. . . . . . . . 9 ⊢ (𝑦 = (1 / 𝑗) → ((abs‘(𝑧 − 𝐴)) < 𝑦 ↔ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)))
408	407	anbi2d 736	. . . . . . . 8 ⊢ (𝑦 = (1 / 𝑗) → ((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) ↔ (𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))))
409	408	imbi1d 330	. . . . . . 7 ⊢ (𝑦 = (1 / 𝑗) → (((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) ↔ ((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)))
410	409	ralbidv 2969	. . . . . 6 ⊢ (𝑦 = (1 / 𝑗) → (∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) ↔ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)))
411	410	rspcev 3282	. . . . 5 ⊢ (((1 / 𝑗) ∈ ℝ⁺ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
412	199, 406, 411	syl2anc 691	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
413		simpr 476	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → 𝑏 ≤ 𝑁)
414	413	iftrued 4044	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑁)
415		uzid 11578	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ_≥‘𝑁))
416	183, 415	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ (ℤ_≥‘𝑁))
417	416	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → 𝑁 ∈ (ℤ_≥‘𝑁))
418	414, 417	eqeltrd 2688	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
419	418	adantlr 747	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
420		iffalse 4045	. . . . . . . . . 10 ⊢ (¬ 𝑏 ≤ 𝑁 → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏)
421	420	adantl 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏)
422	183	ad2antrr 758	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ∈ ℤ)
423		simplr 788	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ ℤ)
424	422	zred 11358	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ∈ ℝ)
425	423	zred 11358	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ ℝ)
426		simpr 476	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → ¬ 𝑏 ≤ 𝑁)
427	424, 425	ltnled 10063	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑁))
428	426, 427	mpbird 246	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 < 𝑏)
429	424, 425, 428	ltled 10064	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ≤ 𝑏)
430		eluz2 11569	. . . . . . . . . 10 ⊢ (𝑏 ∈ (ℤ_≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ≤ 𝑏))
431	422, 423, 429, 430	syl3anbrc 1239	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ (ℤ_≥‘𝑁))
432	421, 431	eqeltrd 2688	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
433	419, 432	pm2.61dan 828	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
434	433	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
435		simpr 476	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
436		simpr 476	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
437	183	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
438	437, 436	ifcld 4081	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ)
439	436	zred 11358	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
440	437	zred 11358	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℝ)
441		max1 11890	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))
442	439, 440, 441	syl2anc 691	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))
443		eluz2 11569	. . . . . . . . . 10 ⊢ (if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
444	436, 438, 442, 443	syl3anbrc 1239	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏))
445	444	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏))
446		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑐) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
447	446	eleq1d 2672	. . . . . . . . . 10 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ))
448	446	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑐) − (lim sup‘𝑆)) = ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))
449	448	fveq2d 6107	. . . . . . . . . . 11 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
450	449	breq1d 4593	. . . . . . . . . 10 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
451	447, 450	anbi12d 743	. . . . . . . . 9 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))))
452	451	rspccva 3281	. . . . . . . 8 ⊢ ((∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏)) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
453	435, 445, 452	syl2anc 691	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
454	453	simprd 478	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))
455		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑗) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
456	455	oveq1d 6564	. . . . . . . . 9 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑗) − (lim sup‘𝑆)) = ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))
457	456	fveq2d 6107	. . . . . . . 8 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
458	457	breq1d 4593	. . . . . . 7 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
459	458	rspcev 3282	. . . . . 6 ⊢ ((if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁) ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
460	434, 454, 459	syl2anc 691	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
461		ax-resscn 9872	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
462	461	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℝ ⊆ ℂ)
463	26, 462	fssd 5970	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ)
464		dvcn 23490	. . . . . . . . . . . . . 14 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
465	462, 463, 154, 109, 464	syl31anc 1321	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
466		cncffvrn 22509	. . . . . . . . . . . . 13 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
467	462, 465, 466	syl2anc 691	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
468	26, 467	mpbird 246	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
469		ioodvbdlimc1lem2.r	. . . . . . . . . . . 12 ⊢ 𝑅 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐴 + (1 / 𝑗)))
470	105, 469	fmptd 6292	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅:(ℤ_≥‘𝑀)⟶(𝐴(,)𝐵))
471		eqid 2610	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))
472		climrel 14071	. . . . . . . . . . . . 13 ⊢ Rel ⇝
473	472	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Rel ⇝ )
474		fvex 6113	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑀) ∈ V
475	474	mptex 6390	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) ∈ V
476	475	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) ∈ V)
477		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴))
478		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑚) → 𝐴 = 𝐴)
479		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ (ℤ_≥‘𝑀))
480	7	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
481	477, 478, 479, 480	fvmptd 6197	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑚) = 𝐴)
482	23, 142, 476, 98, 481	climconst 14122	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) ⇝ 𝐴)
483	474	mptex 6390	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐴 + (1 / 𝑗))) ∈ V
484	469, 483	eqeltri 2684	. . . . . . . . . . . . . . 15 ⊢ 𝑅 ∈ V
485	484	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ V)
486		1cnd 9935	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
487		elnnnn0b 11214	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ₀ ∧ 0 < 𝑀))
488	21, 67, 487	sylanbrc 695	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
489		divcnvg 38694	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0)
490	486, 488, 489	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0)
491		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴))
492		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → 𝐴 = 𝐴)
493		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ (ℤ_≥‘𝑀))
494	7	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
495	491, 492, 493, 494	fvmptd 6197	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) = 𝐴)
496	98	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℂ)
497	495, 496	eqeltrd 2688	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) ∈ ℂ)
498		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)))
499		oveq2 6557	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖))
500	499	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖))
501	3, 493	sseldi 3566	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℝ)
502		0red 9920	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 ∈ ℝ)
503	62	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
504	67	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑀)
505		eluzle 11576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑖)
506	505	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑖)
507	502, 503, 501, 504, 506	ltletrd 10076	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑖)
508	507	gt0ne0d 10471	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ≠ 0)
509	501, 508	rereccld 10731	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑖) ∈ ℝ)
510	498, 500, 493, 509	fvmptd 6197	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖))
511	501	recnd 9947	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℂ)
512	511, 508	reccld 10673	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑖) ∈ ℂ)
513	510, 512	eqeltrd 2688	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ)
514	469	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑅 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐴 + (1 / 𝑗))))
515	499	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
516	515	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
517	494, 509	readdcld 9948	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑖)) ∈ ℝ)
518	514, 516, 493, 517	fvmptd 6197	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑖) = (𝐴 + (1 / 𝑖)))
519	495, 510	oveq12d 6567	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐴 + (1 / 𝑖)))
520	518, 519	eqtr4d 2647	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑖) = (((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)))
521	23, 142, 482, 485, 490, 497, 513, 520	climadd 14210	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ⇝ (𝐴 + 0))
522	98	addid1d 10115	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 + 0) = 𝐴)
523	521, 522	breqtrd 4609	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ⇝ 𝐴)
524		releldm 5279	. . . . . . . . . . . 12 ⊢ ((Rel ⇝ ∧ 𝑅 ⇝ 𝐴) → 𝑅 ∈ dom ⇝ )
525	473, 523, 524	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ dom ⇝ )
526		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → (ℤ_≥‘𝑙) = (ℤ_≥‘𝑘))
527		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = 𝑘 → (𝑅‘𝑙) = (𝑅‘𝑘))
528	527	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 𝑘 → ((𝑅‘ℎ) − (𝑅‘𝑙)) = ((𝑅‘ℎ) − (𝑅‘𝑘)))
529	528	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑘 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) = (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))))
530	529	breq1d 4593	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
531	526, 530	raleqbidv 3129	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → (∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
532	531	cbvrabv 3172	. . . . . . . . . . . . 13 ⊢ {𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
533		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = 𝑖 → (𝑅‘ℎ) = (𝑅‘𝑖))
534	533	oveq1d 6564	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = 𝑖 → ((𝑅‘ℎ) − (𝑅‘𝑘)) = ((𝑅‘𝑖) − (𝑅‘𝑘)))
535	534	fveq2d 6107	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑖 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) = (abs‘((𝑅‘𝑖) − (𝑅‘𝑘))))
536	535	breq1d 4593	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑖 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
537	536	cbvralv 3147	. . . . . . . . . . . . . . 15 ⊢ (∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
538	537	rgenw 2908	. . . . . . . . . . . . . 14 ⊢ ∀𝑘 ∈ (ℤ_≥‘𝑀)(∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
539		rabbi 3097	. . . . . . . . . . . . . 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 219	. . . . . . . . . . . . 13 ⊢ {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
541	532, 540	eqtri 2632	. . . . . . . . . . . 12 ⊢ {𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
542	541	infeq1i 8267	. . . . . . . . . . 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 38821	. . . . . . . . . 10 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) ⇝ (lim sup‘(𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))))
544	469	fvmpt2 6200	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (ℤ_≥‘𝑀) ∧ (𝐴 + (1 / 𝑗)) ∈ ℝ) → (𝑅‘𝑗) = (𝐴 + (1 / 𝑗)))
545	113, 58, 544	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑗) = (𝐴 + (1 / 𝑗)))
546	545	eqcomd 2616	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) = (𝑅‘𝑗))
547	546	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) = (𝐹‘(𝑅‘𝑗)))
548	547	mpteq2dva 4672	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))
549	107, 548	syl5eq 2656	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))
550	549	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))))
551	543, 549, 550	3brtr4d 4615	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⇝ (lim sup‘𝑆))
552	474	mptex 6390	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) ∈ V
553	107, 552	eqeltri 2684	. . . . . . . . . . 11 ⊢ 𝑆 ∈ V
554	553	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ V)
555		eqidd 2611	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ℤ) → (𝑆‘𝑐) = (𝑆‘𝑐))
556	554, 555	clim 14073	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))))
557	551, 556	mpbid 221	. . . . . . . 8 ⊢ (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)))
558	557	simprd 478	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))
559	558	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))
560		simpr 476	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
561	560	rphalfcld 11760	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
562		breq2 4587	. . . . . . . . 9 ⊢ (𝑎 = (𝑥 / 2) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
563	562	anbi2d 736	. . . . . . . 8 ⊢ (𝑎 = (𝑥 / 2) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
564	563	rexralbidv 3040	. . . . . . 7 ⊢ (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
565	564	rspccva 3281	. . . . . 6 ⊢ ((∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ⁺) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
566	559, 561, 565	syl2anc 691	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
567	460, 566	r19.29a 3060	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
568	412, 567	r19.29a 3060	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
569	568	ralrimiva 2949	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
570		ioosscn 38563	. . . 4 ⊢ (𝐴(,)𝐵) ⊆ ℂ
571	570	a1i 11	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
572	463, 571, 98	ellimc3 23449	. 2 ⊢ (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐴) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))))
573	137, 569, 572	mpbir2and 959	1 ⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 Vcvv 3173 ⊆ wss 3540 ∅c0 3874 ifcif 4036 class class class wbr 4583 ↦ cmpt 4643 dom cdm 5038 ran crn 5039 Rel wrel 5043 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 supcsup 8229 infcinf 8230 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 +∞cpnf 9950 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 − cmin 10145 / cdiv 10563 ℕcn 10897 2c2 10947 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ℝ⁺crp 11708 (,)cioo 12046 ⌊cfl 12453 abscabs 13822 lim supclsp 14049 ⇝ cli 14063 –cn→ccncf 22487 lim_ℂ climc 23432 D cdv 23433

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-supp 7183 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fsupp 8159 df-fi 8200 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-z 11255 df-dec 11370 df-uz 11564 df-q 11665 df-rp 11709 df-xneg 11822 df-xadd 11823 df-xmul 11824 df-ioo 12050 df-ico 12052 df-icc 12053 df-fz 12198 df-fzo 12335 df-fl 12455 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-limsup 14050 df-clim 14067 df-rlim 14068 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-starv 15783 df-sca 15784 df-vsca 15785 df-ip 15786 df-tset 15787 df-ple 15788 df-ds 15791 df-unif 15792 df-hom 15793 df-cco 15794 df-rest 15906 df-topn 15907 df-0g 15925 df-gsum 15926 df-topgen 15927 df-pt 15928 df-prds 15931 df-xrs 15985 df-qtop 15990 df-imas 15991 df-xps 15993 df-mre 16069 df-mrc 16070 df-acs 16072 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-submnd 17159 df-mulg 17364 df-cntz 17573 df-cmn 18018 df-psmet 19559 df-xmet 19560 df-met 19561 df-bl 19562 df-mopn 19563 df-fbas 19564 df-fg 19565 df-cnfld 19568 df-top 20521 df-bases 20522 df-topon 20523 df-topsp 20524 df-cld 20633 df-ntr 20634 df-cls 20635 df-nei 20712 df-lp 20750 df-perf 20751 df-cn 20841 df-cnp 20842 df-haus 20929 df-cmp 21000 df-tx 21175 df-hmeo 21368 df-fil 21460 df-fm 21552 df-flim 21553 df-flf 21554 df-xms 21935 df-ms 21936 df-tms 21937 df-cncf 22489 df-limc 23436 df-dv 23437

This theorem is referenced by: ioodvbdlimc1 38823

W3C validator