| Step | Hyp | Ref
| Expression |
| 1 | | simplr 769 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → 𝑑 ∈ ℝ+) |
| 2 | | simpr 484 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) |
| 3 | | rpxr 13044 |
. . . . . . . 8
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ∈
ℝ*) |
| 4 | 3 | xrleidd 13194 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ≤ 𝑑) |
| 5 | 4 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → 𝑑 ≤ 𝑑) |
| 6 | | id 22 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ∈
ℝ+) |
| 7 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → 𝑓 = 𝑑) |
| 8 | 7 | breq2d 5155 |
. . . . . . . 8
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (𝑑 ≤ 𝑓 ↔ 𝑑 ≤ 𝑑)) |
| 9 | 7 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (𝐹‘𝑓) = (𝐹‘𝑑)) |
| 10 | 7 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (𝑓↑𝐷) = (𝑑↑𝐷)) |
| 11 | 9, 10 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((𝐹‘𝑓) / (𝑓↑𝐷)) = ((𝐹‘𝑑) / (𝑑↑𝐷))) |
| 12 | 11 | fvoveq1d 7453 |
. . . . . . . . 9
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) = (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵))) |
| 13 | 12 | breq1d 5153 |
. . . . . . . 8
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵 ↔ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵)) |
| 14 | 8, 13 | imbi12d 344 |
. . . . . . 7
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵) ↔ (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵))) |
| 15 | 6, 14 | rspcdv 3614 |
. . . . . 6
⊢ (𝑑 ∈ ℝ+
→ (∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵) → (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵))) |
| 16 | 1, 2, 5, 15 | syl3c 66 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) |
| 17 | | signsply0.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℝ)) |
| 18 | 17 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐹 ∈
(Poly‘ℝ)) |
| 19 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ+) |
| 20 | 19 | rpred 13077 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ) |
| 21 | 18, 20 | plyrecld 34564 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐹‘𝑑) ∈
ℝ) |
| 22 | | signsply0.d |
. . . . . . . . . . . . 13
⊢ 𝐷 = (deg‘𝐹) |
| 23 | | dgrcl 26272 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (deg‘𝐹) ∈
ℕ0) |
| 24 | 17, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
| 25 | 22, 24 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
| 26 | 25 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℕ0) |
| 27 | 20, 26 | reexpcld 14203 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ) |
| 28 | 19 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℂ) |
| 29 | 19 | rpne0d 13082 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ≠
0) |
| 30 | 25 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈ ℤ) |
| 31 | 30 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℤ) |
| 32 | 28, 29, 31 | expne0d 14192 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ≠ 0) |
| 33 | 21, 27, 32 | redivcld 12095 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) / (𝑑↑𝐷)) ∈ ℝ) |
| 34 | | signsply0.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (𝐶‘𝐷) |
| 35 | | 0re 11263 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
| 36 | | signsply0.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = (coeff‘𝐹) |
| 37 | 36 | coef2 26270 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 0 ∈ ℝ) → 𝐶:ℕ0⟶ℝ) |
| 38 | 35, 37 | mpan2 691 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐶:ℕ0⟶ℝ) |
| 39 | 38 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝐷 ∈
ℕ0) → (𝐶‘𝐷) ∈ ℝ) |
| 40 | 34, 39 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝐷 ∈
ℕ0) → 𝐵 ∈ ℝ) |
| 41 | 17, 25, 40 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 42 | 41 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
| 43 | 42 | renegcld 11690 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ -𝐵 ∈
ℝ) |
| 44 | 33, 42, 43 | absdifltd 15472 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵 ↔ ((𝐵 − -𝐵) < ((𝐹‘𝑑) / (𝑑↑𝐷)) ∧ ((𝐹‘𝑑) / (𝑑↑𝐷)) < (𝐵 + -𝐵)))) |
| 45 | 44 | simplbda 499 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → ((𝐹‘𝑑) / (𝑑↑𝐷)) < (𝐵 + -𝐵)) |
| 46 | 41 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 47 | 46 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
| 48 | 47 | negidd 11610 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐵 + -𝐵) = 0) |
| 49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → (𝐵 + -𝐵) = 0) |
| 50 | 45, 49 | breqtrd 5169 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → ((𝐹‘𝑑) / (𝑑↑𝐷)) < 0) |
| 51 | 19, 31 | rpexpcld 14286 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ+) |
| 52 | 21, 51 | ge0divd 13115 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (0 ≤ (𝐹‘𝑑) ↔ 0 ≤ ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
| 53 | 52 | notbid 318 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (¬ 0 ≤ (𝐹‘𝑑) ↔ ¬ 0 ≤ ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
| 54 | | 0red 11264 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 0 ∈ ℝ) |
| 55 | 21, 54 | ltnled 11408 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) < 0 ↔ ¬ 0 ≤
(𝐹‘𝑑))) |
| 56 | 33, 54 | ltnled 11408 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (((𝐹‘𝑑) / (𝑑↑𝐷)) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
| 57 | 53, 55, 56 | 3bitr4d 311 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) < 0 ↔ ((𝐹‘𝑑) / (𝑑↑𝐷)) < 0)) |
| 58 | 57 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → ((𝐹‘𝑑) < 0 ↔ ((𝐹‘𝑑) / (𝑑↑𝐷)) < 0)) |
| 59 | 50, 58 | mpbird 257 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → (𝐹‘𝑑) < 0) |
| 60 | 16, 59 | syldan 591 |
. . . 4
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → (𝐹‘𝑑) < 0) |
| 61 | | 0red 11264 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 ∈
ℝ) |
| 62 | | simplr 769 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝑑 ∈
ℝ+) |
| 63 | 62 | rpred 13077 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝑑 ∈
ℝ) |
| 64 | 62 | rpgt0d 13080 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 < 𝑑) |
| 65 | | iccssre 13469 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝑑
∈ ℝ) → (0[,]𝑑) ⊆ ℝ) |
| 66 | 35, 63, 65 | sylancr 587 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (0[,]𝑑) ⊆
ℝ) |
| 67 | | ax-resscn 11212 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
| 68 | 66, 67 | sstrdi 3996 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (0[,]𝑑) ⊆
ℂ) |
| 69 | | plycn 26300 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐹 ∈
(ℂ–cn→ℂ)) |
| 70 | 17, 69 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) |
| 71 | 70 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝐹 ∈ (ℂ–cn→ℂ)) |
| 72 | 17 | ad4antr 732 |
. . . . . . 7
⊢
(((((𝜑 ∧ -𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ (𝐹‘𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝐹 ∈
(Poly‘ℝ)) |
| 73 | 66 | sselda 3983 |
. . . . . . 7
⊢
(((((𝜑 ∧ -𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ (𝐹‘𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝑥 ∈ ℝ) |
| 74 | 72, 73 | plyrecld 34564 |
. . . . . 6
⊢
(((((𝜑 ∧ -𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ (𝐹‘𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → (𝐹‘𝑥) ∈ ℝ) |
| 75 | | simpr 484 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (𝐹‘𝑑) < 0) |
| 76 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝜑) |
| 77 | 76, 41 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝐵 ∈
ℝ) |
| 78 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) → -𝐵 ∈
ℝ+) |
| 79 | 78 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → -𝐵 ∈
ℝ+) |
| 80 | | negelrp 13068 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (-𝐵 ∈ ℝ+
↔ 𝐵 <
0)) |
| 81 | 80 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ -𝐵 ∈ ℝ+)
→ 𝐵 <
0) |
| 82 | 77, 79, 81 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝐵 < 0) |
| 83 | | signsply0.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝐶‘0) |
| 84 | 17, 35, 37 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶:ℕ0⟶ℝ) |
| 85 | | 0nn0 12541 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
| 86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℕ0) |
| 87 | 84, 86 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶‘0) ∈ ℝ) |
| 88 | 83, 87 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 89 | | signsply0.3 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · 𝐵) < 0) |
| 90 | 88, 41, 89 | mul2lt0rlt0 13137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 < 0) → 0 < 𝐴) |
| 91 | 90, 83 | breqtrdi 5184 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 < 0) → 0 < (𝐶‘0)) |
| 92 | 76, 82, 91 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 < (𝐶‘0)) |
| 93 | 36 | coefv0 26287 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹‘0) = (𝐶‘0)) |
| 94 | 17, 93 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘0) = (𝐶‘0)) |
| 95 | 94 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (𝐹‘0) = (𝐶‘0)) |
| 96 | 92, 95 | breqtrrd 5171 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 < (𝐹‘0)) |
| 97 | 75, 96 | jca 511 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → ((𝐹‘𝑑) < 0 ∧ 0 < (𝐹‘0))) |
| 98 | 61, 63, 61, 64, 68, 71, 74, 97 | ivth2 25490 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → ∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0) |
| 99 | | 0le0 12367 |
. . . . . . . 8
⊢ 0 ≤
0 |
| 100 | | pnfge 13172 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℝ*
→ 𝑑 ≤
+∞) |
| 101 | 3, 100 | syl 17 |
. . . . . . . 8
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ≤
+∞) |
| 102 | | 0xr 11308 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
| 103 | | pnfxr 11315 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
| 104 | | ioossioo 13481 |
. . . . . . . . 9
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
≤ 0 ∧ 𝑑 ≤
+∞)) → (0(,)𝑑)
⊆ (0(,)+∞)) |
| 105 | 102, 103,
104 | mpanl12 702 |
. . . . . . . 8
⊢ ((0 ≤
0 ∧ 𝑑 ≤ +∞)
→ (0(,)𝑑) ⊆
(0(,)+∞)) |
| 106 | 99, 101, 105 | sylancr 587 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ (0(,)𝑑) ⊆
(0(,)+∞)) |
| 107 | | ioorp 13465 |
. . . . . . 7
⊢
(0(,)+∞) = ℝ+ |
| 108 | 106, 107 | sseqtrdi 4024 |
. . . . . 6
⊢ (𝑑 ∈ ℝ+
→ (0(,)𝑑) ⊆
ℝ+) |
| 109 | | ssrexv 4053 |
. . . . . 6
⊢
((0(,)𝑑) ⊆
ℝ+ → (∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0 → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0)) |
| 110 | 62, 108, 109 | 3syl 18 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0 → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0)) |
| 111 | 98, 110 | mpd 15 |
. . . 4
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → ∃𝑧 ∈ ℝ+
(𝐹‘𝑧) = 0) |
| 112 | 60, 111 | syldan 591 |
. . 3
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0) |
| 113 | | plyf 26237 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐹:ℂ⟶ℂ) |
| 114 | 17, 113 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
| 115 | 114 | ffnd 6737 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn ℂ) |
| 116 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑥↑𝐷) ∈ V |
| 117 | 116 | rgenw 3065 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
ℝ+ (𝑥↑𝐷) ∈ V |
| 118 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷)) = (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) |
| 119 | 118 | fnmpt 6708 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
ℝ+ (𝑥↑𝐷) ∈ V → (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) Fn ℝ+) |
| 120 | 117, 119 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) Fn ℝ+) |
| 121 | | cnex 11236 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
| 122 | 121 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℂ ∈
V) |
| 123 | | rpssre 13042 |
. . . . . . . . . . . 12
⊢
ℝ+ ⊆ ℝ |
| 124 | 123, 67 | sstri 3993 |
. . . . . . . . . . 11
⊢
ℝ+ ⊆ ℂ |
| 125 | 121, 124 | ssexi 5322 |
. . . . . . . . . 10
⊢
ℝ+ ∈ V |
| 126 | 125 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ+ ∈
V) |
| 127 | | sseqin2 4223 |
. . . . . . . . . 10
⊢
(ℝ+ ⊆ ℂ ↔ (ℂ ∩
ℝ+) = ℝ+) |
| 128 | 124, 127 | mpbi 230 |
. . . . . . . . 9
⊢ (ℂ
∩ ℝ+) = ℝ+ |
| 129 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ℂ) → (𝐹‘𝑓) = (𝐹‘𝑓)) |
| 130 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷)) = (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷))) |
| 131 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ℝ+) ∧ 𝑥 = 𝑓) → 𝑥 = 𝑓) |
| 132 | 131 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ℝ+) ∧ 𝑥 = 𝑓) → (𝑥↑𝐷) = (𝑓↑𝐷)) |
| 133 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝑓 ∈
ℝ+) |
| 134 | | ovexd 7466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑓↑𝐷) ∈ V) |
| 135 | 130, 132,
133, 134 | fvmptd 7023 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → ((𝑥 ∈ ℝ+
↦ (𝑥↑𝐷))‘𝑓) = (𝑓↑𝐷)) |
| 136 | 115, 120,
122, 126, 128, 129, 135 | offval 7706 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘f / (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷))) = (𝑓 ∈ ℝ+ ↦ ((𝐹‘𝑓) / (𝑓↑𝐷)))) |
| 137 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑓 → (𝑥↑𝐷) = (𝑓↑𝐷)) |
| 138 | 137 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷)) = (𝑓 ∈ ℝ+ ↦ (𝑓↑𝐷)) |
| 139 | 22, 36, 34, 138 | signsplypnf 34565 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹
∘f / (𝑥
∈ ℝ+ ↦ (𝑥↑𝐷))) ⇝𝑟 𝐵) |
| 140 | 17, 139 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘f / (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷))) ⇝𝑟 𝐵) |
| 141 | 136, 140 | eqbrtrrd 5167 |
. . . . . . 7
⊢ (𝜑 → (𝑓 ∈ ℝ+ ↦ ((𝐹‘𝑓) / (𝑓↑𝐷))) ⇝𝑟 𝐵) |
| 142 | 114 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝐹:ℂ⟶ℂ) |
| 143 | 133 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝑓 ∈
ℂ) |
| 144 | 142, 143 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝐹‘𝑓) ∈ ℂ) |
| 145 | 25 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝐷 ∈
ℕ0) |
| 146 | 143, 145 | expcld 14186 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑓↑𝐷) ∈ ℂ) |
| 147 | 133 | rpne0d 13082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝑓 ≠ 0) |
| 148 | 30 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝐷 ∈
ℤ) |
| 149 | 143, 147,
148 | expne0d 14192 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑓↑𝐷) ≠ 0) |
| 150 | 144, 146,
149 | divcld 12043 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → ((𝐹‘𝑓) / (𝑓↑𝐷)) ∈ ℂ) |
| 151 | 150 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑓 ∈ ℝ+ ((𝐹‘𝑓) / (𝑓↑𝐷)) ∈ ℂ) |
| 152 | 123 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ+
⊆ ℝ) |
| 153 | | 1red 11262 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
| 154 | 151, 152,
46, 153 | rlim3 15534 |
. . . . . . 7
⊢ (𝜑 → ((𝑓 ∈ ℝ+ ↦ ((𝐹‘𝑓) / (𝑓↑𝐷))) ⇝𝑟 𝐵 ↔ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒))) |
| 155 | 141, 154 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
| 156 | | 0lt1 11785 |
. . . . . . . . . 10
⊢ 0 <
1 |
| 157 | | pnfge 13172 |
. . . . . . . . . . 11
⊢ (+∞
∈ ℝ* → +∞ ≤ +∞) |
| 158 | 103, 157 | ax-mp 5 |
. . . . . . . . . 10
⊢ +∞
≤ +∞ |
| 159 | | icossioo 13480 |
. . . . . . . . . 10
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
< 1 ∧ +∞ ≤ +∞)) → (1[,)+∞) ⊆
(0(,)+∞)) |
| 160 | 102, 103,
156, 158, 159 | mp4an 693 |
. . . . . . . . 9
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
| 161 | 160, 107 | sseqtri 4032 |
. . . . . . . 8
⊢
(1[,)+∞) ⊆ ℝ+ |
| 162 | | ssrexv 4053 |
. . . . . . . 8
⊢
((1[,)+∞) ⊆ ℝ+ → (∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒))) |
| 163 | 161, 162 | ax-mp 5 |
. . . . . . 7
⊢
(∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
| 164 | 163 | ralimi 3083 |
. . . . . 6
⊢
(∀𝑒 ∈
ℝ+ ∃𝑑 ∈ (1[,)+∞)∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
| 165 | 155, 164 | syl 17 |
. . . . 5
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
| 166 | 165 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
| 167 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → 𝑒 = -𝐵) |
| 168 | 167 | breq2d 5155 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒 ↔ (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) |
| 169 | 168 | imbi2d 340 |
. . . . . 6
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵))) |
| 170 | 169 | rexralbidv 3223 |
. . . . 5
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → (∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵))) |
| 171 | 78, 170 | rspcdv 3614 |
. . . 4
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
(∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵))) |
| 172 | 166, 171 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) |
| 173 | 112, 172 | r19.29a 3162 |
. 2
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ (𝐹‘𝑧) = 0) |
| 174 | | simplr 769 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → 𝑑 ∈ ℝ+) |
| 175 | | simpr 484 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) |
| 176 | 4 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → 𝑑 ≤ 𝑑) |
| 177 | 12 | breq1d 5153 |
. . . . . . . 8
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵 ↔ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵)) |
| 178 | 8, 177 | imbi12d 344 |
. . . . . . 7
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵) ↔ (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵))) |
| 179 | 6, 178 | rspcdv 3614 |
. . . . . 6
⊢ (𝑑 ∈ ℝ+
→ (∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵) → (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵))) |
| 180 | 174, 175,
176, 179 | syl3c 66 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) |
| 181 | 46 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
| 182 | 181 | subidd 11608 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐵 − 𝐵) = 0) |
| 183 | 182 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → (𝐵 − 𝐵) = 0) |
| 184 | 17 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐹 ∈
(Poly‘ℝ)) |
| 185 | 123 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
ℝ+ ⊆ ℝ) |
| 186 | 185 | sselda 3983 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ) |
| 187 | 184, 186 | plyrecld 34564 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐹‘𝑑) ∈
ℝ) |
| 188 | 25 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℕ0) |
| 189 | 186, 188 | reexpcld 14203 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ) |
| 190 | 186 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℂ) |
| 191 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ+) |
| 192 | 191 | rpne0d 13082 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ≠
0) |
| 193 | 30 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℤ) |
| 194 | 190, 192,
193 | expne0d 14192 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ≠ 0) |
| 195 | 187, 189,
194 | redivcld 12095 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) / (𝑑↑𝐷)) ∈ ℝ) |
| 196 | 41 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
| 197 | 195, 196,
196 | absdifltd 15472 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵 ↔ ((𝐵 − 𝐵) < ((𝐹‘𝑑) / (𝑑↑𝐷)) ∧ ((𝐹‘𝑑) / (𝑑↑𝐷)) < (𝐵 + 𝐵)))) |
| 198 | 197 | simprbda 498 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → (𝐵 − 𝐵) < ((𝐹‘𝑑) / (𝑑↑𝐷))) |
| 199 | 183, 198 | eqbrtrrd 5167 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → 0 < ((𝐹‘𝑑) / (𝑑↑𝐷))) |
| 200 | 191, 193 | rpexpcld 14286 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ+) |
| 201 | 187, 200 | gt0divd 13114 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (0 < (𝐹‘𝑑) ↔ 0 < ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
| 202 | 201 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → (0 < (𝐹‘𝑑) ↔ 0 < ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
| 203 | 199, 202 | mpbird 257 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → 0 < (𝐹‘𝑑)) |
| 204 | 180, 203 | syldan 591 |
. . . 4
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → 0 < (𝐹‘𝑑)) |
| 205 | | 0red 11264 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 ∈
ℝ) |
| 206 | | simplr 769 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝑑 ∈ ℝ+) |
| 207 | 206 | rpred 13077 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝑑 ∈ ℝ) |
| 208 | 206 | rpgt0d 13080 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 < 𝑑) |
| 209 | 35, 207, 65 | sylancr 587 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (0[,]𝑑) ⊆
ℝ) |
| 210 | 209, 67 | sstrdi 3996 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (0[,]𝑑) ⊆
ℂ) |
| 211 | 70 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝐹 ∈ (ℂ–cn→ℂ)) |
| 212 | 17 | ad4antr 732 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ 0 < (𝐹‘𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝐹 ∈
(Poly‘ℝ)) |
| 213 | 209 | sselda 3983 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ 0 < (𝐹‘𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝑥 ∈ ℝ) |
| 214 | 212, 213 | plyrecld 34564 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ 0 < (𝐹‘𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → (𝐹‘𝑥) ∈ ℝ) |
| 215 | 94 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (𝐹‘0) = (𝐶‘0)) |
| 216 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝜑) |
| 217 | | simpr1 1195 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+
∧ 0 < (𝐹‘𝑑))) → 𝐵 ∈
ℝ+) |
| 218 | 217 | rpgt0d 13080 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+
∧ 0 < (𝐹‘𝑑))) → 0 < 𝐵) |
| 219 | 218 | 3anassrs 1361 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 < 𝐵) |
| 220 | 88, 41, 89 | mul2lt0rgt0 13138 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐴 < 0) |
| 221 | 216, 219,
220 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝐴 < 0) |
| 222 | 83, 221 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (𝐶‘0) < 0) |
| 223 | 215, 222 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (𝐹‘0) < 0) |
| 224 | | simpr 484 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 < (𝐹‘𝑑)) |
| 225 | 223, 224 | jca 511 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → ((𝐹‘0) < 0 ∧ 0 < (𝐹‘𝑑))) |
| 226 | 205, 207,
205, 208, 210, 211, 214, 225 | ivth 25489 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → ∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0) |
| 227 | 206, 108,
109 | 3syl 18 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0 → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0)) |
| 228 | 226, 227 | mpd 15 |
. . . 4
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → ∃𝑧 ∈ ℝ+
(𝐹‘𝑧) = 0) |
| 229 | 204, 228 | syldan 591 |
. . 3
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0) |
| 230 | 165 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
| 231 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) → 𝐵 ∈
ℝ+) |
| 232 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵) |
| 233 | 232 | breq2d 5155 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒 ↔ (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) |
| 234 | 233 | imbi2d 340 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵))) |
| 235 | 234 | rexralbidv 3223 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → (∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵))) |
| 236 | 231, 235 | rspcdv 3614 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
(∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵))) |
| 237 | 230, 236 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) |
| 238 | 229, 237 | r19.29a 3162 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ (𝐹‘𝑧) = 0) |
| 239 | | signsply0.2 |
. . . . 5
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
| 240 | 22, 36 | dgreq0 26305 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹 =
0𝑝 ↔ (𝐶‘𝐷) = 0)) |
| 241 | 17, 240 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐶‘𝐷) = 0)) |
| 242 | 241 | necon3bid 2985 |
. . . . 5
⊢ (𝜑 → (𝐹 ≠ 0𝑝 ↔ (𝐶‘𝐷) ≠ 0)) |
| 243 | 239, 242 | mpbid 232 |
. . . 4
⊢ (𝜑 → (𝐶‘𝐷) ≠ 0) |
| 244 | 34 | neeq1i 3005 |
. . . 4
⊢ (𝐵 ≠ 0 ↔ (𝐶‘𝐷) ≠ 0) |
| 245 | 243, 244 | sylibr 234 |
. . 3
⊢ (𝜑 → 𝐵 ≠ 0) |
| 246 | | rpneg 13067 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐵 ∈ ℝ+
↔ ¬ -𝐵 ∈
ℝ+)) |
| 247 | 246 | biimprd 248 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (¬ -𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ+)) |
| 248 | 247 | orrd 864 |
. . 3
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (-𝐵 ∈ ℝ+ ∨
𝐵 ∈
ℝ+)) |
| 249 | 41, 245, 248 | syl2anc 584 |
. 2
⊢ (𝜑 → (-𝐵 ∈ ℝ+ ∨ 𝐵 ∈
ℝ+)) |
| 250 | 173, 238,
249 | mpjaodan 961 |
1
⊢ (𝜑 → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0) |