ioodvbdlimc2lem - Mathbox for Glauco Siliprandi

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

Theorem ioodvbdlimc2lem 45919

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

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

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

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

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

Step	Hyp	Ref	Expression
1		uzssz 12756	. . . . . 6 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
2		zssre 12478	. . . . . 6 ⊢ ℤ ⊆ ℝ
3	1, 2	sstri 3945	. . . . 5 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (ℤ_≥‘𝑀) ⊆ ℝ)
5		ioodvbdlimc2lem.m	. . . . . . 7 ⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1)
6		ioodvbdlimc2lem.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
7		ioodvbdlimc2lem.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
8	6, 7	resubcld 11548	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
9		ioodvbdlimc2lem.altb	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
10	7, 6	posdifd 11707	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
11	9, 10	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
12	11	gt0ne0d 11684	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0)
13	8, 12	rereccld 11951	. . . . . . . . 9 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ)
14		0red 11118	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
15	8, 11	recgt0d 12059	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (1 / (𝐵 − 𝐴)))
16	14, 13, 15	ltled 11264	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (1 / (𝐵 − 𝐴)))
17		flge0nn0 13724	. . . . . . . . 9 ⊢ (((1 / (𝐵 − 𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐵 − 𝐴))) → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀)
18	13, 16, 17	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀)
19		peano2nn0 12424	. . . . . . . 8 ⊢ ((⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ₀ → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℕ₀)
20	18, 19	syl 17	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℕ₀)
21	5, 20	eqeltrid 2832	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
22	21	nn0zd 12497	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
23		eqid 2729	. . . . . 6 ⊢ (ℤ_≥‘𝑀) = (ℤ_≥‘𝑀)
24	23	uzsup 13767	. . . . 5 ⊢ (𝑀 ∈ ℤ → sup((ℤ_≥‘𝑀), ℝ^*, < ) = +∞)
25	22, 24	syl 17	. . . 4 ⊢ (𝜑 → sup((ℤ_≥‘𝑀), ℝ^*, < ) = +∞)
26		ioodvbdlimc2lem.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
27	26	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
28	7	rexrd 11165	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
29	28	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ^*)
30	6	rexrd 11165	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
31	30	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ^*)
32	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ)
33		eluzelre 12746	. . . . . . . . . 10 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑗 ∈ ℝ)
34	33	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℝ)
35		0red 11118	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 ∈ ℝ)
36		0red 11118	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 0 ∈ ℝ)
37		1red 11116	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 1 ∈ ℝ)
38	36, 37	readdcld 11144	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → (0 + 1) ∈ ℝ)
39	38	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ∈ ℝ)
40	36	ltp1d 12055	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 0 < (0 + 1))
41	40	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 < (0 + 1))
42		eluzel2 12740	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
43	42	zred 12580	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℝ)
44	43	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
45	13	flcld 13702	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℤ)
46	45	zred 12580	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℝ)
47		1red 11116	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℝ)
48	18	nn0ge0d 12448	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ≤ (⌊‘(1 / (𝐵 − 𝐴))))
49	14, 46, 47, 48	leadd1dd 11734	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + 1) ≤ ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
50	49, 5	breqtrrdi 5134	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 + 1) ≤ 𝑀)
51	50	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ≤ 𝑀)
52		eluzle 12748	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑗)
53	52	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑗)
54	39, 44, 34, 51, 53	letrd 11273	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (0 + 1) ≤ 𝑗)
55	35, 39, 34, 41, 54	ltletrd 11276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑗)
56	55	gt0ne0d 11684	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ≠ 0)
57	34, 56	rereccld 11951	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ∈ ℝ)
58	32, 57	resubcld 11548	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑗)) ∈ ℝ)
59	7	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 ∈ ℝ)
60	21	nn0red 12446	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
61	14, 47	readdcld 11144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + 1) ∈ ℝ)
62	46, 47	readdcld 11144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℝ)
63	14	ltp1d 12055	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (0 + 1))
64	14, 61, 62, 63, 49	ltletrd 11276	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
65	64, 5	breqtrrdi 5134	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝑀)
66	65	gt0ne0d 11684	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≠ 0)
67	60, 66	rereccld 11951	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 𝑀) ∈ ℝ)
68	67	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑀) ∈ ℝ)
69	32, 68	resubcld 11548	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑀)) ∈ ℝ)
70	5	eqcomi 2738	. . . . . . . . . . . . 13 ⊢ ((⌊‘(1 / (𝐵 − 𝐴))) + 1) = 𝑀
71	70	oveq2i 7360	. . . . . . . . . . . 12 ⊢ (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) = (1 / 𝑀)
72	71, 67	eqeltrid 2832	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) ∈ ℝ)
73	13, 15	elrpd 12934	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ⁺)
74	62, 64	elrpd 12934	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℝ⁺)
75		1rp 12897	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ⁺
76	75	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ⁺)
77		fllelt 13701	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) ∈ ℝ → ((⌊‘(1 / (𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
78	13, 77	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))
79	78	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))
80	73, 74, 76, 79	ltdiv2dd 45280	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) < (1 / (1 / (𝐵 − 𝐴))))
81	8	recnd 11143	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ)
82	81, 12	recrecd 11897	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / (1 / (𝐵 − 𝐴))) = (𝐵 − 𝐴))
83	80, 82	breqtrd 5118	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) < (𝐵 − 𝐴))
84	72, 8, 6, 83	ltsub2dd 11733	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) < (𝐵 − (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))))
85	6	recnd 11143	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
86	7	recnd 11143	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
87	85, 86	nncand 11480	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) = 𝐴)
88	71	oveq2i 7360	. . . . . . . . . . 11 ⊢ (𝐵 − (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) = (𝐵 − (1 / 𝑀))
89	88	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) = (𝐵 − (1 / 𝑀)))
90	84, 87, 89	3brtr3d 5123	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 < (𝐵 − (1 / 𝑀)))
91	90	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 < (𝐵 − (1 / 𝑀)))
92	60, 65	elrpd 12934	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
93	92	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ⁺)
94	34, 55	elrpd 12934	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℝ⁺)
95		1red 11116	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 1 ∈ ℝ)
96		0le1 11643	. . . . . . . . . . 11 ⊢ 0 ≤ 1
97	96	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 0 ≤ 1)
98	93, 94, 95, 97, 53	lediv2ad 12959	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀))
99	57, 68, 32, 98	lesub2dd 11737	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑀)) ≤ (𝐵 − (1 / 𝑗)))
100	59, 69, 58, 91, 99	ltletrd 11276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝐴 < (𝐵 − (1 / 𝑗)))
101	94	rpreccld 12947	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑗) ∈ ℝ⁺)
102	32, 101	ltsubrpd 12969	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑗)) < 𝐵)
103	29, 31, 58, 100, 102	eliood 45483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵))
104	27, 103	ffvelcdmd 7019	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘(𝐵 − (1 / 𝑗))) ∈ ℝ)
105		ioodvbdlimc2lem.s	. . . . 5 ⊢ 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗))))
106	104, 105	fmptd 7048	. . . 4 ⊢ (𝜑 → 𝑆:(ℤ_≥‘𝑀)⟶ℝ)
107		ioodvbdlimc2lem.dmdv	. . . . . 6 ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
108		ioodvbdlimc2lem.dvbd	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
109	7, 6, 9, 26, 107, 108	dvbdfbdioo 45915	. . . . 5 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏)
110	60	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ)
111		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ (ℤ_≥‘𝑀))
112	105	fvmpt2 6941	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (ℤ_≥‘𝑀) ∧ (𝐹‘(𝐵 − (1 / 𝑗))) ∈ ℝ) → (𝑆‘𝑗) = (𝐹‘(𝐵 − (1 / 𝑗))))
113	111, 104, 112	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑆‘𝑗) = (𝐹‘(𝐵 − (1 / 𝑗))))
114	113	fveq2d 6826	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))))
115	114	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))))
116		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏)
117	103	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵))
118		2fveq3 6827	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐵 − (1 / 𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))))
119	118	breq1d 5102	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐵 − (1 / 𝑗)) → ((abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏))
120	119	rspccva 3576	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 ∧ (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏)
121	116, 117, 120	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏)
122	115, 121	eqbrtrd 5114	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (abs‘(𝑆‘𝑗)) ≤ 𝑏)
123	122	a1d 25	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
124	123	ralrimiva 3121	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
125		breq1 5095	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑀 → (𝑘 ≤ 𝑗 ↔ 𝑀 ≤ 𝑗))
126	125	imbi1d 341	. . . . . . . . . 10 ⊢ (𝑘 = 𝑀 → ((𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
127	126	ralbidv 3152	. . . . . . . . 9 ⊢ (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
128	127	rspcev 3577	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
129	110, 124, 128	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
130	129	ex 412	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
131	130	reximdv 3144	. . . . 5 ⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)))
132	109, 131	mpd 15	. . . 4 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ_≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))
133	4, 25, 106, 132	limsupre 45626	. . 3 ⊢ (𝜑 → (lim sup‘𝑆) ∈ ℝ)
134	133	recnd 11143	. 2 ⊢ (𝜑 → (lim sup‘𝑆) ∈ ℂ)
135		eluzelre 12746	. . . . . . . . 9 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑗 ∈ ℝ)
136	135	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑗 ∈ ℝ)
137		0red 11118	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 ∈ ℝ)
138	45	peano2zd 12583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘(1 / (𝐵 − 𝐴))) + 1) ∈ ℤ)
139	5, 138	eqeltrid 2832	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
140	139	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ∈ ℤ)
141	140	zred 12580	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ∈ ℝ)
142	141	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ∈ ℝ)
143	65	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < 𝑀)
144		ioodvbdlimc2lem.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
145		ioodvbdlimc2lem.y	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
146		ioomidp 45499	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
147	7, 6, 9, 146	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
148		ne0i 4292	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
149	147, 148	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴(,)𝐵) ≠ ∅)
150		ioossre 13310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴(,)𝐵) ⊆ ℝ
151	150	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
152		dvfre 25853	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
153	26, 151, 152	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
154	107	feq2d 6636	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
155	153, 154	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
156	155	ffvelcdmda 7018	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
157	156	recnd 11143	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
158	157	abscld 15346	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
159		eqid 2729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥)))
160		eqid 2729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
161	149, 158, 108, 159, 160	suprnmpt 45156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )))
162	161	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ)
163	145, 162	eqeltrid 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑌 ∈ ℝ)
164	163	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑌 ∈ ℝ)
165		rpre 12902	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
166	165	rehalfcld 12371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ)
167	166	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
168	165	recnd 11143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
169	168	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
170		2cnd 12206	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℂ)
171		rpne0 12910	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
172	171	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
173		2ne0 12232	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
174	173	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ≠ 0)
175	169, 170, 172, 174	divne0d 11916	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ≠ 0)
176	164, 167, 175	redivcld 11952	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
177	176	flcld 13702	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
178	177	peano2zd 12583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
179	178, 140	ifcld 4523	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
180	144, 179	eqeltrid 2832	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ ℤ)
181	180	zred 12580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ ℝ)
182	181	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑁 ∈ ℝ)
183	178	zred 12580	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
184		max1 13087	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
185	141, 183, 184	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
186	185, 144	breqtrrdi 5134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑀 ≤ 𝑁)
187	186	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ≤ 𝑁)
188		eluzle 12748	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑁 ≤ 𝑗)
189	188	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑁 ≤ 𝑗)
190	142, 182, 136, 187, 189	letrd 11273	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑀 ≤ 𝑗)
191	137, 142, 136, 143, 190	ltletrd 11276	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < 𝑗)
192	191	gt0ne0d 11684	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 𝑗 ≠ 0)
193	136, 192	rereccld 11951	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (1 / 𝑗) ∈ ℝ)
194	136, 191	recgt0d 12059	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → 0 < (1 / 𝑗))
195	193, 194	elrpd 12934	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (1 / 𝑗) ∈ ℝ⁺)
196	195	adantr 480	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈ ℝ⁺)
197		ioodvbdlimc2lem.ch	. . . . . . . . 9 ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)))
198	197	biimpi 216	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)))
199		simp-5l 784	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → 𝜑)
200	198, 199	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝜑)
201	200, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
202	198	simplrd 769	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑧 ∈ (𝐴(,)𝐵))
203	201, 202	ffvelcdmd 7019	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝐹‘𝑧) ∈ ℝ)
204	203	recnd 11143	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝐹‘𝑧) ∈ ℂ)
205	200, 106	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑆:(ℤ_≥‘𝑀)⟶ℝ)
206		simp-5r 785	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → 𝑥 ∈ ℝ⁺)
207	198, 206	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑥 ∈ ℝ⁺)
208		eluz2 12741	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
209	140, 180, 186, 208	syl3anbrc 1344	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ (ℤ_≥‘𝑀))
210	200, 207, 209	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑁 ∈ (ℤ_≥‘𝑀))
211		uzss 12758	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
212	210, 211	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
213		simp-4r 783	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ_≥‘𝑁))
214	198, 213	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑗 ∈ (ℤ_≥‘𝑁))
215	212, 214	sseldd 3936	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑗 ∈ (ℤ_≥‘𝑀))
216	205, 215	ffvelcdmd 7019	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
217	216	recnd 11143	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ)
218	200, 134	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → (lim sup‘𝑆) ∈ ℂ)
219	204, 217, 218	npncand 11499	. . . . . . . . . . . 12 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) = ((𝐹‘𝑧) − (lim sup‘𝑆)))
220	219	eqcomd 2735	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹‘𝑧) − (lim sup‘𝑆)) = (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))))
221	220	fveq2d 6826	. . . . . . . . . 10 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))))
222	203, 216	resubcld 11548	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℝ)
223	200, 133	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (lim sup‘𝑆) ∈ ℝ)
224	216, 223	resubcld 11548	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℝ)
225	222, 224	readdcld 11144	. . . . . . . . . . . . 13 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ)
226	225	recnd 11143	. . . . . . . . . . . 12 ⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℂ)
227	226	abscld 15346	. . . . . . . . . . 11 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
228	222	recnd 11143	. . . . . . . . . . . . 13 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℂ)
229	228	abscld 15346	. . . . . . . . . . . 12 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ∈ ℝ)
230	224	recnd 11143	. . . . . . . . . . . . 13 ⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℂ)
231	230	abscld 15346	. . . . . . . . . . . 12 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ)
232	229, 231	readdcld 11144	. . . . . . . . . . 11 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
233	207	rpred 12937	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑥 ∈ ℝ)
234	228, 230	abstrid 15366	. . . . . . . . . . 11 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))))
235	233	rehalfcld 12371	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑥 / 2) ∈ ℝ)
236	200, 215, 113	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑆‘𝑗) = (𝐹‘(𝐵 − (1 / 𝑗))))
237	236	oveq2d 7365	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) = ((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗)))))
238	237	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) = (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))))
239	238, 229	eqeltrrd 2829	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ∈ ℝ)
240	200, 163	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑌 ∈ ℝ)
241	150, 202	sselid 3933	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑧 ∈ ℝ)
242	200, 215, 58	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝐵 − (1 / 𝑗)) ∈ ℝ)
243	241, 242	resubcld 11548	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) ∈ ℝ)
244	240, 243	remulcld 11145	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ∈ ℝ)
245	200, 7	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝐴 ∈ ℝ)
246	200, 6	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝐵 ∈ ℝ)
247	200, 107	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
248	161	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
249	145	breq2i 5100	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
250	249	ralbii 3075	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
251	248, 250	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
252	200, 251	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
253		2fveq3 6827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥)))
254	253	breq1d 5102	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌))
255	254	cbvralvw 3207	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
256	252, 255	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌)
257	200, 215, 103	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵))
258	242	rexrd 11165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝐵 − (1 / 𝑗)) ∈ ℝ^*)
259	200, 30	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝐵 ∈ ℝ^*)
260	3, 215	sselid 3933	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → 𝑗 ∈ ℝ)
261	200, 215, 56	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → 𝑗 ≠ 0)
262	260, 261	rereccld 11951	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (1 / 𝑗) ∈ ℝ)
263	246, 241	resubcld 11548	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝐵 − 𝑧) ∈ ℝ)
264	241, 246	resubcld 11548	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (𝑧 − 𝐵) ∈ ℝ)
265	264	recnd 11143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑧 − 𝐵) ∈ ℂ)
266	265	abscld 15346	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (abs‘(𝑧 − 𝐵)) ∈ ℝ)
267	263	leabsd 15322	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝐵 − 𝑧) ≤ (abs‘(𝐵 − 𝑧)))
268	200, 85	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝐵 ∈ ℂ)
269	241	recnd 11143	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑧 ∈ ℂ)
270	268, 269	abssubd 15363	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (abs‘(𝐵 − 𝑧)) = (abs‘(𝑧 − 𝐵)))
271	267, 270	breqtrd 5118	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝐵 − 𝑧) ≤ (abs‘(𝑧 − 𝐵)))
272	198	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (abs‘(𝑧 − 𝐵)) < (1 / 𝑗))
273	263, 266, 262, 271, 272	lelttrd 11274	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝐵 − 𝑧) < (1 / 𝑗))
274	246, 241, 262, 273	ltsub23d 11725	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝐵 − (1 / 𝑗)) < 𝑧)
275	200, 28	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐴 ∈ ℝ^*)
276		iooltub 45495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 < 𝐵)
277	275, 259, 202, 276	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑧 < 𝐵)
278	258, 259, 241, 274, 277	eliood 45483	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑧 ∈ ((𝐵 − (1 / 𝑗))(,)𝐵))
279	245, 246, 201, 247, 240, 256, 257, 278	dvbdfbdioolem1 45913	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ∧ (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝐵 − 𝐴))))
280	279	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))))
281	200, 215, 57	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (1 / 𝑗) ∈ ℝ)
282	240, 281	remulcld 11145	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ)
283	155, 147	ffvelcdmd 7019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ)
284	283	recnd 11143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ)
285	284	abscld 15346	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ)
286	284	absge0d 15354	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≤ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
287		2fveq3 6827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
288	145	eqcomi 2738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌
289	288	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌)
290	287, 289	breq12d 5105	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌))
291	290	rspcva 3575	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
292	147, 248, 291	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
293	14, 285, 163, 286, 292	letrd 11273	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ≤ 𝑌)
294	200, 293	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 0 ≤ 𝑌)
295	281	recnd 11143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (1 / 𝑗) ∈ ℂ)
296		sub31 45276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (1 / 𝑗) ∈ ℂ) → (𝑧 − (𝐵 − (1 / 𝑗))) = ((1 / 𝑗) − (𝐵 − 𝑧)))
297	269, 268, 295, 296	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) = ((1 / 𝑗) − (𝐵 − 𝑧)))
298	241, 246	posdifd 11707	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (𝑧 < 𝐵 ↔ 0 < (𝐵 − 𝑧)))
299	277, 298	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → 0 < (𝐵 − 𝑧))
300	263, 299	elrpd 12934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝐵 − 𝑧) ∈ ℝ⁺)
301	281, 300	ltsubrpd 12969	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ((1 / 𝑗) − (𝐵 − 𝑧)) < (1 / 𝑗))
302	297, 301	eqbrtrd 5114	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) < (1 / 𝑗))
303	243, 281, 302	ltled 11264	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) ≤ (1 / 𝑗))
304	243, 281, 240, 294, 303	lemul2ad 12065	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ≤ (𝑌 · (1 / 𝑗)))
305	282	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
306	235	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑥 / 2) ∈ ℝ)
307		oveq1 7356	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗)))
308	295	mul02d 11314	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (0 · (1 / 𝑗)) = 0)
309	307, 308	sylan9eqr 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0)
310	207	rphalfcld 12949	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (𝑥 / 2) ∈ ℝ⁺)
311	310	rpgt0d 12940	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → 0 < (𝑥 / 2))
312	311	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑌 = 0) → 0 < (𝑥 / 2))
313	309, 312	eqbrtrd 5114	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2))
314	305, 306, 313	ltled 11264	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
315	240	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ)
316	294	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌)
317		neqne 2933	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑌 = 0 → 𝑌 ≠ 0)
318	317	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0)
319	315, 316, 318	ne0gt0d 11253	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌)
320	282	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
321	3, 210	sselid 3933	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑁 ∈ ℝ)
322		0red 11118	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 0 ∈ ℝ)
323	200, 207, 141	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 𝑀 ∈ ℝ)
324	200, 65	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 0 < 𝑀)
325	200, 207, 186	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → 𝑀 ≤ 𝑁)
326	322, 323, 321, 324, 325	ltletrd 11276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → 0 < 𝑁)
327	326	gt0ne0d 11684	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑁 ≠ 0)
328	321, 327	rereccld 11951	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (1 / 𝑁) ∈ ℝ)
329	240, 328	remulcld 11145	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ)
330	329	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ)
331	235	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ)
332	281	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ)
333	328	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ)
334	240	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ)
335	294	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌)
336	321, 326	elrpd 12934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑁 ∈ ℝ⁺)
337	200, 215, 94	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑗 ∈ ℝ⁺)
338		1red 11116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 1 ∈ ℝ)
339	96	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 0 ≤ 1)
340	214, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → 𝑁 ≤ 𝑗)
341	336, 337, 338, 339, 340	lediv2ad 12959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁))
342	341	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁))
343	332, 333, 334, 335, 342	lemul2ad 12065	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁)))
344	233	recnd 11143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 𝑥 ∈ ℂ)
345		2cnd 12206	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 2 ∈ ℂ)
346	207	rpne0d 12942	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 𝑥 ≠ 0)
347	173	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 2 ≠ 0)
348	344, 345, 346, 347	divne0d 11916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → (𝑥 / 2) ≠ 0)
349	240, 235, 348	redivcld 11952	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ)
350	349	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
351		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌)
352	311	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2))
353	334, 331, 351, 352	divgt0d 12060	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2)))
354	350, 353	elrpd 12934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ⁺)
355	354	rprecred 12948	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ)
356	336	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈ ℝ⁺)
357		1red 11116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ)
358	96	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1)
359	349	flcld 13702	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
360	359	peano2zd 12583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
361	360	zred 12580	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
362	200, 139	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → 𝑀 ∈ ℤ)
363	360, 362	ifcld 4523	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
364	144, 363	eqeltrid 2832	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → 𝑁 ∈ ℤ)
365	364	zred 12580	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑁 ∈ ℝ)
366		flltp1 13704	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
367	349, 366	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
368	200, 60	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → 𝑀 ∈ ℝ)
369		max2 13089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
370	368, 361, 369	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
371	370, 144	breqtrrdi 5134	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁)
372	349, 361, 365, 367, 371	ltletrd 11276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁)
373	349, 321, 372	ltled 11264	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
374	373	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
375	354, 356, 357, 358, 374	lediv2ad 12959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2))))
376	333, 355, 334, 335, 375	lemul2ad 12065	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
377	334	recnd 11143	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ)
378	350	recnd 11143	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ)
379	353	gt0ne0d 11684	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0)
380	377, 378, 379	divrecd 11903	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
381	331	recnd 11143	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ)
382	351	gt0ne0d 11684	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0)
383	348	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0)
384	377, 381, 382, 383	ddcand 11920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2))
385	380, 384	eqtr3d 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2))
386	376, 385	breqtrd 5118	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2))
387	320, 330, 331, 343, 386	letrd 11273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
388	319, 387	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
389	314, 388	pm2.61dan 812	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
390	244, 282, 235, 304, 389	letrd 11273	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ≤ (𝑥 / 2))
391	239, 244, 235, 280, 390	letrd 11273	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑥 / 2))
392	238, 391	eqbrtrd 5114	. . . . . . . . . . . . 13 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ≤ (𝑥 / 2))
393		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
394	198, 393	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
395	229, 231, 235, 235, 392, 394	leltaddd 11742	. . . . . . . . . . . 12 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2)))
396	344	2halvesd 12370	. . . . . . . . . . . 12 ⊢ (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
397	395, 396	breqtrd 5118	. . . . . . . . . . 11 ⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥)
398	227, 232, 233, 234, 397	lelttrd 11274	. . . . . . . . . 10 ⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥)
399	221, 398	eqbrtrd 5114	. . . . . . . . 9 ⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
400	197, 399	sylbir 235	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
401	400	adantrl 716	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗))) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)
402	401	ex 412	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
403	402	ralrimiva 3121	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
404		brimralrspcev 5153	. . . . 5 ⊢ (((1 / 𝑗) ∈ ℝ⁺ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
405	196, 403, 404	syl2anc 584	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
406		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → 𝑏 ≤ 𝑁)
407	406	iftrued 4484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑁)
408		uzid 12750	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ_≥‘𝑁))
409	180, 408	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑁 ∈ (ℤ_≥‘𝑁))
410	409	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → 𝑁 ∈ (ℤ_≥‘𝑁))
411	407, 410	eqeltrd 2828	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
412	411	adantlr 715	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
413		iffalse 4485	. . . . . . . . . 10 ⊢ (¬ 𝑏 ≤ 𝑁 → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏)
414	413	adantl 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏)
415	180	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ∈ ℤ)
416		simplr 768	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ ℤ)
417	415	zred 12580	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ∈ ℝ)
418	416	zred 12580	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ ℝ)
419		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → ¬ 𝑏 ≤ 𝑁)
420	417, 418	ltnled 11263	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑁))
421	419, 420	mpbird 257	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 < 𝑏)
422	417, 418, 421	ltled 11264	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑁 ≤ 𝑏)
423		eluz2 12741	. . . . . . . . . 10 ⊢ (𝑏 ∈ (ℤ_≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ≤ 𝑏))
424	415, 416, 422, 423	syl3anbrc 1344	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → 𝑏 ∈ (ℤ_≥‘𝑁))
425	414, 424	eqeltrd 2828	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
426	412, 425	pm2.61dan 812	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
427	426	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁))
428		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
429		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
430	180	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
431	430, 429	ifcld 4523	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ)
432	429	zred 12580	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
433	430	zred 12580	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℝ)
434		max1 13087	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))
435	432, 433, 434	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))
436		eluz2 12741	. . . . . . . . . 10 ⊢ (if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
437	429, 431, 435, 436	syl3anbrc 1344	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏))
438	437	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏))
439		fveq2 6822	. . . . . . . . . . 11 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑐) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
440	439	eleq1d 2813	. . . . . . . . . 10 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ))
441	439	fvoveq1d 7371	. . . . . . . . . . 11 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
442	441	breq1d 5102	. . . . . . . . . 10 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
443	440, 442	anbi12d 632	. . . . . . . . 9 ⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))))
444	443	rspccva 3576	. . . . . . . 8 ⊢ ((∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑏)) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
445	428, 438, 444	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
446	445	simprd 495	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))
447		fveq2 6822	. . . . . . . . 9 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑗) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)))
448	447	fvoveq1d 7371	. . . . . . . 8 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
449	448	breq1d 5102	. . . . . . 7 ⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
450	449	rspcev 3577	. . . . . 6 ⊢ ((if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ_≥‘𝑁) ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
451	427, 446, 450	syl2anc 584	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
452		ax-resscn 11066	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
453	452	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℝ ⊆ ℂ)
454	26, 453	fssd 6669	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ)
455		dvcn 25821	. . . . . . . . . . . . . 14 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
456	453, 454, 151, 107, 455	syl31anc 1375	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
457		cncfcdm 24789	. . . . . . . . . . . . 13 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
458	453, 456, 457	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
459	26, 458	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
460		ioodvbdlimc2lem.r	. . . . . . . . . . . 12 ⊢ 𝑅 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐵 − (1 / 𝑗)))
461	103, 460	fmptd 7048	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅:(ℤ_≥‘𝑀)⟶(𝐴(,)𝐵))
462		eqid 2729	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))
463		climrel 15399	. . . . . . . . . . . . 13 ⊢ Rel ⇝
464	463	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Rel ⇝ )
465		fvex 6835	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑀) ∈ V
466	465	mptex 7159	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵) ∈ V
467	466	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵) ∈ V)
468		eqidd 2730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵))
469		eqidd 2730	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑚) → 𝐵 = 𝐵)
470		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ (ℤ_≥‘𝑀))
471	6	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ)
472	468, 469, 470, 471	fvmptd 6937	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑚) = 𝐵)
473	23, 22, 467, 85, 472	climconst 15450	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵) ⇝ 𝐵)
474	465	mptex 7159	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐵 − (1 / 𝑗))) ∈ V
475	460, 474	eqeltri 2824	. . . . . . . . . . . . . . 15 ⊢ 𝑅 ∈ V
476	475	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ V)
477		1cnd 11110	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
478		elnnnn0b 12428	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ₀ ∧ 0 < 𝑀))
479	21, 65, 478	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
480		divcnvg 45612	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0)
481	477, 479, 480	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0)
482		eqidd 2730	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵))
483		eqidd 2730	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → 𝐵 = 𝐵)
484		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ (ℤ_≥‘𝑀))
485	6	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝐵 ∈ ℝ)
486	482, 483, 484, 485	fvmptd 6937	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑖) = 𝐵)
487	486, 485	eqeltrd 2828	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑖) ∈ ℝ)
488	487	recnd 11143	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑖) ∈ ℂ)
489		eqidd 2730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗)))
490		oveq2 7357	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖))
491	490	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖))
492	3, 484	sselid 3933	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℝ)
493		0red 11118	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 ∈ ℝ)
494	60	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
495	65	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑀)
496		eluzle 12748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑖)
497	496	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑖)
498	493, 494, 492, 495, 497	ltletrd 11276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 0 < 𝑖)
499	498	gt0ne0d 11684	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ≠ 0)
500	492, 499	rereccld 11951	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑖) ∈ ℝ)
501	489, 491, 484, 500	fvmptd 6937	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖))
502	492	recnd 11143	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℂ)
503	502, 499	reccld 11893	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (1 / 𝑖) ∈ ℂ)
504	501, 503	eqeltrd 2828	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ)
505	490	oveq2d 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (𝐵 − (1 / 𝑗)) = (𝐵 − (1 / 𝑖)))
506		ovex 7382	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 − (1 / 𝑖)) ∈ V
507	505, 460, 506	fvmpt 6930	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (ℤ_≥‘𝑀) → (𝑅‘𝑖) = (𝐵 − (1 / 𝑖)))
508	507	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑖) = (𝐵 − (1 / 𝑖)))
509	486, 501	oveq12d 7367	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑖) − ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐵 − (1 / 𝑖)))
510	508, 509	eqtr4d 2767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑖) = (((𝑗 ∈ (ℤ_≥‘𝑀) ↦ 𝐵)‘𝑖) − ((𝑗 ∈ (ℤ_≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)))
511	23, 22, 473, 476, 481, 488, 504, 510	climsub 15541	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ⇝ (𝐵 − 0))
512	85	subid1d 11464	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 0) = 𝐵)
513	511, 512	breqtrd 5118	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ⇝ 𝐵)
514		releldm 5886	. . . . . . . . . . . 12 ⊢ ((Rel ⇝ ∧ 𝑅 ⇝ 𝐵) → 𝑅 ∈ dom ⇝ )
515	464, 513, 514	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ dom ⇝ )
516		fveq2 6822	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → (ℤ_≥‘𝑙) = (ℤ_≥‘𝑘))
517		fveq2 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = 𝑘 → (𝑅‘𝑙) = (𝑅‘𝑘))
518	517	oveq2d 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 𝑘 → ((𝑅‘ℎ) − (𝑅‘𝑙)) = ((𝑅‘ℎ) − (𝑅‘𝑘)))
519	518	fveq2d 6826	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑘 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) = (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))))
520	519	breq1d 5102	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
521	516, 520	raleqbidv 3309	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → (∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
522	521	cbvrabv 3405	. . . . . . . . . . . . 13 ⊢ {𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
523		fveq2 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = 𝑖 → (𝑅‘ℎ) = (𝑅‘𝑖))
524	523	fvoveq1d 7371	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝑖 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) = (abs‘((𝑅‘𝑖) − (𝑅‘𝑘))))
525	524	breq1d 5102	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = 𝑖 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
526	525	cbvralvw 3207	. . . . . . . . . . . . . . 15 ⊢ (∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
527	526	rgenw 3048	. . . . . . . . . . . . . 14 ⊢ ∀𝑘 ∈ (ℤ_≥‘𝑀)(∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
528		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))})
529	527, 528	mpbi 230	. . . . . . . . . . . . 13 ⊢ {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
530	522, 529	eqtri 2752	. . . . . . . . . . . 12 ⊢ {𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
531	530	infeq1i 9369	. . . . . . . . . . 11 ⊢ inf({𝑙 ∈ (ℤ_≥‘𝑀) ∣ ∀ℎ ∈ (ℤ_≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < ) = inf({𝑘 ∈ (ℤ_≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ_≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
532	7, 6, 9, 459, 107, 108, 22, 461, 462, 515, 531	ioodvbdlimc1lem1 45916	. . . . . . . . . 10 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) ⇝ (lim sup‘(𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))))
533	460	fvmpt2 6941	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (ℤ_≥‘𝑀) ∧ (𝐵 − (1 / 𝑗)) ∈ ℝ) → (𝑅‘𝑗) = (𝐵 − (1 / 𝑗)))
534	111, 58, 533	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝑅‘𝑗) = (𝐵 − (1 / 𝑗)))
535	534	eqcomd 2735	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐵 − (1 / 𝑗)) = (𝑅‘𝑗))
536	535	fveq2d 6826	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘(𝐵 − (1 / 𝑗))) = (𝐹‘(𝑅‘𝑗)))
537	536	mpteq2dva 5185	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗)))) = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))
538	105, 537	eqtrid 2776	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 = (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))
539	538	fveq2d 6826	. . . . . . . . . 10 ⊢ (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))))
540	532, 538, 539	3brtr4d 5124	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⇝ (lim sup‘𝑆))
541	465	mptex 7159	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗)))) ∈ V
542	105, 541	eqeltri 2824	. . . . . . . . . . 11 ⊢ 𝑆 ∈ V
543	542	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ V)
544		eqidd 2730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ℤ) → (𝑆‘𝑐) = (𝑆‘𝑐))
545	543, 544	clim 15401	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))))
546	540, 545	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)))
547	546	simprd 495	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))
548	547	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))
549		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
550	549	rphalfcld 12949	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
551		breq2 5096	. . . . . . . . 9 ⊢ (𝑎 = (𝑥 / 2) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
552	551	anbi2d 630	. . . . . . . 8 ⊢ (𝑎 = (𝑥 / 2) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
553	552	rexralbidv 3195	. . . . . . 7 ⊢ (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
554	553	rspccva 3576	. . . . . 6 ⊢ ((∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ⁺) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
555	548, 550, 554	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ_≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
556	451, 555	r19.29a 3137	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑗 ∈ (ℤ_≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
557	405, 556	r19.29a 3137	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
558	557	ralrimiva 3121	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))
559		ioosscn 13311	. . . 4 ⊢ (𝐴(,)𝐵) ⊆ ℂ
560	559	a1i 11	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
561	454, 560, 85	ellimc3 25778	. 2 ⊢ (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐵) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))))
562	134, 558, 561	mpbir2and 713	1 ⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim_ℂ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3394 Vcvv 3436 ⊆ wss 3903 ∅c0 4284 ifcif 4476 class class class wbr 5092 ↦ cmpt 5173 dom cdm 5619 ran crn 5620 Rel wrel 5624 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 supcsup 9330 infcinf 9331 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 +∞cpnf 11146 ℝ^*cxr 11148 < clt 11149 ≤ cle 11150 − cmin 11347 / cdiv 11777 ℕcn 12128 2c2 12183 ℕ₀cn0 12384 ℤcz 12471 ℤ_≥cuz 12735 ℝ⁺crp 12893 (,)cioo 13248 ⌊cfl 13694 abscabs 15141 lim supclsp 15377 ⇝ cli 15391 –cn→ccncf 24767 lim_ℂ climc 25761 D cdv 25762

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087 ax-addf 11088

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-om 7800 df-1st 7924 df-2nd 7925 df-supp 8094 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-map 8755 df-pm 8756 df-ixp 8825 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fsupp 9252 df-fi 9301 df-sup 9332 df-inf 9333 df-oi 9402 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-z 12472 df-dec 12592 df-uz 12736 df-q 12850 df-rp 12894 df-xneg 13014 df-xadd 13015 df-xmul 13016 df-ioo 13252 df-ico 13254 df-icc 13255 df-fz 13411 df-fzo 13558 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 18514 df-sgrp 18593 df-mnd 18609 df-submnd 18658 df-mulg 18947 df-cntz 19196 df-cmn 19661 df-psmet 21253 df-xmet 21254 df-met 21255 df-bl 21256 df-mopn 21257 df-fbas 21258 df-fg 21259 df-cnfld 21262 df-top 22779 df-topon 22796 df-topsp 22818 df-bases 22831 df-cld 22904 df-ntr 22905 df-cls 22906 df-nei 22983 df-lp 23021 df-perf 23022 df-cn 23112 df-cnp 23113 df-haus 23200 df-cmp 23272 df-tx 23447 df-hmeo 23640 df-fil 23731 df-fm 23823 df-flim 23824 df-flf 23825 df-xms 24206 df-ms 24207 df-tms 24208 df-cncf 24769 df-limc 25765 df-dv 25766

This theorem is referenced by: ioodvbdlimc2 45920

W3C validator