Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  aalioulem3 Structured version   Visualization version   GIF version

Theorem aalioulem3 24134
 Description: Lemma for aaliou 24138. (Contributed by Stefan O'Rear, 15-Nov-2014.)
Hypotheses
Ref Expression
aalioulem2.a 𝑁 = (deg‘𝐹)
aalioulem2.b (𝜑𝐹 ∈ (Poly‘ℤ))
aalioulem2.c (𝜑𝑁 ∈ ℕ)
aalioulem2.d (𝜑𝐴 ∈ ℝ)
aalioulem3.e (𝜑 → (𝐹𝐴) = 0)
Assertion
Ref Expression
aalioulem3 (𝜑 → ∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
Distinct variable groups:   𝜑,𝑥,𝑟   𝑥,𝐴,𝑟   𝑥,𝐹,𝑟
Allowed substitution hints:   𝑁(𝑥,𝑟)

Proof of Theorem aalioulem3
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 aalioulem2.d . . . . 5 (𝜑𝐴 ∈ ℝ)
2 1re 10077 . . . . 5 1 ∈ ℝ
3 resubcl 10383 . . . . 5 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 − 1) ∈ ℝ)
41, 2, 3sylancl 695 . . . 4 (𝜑 → (𝐴 − 1) ∈ ℝ)
5 peano2re 10247 . . . . 5 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
61, 5syl 17 . . . 4 (𝜑 → (𝐴 + 1) ∈ ℝ)
7 reelprrecn 10066 . . . . 5 ℝ ∈ {ℝ, ℂ}
8 ssid 3657 . . . . . . . . 9 ℂ ⊆ ℂ
9 fncpn 23741 . . . . . . . . 9 (ℂ ⊆ ℂ → (Cn‘ℂ) Fn ℕ0)
108, 9ax-mp 5 . . . . . . . 8 (Cn‘ℂ) Fn ℕ0
11 1nn0 11346 . . . . . . . 8 1 ∈ ℕ0
12 fnfvelrn 6396 . . . . . . . 8 (((Cn‘ℂ) Fn ℕ0 ∧ 1 ∈ ℕ0) → ((Cn‘ℂ)‘1) ∈ ran (Cn‘ℂ))
1310, 11, 12mp2an 708 . . . . . . 7 ((Cn‘ℂ)‘1) ∈ ran (Cn‘ℂ)
14 intss1 4524 . . . . . . 7 (((Cn‘ℂ)‘1) ∈ ran (Cn‘ℂ) → ran (Cn‘ℂ) ⊆ ((Cn‘ℂ)‘1))
1513, 14ax-mp 5 . . . . . 6 ran (Cn‘ℂ) ⊆ ((Cn‘ℂ)‘1)
16 aalioulem2.b . . . . . . 7 (𝜑𝐹 ∈ (Poly‘ℤ))
17 plycpn 24089 . . . . . . 7 (𝐹 ∈ (Poly‘ℤ) → 𝐹 ran (Cn‘ℂ))
1816, 17syl 17 . . . . . 6 (𝜑𝐹 ran (Cn‘ℂ))
1915, 18sseldi 3634 . . . . 5 (𝜑𝐹 ∈ ((Cn‘ℂ)‘1))
20 cpnres 23745 . . . . 5 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ ((Cn‘ℂ)‘1)) → (𝐹 ↾ ℝ) ∈ ((Cn‘ℝ)‘1))
217, 19, 20sylancr 696 . . . 4 (𝜑 → (𝐹 ↾ ℝ) ∈ ((Cn‘ℝ)‘1))
22 df-ima 5156 . . . . 5 (𝐹 “ ℝ) = ran (𝐹 ↾ ℝ)
23 zssre 11422 . . . . . . . . 9 ℤ ⊆ ℝ
24 ax-resscn 10031 . . . . . . . . 9 ℝ ⊆ ℂ
25 plyss 24000 . . . . . . . . 9 ((ℤ ⊆ ℝ ∧ ℝ ⊆ ℂ) → (Poly‘ℤ) ⊆ (Poly‘ℝ))
2623, 24, 25mp2an 708 . . . . . . . 8 (Poly‘ℤ) ⊆ (Poly‘ℝ)
2726, 16sseldi 3634 . . . . . . 7 (𝜑𝐹 ∈ (Poly‘ℝ))
28 plyreres 24083 . . . . . . 7 (𝐹 ∈ (Poly‘ℝ) → (𝐹 ↾ ℝ):ℝ⟶ℝ)
2927, 28syl 17 . . . . . 6 (𝜑 → (𝐹 ↾ ℝ):ℝ⟶ℝ)
30 frn 6091 . . . . . 6 ((𝐹 ↾ ℝ):ℝ⟶ℝ → ran (𝐹 ↾ ℝ) ⊆ ℝ)
3129, 30syl 17 . . . . 5 (𝜑 → ran (𝐹 ↾ ℝ) ⊆ ℝ)
3222, 31syl5eqss 3682 . . . 4 (𝜑 → (𝐹 “ ℝ) ⊆ ℝ)
33 iccssre 12293 . . . . . . 7 (((𝐴 − 1) ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ) → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ ℝ)
344, 6, 33syl2anc 694 . . . . . 6 (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ ℝ)
3534, 24syl6ss 3648 . . . . 5 (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ ℂ)
36 plyf 23999 . . . . . . 7 (𝐹 ∈ (Poly‘ℤ) → 𝐹:ℂ⟶ℂ)
3716, 36syl 17 . . . . . 6 (𝜑𝐹:ℂ⟶ℂ)
38 fdm 6089 . . . . . 6 (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
3937, 38syl 17 . . . . 5 (𝜑 → dom 𝐹 = ℂ)
4035, 39sseqtr4d 3675 . . . 4 (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ dom 𝐹)
414, 6, 21, 32, 40c1lip3 23807 . . 3 (𝜑 → ∃𝑎 ∈ ℝ ∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹𝑐) − (𝐹𝑏))) ≤ (𝑎 · (abs‘(𝑐𝑏))))
42 simp2 1082 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → 𝑟 ∈ ℝ)
4342recnd 10106 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → 𝑟 ∈ ℂ)
441adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ ℝ) → 𝐴 ∈ ℝ)
45443ad2ant1 1102 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → 𝐴 ∈ ℝ)
4645recnd 10106 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → 𝐴 ∈ ℂ)
4743, 46abssubd 14236 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (abs‘(𝑟𝐴)) = (abs‘(𝐴𝑟)))
48 simp3 1083 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (abs‘(𝐴𝑟)) ≤ 1)
4947, 48eqbrtrd 4707 . . . . . . . . . . 11 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (abs‘(𝑟𝐴)) ≤ 1)
50 1red 10093 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → 1 ∈ ℝ)
51 elicc4abs 14103 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝑟𝐴)) ≤ 1))
5245, 50, 42, 51syl3anc 1366 . . . . . . . . . . 11 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝑟𝐴)) ≤ 1))
5349, 52mpbird 247 . . . . . . . . . 10 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → 𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1)))
541recnd 10106 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℂ)
5554subidd 10418 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐴) = 0)
5655fveq2d 6233 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐴𝐴)) = (abs‘0))
57 abs0 14069 . . . . . . . . . . . . . . 15 (abs‘0) = 0
58 0le1 10589 . . . . . . . . . . . . . . 15 0 ≤ 1
5957, 58eqbrtri 4706 . . . . . . . . . . . . . 14 (abs‘0) ≤ 1
6056, 59syl6eqbr 4724 . . . . . . . . . . . . 13 (𝜑 → (abs‘(𝐴𝐴)) ≤ 1)
61 1red 10093 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℝ)
62 elicc4abs 14103 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝐴𝐴)) ≤ 1))
631, 61, 1, 62syl3anc 1366 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝐴𝐴)) ≤ 1))
6460, 63mpbird 247 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1)))
6564adantr 480 . . . . . . . . . . 11 ((𝜑𝑎 ∈ ℝ) → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1)))
66653ad2ant1 1102 . . . . . . . . . 10 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1)))
67 fveq2 6229 . . . . . . . . . . . . . 14 (𝑏 = 𝑟 → (𝐹𝑏) = (𝐹𝑟))
6867oveq2d 6706 . . . . . . . . . . . . 13 (𝑏 = 𝑟 → ((𝐹𝑐) − (𝐹𝑏)) = ((𝐹𝑐) − (𝐹𝑟)))
6968fveq2d 6233 . . . . . . . . . . . 12 (𝑏 = 𝑟 → (abs‘((𝐹𝑐) − (𝐹𝑏))) = (abs‘((𝐹𝑐) − (𝐹𝑟))))
70 oveq2 6698 . . . . . . . . . . . . . 14 (𝑏 = 𝑟 → (𝑐𝑏) = (𝑐𝑟))
7170fveq2d 6233 . . . . . . . . . . . . 13 (𝑏 = 𝑟 → (abs‘(𝑐𝑏)) = (abs‘(𝑐𝑟)))
7271oveq2d 6706 . . . . . . . . . . . 12 (𝑏 = 𝑟 → (𝑎 · (abs‘(𝑐𝑏))) = (𝑎 · (abs‘(𝑐𝑟))))
7369, 72breq12d 4698 . . . . . . . . . . 11 (𝑏 = 𝑟 → ((abs‘((𝐹𝑐) − (𝐹𝑏))) ≤ (𝑎 · (abs‘(𝑐𝑏))) ↔ (abs‘((𝐹𝑐) − (𝐹𝑟))) ≤ (𝑎 · (abs‘(𝑐𝑟)))))
74 fveq2 6229 . . . . . . . . . . . . . 14 (𝑐 = 𝐴 → (𝐹𝑐) = (𝐹𝐴))
7574oveq1d 6705 . . . . . . . . . . . . 13 (𝑐 = 𝐴 → ((𝐹𝑐) − (𝐹𝑟)) = ((𝐹𝐴) − (𝐹𝑟)))
7675fveq2d 6233 . . . . . . . . . . . 12 (𝑐 = 𝐴 → (abs‘((𝐹𝑐) − (𝐹𝑟))) = (abs‘((𝐹𝐴) − (𝐹𝑟))))
77 oveq1 6697 . . . . . . . . . . . . . 14 (𝑐 = 𝐴 → (𝑐𝑟) = (𝐴𝑟))
7877fveq2d 6233 . . . . . . . . . . . . 13 (𝑐 = 𝐴 → (abs‘(𝑐𝑟)) = (abs‘(𝐴𝑟)))
7978oveq2d 6706 . . . . . . . . . . . 12 (𝑐 = 𝐴 → (𝑎 · (abs‘(𝑐𝑟))) = (𝑎 · (abs‘(𝐴𝑟))))
8076, 79breq12d 4698 . . . . . . . . . . 11 (𝑐 = 𝐴 → ((abs‘((𝐹𝑐) − (𝐹𝑟))) ≤ (𝑎 · (abs‘(𝑐𝑟))) ↔ (abs‘((𝐹𝐴) − (𝐹𝑟))) ≤ (𝑎 · (abs‘(𝐴𝑟)))))
8173, 80rspc2v 3353 . . . . . . . . . 10 ((𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ∧ 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹𝑐) − (𝐹𝑏))) ≤ (𝑎 · (abs‘(𝑐𝑏))) → (abs‘((𝐹𝐴) − (𝐹𝑟))) ≤ (𝑎 · (abs‘(𝐴𝑟)))))
8253, 66, 81syl2anc 694 . . . . . . . . 9 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹𝑐) − (𝐹𝑏))) ≤ (𝑎 · (abs‘(𝑐𝑏))) → (abs‘((𝐹𝐴) − (𝐹𝑟))) ≤ (𝑎 · (abs‘(𝐴𝑟)))))
83 simp1l 1105 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → 𝜑)
84 aalioulem3.e . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐴) = 0)
8583, 84syl 17 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (𝐹𝐴) = 0)
86 0cn 10070 . . . . . . . . . . . . 13 0 ∈ ℂ
8785, 86syl6eqel 2738 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (𝐹𝐴) ∈ ℂ)
8837adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ ℝ) → 𝐹:ℂ⟶ℂ)
89883ad2ant1 1102 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → 𝐹:ℂ⟶ℂ)
9089, 43ffvelrnd 6400 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (𝐹𝑟) ∈ ℂ)
9187, 90abssubd 14236 . . . . . . . . . . 11 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (abs‘((𝐹𝐴) − (𝐹𝑟))) = (abs‘((𝐹𝑟) − (𝐹𝐴))))
9285oveq2d 6706 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → ((𝐹𝑟) − (𝐹𝐴)) = ((𝐹𝑟) − 0))
9390subid1d 10419 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → ((𝐹𝑟) − 0) = (𝐹𝑟))
9492, 93eqtrd 2685 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → ((𝐹𝑟) − (𝐹𝐴)) = (𝐹𝑟))
9594fveq2d 6233 . . . . . . . . . . 11 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (abs‘((𝐹𝑟) − (𝐹𝐴))) = (abs‘(𝐹𝑟)))
9691, 95eqtrd 2685 . . . . . . . . . 10 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (abs‘((𝐹𝐴) − (𝐹𝑟))) = (abs‘(𝐹𝑟)))
9796breq1d 4695 . . . . . . . . 9 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → ((abs‘((𝐹𝐴) − (𝐹𝑟))) ≤ (𝑎 · (abs‘(𝐴𝑟))) ↔ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟)))))
9882, 97sylibd 229 . . . . . . . 8 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴𝑟)) ≤ 1) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹𝑐) − (𝐹𝑏))) ≤ (𝑎 · (abs‘(𝑐𝑏))) → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟)))))
99983exp 1283 . . . . . . 7 ((𝜑𝑎 ∈ ℝ) → (𝑟 ∈ ℝ → ((abs‘(𝐴𝑟)) ≤ 1 → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹𝑐) − (𝐹𝑏))) ≤ (𝑎 · (abs‘(𝑐𝑏))) → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟)))))))
10099com34 91 . . . . . 6 ((𝜑𝑎 ∈ ℝ) → (𝑟 ∈ ℝ → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹𝑐) − (𝐹𝑏))) ≤ (𝑎 · (abs‘(𝑐𝑏))) → ((abs‘(𝐴𝑟)) ≤ 1 → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟)))))))
101100com23 86 . . . . 5 ((𝜑𝑎 ∈ ℝ) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹𝑐) − (𝐹𝑏))) ≤ (𝑎 · (abs‘(𝑐𝑏))) → (𝑟 ∈ ℝ → ((abs‘(𝐴𝑟)) ≤ 1 → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟)))))))
102101ralrimdv 2997 . . . 4 ((𝜑𝑎 ∈ ℝ) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹𝑐) − (𝐹𝑏))) ≤ (𝑎 · (abs‘(𝑐𝑏))) → ∀𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))))
103102reximdva 3046 . . 3 (𝜑 → (∃𝑎 ∈ ℝ ∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹𝑐) − (𝐹𝑏))) ≤ (𝑎 · (abs‘(𝑐𝑏))) → ∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))))
10441, 103mpd 15 . 2 (𝜑 → ∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟)))))
105 1rp 11874 . . . . . 6 1 ∈ ℝ+
106105a1i 11 . . . . 5 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 = 0) → 1 ∈ ℝ+)
107 recn 10064 . . . . . . . 8 (𝑎 ∈ ℝ → 𝑎 ∈ ℂ)
108107adantl 481 . . . . . . 7 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℂ)
109 df-ne 2824 . . . . . . . 8 (𝑎 ≠ 0 ↔ ¬ 𝑎 = 0)
110109biimpri 218 . . . . . . 7 𝑎 = 0 → 𝑎 ≠ 0)
111 absrpcl 14072 . . . . . . 7 ((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) → (abs‘𝑎) ∈ ℝ+)
112108, 110, 111syl2an 493 . . . . . 6 (((𝜑𝑎 ∈ ℝ) ∧ ¬ 𝑎 = 0) → (abs‘𝑎) ∈ ℝ+)
113112rpreccld 11920 . . . . 5 (((𝜑𝑎 ∈ ℝ) ∧ ¬ 𝑎 = 0) → (1 / (abs‘𝑎)) ∈ ℝ+)
114106, 113ifclda 4153 . . . 4 ((𝜑𝑎 ∈ ℝ) → if(𝑎 = 0, 1, (1 / (abs‘𝑎))) ∈ ℝ+)
115 eqid 2651 . . . . . . . . 9 if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = if(𝑎 = 0, 1, (1 / (abs‘𝑎)))
116 eqif 4159 . . . . . . . . 9 (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‘𝑎)))))
117115, 116mpbi 220 . . . . . . . 8 ((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) ∨ (¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎))))
118 simplrr 818 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))
119 oveq1 6697 . . . . . . . . . . . . . . . . . 18 (𝑎 = 0 → (𝑎 · (abs‘(𝐴𝑟))) = (0 · (abs‘(𝐴𝑟))))
120119adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (𝑎 · (abs‘(𝐴𝑟))) = (0 · (abs‘(𝐴𝑟))))
1211ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → 𝐴 ∈ ℝ)
122 simprl 809 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → 𝑟 ∈ ℝ)
123121, 122resubcld 10496 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (𝐴𝑟) ∈ ℝ)
124123recnd 10106 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (𝐴𝑟) ∈ ℂ)
125124abscld 14219 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (abs‘(𝐴𝑟)) ∈ ℝ)
126125recnd 10106 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (abs‘(𝐴𝑟)) ∈ ℂ)
127126adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐴𝑟)) ∈ ℂ)
128127mul02d 10272 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (0 · (abs‘(𝐴𝑟))) = 0)
129120, 128eqtrd 2685 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (𝑎 · (abs‘(𝐴𝑟))) = 0)
130118, 129breqtrd 4711 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹𝑟)) ≤ 0)
13137ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → 𝐹:ℂ⟶ℂ)
132122recnd 10106 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → 𝑟 ∈ ℂ)
133131, 132ffvelrnd 6400 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (𝐹𝑟) ∈ ℂ)
134133adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (𝐹𝑟) ∈ ℂ)
135134absge0d 14227 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → 0 ≤ (abs‘(𝐹𝑟)))
136133abscld 14219 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (abs‘(𝐹𝑟)) ∈ ℝ)
137136adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹𝑟)) ∈ ℝ)
138 0re 10078 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
139 letri3 10161 . . . . . . . . . . . . . . . 16 (((abs‘(𝐹𝑟)) ∈ ℝ ∧ 0 ∈ ℝ) → ((abs‘(𝐹𝑟)) = 0 ↔ ((abs‘(𝐹𝑟)) ≤ 0 ∧ 0 ≤ (abs‘(𝐹𝑟)))))
140137, 138, 139sylancl 695 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → ((abs‘(𝐹𝑟)) = 0 ↔ ((abs‘(𝐹𝑟)) ≤ 0 ∧ 0 ≤ (abs‘(𝐹𝑟)))))
141130, 135, 140mpbir2and 977 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹𝑟)) = 0)
142141oveq2d 6706 . . . . . . . . . . . . 13 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹𝑟))) = (1 · 0))
143 ax-1cn 10032 . . . . . . . . . . . . . 14 1 ∈ ℂ
144143mul01i 10264 . . . . . . . . . . . . 13 (1 · 0) = 0
145142, 144syl6eq 2701 . . . . . . . . . . . 12 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹𝑟))) = 0)
146124adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (𝐴𝑟) ∈ ℂ)
147146absge0d 14227 . . . . . . . . . . . 12 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → 0 ≤ (abs‘(𝐴𝑟)))
148145, 147eqbrtrd 4707 . . . . . . . . . . 11 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))
149 oveq1 6697 . . . . . . . . . . . 12 (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) = (1 · (abs‘(𝐹𝑟))))
150149breq1d 4695 . . . . . . . . . . 11 (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → ((if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)) ↔ (1 · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
151148, 150syl5ibrcom 237 . . . . . . . . . 10 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 = 0) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
152151expimpd 628 . . . . . . . . 9 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → ((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
153136adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹𝑟)) ∈ ℝ)
154153recnd 10106 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹𝑟)) ∈ ℂ)
155 simpllr 815 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → 𝑎 ∈ ℝ)
156155recnd 10106 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → 𝑎 ∈ ℂ)
157156, 111sylancom 702 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘𝑎) ∈ ℝ+)
158157rpcnne0d 11919 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘𝑎) ∈ ℂ ∧ (abs‘𝑎) ≠ 0))
159 divrec2 10740 . . . . . . . . . . . . . . 15 (((abs‘(𝐹𝑟)) ∈ ℂ ∧ (abs‘𝑎) ∈ ℂ ∧ (abs‘𝑎) ≠ 0) → ((abs‘(𝐹𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹𝑟))))
1601593expb 1285 . . . . . . . . . . . . . 14 (((abs‘(𝐹𝑟)) ∈ ℂ ∧ ((abs‘𝑎) ∈ ℂ ∧ (abs‘𝑎) ≠ 0)) → ((abs‘(𝐹𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹𝑟))))
161154, 158, 160syl2anc 694 . . . . . . . . . . . . 13 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘(𝐹𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹𝑟))))
162 simplr 807 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → 𝑎 ∈ ℝ)
163162, 125remulcld 10108 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (𝑎 · (abs‘(𝐴𝑟))) ∈ ℝ)
164162recnd 10106 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → 𝑎 ∈ ℂ)
165164abscld 14219 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (abs‘𝑎) ∈ ℝ)
166165, 125remulcld 10108 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → ((abs‘𝑎) · (abs‘(𝐴𝑟))) ∈ ℝ)
167 simprr 811 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))
168124absge0d 14227 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → 0 ≤ (abs‘(𝐴𝑟)))
169 leabs 14083 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ℝ → 𝑎 ≤ (abs‘𝑎))
170169ad2antlr 763 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → 𝑎 ≤ (abs‘𝑎))
171162, 165, 125, 168, 170lemul1ad 11001 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (𝑎 · (abs‘(𝐴𝑟))) ≤ ((abs‘𝑎) · (abs‘(𝐴𝑟))))
172136, 163, 166, 167, 171letrd 10232 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (abs‘(𝐹𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴𝑟))))
173172adantr 480 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴𝑟))))
174125adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐴𝑟)) ∈ ℝ)
175153, 174, 157ledivmuld 11963 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → (((abs‘(𝐹𝑟)) / (abs‘𝑎)) ≤ (abs‘(𝐴𝑟)) ↔ (abs‘(𝐹𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴𝑟)))))
176173, 175mpbird 247 . . . . . . . . . . . . 13 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘(𝐹𝑟)) / (abs‘𝑎)) ≤ (abs‘(𝐴𝑟)))
177161, 176eqbrtrrd 4709 . . . . . . . . . . . 12 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ 𝑎 ≠ 0) → ((1 / (abs‘𝑎)) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))
178109, 177sylan2br 492 . . . . . . . . . . 11 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ ¬ 𝑎 = 0) → ((1 / (abs‘𝑎)) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))
179 oveq1 6697 . . . . . . . . . . . 12 (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) = ((1 / (abs‘𝑎)) · (abs‘(𝐹𝑟))))
180179breq1d 4695 . . . . . . . . . . 11 (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → ((if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)) ↔ ((1 / (abs‘𝑎)) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
181178, 180syl5ibrcom 237 . . . . . . . . . 10 ((((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) ∧ ¬ 𝑎 = 0) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
182181expimpd 628 . . . . . . . . 9 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → ((¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
183152, 182jaod 394 . . . . . . . 8 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) ∨ (¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
184117, 183mpi 20 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))
185184expr 642 . . . . . 6 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ) → ((abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
186185imim2d 57 . . . . 5 (((𝜑𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ) → (((abs‘(𝐴𝑟)) ≤ 1 → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟)))) → ((abs‘(𝐴𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))))
187186ralimdva 2991 . . . 4 ((𝜑𝑎 ∈ ℝ) → (∀𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟)))) → ∀𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))))
188 oveq1 6697 . . . . . . . 8 (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (𝑥 · (abs‘(𝐹𝑟))) = (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))))
189188breq1d 4695 . . . . . . 7 (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → ((𝑥 · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)) ↔ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
190189imbi2d 329 . . . . . 6 (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (((abs‘(𝐴𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))) ↔ ((abs‘(𝐴𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))))
191190ralbidv 3015 . . . . 5 (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (∀𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))) ↔ ∀𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))))
192191rspcev 3340 . . . 4 ((if(𝑎 = 0, 1, (1 / (abs‘𝑎))) ∈ ℝ+ ∧ ∀𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))) → ∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
193114, 187, 192syl6an 567 . . 3 ((𝜑𝑎 ∈ ℝ) → (∀𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟)))) → ∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))))
194193rexlimdva 3060 . 2 (𝜑 → (∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (abs‘(𝐹𝑟)) ≤ (𝑎 · (abs‘(𝐴𝑟)))) → ∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟)))))
195104, 194mpd 15 1 (𝜑 → ∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((abs‘(𝐴𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹𝑟))) ≤ (abs‘(𝐴𝑟))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942   ⊆ wss 3607  ifcif 4119  {cpr 4212  ∩ cint 4507   class class class wbr 4685  dom cdm 5143  ran crn 5144   ↾ cres 5145   “ cima 5146   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   ≤ cle 10113   − cmin 10304   / cdiv 10722  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ℝ+crp 11870  [,]cicc 12216  abscabs 14018  Cnccpn 23674  Polycply 23985  degcdgr 23988 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-grp 17472  df-minusg 17473  df-mulg 17588  df-subg 17638  df-cntz 17796  df-cmn 18241  df-mgp 18536  df-ur 18548  df-ring 18595  df-cring 18596  df-subrg 18826  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-0p 23482  df-limc 23675  df-dv 23676  df-dvn 23677  df-cpn 23678  df-ply 23989  df-coe 23991  df-dgr 23992 This theorem is referenced by:  aalioulem4  24135
 Copyright terms: Public domain W3C validator