Theorem pntleml

Description: Lemma for pnt . Equation 10.6.35 in Shapiro, p. 436. (Contributed by Mario Carneiro, 14-Apr-2016)

	Ref	Expression
Hypotheses	pntlem3.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntlem3.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	pntlem3.A	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
	pntlemp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	pntlemp.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
	pntlemp.d	⊢ 𝐷 = ( 𝐴 + 1 )
	pntlemp.f	⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
	pntlemp.K	⊢ ( 𝜑 → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
Assertion	pntleml	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 )

Proof

Step	Hyp	Ref	Expression
1		pntlem3.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		pntlem3.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3		pntlem3.A	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
4		pntlemp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
5		pntlemp.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
6		pntlemp.d	⊢ 𝐷 = ( 𝐴 + 1 )
7		pntlemp.f	⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
8		pntlemp.K	⊢ ( 𝜑 → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
9		eqid	⊢ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } = { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 }
10	1 2 4 5 6 7	pntlemd	⊢ ( 𝜑 → ( 𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+ ) )
11	10	simp3d	⊢ ( 𝜑 → 𝐹 ∈ ℝ+ )
12		0m0e0	⊢ ( 0 − 0 ) = 0
13		simpr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 = 0 ) → 𝑟 = 0 )
14	13	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 = 0 ) → ( 𝑟 ↑ 3 ) = ( 0 ↑ 3 ) )
15		3nn	⊢ 3 ∈ ℕ
16		0exp	⊢ ( 3 ∈ ℕ → ( 0 ↑ 3 ) = 0 )
17	15 16	ax-mp	⊢ ( 0 ↑ 3 ) = 0
18	14 17	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 = 0 ) → ( 𝑟 ↑ 3 ) = 0 )
19	18	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 = 0 ) → ( 𝐹 · ( 𝑟 ↑ 3 ) ) = ( 𝐹 · 0 ) )
20	11	rpcnd	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
21	20	mul01d	⊢ ( 𝜑 → ( 𝐹 · 0 ) = 0 )
22	21	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 = 0 ) → ( 𝐹 · 0 ) = 0 )
23	19 22	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 = 0 ) → ( 𝐹 · ( 𝑟 ↑ 3 ) ) = 0 )
24	13 23	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 = 0 ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) = ( 0 − 0 ) )
25	12 24 13	3eqtr4a	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 = 0 ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) = 𝑟 )
26		simplr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 = 0 ) → 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } )
27	25 26	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 = 0 ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } )
28		oveq1	⊢ ( 𝑦 = 𝑠 → ( 𝑦 [,) +∞ ) = ( 𝑠 [,) +∞ ) )
29	28	raleqdv	⊢ ( 𝑦 = 𝑠 → ( ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ↔ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) )
30	29	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ↔ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 )
31		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝑟 ∈ ( 0 [,] 𝐴 ) )
32		0re	⊢ 0 ∈ ℝ
33	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝐴 ∈ ℝ+ )
34	33	rpred	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝐴 ∈ ℝ )
35		elicc2	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑟 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑟 ∈ ℝ ∧ 0 ≤ 𝑟 ∧ 𝑟 ≤ 𝐴 ) ) )
36	32 34 35	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 𝑟 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑟 ∈ ℝ ∧ 0 ≤ 𝑟 ∧ 𝑟 ≤ 𝐴 ) ) )
37	31 36	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 𝑟 ∈ ℝ ∧ 0 ≤ 𝑟 ∧ 𝑟 ≤ 𝐴 ) )
38	37	simp1d	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝑟 ∈ ℝ )
39	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝐹 ∈ ℝ+ )
40	37	simp2d	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 0 ≤ 𝑟 )
41		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝑟 ≠ 0 )
42	38 40 41	ne0gt0d	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 0 < 𝑟 )
43	38 42	elrpd	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝑟 ∈ ℝ+ )
44		3z	⊢ 3 ∈ ℤ
45		rpexpcl	⊢ ( ( 𝑟 ∈ ℝ+ ∧ 3 ∈ ℤ ) → ( 𝑟 ↑ 3 ) ∈ ℝ+ )
46	43 44 45	sylancl	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 𝑟 ↑ 3 ) ∈ ℝ+ )
47	39 46	rpmulcld	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 𝐹 · ( 𝑟 ↑ 3 ) ) ∈ ℝ+ )
48	47	rpred	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 𝐹 · ( 𝑟 ↑ 3 ) ) ∈ ℝ )
49	38 48	resubcld	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ℝ )
50	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
51	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝐵 ∈ ℝ+ )
52	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝐿 ∈ ( 0 (,) 1 ) )
53	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
54	37	simp3d	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝑟 ≤ 𝐴 )
55		eqid	⊢ ( 𝑟 / 𝐷 ) = ( 𝑟 / 𝐷 )
56		eqid	⊢ ( exp ‘ ( 𝐵 / ( 𝑟 / 𝐷 ) ) ) = ( exp ‘ ( 𝐵 / ( 𝑟 / 𝐷 ) ) )
57		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝑠 ∈ ℝ+ )
58		1rp	⊢ 1 ∈ ℝ+
59		rpaddcl	⊢ ( ( 𝑠 ∈ ℝ+ ∧ 1 ∈ ℝ+ ) → ( 𝑠 + 1 ) ∈ ℝ+ )
60	57 58 59	sylancl	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 𝑠 + 1 ) ∈ ℝ+ )
61	57	rpge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 0 ≤ 𝑠 )
62		1re	⊢ 1 ∈ ℝ
63	57	rpred	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝑠 ∈ ℝ )
64		addge02	⊢ ( ( 1 ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( 0 ≤ 𝑠 ↔ 1 ≤ ( 𝑠 + 1 ) ) )
65	62 63 64	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 0 ≤ 𝑠 ↔ 1 ≤ ( 𝑠 + 1 ) ) )
66	61 65	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 1 ≤ ( 𝑠 + 1 ) )
67	60 66	jca	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( ( 𝑠 + 1 ) ∈ ℝ+ ∧ 1 ≤ ( 𝑠 + 1 ) ) )
68	57	rpxrd	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝑠 ∈ ℝ* )
69	63	lep1d	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 𝑠 ≤ ( 𝑠 + 1 ) )
70		df-ico	⊢ [,) = ( 𝑡 ∈ ℝ* , 𝑟 ∈ ℝ* ↦ { 𝑤 ∈ ℝ* ∣ ( 𝑡 ≤ 𝑤 ∧ 𝑤 < 𝑟 ) } )
71		xrletr	⊢ ( ( 𝑠 ∈ ℝ* ∧ ( 𝑠 + 1 ) ∈ ℝ* ∧ 𝑣 ∈ ℝ* ) → ( ( 𝑠 ≤ ( 𝑠 + 1 ) ∧ ( 𝑠 + 1 ) ≤ 𝑣 ) → 𝑠 ≤ 𝑣 ) )
72	70 70 71	ixxss1	⊢ ( ( 𝑠 ∈ ℝ* ∧ 𝑠 ≤ ( 𝑠 + 1 ) ) → ( ( 𝑠 + 1 ) [,) +∞ ) ⊆ ( 𝑠 [,) +∞ ) )
73	68 69 72	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( ( 𝑠 + 1 ) [,) +∞ ) ⊆ ( 𝑠 [,) +∞ ) )
74		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 )
75		ssralv	⊢ ( ( ( 𝑠 + 1 ) [,) +∞ ) ⊆ ( 𝑠 [,) +∞ ) → ( ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 → ∀ 𝑧 ∈ ( ( 𝑠 + 1 ) [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) )
76	73 74 75	sylc	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ∀ 𝑧 ∈ ( ( 𝑠 + 1 ) [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 )
77	1 33 50 51 52 6 7 53 43 54 55 56 67 76	pntlemp	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) )
78		rpre	⊢ ( 𝑤 ∈ ℝ+ → 𝑤 ∈ ℝ )
79	78	adantl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ )
80	79	leidd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ≤ 𝑤 )
81		elicopnf	⊢ ( 𝑤 ∈ ℝ → ( 𝑤 ∈ ( 𝑤 [,) +∞ ) ↔ ( 𝑤 ∈ ℝ ∧ 𝑤 ≤ 𝑤 ) ) )
82	79 81	syl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( 𝑤 ∈ ( 𝑤 [,) +∞ ) ↔ ( 𝑤 ∈ ℝ ∧ 𝑤 ≤ 𝑤 ) ) )
83	79 80 82	mpbir2and	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ( 𝑤 [,) +∞ ) )
84		fveq2	⊢ ( 𝑣 = 𝑤 → ( 𝑅 ‘ 𝑣 ) = ( 𝑅 ‘ 𝑤 ) )
85		id	⊢ ( 𝑣 = 𝑤 → 𝑣 = 𝑤 )
86	84 85	oveq12d	⊢ ( 𝑣 = 𝑤 → ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) = ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) )
87	86	fveq2d	⊢ ( 𝑣 = 𝑤 → ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) )
88	87	breq1d	⊢ ( 𝑣 = 𝑤 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
89	88	rspcv	⊢ ( 𝑤 ∈ ( 𝑤 [,) +∞ ) → ( ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
90	83 89	syl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
91	1	pntrf	⊢ 𝑅 : ℝ+ ⟶ ℝ
92	91	ffvelcdmi	⊢ ( 𝑤 ∈ ℝ+ → ( 𝑅 ‘ 𝑤 ) ∈ ℝ )
93		rerpdivcl	⊢ ( ( ( 𝑅 ‘ 𝑤 ) ∈ ℝ ∧ 𝑤 ∈ ℝ+ ) → ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ∈ ℝ )
94	92 93	mpancom	⊢ ( 𝑤 ∈ ℝ+ → ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ∈ ℝ )
95	94	adantl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ∈ ℝ )
96	95	recnd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ∈ ℂ )
97	96	absge0d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → 0 ≤ ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) )
98	96	abscld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) ∈ ℝ )
99	49	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ℝ )
100		letr	⊢ ( ( 0 ∈ ℝ ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) ∈ ℝ ∧ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ℝ ) → ( ( 0 ≤ ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) → 0 ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
101	32 98 99 100	mp3an2i	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( ( 0 ≤ ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) → 0 ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
102	97 101	mpand	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑤 ) / 𝑤 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) → 0 ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
103	90 102	syld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) → 0 ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
104	103	rexlimdva	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) → 0 ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
105	77 104	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 0 ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) )
106	47	rpge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → 0 ≤ ( 𝐹 · ( 𝑟 ↑ 3 ) ) )
107	38 48	subge02d	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 0 ≤ ( 𝐹 · ( 𝑟 ↑ 3 ) ) ↔ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ≤ 𝑟 ) )
108	106 107	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ≤ 𝑟 )
109	49 38 34 108 54	letrd	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ≤ 𝐴 )
110		elicc2	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ( 0 [,] 𝐴 ) ↔ ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∧ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ≤ 𝐴 ) ) )
111	32 34 110	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ( 0 [,] 𝐴 ) ↔ ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∧ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ≤ 𝐴 ) ) )
112	49 105 109 111	mpbir3and	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ( 0 [,] 𝐴 ) )
113	112 77	jca	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) ∧ ( 𝑠 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) ) → ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ( 0 [,] 𝐴 ) ∧ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
114	113	rexlimdvaa	⊢ ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) → ( ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑠 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 → ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ( 0 [,] 𝐴 ) ∧ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) ) )
115	30 114	biimtrid	⊢ ( ( 𝜑 ∧ ( 𝑟 ≠ 0 ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) ) → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 → ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ( 0 [,] 𝐴 ) ∧ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) ) )
116	115	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑟 ≠ 0 ) ∧ 𝑟 ∈ ( 0 [,] 𝐴 ) ) → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 → ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ( 0 [,] 𝐴 ) ∧ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) ) )
117	116	expimpd	⊢ ( ( 𝜑 ∧ 𝑟 ≠ 0 ) → ( ( 𝑟 ∈ ( 0 [,] 𝐴 ) ∧ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) → ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ( 0 [,] 𝐴 ) ∧ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) ) )
118		breq2	⊢ ( 𝑡 = 𝑟 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) )
119	118	rexralbidv	⊢ ( 𝑡 = 𝑟 → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ↔ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) )
120	119	elrab	⊢ ( 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ↔ ( 𝑟 ∈ ( 0 [,] 𝐴 ) ∧ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑟 ) )
121		breq2	⊢ ( 𝑡 = ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
122	121	rexralbidv	⊢ ( 𝑡 = ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ↔ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
123		fveq2	⊢ ( 𝑣 = 𝑧 → ( 𝑅 ‘ 𝑣 ) = ( 𝑅 ‘ 𝑧 ) )
124		id	⊢ ( 𝑣 = 𝑧 → 𝑣 = 𝑧 )
125	123 124	oveq12d	⊢ ( 𝑣 = 𝑧 → ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) = ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) )
126	125	fveq2d	⊢ ( 𝑣 = 𝑧 → ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) )
127	126	breq1d	⊢ ( 𝑣 = 𝑧 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
128	127	cbvralvw	⊢ ( ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ↔ ∀ 𝑧 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) )
129		oveq1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 [,) +∞ ) = ( 𝑦 [,) +∞ ) )
130	129	raleqdv	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑧 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ↔ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
131	128 130	bitrid	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ↔ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
132	131	cbvrexvw	⊢ ( ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ↔ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) )
133	122 132	bitr4di	⊢ ( 𝑡 = ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ↔ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
134	133	elrab	⊢ ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ↔ ( ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ ( 0 [,] 𝐴 ) ∧ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ) )
135	117 120 134	3imtr4g	⊢ ( ( 𝜑 ∧ 𝑟 ≠ 0 ) → ( 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) )
136	135	imp	⊢ ( ( ( 𝜑 ∧ 𝑟 ≠ 0 ) ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } )
137	136	an32s	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) ∧ 𝑟 ≠ 0 ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } )
138	27 137	pm2.61dane	⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } ) → ( 𝑟 − ( 𝐹 · ( 𝑟 ↑ 3 ) ) ) ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } )
139	1 2 3 9 11 138	pntlem3	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 )