| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aalioulem2.d | . . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 2 |  | 1re 11262 | . . . . 5
⊢ 1 ∈
ℝ | 
| 3 |  | resubcl 11574 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐴 −
1) ∈ ℝ) | 
| 4 | 1, 2, 3 | sylancl 586 | . . . 4
⊢ (𝜑 → (𝐴 − 1) ∈ ℝ) | 
| 5 |  | peano2re 11435 | . . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) | 
| 6 | 1, 5 | syl 17 | . . . 4
⊢ (𝜑 → (𝐴 + 1) ∈ ℝ) | 
| 7 |  | reelprrecn 11248 | . . . . 5
⊢ ℝ
∈ {ℝ, ℂ} | 
| 8 |  | ssid 4005 | . . . . . . . . 9
⊢ ℂ
⊆ ℂ | 
| 9 |  | fncpn 25970 | . . . . . . . . 9
⊢ (ℂ
⊆ ℂ → (𝓑C𝑛‘ℂ) Fn
ℕ0) | 
| 10 | 8, 9 | ax-mp 5 | . . . . . . . 8
⊢
(𝓑C𝑛‘ℂ) Fn
ℕ0 | 
| 11 |  | 1nn0 12544 | . . . . . . . 8
⊢ 1 ∈
ℕ0 | 
| 12 |  | fnfvelrn 7099 | . . . . . . . 8
⊢
(((𝓑C𝑛‘ℂ) Fn ℕ0
∧ 1 ∈ ℕ0) →
((𝓑C𝑛‘ℂ)‘1) ∈ ran
(𝓑C𝑛‘ℂ)) | 
| 13 | 10, 11, 12 | mp2an 692 | . . . . . . 7
⊢
((𝓑C𝑛‘ℂ)‘1) ∈ ran
(𝓑C𝑛‘ℂ) | 
| 14 |  | intss1 4962 | . . . . . . 7
⊢
(((𝓑C𝑛‘ℂ)‘1) ∈ ran
(𝓑C𝑛‘ℂ) → ∩ ran (𝓑C𝑛‘ℂ)
⊆
((𝓑C𝑛‘ℂ)‘1)) | 
| 15 | 13, 14 | ax-mp 5 | . . . . . 6
⊢ ∩ ran (𝓑C𝑛‘ℂ)
⊆
((𝓑C𝑛‘ℂ)‘1) | 
| 16 |  | aalioulem2.b | . . . . . . 7
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℤ)) | 
| 17 |  | plycpn 26332 | . . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℤ)
→ 𝐹 ∈ ∩ ran
(𝓑C𝑛‘ℂ)) | 
| 18 | 16, 17 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ ∩ ran
(𝓑C𝑛‘ℂ)) | 
| 19 | 15, 18 | sselid 3980 | . . . . 5
⊢ (𝜑 → 𝐹 ∈
((𝓑C𝑛‘ℂ)‘1)) | 
| 20 |  | cpnres 25974 | . . . . 5
⊢ ((ℝ
∈ {ℝ, ℂ} ∧ 𝐹 ∈
((𝓑C𝑛‘ℂ)‘1)) → (𝐹 ↾ ℝ) ∈
((𝓑C𝑛‘ℝ)‘1)) | 
| 21 | 7, 19, 20 | sylancr 587 | . . . 4
⊢ (𝜑 → (𝐹 ↾ ℝ) ∈
((𝓑C𝑛‘ℝ)‘1)) | 
| 22 |  | df-ima 5697 | . . . . 5
⊢ (𝐹 “ ℝ) = ran (𝐹 ↾
ℝ) | 
| 23 |  | zssre 12622 | . . . . . . . . 9
⊢ ℤ
⊆ ℝ | 
| 24 |  | ax-resscn 11213 | . . . . . . . . 9
⊢ ℝ
⊆ ℂ | 
| 25 |  | plyss 26239 | . . . . . . . . 9
⊢ ((ℤ
⊆ ℝ ∧ ℝ ⊆ ℂ) → (Poly‘ℤ)
⊆ (Poly‘ℝ)) | 
| 26 | 23, 24, 25 | mp2an 692 | . . . . . . . 8
⊢
(Poly‘ℤ) ⊆ (Poly‘ℝ) | 
| 27 | 26, 16 | sselid 3980 | . . . . . . 7
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℝ)) | 
| 28 |  | plyreres 26325 | . . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹 ↾
ℝ):ℝ⟶ℝ) | 
| 29 | 27, 28 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝐹 ↾
ℝ):ℝ⟶ℝ) | 
| 30 | 29 | frnd 6743 | . . . . 5
⊢ (𝜑 → ran (𝐹 ↾ ℝ) ⊆
ℝ) | 
| 31 | 22, 30 | eqsstrid 4021 | . . . 4
⊢ (𝜑 → (𝐹 “ ℝ) ⊆
ℝ) | 
| 32 |  | iccssre 13470 | . . . . . . 7
⊢ (((𝐴 − 1) ∈ ℝ ∧
(𝐴 + 1) ∈ ℝ)
→ ((𝐴 −
1)[,](𝐴 + 1)) ⊆
ℝ) | 
| 33 | 4, 6, 32 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ ℝ) | 
| 34 | 33, 24 | sstrdi 3995 | . . . . 5
⊢ (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ ℂ) | 
| 35 |  | plyf 26238 | . . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℤ)
→ 𝐹:ℂ⟶ℂ) | 
| 36 | 16, 35 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) | 
| 37 | 36 | fdmd 6745 | . . . . 5
⊢ (𝜑 → dom 𝐹 = ℂ) | 
| 38 | 34, 37 | sseqtrrd 4020 | . . . 4
⊢ (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ dom 𝐹) | 
| 39 | 4, 6, 21, 31, 38 | c1lip3 26039 | . . 3
⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏)))) | 
| 40 |  | simp2 1137 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝑟 ∈ ℝ) | 
| 41 | 40 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝑟 ∈ ℂ) | 
| 42 | 1 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐴 ∈ ℝ) | 
| 43 | 42 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐴 ∈ ℝ) | 
| 44 | 43 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐴 ∈ ℂ) | 
| 45 | 41, 44 | abssubd 15493 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘(𝑟 − 𝐴)) = (abs‘(𝐴 − 𝑟))) | 
| 46 |  | simp3 1138 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘(𝐴 − 𝑟)) ≤ 1) | 
| 47 | 45, 46 | eqbrtrd 5164 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘(𝑟 − 𝐴)) ≤ 1) | 
| 48 |  | 1red 11263 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 1 ∈
ℝ) | 
| 49 |  | elicc4abs 15359 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑟 ∈
ℝ) → (𝑟 ∈
((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝑟 − 𝐴)) ≤ 1)) | 
| 50 | 43, 48, 40, 49 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝑟 − 𝐴)) ≤ 1)) | 
| 51 | 47, 50 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1))) | 
| 52 | 1 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 53 | 52 | subidd 11609 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 − 𝐴) = 0) | 
| 54 | 53 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘(𝐴 − 𝐴)) = (abs‘0)) | 
| 55 |  | abs0 15325 | . . . . . . . . . . . . . . 15
⊢
(abs‘0) = 0 | 
| 56 |  | 0le1 11787 | . . . . . . . . . . . . . . 15
⊢ 0 ≤
1 | 
| 57 | 55, 56 | eqbrtri 5163 | . . . . . . . . . . . . . 14
⊢
(abs‘0) ≤ 1 | 
| 58 | 54, 57 | eqbrtrdi 5181 | . . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘(𝐴 − 𝐴)) ≤ 1) | 
| 59 |  | 1red 11263 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) | 
| 60 |  | elicc4abs 15359 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝐴 ∈
ℝ) → (𝐴 ∈
((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝐴 − 𝐴)) ≤ 1)) | 
| 61 | 1, 59, 1, 60 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝐴 − 𝐴)) ≤ 1)) | 
| 62 | 58, 61 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) | 
| 63 | 62 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) | 
| 64 | 63 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) | 
| 65 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑟 → (𝐹‘𝑏) = (𝐹‘𝑟)) | 
| 66 | 65 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑏 = 𝑟 → ((𝐹‘𝑐) − (𝐹‘𝑏)) = ((𝐹‘𝑐) − (𝐹‘𝑟))) | 
| 67 | 66 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑟 → (abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) = (abs‘((𝐹‘𝑐) − (𝐹‘𝑟)))) | 
| 68 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑟 → (𝑐 − 𝑏) = (𝑐 − 𝑟)) | 
| 69 | 68 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝑏 = 𝑟 → (abs‘(𝑐 − 𝑏)) = (abs‘(𝑐 − 𝑟))) | 
| 70 | 69 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑟 → (𝑎 · (abs‘(𝑐 − 𝑏))) = (𝑎 · (abs‘(𝑐 − 𝑟)))) | 
| 71 | 67, 70 | breq12d 5155 | . . . . . . . . . . 11
⊢ (𝑏 = 𝑟 → ((abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) ↔ (abs‘((𝐹‘𝑐) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝑐 − 𝑟))))) | 
| 72 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑐 = 𝐴 → (𝐹‘𝑐) = (𝐹‘𝐴)) | 
| 73 | 72 | fvoveq1d 7454 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝐴 → (abs‘((𝐹‘𝑐) − (𝐹‘𝑟))) = (abs‘((𝐹‘𝐴) − (𝐹‘𝑟)))) | 
| 74 |  | fvoveq1 7455 | . . . . . . . . . . . . 13
⊢ (𝑐 = 𝐴 → (abs‘(𝑐 − 𝑟)) = (abs‘(𝐴 − 𝑟))) | 
| 75 | 74 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝐴 → (𝑎 · (abs‘(𝑐 − 𝑟))) = (𝑎 · (abs‘(𝐴 − 𝑟)))) | 
| 76 | 73, 75 | breq12d 5155 | . . . . . . . . . . 11
⊢ (𝑐 = 𝐴 → ((abs‘((𝐹‘𝑐) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝑐 − 𝑟))) ↔ (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) | 
| 77 | 71, 76 | rspc2v 3632 | . . . . . . . . . 10
⊢ ((𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ∧ 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) | 
| 78 | 51, 64, 77 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) | 
| 79 |  | simp1l 1197 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝜑) | 
| 80 |  | aalioulem3.e | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘𝐴) = 0) | 
| 81 | 79, 80 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝐹‘𝐴) = 0) | 
| 82 |  | 0cn 11254 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℂ | 
| 83 | 81, 82 | eqeltrdi 2848 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝐹‘𝐴) ∈ ℂ) | 
| 84 | 36 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐹:ℂ⟶ℂ) | 
| 85 | 84 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐹:ℂ⟶ℂ) | 
| 86 | 85, 41 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝐹‘𝑟) ∈ ℂ) | 
| 87 | 83, 86 | abssubd 15493 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) = (abs‘((𝐹‘𝑟) − (𝐹‘𝐴)))) | 
| 88 | 81 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((𝐹‘𝑟) − (𝐹‘𝐴)) = ((𝐹‘𝑟) − 0)) | 
| 89 | 86 | subid1d 11610 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((𝐹‘𝑟) − 0) = (𝐹‘𝑟)) | 
| 90 | 88, 89 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((𝐹‘𝑟) − (𝐹‘𝐴)) = (𝐹‘𝑟)) | 
| 91 | 90 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘((𝐹‘𝑟) − (𝐹‘𝐴))) = (abs‘(𝐹‘𝑟))) | 
| 92 | 87, 91 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) = (abs‘(𝐹‘𝑟))) | 
| 93 | 92 | breq1d 5152 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))) ↔ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) | 
| 94 | 78, 93 | sylibd 239 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) | 
| 95 | 94 | 3exp 1119 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑟 ∈ ℝ → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))))) | 
| 96 | 95 | com34 91 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑟 ∈ ℝ → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))))) | 
| 97 | 96 | com23 86 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (𝑟 ∈ ℝ → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))))) | 
| 98 | 97 | ralrimdv 3151 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))))) | 
| 99 | 98 | reximdva 3167 | . . 3
⊢ (𝜑 → (∃𝑎 ∈ ℝ ∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → ∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))))) | 
| 100 | 39, 99 | mpd 15 | . 2
⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) | 
| 101 |  | 1rp 13039 | . . . . . 6
⊢ 1 ∈
ℝ+ | 
| 102 | 101 | a1i 11 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 = 0) → 1 ∈
ℝ+) | 
| 103 |  | recn 11246 | . . . . . . . 8
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℂ) | 
| 104 | 103 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℂ) | 
| 105 |  | neqne 2947 | . . . . . . 7
⊢ (¬
𝑎 = 0 → 𝑎 ≠ 0) | 
| 106 |  | absrpcl 15328 | . . . . . . 7
⊢ ((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) → (abs‘𝑎) ∈
ℝ+) | 
| 107 | 104, 105,
106 | syl2an 596 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 𝑎 = 0) → (abs‘𝑎) ∈
ℝ+) | 
| 108 | 107 | rpreccld 13088 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 𝑎 = 0) → (1 /
(abs‘𝑎)) ∈
ℝ+) | 
| 109 | 102, 108 | ifclda 4560 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → if(𝑎 = 0, 1, (1 / (abs‘𝑎))) ∈
ℝ+) | 
| 110 |  | eqid 2736 | . . . . . . . . 9
⊢ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) | 
| 111 |  | eqif 4566 | . . . . . . . . 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‘𝑎))))) | 
| 112 | 110, 111 | mpbi 230 | . . . . . . . 8
⊢ ((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) ∨ (¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)))) | 
| 113 |  | simplrr 777 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) | 
| 114 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 0 → (𝑎 · (abs‘(𝐴 − 𝑟))) = (0 · (abs‘(𝐴 − 𝑟)))) | 
| 115 | 114 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝑎 · (abs‘(𝐴 − 𝑟))) = (0 · (abs‘(𝐴 − 𝑟)))) | 
| 116 | 1 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝐴 ∈ ℝ) | 
| 117 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑟 ∈ ℝ) | 
| 118 | 116, 117 | resubcld 11692 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝐴 − 𝑟) ∈ ℝ) | 
| 119 | 118 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝐴 − 𝑟) ∈ ℂ) | 
| 120 | 119 | abscld 15476 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐴 − 𝑟)) ∈ ℝ) | 
| 121 | 120 | recnd 11290 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐴 − 𝑟)) ∈ ℂ) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐴 − 𝑟)) ∈ ℂ) | 
| 123 | 122 | mul02d 11460 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (0 · (abs‘(𝐴 − 𝑟))) = 0) | 
| 124 | 115, 123 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝑎 · (abs‘(𝐴 − 𝑟))) = 0) | 
| 125 | 113, 124 | breqtrd 5168 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) ≤ 0) | 
| 126 | 36 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝐹:ℂ⟶ℂ) | 
| 127 | 117 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑟 ∈ ℂ) | 
| 128 | 126, 127 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝐹‘𝑟) ∈ ℂ) | 
| 129 | 128 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝐹‘𝑟) ∈ ℂ) | 
| 130 | 129 | absge0d 15484 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → 0 ≤ (abs‘(𝐹‘𝑟))) | 
| 131 | 128 | abscld 15476 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐹‘𝑟)) ∈ ℝ) | 
| 132 | 131 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) ∈ ℝ) | 
| 133 |  | 0re 11264 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ | 
| 134 |  | letri3 11347 | . . . . . . . . . . . . . . . 16
⊢
(((abs‘(𝐹‘𝑟)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((abs‘(𝐹‘𝑟)) = 0 ↔ ((abs‘(𝐹‘𝑟)) ≤ 0 ∧ 0 ≤ (abs‘(𝐹‘𝑟))))) | 
| 135 | 132, 133,
134 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → ((abs‘(𝐹‘𝑟)) = 0 ↔ ((abs‘(𝐹‘𝑟)) ≤ 0 ∧ 0 ≤ (abs‘(𝐹‘𝑟))))) | 
| 136 | 125, 130,
135 | mpbir2and 713 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) = 0) | 
| 137 | 136 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹‘𝑟))) = (1 · 0)) | 
| 138 |  | ax-1cn 11214 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ | 
| 139 | 138 | mul01i 11452 | . . . . . . . . . . . . 13
⊢ (1
· 0) = 0 | 
| 140 | 137, 139 | eqtrdi 2792 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹‘𝑟))) = 0) | 
| 141 | 119 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝐴 − 𝑟) ∈ ℂ) | 
| 142 | 141 | absge0d 15484 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → 0 ≤ (abs‘(𝐴 − 𝑟))) | 
| 143 | 140, 142 | eqbrtrd 5164 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) | 
| 144 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) = (1 · (abs‘(𝐹‘𝑟)))) | 
| 145 | 144 | breq1d 5152 | . . . . . . . . . . 11
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → ((if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)) ↔ (1 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) | 
| 146 | 143, 145 | syl5ibrcom 247 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) | 
| 147 | 146 | expimpd 453 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → ((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) | 
| 148 |  | df-ne 2940 | . . . . . . . . . . . 12
⊢ (𝑎 ≠ 0 ↔ ¬ 𝑎 = 0) | 
| 149 | 131 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹‘𝑟)) ∈ ℝ) | 
| 150 | 149 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹‘𝑟)) ∈ ℂ) | 
| 151 |  | simpllr 775 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → 𝑎 ∈ ℝ) | 
| 152 | 151 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → 𝑎 ∈ ℂ) | 
| 153 | 152, 106 | sylancom 588 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘𝑎) ∈
ℝ+) | 
| 154 | 153 | rpcnne0d 13087 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘𝑎) ∈ ℂ ∧
(abs‘𝑎) ≠
0)) | 
| 155 |  | divrec2 11940 | . . . . . . . . . . . . . . 15
⊢
(((abs‘(𝐹‘𝑟)) ∈ ℂ ∧ (abs‘𝑎) ∈ ℂ ∧
(abs‘𝑎) ≠ 0)
→ ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) | 
| 156 | 155 | 3expb 1120 | . . . . . . . . . . . . . 14
⊢
(((abs‘(𝐹‘𝑟)) ∈ ℂ ∧ ((abs‘𝑎) ∈ ℂ ∧
(abs‘𝑎) ≠ 0))
→ ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) | 
| 157 | 150, 154,
156 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) | 
| 158 |  | simplr 768 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑎 ∈ ℝ) | 
| 159 | 158, 120 | remulcld 11292 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝑎 · (abs‘(𝐴 − 𝑟))) ∈ ℝ) | 
| 160 | 158 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑎 ∈ ℂ) | 
| 161 | 160 | abscld 15476 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘𝑎) ∈ ℝ) | 
| 162 | 161, 120 | remulcld 11292 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → ((abs‘𝑎) · (abs‘(𝐴 − 𝑟))) ∈ ℝ) | 
| 163 |  | simprr 772 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) | 
| 164 | 119 | absge0d 15484 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 0 ≤ (abs‘(𝐴 − 𝑟))) | 
| 165 |  | leabs 15339 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ ℝ → 𝑎 ≤ (abs‘𝑎)) | 
| 166 | 165 | ad2antlr 727 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑎 ≤ (abs‘𝑎)) | 
| 167 | 158, 161,
120, 164, 166 | lemul1ad 12208 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝑎 · (abs‘(𝐴 − 𝑟))) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟)))) | 
| 168 | 131, 159,
162, 163, 167 | letrd 11419 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐹‘𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟)))) | 
| 169 | 168 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹‘𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟)))) | 
| 170 | 120 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐴 − 𝑟)) ∈ ℝ) | 
| 171 | 149, 170,
153 | ledivmuld 13131 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) ≤ (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐹‘𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟))))) | 
| 172 | 169, 171 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) ≤ (abs‘(𝐴 − 𝑟))) | 
| 173 | 157, 172 | eqbrtrrd 5166 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) | 
| 174 | 148, 173 | sylan2br 595 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ ¬ 𝑎 = 0) → ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) | 
| 175 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) | 
| 176 | 175 | breq1d 5152 | . . . . . . . . . . 11
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → ((if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)) ↔ ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) | 
| 177 | 174, 176 | syl5ibrcom 247 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ ¬ 𝑎 = 0) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) | 
| 178 | 177 | expimpd 453 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → ((¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) | 
| 179 | 147, 178 | jaod 859 | . . . . . . . 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‘(𝐴 − 𝑟)))) | 
| 180 | 112, 179 | mpi 20 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) | 
| 181 | 180 | expr 456 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ) → ((abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) | 
| 182 | 181 | imim2d 57 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ) → (((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) | 
| 183 | 182 | ralimdva 3166 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 →
(abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) | 
| 184 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (𝑥 · (abs‘(𝐹‘𝑟))) = (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟)))) | 
| 185 | 184 | breq1d 5152 | . . . . . . 7
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → ((𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)) ↔ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) | 
| 186 | 185 | imbi2d 340 | . . . . . 6
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (((abs‘(𝐴 − 𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) ↔ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) | 
| 187 | 186 | ralbidv 3177 | . . . . 5
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) ↔ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) | 
| 188 | 187 | rspcev 3621 | . . . 4
⊢
((if(𝑎 = 0, 1, (1 /
(abs‘𝑎))) ∈
ℝ+ ∧ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) | 
| 189 | 109, 183,
188 | syl6an 684 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 →
(abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) | 
| 190 | 189 | rexlimdva 3154 | . 2
⊢ (𝜑 → (∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) | 
| 191 | 100, 190 | mpd 15 | 1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |