Step | Hyp | Ref
| Expression |
1 | | simplr 759 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → 𝑑 ∈ ℝ+) |
2 | | simpr 479 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) |
3 | | rpxr 12153 |
. . . . . . . 8
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ∈
ℝ*) |
4 | 3 | xrleidd 12300 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ≤ 𝑑) |
5 | 4 | ad2antlr 717 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → 𝑑 ≤ 𝑑) |
6 | | id 22 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ∈
ℝ+) |
7 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → 𝑓 = 𝑑) |
8 | 7 | breq2d 4900 |
. . . . . . . 8
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (𝑑 ≤ 𝑓 ↔ 𝑑 ≤ 𝑑)) |
9 | 7 | fveq2d 6452 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (𝐹‘𝑓) = (𝐹‘𝑑)) |
10 | 7 | oveq1d 6939 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (𝑓↑𝐷) = (𝑑↑𝐷)) |
11 | 9, 10 | oveq12d 6942 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((𝐹‘𝑓) / (𝑓↑𝐷)) = ((𝐹‘𝑑) / (𝑑↑𝐷))) |
12 | 11 | fvoveq1d 6946 |
. . . . . . . . 9
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) = (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵))) |
13 | 12 | breq1d 4898 |
. . . . . . . 8
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵 ↔ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵)) |
14 | 8, 13 | imbi12d 336 |
. . . . . . 7
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵) ↔ (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵))) |
15 | 6, 14 | rspcdv 3514 |
. . . . . 6
⊢ (𝑑 ∈ ℝ+
→ (∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵) → (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵))) |
16 | 1, 2, 5, 15 | syl3c 66 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) |
17 | | signsply0.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℝ)) |
18 | 17 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐹 ∈
(Poly‘ℝ)) |
19 | | simpr 479 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ+) |
20 | 19 | rpred 12186 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ) |
21 | 18, 20 | plyrecld 31234 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐹‘𝑑) ∈
ℝ) |
22 | | signsply0.d |
. . . . . . . . . . . . 13
⊢ 𝐷 = (deg‘𝐹) |
23 | | dgrcl 24437 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (deg‘𝐹) ∈
ℕ0) |
24 | 17, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
25 | 22, 24 | syl5eqel 2863 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
26 | 25 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℕ0) |
27 | 20, 26 | reexpcld 13349 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ) |
28 | 19 | rpcnd 12188 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℂ) |
29 | 19 | rpne0d 12191 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ≠
0) |
30 | 25 | nn0zd 11837 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈ ℤ) |
31 | 30 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℤ) |
32 | 28, 29, 31 | expne0d 13338 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ≠ 0) |
33 | 21, 27, 32 | redivcld 11206 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) / (𝑑↑𝐷)) ∈ ℝ) |
34 | | signsply0.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (𝐶‘𝐷) |
35 | | 0re 10380 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
36 | | signsply0.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = (coeff‘𝐹) |
37 | 36 | coef2 24435 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 0 ∈ ℝ) → 𝐶:ℕ0⟶ℝ) |
38 | 35, 37 | mpan2 681 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐶:ℕ0⟶ℝ) |
39 | 38 | ffvelrnda 6625 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝐷 ∈
ℕ0) → (𝐶‘𝐷) ∈ ℝ) |
40 | 34, 39 | syl5eqel 2863 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝐷 ∈
ℕ0) → 𝐵 ∈ ℝ) |
41 | 17, 25, 40 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
42 | 41 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
43 | 42 | renegcld 10805 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ -𝐵 ∈
ℝ) |
44 | 33, 42, 43 | absdifltd 14587 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵 ↔ ((𝐵 − -𝐵) < ((𝐹‘𝑑) / (𝑑↑𝐷)) ∧ ((𝐹‘𝑑) / (𝑑↑𝐷)) < (𝐵 + -𝐵)))) |
45 | 44 | simplbda 495 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → ((𝐹‘𝑑) / (𝑑↑𝐷)) < (𝐵 + -𝐵)) |
46 | 41 | recnd 10407 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
47 | 46 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
48 | 47 | negidd 10726 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐵 + -𝐵) = 0) |
49 | 48 | adantr 474 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → (𝐵 + -𝐵) = 0) |
50 | 45, 49 | breqtrd 4914 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → ((𝐹‘𝑑) / (𝑑↑𝐷)) < 0) |
51 | 19, 31 | rpexpcld 13359 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ+) |
52 | 21, 51 | ge0divd 12224 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (0 ≤ (𝐹‘𝑑) ↔ 0 ≤ ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
53 | 52 | notbid 310 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (¬ 0 ≤ (𝐹‘𝑑) ↔ ¬ 0 ≤ ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
54 | | 0red 10382 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 0 ∈ ℝ) |
55 | 21, 54 | ltnled 10525 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) < 0 ↔ ¬ 0 ≤
(𝐹‘𝑑))) |
56 | 33, 54 | ltnled 10525 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (((𝐹‘𝑑) / (𝑑↑𝐷)) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
57 | 53, 55, 56 | 3bitr4d 303 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) < 0 ↔ ((𝐹‘𝑑) / (𝑑↑𝐷)) < 0)) |
58 | 57 | adantr 474 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → ((𝐹‘𝑑) < 0 ↔ ((𝐹‘𝑑) / (𝑑↑𝐷)) < 0)) |
59 | 50, 58 | mpbird 249 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → (𝐹‘𝑑) < 0) |
60 | 16, 59 | syldan 585 |
. . . 4
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → (𝐹‘𝑑) < 0) |
61 | | 0red 10382 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 ∈
ℝ) |
62 | | simplr 759 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝑑 ∈
ℝ+) |
63 | 62 | rpred 12186 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝑑 ∈
ℝ) |
64 | 62 | rpgt0d 12189 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 < 𝑑) |
65 | | iccssre 12572 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝑑
∈ ℝ) → (0[,]𝑑) ⊆ ℝ) |
66 | 35, 63, 65 | sylancr 581 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (0[,]𝑑) ⊆
ℝ) |
67 | | ax-resscn 10331 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
68 | 66, 67 | syl6ss 3833 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (0[,]𝑑) ⊆
ℂ) |
69 | | plycn 24465 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐹 ∈
(ℂ–cn→ℂ)) |
70 | 17, 69 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) |
71 | 70 | ad3antrrr 720 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝐹 ∈ (ℂ–cn→ℂ)) |
72 | 17 | ad4antr 722 |
. . . . . . 7
⊢
(((((𝜑 ∧ -𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ (𝐹‘𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝐹 ∈
(Poly‘ℝ)) |
73 | 66 | sselda 3821 |
. . . . . . 7
⊢
(((((𝜑 ∧ -𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ (𝐹‘𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝑥 ∈ ℝ) |
74 | 72, 73 | plyrecld 31234 |
. . . . . 6
⊢
(((((𝜑 ∧ -𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ (𝐹‘𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → (𝐹‘𝑥) ∈ ℝ) |
75 | | simpr 479 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (𝐹‘𝑑) < 0) |
76 | | simplll 765 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝜑) |
77 | 76, 41 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝐵 ∈
ℝ) |
78 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) → -𝐵 ∈
ℝ+) |
79 | 78 | ad2antrr 716 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → -𝐵 ∈
ℝ+) |
80 | | negelrp 12177 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (-𝐵 ∈ ℝ+
↔ 𝐵 <
0)) |
81 | 80 | biimpa 470 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ -𝐵 ∈ ℝ+)
→ 𝐵 <
0) |
82 | 77, 79, 81 | syl2anc 579 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝐵 < 0) |
83 | | signsply0.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝐶‘0) |
84 | 17, 35, 37 | sylancl 580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶:ℕ0⟶ℝ) |
85 | | 0nn0 11664 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℕ0) |
87 | 84, 86 | ffvelrnd 6626 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶‘0) ∈ ℝ) |
88 | 83, 87 | syl5eqel 2863 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
89 | | signsply0.3 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · 𝐵) < 0) |
90 | 88, 41, 89 | mul2lt0rlt0 12246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 < 0) → 0 < 𝐴) |
91 | 90, 83 | syl6breq 4929 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 < 0) → 0 < (𝐶‘0)) |
92 | 76, 82, 91 | syl2anc 579 |
. . . . . . . 8
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 < (𝐶‘0)) |
93 | 36 | coefv0 24452 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹‘0) = (𝐶‘0)) |
94 | 17, 93 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘0) = (𝐶‘0)) |
95 | 94 | ad3antrrr 720 |
. . . . . . . 8
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (𝐹‘0) = (𝐶‘0)) |
96 | 92, 95 | breqtrrd 4916 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 < (𝐹‘0)) |
97 | 75, 96 | jca 507 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → ((𝐹‘𝑑) < 0 ∧ 0 < (𝐹‘0))) |
98 | 61, 63, 61, 64, 68, 71, 74, 97 | ivth2 23670 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → ∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0) |
99 | | 0le0 11488 |
. . . . . . . 8
⊢ 0 ≤
0 |
100 | | pnfge 12280 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℝ*
→ 𝑑 ≤
+∞) |
101 | 3, 100 | syl 17 |
. . . . . . . 8
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ≤
+∞) |
102 | | 0xr 10425 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
103 | | pnfxr 10432 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
104 | | ioossioo 12583 |
. . . . . . . . 9
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
≤ 0 ∧ 𝑑 ≤
+∞)) → (0(,)𝑑)
⊆ (0(,)+∞)) |
105 | 102, 103,
104 | mpanl12 692 |
. . . . . . . 8
⊢ ((0 ≤
0 ∧ 𝑑 ≤ +∞)
→ (0(,)𝑑) ⊆
(0(,)+∞)) |
106 | 99, 101, 105 | sylancr 581 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ (0(,)𝑑) ⊆
(0(,)+∞)) |
107 | | ioorp 12568 |
. . . . . . 7
⊢
(0(,)+∞) = ℝ+ |
108 | 106, 107 | syl6sseq 3870 |
. . . . . 6
⊢ (𝑑 ∈ ℝ+
→ (0(,)𝑑) ⊆
ℝ+) |
109 | | ssrexv 3886 |
. . . . . 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 585 |
. . 3
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0) |
113 | | plyf 24402 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐹:ℂ⟶ℂ) |
114 | 17, 113 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
115 | 114 | ffnd 6294 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn ℂ) |
116 | | ovex 6956 |
. . . . . . . . . . 11
⊢ (𝑥↑𝐷) ∈ V |
117 | 116 | rgenw 3106 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
ℝ+ (𝑥↑𝐷) ∈ V |
118 | | eqid 2778 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷)) = (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) |
119 | 118 | fnmpt 6268 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
ℝ+ (𝑥↑𝐷) ∈ V → (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) Fn ℝ+) |
120 | 117, 119 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) Fn ℝ+) |
121 | | cnex 10355 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
122 | 121 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℂ ∈
V) |
123 | | rpssre 12149 |
. . . . . . . . . . . 12
⊢
ℝ+ ⊆ ℝ |
124 | 123, 67 | sstri 3830 |
. . . . . . . . . . 11
⊢
ℝ+ ⊆ ℂ |
125 | 121, 124 | ssexi 5042 |
. . . . . . . . . 10
⊢
ℝ+ ∈ V |
126 | 125 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ+ ∈
V) |
127 | | sseqin2 4040 |
. . . . . . . . . 10
⊢
(ℝ+ ⊆ ℂ ↔ (ℂ ∩
ℝ+) = ℝ+) |
128 | 124, 127 | mpbi 222 |
. . . . . . . . 9
⊢ (ℂ
∩ ℝ+) = ℝ+ |
129 | | eqidd 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ℂ) → (𝐹‘𝑓) = (𝐹‘𝑓)) |
130 | | eqidd 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷)) = (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷))) |
131 | | simpr 479 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ℝ+) ∧ 𝑥 = 𝑓) → 𝑥 = 𝑓) |
132 | 131 | oveq1d 6939 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ℝ+) ∧ 𝑥 = 𝑓) → (𝑥↑𝐷) = (𝑓↑𝐷)) |
133 | | simpr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝑓 ∈
ℝ+) |
134 | | ovexd 6958 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑓↑𝐷) ∈ V) |
135 | 130, 132,
133, 134 | fvmptd 6550 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → ((𝑥 ∈ ℝ+
↦ (𝑥↑𝐷))‘𝑓) = (𝑓↑𝐷)) |
136 | 115, 120,
122, 126, 128, 129, 135 | offval 7183 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘𝑓 / (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷))) = (𝑓 ∈ ℝ+ ↦ ((𝐹‘𝑓) / (𝑓↑𝐷)))) |
137 | | oveq1 6931 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑓 → (𝑥↑𝐷) = (𝑓↑𝐷)) |
138 | 137 | cbvmptv 4987 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷)) = (𝑓 ∈ ℝ+ ↦ (𝑓↑𝐷)) |
139 | 22, 36, 34, 138 | signsplypnf 31235 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹
∘𝑓 / (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷))) ⇝𝑟 𝐵) |
140 | 17, 139 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘𝑓 / (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷))) ⇝𝑟
𝐵) |
141 | 136, 140 | eqbrtrrd 4912 |
. . . . . . 7
⊢ (𝜑 → (𝑓 ∈ ℝ+ ↦ ((𝐹‘𝑓) / (𝑓↑𝐷))) ⇝𝑟 𝐵) |
142 | 114 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝐹:ℂ⟶ℂ) |
143 | 133 | rpcnd 12188 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝑓 ∈
ℂ) |
144 | 142, 143 | ffvelrnd 6626 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝐹‘𝑓) ∈ ℂ) |
145 | 25 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝐷 ∈
ℕ0) |
146 | 143, 145 | expcld 13332 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑓↑𝐷) ∈ ℂ) |
147 | 133 | rpne0d 12191 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝑓 ≠ 0) |
148 | 30 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝐷 ∈
ℤ) |
149 | 143, 147,
148 | expne0d 13338 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑓↑𝐷) ≠ 0) |
150 | 144, 146,
149 | divcld 11154 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → ((𝐹‘𝑓) / (𝑓↑𝐷)) ∈ ℂ) |
151 | 150 | ralrimiva 3148 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑓 ∈ ℝ+ ((𝐹‘𝑓) / (𝑓↑𝐷)) ∈ ℂ) |
152 | 123 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ+
⊆ ℝ) |
153 | | 1red 10379 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
154 | 151, 152,
46, 153 | rlim3 14646 |
. . . . . . 7
⊢ (𝜑 → ((𝑓 ∈ ℝ+ ↦ ((𝐹‘𝑓) / (𝑓↑𝐷))) ⇝𝑟 𝐵 ↔ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒))) |
155 | 141, 154 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
156 | | 0lt1 10900 |
. . . . . . . . . 10
⊢ 0 <
1 |
157 | | pnfge 12280 |
. . . . . . . . . . 11
⊢ (+∞
∈ ℝ* → +∞ ≤ +∞) |
158 | 103, 157 | ax-mp 5 |
. . . . . . . . . 10
⊢ +∞
≤ +∞ |
159 | | icossioo 12582 |
. . . . . . . . . 10
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
< 1 ∧ +∞ ≤ +∞)) → (1[,)+∞) ⊆
(0(,)+∞)) |
160 | 102, 103,
156, 158, 159 | mp4an 683 |
. . . . . . . . 9
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
161 | 160, 107 | sseqtri 3856 |
. . . . . . . 8
⊢
(1[,)+∞) ⊆ ℝ+ |
162 | | ssrexv 3886 |
. . . . . . . 8
⊢
((1[,)+∞) ⊆ ℝ+ → (∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒))) |
163 | 161, 162 | ax-mp 5 |
. . . . . . 7
⊢
(∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
164 | 163 | ralimi 3134 |
. . . . . 6
⊢
(∀𝑒 ∈
ℝ+ ∃𝑑 ∈ (1[,)+∞)∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
165 | 155, 164 | syl 17 |
. . . . 5
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
166 | 165 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
167 | | simpr 479 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → 𝑒 = -𝐵) |
168 | 167 | breq2d 4900 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒 ↔ (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) |
169 | 168 | imbi2d 332 |
. . . . . 6
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵))) |
170 | 169 | rexralbidv 3243 |
. . . . 5
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → (∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵))) |
171 | 78, 170 | rspcdv 3514 |
. . . 4
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
(∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵))) |
172 | 166, 171 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) |
173 | 112, 172 | r19.29a 3264 |
. 2
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ (𝐹‘𝑧) = 0) |
174 | | simplr 759 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → 𝑑 ∈ ℝ+) |
175 | | simpr 479 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) |
176 | 4 | ad2antlr 717 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → 𝑑 ≤ 𝑑) |
177 | 12 | breq1d 4898 |
. . . . . . . 8
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵 ↔ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵)) |
178 | 8, 177 | imbi12d 336 |
. . . . . . 7
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵) ↔ (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵))) |
179 | 6, 178 | rspcdv 3514 |
. . . . . 6
⊢ (𝑑 ∈ ℝ+
→ (∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵) → (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵))) |
180 | 174, 175,
176, 179 | syl3c 66 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) |
181 | 46 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
182 | 181 | subidd 10724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐵 − 𝐵) = 0) |
183 | 182 | adantr 474 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → (𝐵 − 𝐵) = 0) |
184 | 17 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐹 ∈
(Poly‘ℝ)) |
185 | 123 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
ℝ+ ⊆ ℝ) |
186 | 185 | sselda 3821 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ) |
187 | 184, 186 | plyrecld 31234 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐹‘𝑑) ∈
ℝ) |
188 | 25 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℕ0) |
189 | 186, 188 | reexpcld 13349 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ) |
190 | 186 | recnd 10407 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℂ) |
191 | | simpr 479 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ+) |
192 | 191 | rpne0d 12191 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ≠
0) |
193 | 30 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℤ) |
194 | 190, 192,
193 | expne0d 13338 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ≠ 0) |
195 | 187, 189,
194 | redivcld 11206 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) / (𝑑↑𝐷)) ∈ ℝ) |
196 | 41 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
197 | 195, 196,
196 | absdifltd 14587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵 ↔ ((𝐵 − 𝐵) < ((𝐹‘𝑑) / (𝑑↑𝐷)) ∧ ((𝐹‘𝑑) / (𝑑↑𝐷)) < (𝐵 + 𝐵)))) |
198 | 197 | simprbda 494 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → (𝐵 − 𝐵) < ((𝐹‘𝑑) / (𝑑↑𝐷))) |
199 | 183, 198 | eqbrtrrd 4912 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → 0 < ((𝐹‘𝑑) / (𝑑↑𝐷))) |
200 | 191, 193 | rpexpcld 13359 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ+) |
201 | 187, 200 | gt0divd 12223 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (0 < (𝐹‘𝑑) ↔ 0 < ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
202 | 201 | adantr 474 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → (0 < (𝐹‘𝑑) ↔ 0 < ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
203 | 199, 202 | mpbird 249 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → 0 < (𝐹‘𝑑)) |
204 | 180, 203 | syldan 585 |
. . . 4
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → 0 < (𝐹‘𝑑)) |
205 | | 0red 10382 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 ∈
ℝ) |
206 | | simplr 759 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝑑 ∈ ℝ+) |
207 | 206 | rpred 12186 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝑑 ∈ ℝ) |
208 | 206 | rpgt0d 12189 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 < 𝑑) |
209 | 35, 207, 65 | sylancr 581 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (0[,]𝑑) ⊆
ℝ) |
210 | 209, 67 | syl6ss 3833 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (0[,]𝑑) ⊆
ℂ) |
211 | 70 | ad3antrrr 720 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝐹 ∈ (ℂ–cn→ℂ)) |
212 | 17 | ad4antr 722 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ 0 < (𝐹‘𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝐹 ∈
(Poly‘ℝ)) |
213 | 209 | sselda 3821 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ 0 < (𝐹‘𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝑥 ∈ ℝ) |
214 | 212, 213 | plyrecld 31234 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ 0 < (𝐹‘𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → (𝐹‘𝑥) ∈ ℝ) |
215 | 94 | ad3antrrr 720 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (𝐹‘0) = (𝐶‘0)) |
216 | | simplll 765 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝜑) |
217 | | simpr1 1205 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+
∧ 0 < (𝐹‘𝑑))) → 𝐵 ∈
ℝ+) |
218 | 217 | rpgt0d 12189 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+
∧ 0 < (𝐹‘𝑑))) → 0 < 𝐵) |
219 | 218 | 3anassrs 1422 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 < 𝐵) |
220 | 88, 41, 89 | mul2lt0rgt0 12247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐴 < 0) |
221 | 216, 219,
220 | syl2anc 579 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝐴 < 0) |
222 | 83, 221 | syl5eqbrr 4924 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (𝐶‘0) < 0) |
223 | 215, 222 | eqbrtrd 4910 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (𝐹‘0) < 0) |
224 | | simpr 479 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 < (𝐹‘𝑑)) |
225 | 223, 224 | jca 507 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → ((𝐹‘0) < 0 ∧ 0 < (𝐹‘𝑑))) |
226 | 205, 207,
205, 208, 210, 211, 214, 225 | ivth 23669 |
. . . . 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 585 |
. . 3
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0) |
230 | 165 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
231 | | simpr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) → 𝐵 ∈
ℝ+) |
232 | | simpr 479 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵) |
233 | 232 | breq2d 4900 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒 ↔ (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) |
234 | 233 | imbi2d 332 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵))) |
235 | 234 | rexralbidv 3243 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → (∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵))) |
236 | 231, 235 | rspcdv 3514 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
(∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵))) |
237 | 230, 236 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) |
238 | 229, 237 | r19.29a 3264 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ (𝐹‘𝑧) = 0) |
239 | | signsply0.2 |
. . . . 5
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
240 | 22, 36 | dgreq0 24469 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹 =
0𝑝 ↔ (𝐶‘𝐷) = 0)) |
241 | 17, 240 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐶‘𝐷) = 0)) |
242 | 241 | necon3bid 3013 |
. . . . 5
⊢ (𝜑 → (𝐹 ≠ 0𝑝 ↔ (𝐶‘𝐷) ≠ 0)) |
243 | 239, 242 | mpbid 224 |
. . . 4
⊢ (𝜑 → (𝐶‘𝐷) ≠ 0) |
244 | 34 | neeq1i 3033 |
. . . 4
⊢ (𝐵 ≠ 0 ↔ (𝐶‘𝐷) ≠ 0) |
245 | 243, 244 | sylibr 226 |
. . 3
⊢ (𝜑 → 𝐵 ≠ 0) |
246 | | rpneg 12176 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐵 ∈ ℝ+
↔ ¬ -𝐵 ∈
ℝ+)) |
247 | 246 | biimprd 240 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (¬ -𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ+)) |
248 | 247 | orrd 852 |
. . 3
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (-𝐵 ∈ ℝ+ ∨
𝐵 ∈
ℝ+)) |
249 | 41, 245, 248 | syl2anc 579 |
. 2
⊢ (𝜑 → (-𝐵 ∈ ℝ+ ∨ 𝐵 ∈
ℝ+)) |
250 | 173, 238,
249 | mpjaodan 944 |
1
⊢ (𝜑 → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0) |