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 46040

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 12753	. . . . . 6 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
2		zssre 12475	. . . . . 6 ⊢ ℤ ⊆ ℝ
3	1, 2	sstri 3939	. . . . 5 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (ℤ_≥‘𝑀) ⊆ ℝ)
5		ioodvbdlimc1lem2.m	. . . . . . 7 ⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1)
6		ioodvbdlimc1lem2.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
7		ioodvbdlimc1lem2.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
8	6, 7	resubcld 11545	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
9		ioodvbdlimc1lem2.altb	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
10	7, 6	posdifd 11704	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
11	9, 10	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
12	11	gt0ne0d 11681	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0)
13	8, 12	rereccld 11948	. . . . . . . . 9 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ)
14		0red 11115	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
15	8, 11	recgt0d 12056	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (1 / (𝐵 − 𝐴)))
16	14, 13, 15	ltled 11261	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (1 / (𝐵 − 𝐴)))
17		flge0nn0 13724	. . . . . . . . 9 ⊢ (((1 / (𝐵 − 𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐵 − 𝐴))) → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀)
18	13, 16, 17	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀)
19		peano2nn0 12421	. . . . . . . 8 ⊢ ((⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀ → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℕ₀)
20	18, 19	syl 17	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℕ₀)
21	5, 20	eqeltrid 2835	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
22	21	nn0zd 12494	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
23		eqid 2731	. . . . . 6 ⊢ (ℤ_≥‘𝑀) = (ℤ_≥‘𝑀)
24	23	uzsup 13767	. . . . 5 ⊢ (𝑀 ∈ ℤ → sup((ℤ_≥‘𝑀), ℝ^*, < ) = +∞)
25	22, 24	syl 17	. . . 4 ⊢ (𝜑 → sup((ℤ_≥‘𝑀), ℝ^*, < ) = +∞)
26		ioodvbdlimc1lem2.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
27	26	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
28	7	rexrd 11162	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
29	28	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ^*)
30	6	rexrd 11162	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
31	30	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ^*)
32	7	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
33		eluzelre 12743	. . . . . . . . . 10 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑗 ∈ ℝ)
34	33	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℝ)
35		0red 11115	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 ∈ ℝ)
36		0red 11115	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 0 ∈ ℝ)
37		1red 11113	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 1 ∈ ℝ)
38	36, 37	readdcld 11141	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → (0 + 1) ∈ ℝ)
39	38	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ∈ ℝ)
40	36	ltp1d 12052	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 0 < (0 + 1))
41	40	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 < (0 + 1))
42		eluzel2 12737	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
43	42	zred 12577	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℝ)
44	43	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
45	13	flcld 13702	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℤ)
46	45	zred 12577	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℝ)
47		1red 11113	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℝ)
48	18	nn0ge0d 12445	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ≤ (⌊‘(1 / (𝐵 − 𝐴))))
49	14, 46, 47, 48	leadd1dd 11731	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + 1) ≤ ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
50	49, 5	breqtrrdi 5131	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 + 1) ≤ 𝑀)
51	50	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ≤ 𝑀)
52		eluzle 12745	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑗)
53	52	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑗)
54	39, 44, 34, 51, 53	letrd 11270	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ≤ 𝑗)
55	35, 39, 34, 41, 54	ltletrd 11273	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑗)
56	55	gt0ne0d 11681	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ≠ 0)
57	34, 56	rereccld 11948	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ∈ ℝ)
58	32, 57	readdcld 11141	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ ℝ)
59	34, 55	elrpd 12931	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℝ⁺)
60	59	rpreccld 12944	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ∈ ℝ⁺)
61	32, 60	ltaddrpd 12967	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 < (𝐴 + (1 / 𝑗)))
62	21	nn0red 12443	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
63	14, 47	readdcld 11141	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + 1) ∈ ℝ)
64	46, 47	readdcld 11141	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℝ)
65	14	ltp1d 12052	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (0 + 1))
66	14, 63, 64, 65, 49	ltletrd 11273	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
67	66, 5	breqtrrdi 5131	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝑀)
68	67	gt0ne0d 11681	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≠ 0)
69	62, 68	rereccld 11948	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 𝑀) ∈ ℝ)
70	69	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑀) ∈ ℝ)
71	32, 70	readdcld 11141	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑀)) ∈ ℝ)
72	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ)
73	62, 67	elrpd 12931	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
74	73	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ⁺)
75		1red 11113	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 1 ∈ ℝ)
76		0le1 11640	. . . . . . . . . . 11 ⊢ 0 ≤ 1
77	76	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 ≤ 1)
78	74, 59, 75, 77, 53	lediv2ad 12956	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀))
79	57, 70, 32, 78	leadd2dd 11732	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ≤ (𝐴 + (1 / 𝑀)))
80	5	eqcomi 2740	. . . . . . . . . . . . 13 ⊢ ((⌊‘(1 / (𝐵 − 𝐴))) + 1) = 𝑀
81	80	oveq2i 7357	. . . . . . . . . . . 12 ⊢ (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) = (1 / 𝑀)
82	81, 69	eqeltrid 2835	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) ∈ ℝ)
83	13, 15	elrpd 12931	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ⁺)
84	64, 66	elrpd 12931	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℝ⁺)
85		1rp 12894	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ⁺
86	85	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ⁺)
87		fllelt 13701	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) ∈ ℝ → ((⌊‘(1 / (𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
88	13, 87	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
89	88	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
90	83, 84, 86, 89	ltdiv2dd 45405	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) < (1 / (1 / (𝐵 − 𝐴))))
91	8	recnd 11140	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ)
92	91, 12	recrecd 11894	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / (1 / (𝐵 − 𝐴))) = (𝐵 − 𝐴))
93	90, 92	breqtrd 5115	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) < (𝐵 − 𝐴))
94	82, 8, 7, 93	ltadd2dd 11272	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) < (𝐴 + (𝐵 − 𝐴)))
95	5	oveq2i 7357	. . . . . . . . . . . 12 ⊢ (1 / 𝑀) = (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
96	95	oveq2i 7357	. . . . . . . . . . 11 ⊢ (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
97	96	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))))
98	7	recnd 11140	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
99	6	recnd 11140	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
100	98, 99	pncan3d 11475	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
101	100	eqcomd 2737	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = (𝐴 + (𝐵 − 𝐴)))
102	94, 97, 101	3brtr4d 5121	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 + (1 / 𝑀)) < 𝐵)
103	102	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑀)) < 𝐵)
104	58, 71, 72, 79, 103	lelttrd 11271	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) < 𝐵)
105	29, 31, 58, 61, 104	eliood 45608	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
106	27, 105	ffvelcdmd 7018	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
107		ioodvbdlimc1lem2.s	. . . . 5 ⊢ 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗))))
108	106, 107	fmptd 7047	. . . 4 ⊢ (𝜑 → 𝑆:(ℤ_≥‘𝑀)⟶ℝ)
109		ioodvbdlimc1lem2.dmdv	. . . . . 6 ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
110		ioodvbdlimc1lem2.dvbd	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
111	7, 6, 9, 26, 109, 110	dvbdfbdioo 46038	. . . . 5 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏)
112	62	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ)
113		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ (ℤ_≥‘𝑀))
114	107	fvmpt2 6940	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (ℤ_≥‘𝑀) ∧ (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
115	113, 106, 114	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
116	115	fveq2d 6826	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
117	116	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
118		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏)
119	105	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
120		2fveq3 6827	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
121	120	breq1d 5099	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → ((abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏))
122	121	rspccva 3571	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 ∧ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
123	118, 119, 122	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
124	117, 123	eqbrtrd 5111	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) ≤ 𝑏)
125	124	a1d 25	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
126	125	ralrimiva 3124	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
127		breq1 5092	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑀 → (𝑘 ≤ 𝑗 ↔ 𝑀 ≤ 𝑗))
128	127	imbi1d 341	. . . . . . . . . 10 ⊢ (𝑘 = 𝑀 → ((𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
129	128	ralbidv 3155	. . . . . . . . 9 ⊢ (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
130	129	rspcev 3572	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
131	112, 126, 130	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
132	131	ex 412	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
133	132	reximdv 3147	. . . . 5 ⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
134	111, 133	mpd 15	. . . 4 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
135	4, 25, 108, 134	limsupre 45749	. . 3 ⊢ (𝜑 → (lim sup‘𝑆) ∈ ℝ)
136	135	recnd 11140	. 2 ⊢ (𝜑 → (lim sup‘𝑆) ∈ ℂ)
137		eluzelre 12743	. . . . . . . . 9 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑗 ∈ ℝ)
138	137	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑗 ∈ ℝ)
139		0red 11115	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 ∈ ℝ)
140	45	peano2zd 12580	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℤ)
141	5, 140	eqeltrid 2835	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
142	141	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ∈ ℤ)
143	142	zred 12577	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ∈ ℝ)
144	143	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ∈ ℝ)
145	67	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < 𝑀)
146		ioodvbdlimc1lem2.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
147		ioodvbdlimc1lem2.y	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
148		ioomidp 45624	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
149	7, 6, 9, 148	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
150		ne0i 4288	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
151	149, 150	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴(,)𝐵) ≠ ∅)
152		ioossre 13307	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴(,)𝐵) ⊆ ℝ
153	152	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
154		dvfre 25882	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
155	26, 153, 154	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
156	109	feq2d 6635	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
157	155, 156	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
158	157	ffvelcdmda 7017	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
159	158	recnd 11140	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
160	159	abscld 15346	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
161		eqid 2731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥)))
162		eqid 2731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
163	151, 160, 110, 161, 162	suprnmpt 45281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )))
164	163	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ)
165	147, 164	eqeltrid 2835	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑌 ∈ ℝ)
166	165	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑌 ∈ ℝ)
167		rpre 12899	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
168	167	rehalfcld 12368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ)
169	168	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
170	167	recnd 11140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
171	170	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
172		2cnd 12203	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℂ)
173		rpne0 12907	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
174	173	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
175		2ne0 12229	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
176	175	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ≠ 0)
177	171, 172, 174, 176	divne0d 11913	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ≠ 0)
178	166, 169, 177	redivcld 11949	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
179	178	flcld 13702	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
180	179	peano2zd 12580	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
181	180, 142	ifcld 4519	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
182	146, 181	eqeltrid 2835	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ ℤ)
183	182	zred 12577	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ ℝ)
184	183	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑁 ∈ ℝ)
185	180	zred 12577	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
186		max1 13084	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
187	143, 185, 186	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
188	187, 146	breqtrrdi 5131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ≤ 𝑁)
189	188	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ≤ 𝑁)
190		eluzle 12745	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑁 ≤ 𝑗)
191	190	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑁 ≤ 𝑗)
192	144, 184, 138, 189, 191	letrd 11270	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ≤ 𝑗)
193	139, 144, 138, 145, 192	ltletrd 11273	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < 𝑗)
194	193	gt0ne0d 11681	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑗 ≠ 0)
195	138, 194	rereccld 11948	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (1 / 𝑗) ∈ ℝ)
196	138, 193	recgt0d 12056	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < (1 / 𝑗))
197	195, 196	elrpd 12931	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (1 / 𝑗) ∈ ℝ⁺)
198	197	adantr 480	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈ ℝ⁺)
199		ioodvbdlimc1lem2.ch	. . . . . . . . 9 ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)))
200	199	biimpi 216	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)))
201		simp-5l 784	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝜑)
202	200, 201	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝜑)
203	202, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
204	200	simplrd 769	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑧 ∈ (𝐴(,)𝐵))
205	203, 204	ffvelcdmd 7018	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝐹‘𝑧) ∈ ℝ)
206	205	recnd 11140	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝐹‘𝑧) ∈ ℂ)
207	202, 108	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑆:(ℤ_≥‘𝑀)⟶ℝ)
208		simp-5r 785	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝑥 ∈ ℝ⁺)
209	200, 208	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑥 ∈ ℝ⁺)
210		eluz2 12738	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
211	142, 182, 188, 210	syl3anbrc 1344	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ (ℤ_≥‘𝑀))
212	202, 209, 211	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑁 ∈ (ℤ_≥‘𝑀))
213		uzss 12755	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
214	212, 213	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
215		simp-4r 783	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ_≥‘𝑁))
216	200, 215	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑗 ∈ (ℤ_≥‘𝑁))
217	214, 216	sseldd 3930	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑗 ∈ (ℤ_≥‘𝑀))
218	207, 217	ffvelcdmd 7018	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
219	218	recnd 11140	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ)
220	202, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → (lim sup‘𝑆) ∈ ℂ)
221	206, 219, 220	npncand 11496	. . . . . . . . . . . 12 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) = ((𝐹‘𝑧) − (lim sup‘𝑆)))
222	221	eqcomd 2737	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹‘𝑧) − (lim sup‘𝑆)) = (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))))
223	222	fveq2d 6826	. . . . . . . . . 10 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))))
224	205, 218	resubcld 11545	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℝ)
225	202, 135	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (lim sup‘𝑆) ∈ ℝ)
226	218, 225	resubcld 11545	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℝ)
227	224, 226	readdcld 11141	. . . . . . . . . . . . 13 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ)
228	227	recnd 11140	. . . . . . . . . . . 12 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℂ)
229	228	abscld 15346	. . . . . . . . . . 11 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
230	224	recnd 11140	. . . . . . . . . . . . 13 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℂ)
231	230	abscld 15346	. . . . . . . . . . . 12 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ∈ ℝ)
232	226	recnd 11140	. . . . . . . . . . . . 13 ⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℂ)
233	232	abscld 15346	. . . . . . . . . . . 12 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ)
234	231, 233	readdcld 11141	. . . . . . . . . . 11 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
235	209	rpred 12934	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑥 ∈ ℝ)
236	230, 232	abstrid 15366	. . . . . . . . . . 11 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))))
237	235	rehalfcld 12368	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑥 / 2) ∈ ℝ)
238	206, 219	abssubd 15363	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) = (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))))
239	202, 217, 115	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
240	239	fvoveq1d 7368	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))) = (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))))
241	202, 217, 106	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
242	241, 205	resubcld 11545	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)) ∈ ℝ)
243	242	recnd 11140	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)) ∈ ℂ)
244	243	abscld 15346	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ∈ ℝ)
245	202, 165	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑌 ∈ ℝ)
246	202, 217, 58	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝐴 + (1 / 𝑗)) ∈ ℝ)
247	152, 204	sselid 3927	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑧 ∈ ℝ)
248	246, 247	resubcld 11545	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ∈ ℝ)
249	245, 248	remulcld 11142	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∈ ℝ)
250	202, 7	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝐴 ∈ ℝ)
251	202, 6	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝐵 ∈ ℝ)
252	202, 109	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
253	163	simprd 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
254	147	breq2i 5097	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
255	254	ralbii 3078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
256	253, 255	sylibr 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
257	202, 256	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
258		2fveq3 6827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥)))
259	258	breq1d 5099	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌))
260	259	cbvralvw 3210	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
261	257, 260	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌)
262	247	rexrd 11162	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑧 ∈ ℝ^*)
263	202, 30	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐵 ∈ ℝ^*)
264	247, 250	resubcld 11545	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑧 − 𝐴) ∈ ℝ)
265	264	recnd 11140	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (𝑧 − 𝐴) ∈ ℂ)
266	265	abscld 15346	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (abs‘(𝑧 − 𝐴)) ∈ ℝ)
267	3, 217	sselid 3927	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑗 ∈ ℝ)
268	202, 217, 56	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑗 ≠ 0)
269	267, 268	rereccld 11948	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (1 / 𝑗) ∈ ℝ)
270	264	leabsd 15322	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑧 − 𝐴) ≤ (abs‘(𝑧 − 𝐴)))
271	200	simprd 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))
272	264, 266, 269, 270, 271	lelttrd 11271	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝑧 − 𝐴) < (1 / 𝑗))
273	247, 250, 269	ltsubadd2d 11715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ((𝑧 − 𝐴) < (1 / 𝑗) ↔ 𝑧 < (𝐴 + (1 / 𝑗))))
274	272, 273	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑧 < (𝐴 + (1 / 𝑗)))
275	202, 217, 104	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝐴 + (1 / 𝑗)) < 𝐵)
276	262, 263, 246, 274, 275	eliood 45608	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝐴 + (1 / 𝑗)) ∈ (𝑧(,)𝐵))
277	250, 251, 203, 252, 245, 261, 204, 276	dvbdfbdioolem1 46036	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ((abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∧ (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · (𝐵 − 𝐴))))
278	277	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)))
279	202, 217, 57	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (1 / 𝑗) ∈ ℝ)
280	245, 279	remulcld 11142	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ)
281	157, 149	ffvelcdmd 7018	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ)
282	281	recnd 11140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ)
283	282	abscld 15346	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ)
284	282	absge0d 15354	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 ≤ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
285		2fveq3 6827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
286	147	eqcomi 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌
287	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌)
288	285, 287	breq12d 5102	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌))
289	288	rspcva 3570	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
290	149, 253, 289	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
291	14, 283, 165, 284, 290	letrd 11270	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≤ 𝑌)
292	202, 291	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 0 ≤ 𝑌)
293	202, 28	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝐴 ∈ ℝ^*)
294		ioogtlb 45605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑧)
295	293, 263, 204, 294	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 𝐴 < 𝑧)
296	250, 247, 246, 295	ltsub2dd 11730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < ((𝐴 + (1 / 𝑗)) − 𝐴))
297	202, 98	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 𝐴 ∈ ℂ)
298	279	recnd 11140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (1 / 𝑗) ∈ ℂ)
299	297, 298	pncan2d 11474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝐴) = (1 / 𝑗))
300	296, 299	breqtrd 5115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < (1 / 𝑗))
301	248, 269, 300	ltled 11261	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ≤ (1 / 𝑗))
302	248, 269, 245, 292, 301	lemul2ad 12062	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑌 · (1 / 𝑗)))
303	280	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
304	237	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑥 / 2) ∈ ℝ)
305		oveq1 7353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗)))
306	298	mul02d 11311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (0 · (1 / 𝑗)) = 0)
307	305, 306	sylan9eqr 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0)
308	209	rphalfcld 12946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (𝑥 / 2) ∈ ℝ⁺)
309	308	rpgt0d 12937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 0 < (𝑥 / 2))
310	309	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑌 = 0) → 0 < (𝑥 / 2))
311	307, 310	eqbrtrd 5111	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2))
312	303, 304, 311	ltled 11261	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
313	245	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ)
314	292	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌)
315		neqne 2936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑌 = 0 → 𝑌 ≠ 0)
316	315	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0)
317	313, 314, 316	ne0gt0d 11250	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌)
318	280	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
319	3, 212	sselid 3927	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ∈ ℝ)
320		0red 11115	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 0 ∈ ℝ)
321	202, 209, 143	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑀 ∈ ℝ)
322	202, 67	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 0 < 𝑀)
323	202, 209, 188	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑀 ≤ 𝑁)
324	320, 321, 319, 322, 323	ltletrd 11273	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 0 < 𝑁)
325	324	gt0ne0d 11681	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ≠ 0)
326	319, 325	rereccld 11948	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (1 / 𝑁) ∈ ℝ)
327	245, 326	remulcld 11142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ)
328	327	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ)
329	237	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ)
330	279	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ)
331	326	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ)
332	245	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ)
333	292	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌)
334	319, 324	elrpd 12931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ∈ ℝ⁺)
335	202, 217, 59	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑗 ∈ ℝ⁺)
336		1red 11113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 1 ∈ ℝ)
337	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 0 ≤ 1)
338	216, 190	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 𝑁 ≤ 𝑗)
339	334, 335, 336, 337, 338	lediv2ad 12956	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁))
340	339	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁))
341	330, 331, 332, 333, 340	lemul2ad 12062	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁)))
342	235	recnd 11140	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑥 ∈ ℂ)
343		2cnd 12203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 2 ∈ ℂ)
344	209	rpne0d 12939	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑥 ≠ 0)
345	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 2 ≠ 0)
346	342, 343, 344, 345	divne0d 11913	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑥 / 2) ≠ 0)
347	245, 237, 346	redivcld 11949	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ)
348	347	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
349		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌)
350	309	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2))
351	332, 329, 349, 350	divgt0d 12057	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2)))
352	348, 351	elrpd 12931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ⁺)
353	352	rprecred 12945	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ)
354	334	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈ ℝ⁺)
355		1red 11113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ)
356	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1)
357	347	flcld 13702	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
358	357	peano2zd 12580	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
359	358	zred 12577	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
360	202, 141	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜒 → 𝑀 ∈ ℤ)
361	358, 360	ifcld 4519	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
362	146, 361	eqeltrid 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑁 ∈ ℤ)
363	362	zred 12577	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 𝑁 ∈ ℝ)
364		flltp1 13704	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
365	347, 364	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
366	202, 62	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → 𝑀 ∈ ℝ)
367		max2 13086	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
368	366, 359, 367	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
369	368, 146	breqtrrdi 5131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁)
370	347, 359, 363, 365, 369	ltletrd 11273	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁)
371	347, 319, 370	ltled 11261	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
372	371	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
373	352, 354, 355, 356, 372	lediv2ad 12956	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2))))
374	331, 353, 332, 333, 373	lemul2ad 12062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
375	332	recnd 11140	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ)
376	348	recnd 11140	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ)
377	351	gt0ne0d 11681	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0)
378	375, 376, 377	divrecd 11900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
379	329	recnd 11140	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ)
380	349	gt0ne0d 11681	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0)
381	346	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0)
382	375, 379, 380, 381	ddcand 11917	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2))
383	378, 382	eqtr3d 2768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2))
384	374, 383	breqtrd 5115	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2))
385	318, 328, 329, 341, 384	letrd 11270	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
386	317, 385	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
387	312, 386	pm2.61dan 812	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
388	249, 280, 237, 302, 387	letrd 11270	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑥 / 2))
389	244, 249, 237, 278, 388	letrd 11270	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑥 / 2))
390	240, 389	eqbrtrd 5111	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))) ≤ (𝑥 / 2))
391	238, 390	eqbrtrd 5111	. . . . . . . . . . . . 13 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ≤ (𝑥 / 2))
392		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
393	200, 392	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
394	231, 233, 237, 237, 391, 393	leltaddd 11739	. . . . . . . . . . . 12 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2)))
395	342	2halvesd 12367	. . . . . . . . . . . 12 ⊢ (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
396	394, 395	breqtrd 5115	. . . . . . . . . . 11 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥)
397	229, 234, 235, 236, 396	lelttrd 11271	. . . . . . . . . 10 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥)
398	223, 397	eqbrtrd 5111	. . . . . . . . 9 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
399	199, 398	sylbir 235	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
400	399	adantrl 716	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
401	400	ex 412	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
402	401	ralrimiva 3124	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
403		brimralrspcev 5150	. . . . 5 ⊢ (((1 / 𝑗) ∈ ℝ⁺ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
404	198, 402, 403	syl2anc 584	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
405		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → 𝑏 ≤ 𝑁)
406	405	iftrued 4480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑁)
407		uzid 12747	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ_≥‘𝑁))
408	182, 407	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ (ℤ_≥‘𝑁))
409	408	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → 𝑁 ∈ (ℤ_≥‘𝑁))
410	406, 409	eqeltrd 2831	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
411	410	adantlr 715	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
412		iffalse 4481	. . . . . . . . . 10 ⊢ (¬ 𝑏 ≤ 𝑁 → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏)
413	412	adantl 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏)
414	182	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ∈ ℤ)
415		simplr 768	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ ℤ)
416	414	zred 12577	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ∈ ℝ)
417	415	zred 12577	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ ℝ)
418		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → ¬ 𝑏 ≤ 𝑁)
419	416, 417	ltnled 11260	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑁))
420	418, 419	mpbird 257	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 < 𝑏)
421	416, 417, 420	ltled 11261	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ≤ 𝑏)
422		eluz2 12738	. . . . . . . . . 10 ⊢ (𝑏 ∈ (ℤ_≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ≤ 𝑏))
423	414, 415, 421, 422	syl3anbrc 1344	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ (ℤ_≥‘𝑁))
424	413, 423	eqeltrd 2831	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
425	411, 424	pm2.61dan 812	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
426	425	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
427		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
428		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
429	182	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
430	429, 428	ifcld 4519	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ)
431	428	zred 12577	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
432	429	zred 12577	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℝ)
433		max1 13084	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))
434	431, 432, 433	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))
435		eluz2 12738	. . . . . . . . . 10 ⊢ (if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
436	428, 430, 434, 435	syl3anbrc 1344	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏))
437	436	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏))
438		fveq2 6822	. . . . . . . . . . 11 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑐) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
439	438	eleq1d 2816	. . . . . . . . . 10 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ))
440	438	fvoveq1d 7368	. . . . . . . . . . 11 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
441	440	breq1d 5099	. . . . . . . . . 10 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
442	439, 441	anbi12d 632	. . . . . . . . 9 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))))
443	442	rspccva 3571	. . . . . . . 8 ⊢ ((∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏)) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
444	427, 437, 443	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
445	444	simprd 495	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))
446		fveq2 6822	. . . . . . . . 9 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑗) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
447	446	fvoveq1d 7368	. . . . . . . 8 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
448	447	breq1d 5099	. . . . . . 7 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
449	448	rspcev 3572	. . . . . 6 ⊢ ((if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁) ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
450	426, 445, 449	syl2anc 584	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
451		ax-resscn 11063	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
452	451	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℝ ⊆ ℂ)
453	26, 452	fssd 6668	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ)
454		dvcn 25850	. . . . . . . . . . . . . 14 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
455	452, 453, 153, 109, 454	syl31anc 1375	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
456		cncfcdm 24818	. . . . . . . . . . . . 13 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
457	452, 455, 456	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
458	26, 457	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
459		ioodvbdlimc1lem2.r	. . . . . . . . . . . 12 ⊢ 𝑅 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐴 + (1 / 𝑗)))
460	105, 459	fmptd 7047	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅:(ℤ_≥‘𝑀)⟶(𝐴(,)𝐵))
461		eqid 2731	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))
462		climrel 15399	. . . . . . . . . . . . 13 ⊢ Rel ⇝
463	462	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Rel ⇝ )
464		fvex 6835	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑀) ∈ V
465	464	mptex 7157	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) ∈ V
466	465	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) ∈ V)
467		eqidd 2732	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴))
468		eqidd 2732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑚) → 𝐴 = 𝐴)
469		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ (ℤ_≥‘𝑀))
470	7	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
471	467, 468, 469, 470	fvmptd 6936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑚) = 𝐴)
472	23, 141, 466, 98, 471	climconst 15450	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) ⇝ 𝐴)
473	464	mptex 7157	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐴 + (1 / 𝑗))) ∈ V
474	459, 473	eqeltri 2827	. . . . . . . . . . . . . . 15 ⊢ 𝑅 ∈ V
475	474	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ V)
476		1cnd 11107	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
477		elnnnn0b 12425	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ₀ ∧ 0 < 𝑀))
478	21, 67, 477	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
479		divcnvg 45737	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0)
480	476, 478, 479	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0)
481		eqidd 2732	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴))
482		eqidd 2732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → 𝐴 = 𝐴)
483		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ (ℤ_≥‘𝑀))
484	7	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
485	481, 482, 483, 484	fvmptd 6936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) = 𝐴)
486	98	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℂ)
487	485, 486	eqeltrd 2831	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) ∈ ℂ)
488		eqidd 2732	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)))
489		oveq2 7354	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖))
490	489	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖))
491	3, 483	sselid 3927	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℝ)
492		0red 11115	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 ∈ ℝ)
493	62	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
494	67	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑀)
495		eluzle 12745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑖)
496	495	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑖)
497	492, 493, 491, 494, 496	ltletrd 11273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑖)
498	497	gt0ne0d 11681	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ≠ 0)
499	491, 498	rereccld 11948	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑖) ∈ ℝ)
500	488, 490, 483, 499	fvmptd 6936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖))
501	491	recnd 11140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℂ)
502	501, 498	reccld 11890	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑖) ∈ ℂ)
503	500, 502	eqeltrd 2831	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ)
504	489	oveq2d 7362	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑖 → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
505	484, 499	readdcld 11141	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑖)) ∈ ℝ)
506	459, 504, 483, 505	fvmptd3 6952	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑖) = (𝐴 + (1 / 𝑖)))
507	485, 500	oveq12d 7364	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐴 + (1 / 𝑖)))
508	506, 507	eqtr4d 2769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑖) = (((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)))
509	23, 141, 472, 475, 480, 487, 503, 508	climadd 15539	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ⇝ (𝐴 + 0))
510	98	addridd 11313	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 + 0) = 𝐴)
511	509, 510	breqtrd 5115	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ⇝ 𝐴)
512		releldm 5883	. . . . . . . . . . . 12 ⊢ ((Rel ⇝ ∧ 𝑅 ⇝ 𝐴) → 𝑅 ∈ dom ⇝ )
513	463, 511, 512	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ dom ⇝ )
514		fveq2 6822	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → (ℤ_≥‘𝑙) = (ℤ_≥‘𝑘))
515		fveq2 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = 𝑘 → (𝑅‘𝑙) = (𝑅‘𝑘))
516	515	oveq2d 7362	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 𝑘 → ((𝑅‘ℎ) − (𝑅‘𝑙)) = ((𝑅‘ℎ) − (𝑅‘𝑘)))
517	516	fveq2d 6826	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑘 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) = (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))))
518	517	breq1d 5099	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
519	514, 518	raleqbidv 3312	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → (∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
520	519	cbvrabv 3405	. . . . . . . . . . . . 13 ⊢ {𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
521		fveq2 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = 𝑖 → (𝑅‘ℎ) = (𝑅‘𝑖))
522	521	fvoveq1d 7368	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑖 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) = (abs‘((𝑅‘𝑖) − (𝑅‘𝑘))))
523	522	breq1d 5099	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑖 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
524	523	cbvralvw 3210	. . . . . . . . . . . . . . 15 ⊢ (∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
525	524	rgenw 3051	. . . . . . . . . . . . . 14 ⊢ ∀𝑘 ∈ (ℤ_≥‘𝑀)(∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
526		rabbi 3425	. . . . . . . . . . . . . 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))})
527	525, 526	mpbi 230	. . . . . . . . . . . . 13 ⊢ {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
528	520, 527	eqtri 2754	. . . . . . . . . . . 12 ⊢ {𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
529	528	infeq1i 9363	. . . . . . . . . . 11 ⊢ inf({𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < ) = inf({𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
530	7, 6, 9, 458, 109, 110, 22, 460, 461, 513, 529	ioodvbdlimc1lem1 46039	. . . . . . . . . 10 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) ⇝ (lim sup‘(𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))))
531	459	fvmpt2 6940	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (ℤ_≥‘𝑀) ∧ (𝐴 + (1 / 𝑗)) ∈ ℝ) → (𝑅‘𝑗) = (𝐴 + (1 / 𝑗)))
532	113, 58, 531	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑗) = (𝐴 + (1 / 𝑗)))
533	532	eqcomd 2737	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐴 + (1 / 𝑗)) = (𝑅‘𝑗))
534	533	fveq2d 6826	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) = (𝐹‘(𝑅‘𝑗)))
535	534	mpteq2dva 5182	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))
536	107, 535	eqtrid 2778	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))
537	536	fveq2d 6826	. . . . . . . . . 10 ⊢ (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))))
538	530, 536, 537	3brtr4d 5121	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⇝ (lim sup‘𝑆))
539	464	mptex 7157	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) ∈ V
540	107, 539	eqeltri 2827	. . . . . . . . . . 11 ⊢ 𝑆 ∈ V
541	540	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ V)
542		eqidd 2732	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ℤ) → (𝑆‘𝑐) = (𝑆‘𝑐))
543	541, 542	clim 15401	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))))
544	538, 543	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)))
545	544	simprd 495	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))
546	545	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))
547		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
548	547	rphalfcld 12946	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
549		breq2 5093	. . . . . . . . 9 ⊢ (𝑎 = (𝑥 / 2) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
550	549	anbi2d 630	. . . . . . . 8 ⊢ (𝑎 = (𝑥 / 2) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
551	550	rexralbidv 3198	. . . . . . 7 ⊢ (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
552	551	rspccva 3571	. . . . . 6 ⊢ ((∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ⁺) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
553	546, 548, 552	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
554	450, 553	r19.29a 3140	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
555	404, 554	r19.29a 3140	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
556	555	ralrimiva 3124	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
557		ioosscn 13308	. . . 4 ⊢ (𝐴(,)𝐵) ⊆ ℂ
558	557	a1i 11	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
559	453, 558, 98	ellimc3 25807	. 2 ⊢ (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐴) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))))
560	136, 556, 559	mpbir2and 713	1 ⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 {crab 3395 Vcvv 3436 ⊆ wss 3897 ∅c0 4280 ifcif 4472 class class class wbr 5089 ↦ cmpt 5170 dom cdm 5614 ran crn 5615 Rel wrel 5619 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 supcsup 9324 infcinf 9325 ℂcc 11004 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 +∞cpnf 11143 ℝ^*cxr 11145 < clt 11146 ≤ cle 11147 − cmin 11344 / cdiv 11774 ℕcn 12125 2c2 12180 ℕ₀cn0 12381 ℤcz 12468 ℤ_≥cuz 12732 ℝ⁺crp 12890 (,)cioo 13245 ⌊cfl 13694 abscabs 15141 lim supclsp 15377 ⇝ cli 15391 –cn→ccncf 24796 lim_ℂ climc 25790 D cdv 25791

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084 ax-addf 11085

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-iin 4942 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-om 7797 df-1st 7921 df-2nd 7922 df-supp 8091 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-er 8622 df-map 8752 df-pm 8753 df-ixp 8822 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-fsupp 9246 df-fi 9295 df-sup 9326 df-inf 9327 df-oi 9396 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-4 12190 df-5 12191 df-6 12192 df-7 12193 df-8 12194 df-9 12195 df-n0 12382 df-z 12469 df-dec 12589 df-uz 12733 df-q 12847 df-rp 12891 df-xneg 13011 df-xadd 13012 df-xmul 13013 df-ioo 13249 df-ico 13251 df-icc 13252 df-fz 13408 df-fzo 13555 df-fl 13696 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-limsup 15378 df-clim 15395 df-rlim 15396 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-rest 17326 df-topn 17327 df-0g 17345 df-gsum 17346 df-topgen 17347 df-pt 17348 df-prds 17351 df-xrs 17406 df-qtop 17411 df-imas 17412 df-xps 17414 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18548 df-sgrp 18627 df-mnd 18643 df-submnd 18692 df-mulg 18981 df-cntz 19229 df-cmn 19694 df-psmet 21283 df-xmet 21284 df-met 21285 df-bl 21286 df-mopn 21287 df-fbas 21288 df-fg 21289 df-cnfld 21292 df-top 22809 df-topon 22826 df-topsp 22848 df-bases 22861 df-cld 22934 df-ntr 22935 df-cls 22936 df-nei 23013 df-lp 23051 df-perf 23052 df-cn 23142 df-cnp 23143 df-haus 23230 df-cmp 23302 df-tx 23477 df-hmeo 23670 df-fil 23761 df-fm 23853 df-flim 23854 df-flf 23855 df-xms 24235 df-ms 24236 df-tms 24237 df-cncf 24798 df-limc 25794 df-dv 25795

This theorem is referenced by: ioodvbdlimc1 46041

W3C validator