ioodvbdlimc1lem2

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)

	Ref	Expression
Hypotheses	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	ioodvbdlimc1lem2	⊢ ( 𝜑 → ( lim sup ‘ 𝑆 ) ∈ ( 𝐹 lim_ℂ 𝐴 ) )

Proof

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

Metamath Proof Explorer

Theorem ioodvbdlimc1lem2

Proof