Theorem aalioulem3

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 15-Nov-2014)

	Ref	Expression
Hypotheses	aalioulem2.a	⊢ 𝑁 = ( deg ‘ 𝐹 )
	aalioulem2.b	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) )
	aalioulem2.c	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	aalioulem2.d	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	aalioulem3.e	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
Assertion	aalioulem3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		aalioulem2.a	⊢ 𝑁 = ( deg ‘ 𝐹 )
2		aalioulem2.b	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) )
3		aalioulem2.c	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		aalioulem2.d	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5		aalioulem3.e	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
6		1re	⊢ 1 ∈ ℝ
7		resubcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 − 1 ) ∈ ℝ )
8	4 6 7	sylancl	⊢ ( 𝜑 → ( 𝐴 − 1 ) ∈ ℝ )
9		peano2re	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
10	4 9	syl	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℝ )
11		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
12		ssid	⊢ ℂ ⊆ ℂ
13		fncpn	⊢ ( ℂ ⊆ ℂ → ( 𝓑C𝑛 ‘ ℂ ) Fn ℕ0 )
14	12 13	ax-mp	⊢ ( 𝓑C𝑛 ‘ ℂ ) Fn ℕ0
15		1nn0	⊢ 1 ∈ ℕ0
16		fnfvelrn	⊢ ( ( ( 𝓑C𝑛 ‘ ℂ ) Fn ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) ∈ ran ( 𝓑C𝑛 ‘ ℂ ) )
17	14 15 16	mp2an	⊢ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) ∈ ran ( 𝓑C𝑛 ‘ ℂ )
18		intss1	⊢ ( ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) ∈ ran ( 𝓑C𝑛 ‘ ℂ ) → ∩ ran ( 𝓑C𝑛 ‘ ℂ ) ⊆ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) )
19	17 18	ax-mp	⊢ ∩ ran ( 𝓑C𝑛 ‘ ℂ ) ⊆ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 )
20		plycpn	⊢ ( 𝐹 ∈ ( Poly ‘ ℤ ) → 𝐹 ∈ ∩ ran ( 𝓑C𝑛 ‘ ℂ ) )
21	2 20	syl	⊢ ( 𝜑 → 𝐹 ∈ ∩ ran ( 𝓑C𝑛 ‘ ℂ ) )
22	19 21	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) )
23		cpnres	⊢ ( ( ℝ ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) ) → ( 𝐹 ↾ ℝ ) ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) )
24	11 22 23	sylancr	⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) )
25		df-ima	⊢ ( 𝐹 “ ℝ ) = ran ( 𝐹 ↾ ℝ )
26		zssre	⊢ ℤ ⊆ ℝ
27		ax-resscn	⊢ ℝ ⊆ ℂ
28		plyss	⊢ ( ( ℤ ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℝ ) )
29	26 27 28	mp2an	⊢ ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℝ )
30	29 2	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℝ ) )
31		plyreres	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℝ )
32	30 31	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℝ )
33	32	frnd	⊢ ( 𝜑 → ran ( 𝐹 ↾ ℝ ) ⊆ ℝ )
34	25 33	eqsstrid	⊢ ( 𝜑 → ( 𝐹 “ ℝ ) ⊆ ℝ )
35		iccssre	⊢ ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ) → ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ⊆ ℝ )
36	8 10 35	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ⊆ ℝ )
37	36 27	sstrdi	⊢ ( 𝜑 → ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ⊆ ℂ )
38		plyf	⊢ ( 𝐹 ∈ ( Poly ‘ ℤ ) → 𝐹 : ℂ ⟶ ℂ )
39	2 38	syl	⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
40	39	fdmd	⊢ ( 𝜑 → dom 𝐹 = ℂ )
41	37 40	sseqtrrd	⊢ ( 𝜑 → ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ⊆ dom 𝐹 )
42	8 10 24 34 41	c1lip3	⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) )
43		simp2	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝑟 ∈ ℝ )
44	43	recnd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝑟 ∈ ℂ )
45	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐴 ∈ ℝ )
46	45	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝐴 ∈ ℝ )
47	46	recnd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝐴 ∈ ℂ )
48	44 47	abssubd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( 𝑟 − 𝐴 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) )
49		simp3	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 )
50	48 49	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( 𝑟 − 𝐴 ) ) ≤ 1 )
51		1red	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 1 ∈ ℝ )
52		elicc4abs	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑟 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ↔ ( abs ‘ ( 𝑟 − 𝐴 ) ) ≤ 1 ) )
53	46 51 43 52	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( 𝑟 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ↔ ( abs ‘ ( 𝑟 − 𝐴 ) ) ≤ 1 ) )
54	50 53	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝑟 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) )
55	4	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
56	55	subidd	⊢ ( 𝜑 → ( 𝐴 − 𝐴 ) = 0 )
57	56	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐴 ) ) = ( abs ‘ 0 ) )
58		abs0	⊢ ( abs ‘ 0 ) = 0
59		0le1	⊢ 0 ≤ 1
60	58 59	eqbrtri	⊢ ( abs ‘ 0 ) ≤ 1
61	57 60	eqbrtrdi	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐴 ) ) ≤ 1 )
62		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
63		elicc4abs	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ↔ ( abs ‘ ( 𝐴 − 𝐴 ) ) ≤ 1 ) )
64	4 62 4 63	syl3anc	⊢ ( 𝜑 → ( 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ↔ ( abs ‘ ( 𝐴 − 𝐴 ) ) ≤ 1 ) )
65	61 64	mpbird	⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) )
66	65	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) )
67	66	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) )
68		fveq2	⊢ ( 𝑏 = 𝑟 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑟 ) )
69	68	oveq2d	⊢ ( 𝑏 = 𝑟 → ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑟 ) ) )
70	69	fveq2d	⊢ ( 𝑏 = 𝑟 → ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑟 ) ) ) )
71		oveq2	⊢ ( 𝑏 = 𝑟 → ( 𝑐 − 𝑏 ) = ( 𝑐 − 𝑟 ) )
72	71	fveq2d	⊢ ( 𝑏 = 𝑟 → ( abs ‘ ( 𝑐 − 𝑏 ) ) = ( abs ‘ ( 𝑐 − 𝑟 ) ) )
73	72	oveq2d	⊢ ( 𝑏 = 𝑟 → ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) = ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑟 ) ) ) )
74	70 73	breq12d	⊢ ( 𝑏 = 𝑟 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑟 ) ) ) ) )
75		fveq2	⊢ ( 𝑐 = 𝐴 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝐴 ) )
76	75	fvoveq1d	⊢ ( 𝑐 = 𝐴 → ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑟 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) )
77		fvoveq1	⊢ ( 𝑐 = 𝐴 → ( abs ‘ ( 𝑐 − 𝑟 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) )
78	77	oveq2d	⊢ ( 𝑐 = 𝐴 → ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑟 ) ) ) = ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
79	76 78	breq12d	⊢ ( 𝑐 = 𝐴 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑟 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
80	74 79	rspc2v	⊢ ( ( 𝑟 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∧ 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ) → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
81	54 67 80	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
82		simp1l	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝜑 )
83	82 5	syl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( 𝐹 ‘ 𝐴 ) = 0 )
84		0cn	⊢ 0 ∈ ℂ
85	83 84	eqeltrdi	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
86	39	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 : ℂ ⟶ ℂ )
87	86	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝐹 : ℂ ⟶ ℂ )
88	87 44	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( 𝐹 ‘ 𝑟 ) ∈ ℂ )
89	85 88	abssubd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑟 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
90	83	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ( 𝐹 ‘ 𝑟 ) − ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝑟 ) − 0 ) )
91	88	subid1d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ( 𝐹 ‘ 𝑟 ) − 0 ) = ( 𝐹 ‘ 𝑟 ) )
92	90 91	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ( 𝐹 ‘ 𝑟 ) − ( 𝐹 ‘ 𝐴 ) ) = ( 𝐹 ‘ 𝑟 ) )
93	92	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑟 ) − ( 𝐹 ‘ 𝐴 ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) )
94	89 93	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) )
95	94	breq1d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
96	81 95	sylibd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
97	96	3exp	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑟 ∈ ℝ → ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ) )
98	97	com34	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑟 ∈ ℝ → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ) )
99	98	com23	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( 𝑟 ∈ ℝ → ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ) )
100	99	ralrimdv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) )
101	100	reximdva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ∃ 𝑎 ∈ ℝ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) )
102	42 101	mpd	⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
103		1rp	⊢ 1 ∈ ℝ+
104	103	a1i	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑎 = 0 ) → 1 ∈ ℝ+ )
105		recn	⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℂ )
106	105	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℂ )
107		neqne	⊢ ( ¬ 𝑎 = 0 → 𝑎 ≠ 0 )
108		absrpcl	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) → ( abs ‘ 𝑎 ) ∈ ℝ+ )
109	106 107 108	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝑎 = 0 ) → ( abs ‘ 𝑎 ) ∈ ℝ+ )
110	109	rpreccld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝑎 = 0 ) → ( 1 / ( abs ‘ 𝑎 ) ) ∈ ℝ+ )
111	104 110	ifclda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) ∈ ℝ+ )
112		eqid	⊢ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) )
113		eqif	⊢ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) ↔ ( ( 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 ) ∨ ( ¬ 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) ) ) )
114	112 113	mpbi	⊢ ( ( 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 ) ∨ ( ¬ 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) ) )
115		simplrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
116		oveq1	⊢ ( 𝑎 = 0 → ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) = ( 0 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
117	116	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) = ( 0 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
118	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝐴 ∈ ℝ )
119		simprl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝑟 ∈ ℝ )
120	118 119	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( 𝐴 − 𝑟 ) ∈ ℝ )
121	120	recnd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( 𝐴 − 𝑟 ) ∈ ℂ )
122	121	abscld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ℝ )
123	122	recnd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ℂ )
124	123	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ℂ )
125	124	mul02d	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 0 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) = 0 )
126	117 125	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) = 0 )
127	115 126	breqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ 0 )
128	39	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝐹 : ℂ ⟶ ℂ )
129	119	recnd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝑟 ∈ ℂ )
130	128 129	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( 𝐹 ‘ 𝑟 ) ∈ ℂ )
131	130	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 𝐹 ‘ 𝑟 ) ∈ ℂ )
132	131	absge0d	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) )
133	130	abscld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℝ )
134	133	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℝ )
135		0re	⊢ 0 ∈ ℝ
136		letri3	⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) = 0 ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ) )
137	134 135 136	sylancl	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) = 0 ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ) )
138	127 132 137	mpbir2and	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) = 0 )
139	138	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) = ( 1 · 0 ) )
140		ax-1cn	⊢ 1 ∈ ℂ
141	140	mul01i	⊢ ( 1 · 0 ) = 0
142	139 141	eqtrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) = 0 )
143	121	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 𝐴 − 𝑟 ) ∈ ℂ )
144	143	absge0d	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → 0 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) )
145	142 144	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) )
146		oveq1	⊢ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) = ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) )
147	146	breq1d	⊢ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 → ( ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
148	145 147	syl5ibrcom	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
149	148	expimpd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( ( 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
150		df-ne	⊢ ( 𝑎 ≠ 0 ↔ ¬ 𝑎 = 0 )
151	133	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℝ )
152	151	recnd	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℂ )
153		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → 𝑎 ∈ ℝ )
154	153	recnd	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → 𝑎 ∈ ℂ )
155	154 108	sylancom	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ 𝑎 ) ∈ ℝ+ )
156	155	rpcnne0d	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( ( abs ‘ 𝑎 ) ∈ ℂ ∧ ( abs ‘ 𝑎 ) ≠ 0 ) )
157		divrec2	⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ℂ ∧ ( abs ‘ 𝑎 ) ≠ 0 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) / ( abs ‘ 𝑎 ) ) = ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) )
158	157	3expb	⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℂ ∧ ( ( abs ‘ 𝑎 ) ∈ ℂ ∧ ( abs ‘ 𝑎 ) ≠ 0 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) / ( abs ‘ 𝑎 ) ) = ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) )
159	152 156 158	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) / ( abs ‘ 𝑎 ) ) = ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) )
160		simplr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝑎 ∈ ℝ )
161	160 122	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ∈ ℝ )
162	160	recnd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝑎 ∈ ℂ )
163	162	abscld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ 𝑎 ) ∈ ℝ )
164	163 122	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ∈ ℝ )
165		simprr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
166	121	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 0 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) )
167		leabs	⊢ ( 𝑎 ∈ ℝ → 𝑎 ≤ ( abs ‘ 𝑎 ) )
168	167	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝑎 ≤ ( abs ‘ 𝑎 ) )
169	160 163 122 166 168	lemul1ad	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ≤ ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
170	133 161 164 165 169	letrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
171	170	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
172	122	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ℝ )
173	151 172 155	ledivmuld	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) / ( abs ‘ 𝑎 ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
174	171 173	mpbird	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) / ( abs ‘ 𝑎 ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) )
175	159 174	eqbrtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) )
176	150 175	sylan2br	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ ¬ 𝑎 = 0 ) → ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) )
177		oveq1	⊢ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) = ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) )
178	177	breq1d	⊢ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) → ( ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
179	176 178	syl5ibrcom	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ ¬ 𝑎 = 0 ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
180	179	expimpd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( ( ¬ 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
181	149 180	jaod	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( ( ( 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 ) ∨ ( ¬ 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
182	114 181	mpi	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) )
183	182	expr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
184	183	imim2d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) → ( ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
185	184	ralimdva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
186		oveq1	⊢ ( 𝑥 = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) = ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) )
187	186	breq1d	⊢ ( 𝑥 = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) → ( ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
188	187	imbi2d	⊢ ( 𝑥 = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) → ( ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
189	188	ralbidv	⊢ ( 𝑥 = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) → ( ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
190	189	rspcev	⊢ ( ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
191	111 185 190	syl6an	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
192	191	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℝ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
193	102 192	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )