Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → 𝑑 ∈ ℝ+) |
2 | | simpr 476 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) |
3 | | rpxr 11716 |
. . . . . . . 8
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ∈
ℝ*) |
4 | | xrleid 11859 |
. . . . . . . 8
⊢ (𝑑 ∈ ℝ*
→ 𝑑 ≤ 𝑑) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ≤ 𝑑) |
6 | 5 | ad2antlr 759 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → 𝑑 ≤ 𝑑) |
7 | | id 22 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ∈
ℝ+) |
8 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → 𝑓 = 𝑑) |
9 | 8 | breq2d 4595 |
. . . . . . . 8
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (𝑑 ≤ 𝑓 ↔ 𝑑 ≤ 𝑑)) |
10 | 8 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (𝐹‘𝑓) = (𝐹‘𝑑)) |
11 | 8 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (𝑓↑𝐷) = (𝑑↑𝐷)) |
12 | 10, 11 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((𝐹‘𝑓) / (𝑓↑𝐷)) = ((𝐹‘𝑑) / (𝑑↑𝐷))) |
13 | 12 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵) = (((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) |
14 | 13 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) = (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵))) |
15 | 14 | breq1d 4593 |
. . . . . . . 8
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵 ↔ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵)) |
16 | 9, 15 | imbi12d 333 |
. . . . . . 7
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵) ↔ (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵))) |
17 | 7, 16 | rspcdv 3285 |
. . . . . 6
⊢ (𝑑 ∈ ℝ+
→ (∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵) → (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵))) |
18 | 1, 2, 6, 17 | syl3c 64 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) |
19 | | signsply0.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℝ)) |
20 | 19 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐹 ∈
(Poly‘ℝ)) |
21 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ+) |
22 | 21 | rpred 11748 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ) |
23 | 20, 22 | plyrecld 29952 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐹‘𝑑) ∈
ℝ) |
24 | | signsply0.d |
. . . . . . . . . . . . 13
⊢ 𝐷 = (deg‘𝐹) |
25 | | dgrcl 23793 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (deg‘𝐹) ∈
ℕ0) |
26 | 19, 25 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
27 | 24, 26 | syl5eqel 2692 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
28 | 27 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℕ0) |
29 | 22, 28 | reexpcld 12887 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ) |
30 | 21 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℂ) |
31 | 21 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ≠
0) |
32 | 27 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈ ℤ) |
33 | 32 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℤ) |
34 | 30, 31, 33 | expne0d 12876 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ≠ 0) |
35 | 23, 29, 34 | redivcld 10732 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) / (𝑑↑𝐷)) ∈ ℝ) |
36 | | signsply0.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (𝐶‘𝐷) |
37 | | 0re 9919 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
38 | | signsply0.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = (coeff‘𝐹) |
39 | 38 | coef2 23791 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 0 ∈ ℝ) → 𝐶:ℕ0⟶ℝ) |
40 | 37, 39 | mpan2 703 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐶:ℕ0⟶ℝ) |
41 | 40 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝐷 ∈
ℕ0) → (𝐶‘𝐷) ∈ ℝ) |
42 | 36, 41 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝐷 ∈
ℕ0) → 𝐵 ∈ ℝ) |
43 | 19, 27, 42 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
44 | 43 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
45 | 44 | renegcld 10336 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ -𝐵 ∈
ℝ) |
46 | 35, 44, 45 | absdifltd 14020 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵 ↔ ((𝐵 − -𝐵) < ((𝐹‘𝑑) / (𝑑↑𝐷)) ∧ ((𝐹‘𝑑) / (𝑑↑𝐷)) < (𝐵 + -𝐵)))) |
47 | 46 | simplbda 652 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → ((𝐹‘𝑑) / (𝑑↑𝐷)) < (𝐵 + -𝐵)) |
48 | 43 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
49 | 48 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
50 | 49 | negidd 10261 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐵 + -𝐵) = 0) |
51 | 50 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → (𝐵 + -𝐵) = 0) |
52 | 47, 51 | breqtrd 4609 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → ((𝐹‘𝑑) / (𝑑↑𝐷)) < 0) |
53 | 21, 33 | rpexpcld 12894 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ+) |
54 | 23, 53 | ge0divd 11786 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (0 ≤ (𝐹‘𝑑) ↔ 0 ≤ ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
55 | 54 | notbid 307 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (¬ 0 ≤ (𝐹‘𝑑) ↔ ¬ 0 ≤ ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
56 | | 0red 9920 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 0 ∈ ℝ) |
57 | 23, 56 | ltnled 10063 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) < 0 ↔ ¬ 0 ≤
(𝐹‘𝑑))) |
58 | 35, 56 | ltnled 10063 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (((𝐹‘𝑑) / (𝑑↑𝐷)) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
59 | 55, 57, 58 | 3bitr4d 299 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) < 0 ↔ ((𝐹‘𝑑) / (𝑑↑𝐷)) < 0)) |
60 | 59 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → ((𝐹‘𝑑) < 0 ↔ ((𝐹‘𝑑) / (𝑑↑𝐷)) < 0)) |
61 | 52, 60 | mpbird 246 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < -𝐵) → (𝐹‘𝑑) < 0) |
62 | 18, 61 | syldan 486 |
. . . 4
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → (𝐹‘𝑑) < 0) |
63 | | 0red 9920 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 ∈
ℝ) |
64 | | simplr 788 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝑑 ∈
ℝ+) |
65 | 64 | rpred 11748 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝑑 ∈
ℝ) |
66 | 64 | rpgt0d 11751 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 < 𝑑) |
67 | | iccssre 12126 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝑑
∈ ℝ) → (0[,]𝑑) ⊆ ℝ) |
68 | 37, 65, 67 | sylancr 694 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (0[,]𝑑) ⊆
ℝ) |
69 | | ax-resscn 9872 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
70 | 68, 69 | syl6ss 3580 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (0[,]𝑑) ⊆
ℂ) |
71 | | plycn 23821 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐹 ∈
(ℂ–cn→ℂ)) |
72 | 19, 71 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) |
73 | 72 | ad3antrrr 762 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝐹 ∈ (ℂ–cn→ℂ)) |
74 | 19 | ad4antr 764 |
. . . . . . 7
⊢
(((((𝜑 ∧ -𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ (𝐹‘𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝐹 ∈
(Poly‘ℝ)) |
75 | 68 | sselda 3568 |
. . . . . . 7
⊢
(((((𝜑 ∧ -𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ (𝐹‘𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝑥 ∈ ℝ) |
76 | 74, 75 | plyrecld 29952 |
. . . . . 6
⊢
(((((𝜑 ∧ -𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ (𝐹‘𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → (𝐹‘𝑥) ∈ ℝ) |
77 | | simpr 476 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (𝐹‘𝑑) < 0) |
78 | | simplll 794 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝜑) |
79 | 78, 43 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝐵 ∈
ℝ) |
80 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) → -𝐵 ∈
ℝ+) |
81 | 80 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → -𝐵 ∈
ℝ+) |
82 | | negelrp 11740 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (-𝐵 ∈ ℝ+
↔ 𝐵 <
0)) |
83 | 82 | biimpa 500 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ -𝐵 ∈ ℝ+)
→ 𝐵 <
0) |
84 | 79, 81, 83 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 𝐵 < 0) |
85 | | signsply0.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝐶‘0) |
86 | 19, 37, 39 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶:ℕ0⟶ℝ) |
87 | | 0nn0 11184 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℕ0) |
89 | 86, 88 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶‘0) ∈ ℝ) |
90 | 85, 89 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
91 | | signsply0.3 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · 𝐵) < 0) |
92 | 90, 43, 91 | mul2lt0rlt0 11808 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 < 0) → 0 < 𝐴) |
93 | 92, 85 | syl6breq 4624 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 < 0) → 0 < (𝐶‘0)) |
94 | 78, 84, 93 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 < (𝐶‘0)) |
95 | 38 | coefv0 23808 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹‘0) = (𝐶‘0)) |
96 | 19, 95 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘0) = (𝐶‘0)) |
97 | 96 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (𝐹‘0) = (𝐶‘0)) |
98 | 94, 97 | breqtrrd 4611 |
. . . . . . 7
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → 0 < (𝐹‘0)) |
99 | 77, 98 | jca 553 |
. . . . . 6
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → ((𝐹‘𝑑) < 0 ∧ 0 < (𝐹‘0))) |
100 | 63, 65, 63, 66, 70, 73, 76, 99 | ivth2 23031 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → ∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0) |
101 | | 0le0 10987 |
. . . . . . . 8
⊢ 0 ≤
0 |
102 | | pnfge 11840 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℝ*
→ 𝑑 ≤
+∞) |
103 | 3, 102 | syl 17 |
. . . . . . . 8
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ≤
+∞) |
104 | | 0xr 9965 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
105 | | pnfxr 9971 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
106 | | ioossioo 12136 |
. . . . . . . . 9
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
≤ 0 ∧ 𝑑 ≤
+∞)) → (0(,)𝑑)
⊆ (0(,)+∞)) |
107 | 104, 105,
106 | mpanl12 714 |
. . . . . . . 8
⊢ ((0 ≤
0 ∧ 𝑑 ≤ +∞)
→ (0(,)𝑑) ⊆
(0(,)+∞)) |
108 | 101, 103,
107 | sylancr 694 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ (0(,)𝑑) ⊆
(0(,)+∞)) |
109 | | ioorp 12122 |
. . . . . . 7
⊢
(0(,)+∞) = ℝ+ |
110 | 108, 109 | syl6sseq 3614 |
. . . . . 6
⊢ (𝑑 ∈ ℝ+
→ (0(,)𝑑) ⊆
ℝ+) |
111 | | ssrexv 3630 |
. . . . . 6
⊢
((0(,)𝑑) ⊆
ℝ+ → (∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0 → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0)) |
112 | 64, 110, 111 | 3syl 18 |
. . . . 5
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → (∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0 → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0)) |
113 | 100, 112 | mpd 15 |
. . . 4
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (𝐹‘𝑑) < 0) → ∃𝑧 ∈ ℝ+
(𝐹‘𝑧) = 0) |
114 | 62, 113 | syldan 486 |
. . 3
⊢ ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0) |
115 | | plyf 23758 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐹:ℂ⟶ℂ) |
116 | 19, 115 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
117 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:ℂ⟶ℂ →
𝐹 Fn
ℂ) |
118 | 116, 117 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn ℂ) |
119 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑥↑𝐷) ∈ V |
120 | 119 | rgenw 2908 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
ℝ+ (𝑥↑𝐷) ∈ V |
121 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷)) = (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) |
122 | 121 | fnmpt 5933 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
ℝ+ (𝑥↑𝐷) ∈ V → (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) Fn ℝ+) |
123 | 120, 122 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) Fn ℝ+) |
124 | | cnex 9896 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
125 | 124 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℂ ∈
V) |
126 | | rpssre 11719 |
. . . . . . . . . . . 12
⊢
ℝ+ ⊆ ℝ |
127 | 126, 69 | sstri 3577 |
. . . . . . . . . . 11
⊢
ℝ+ ⊆ ℂ |
128 | 124, 127 | ssexi 4731 |
. . . . . . . . . 10
⊢
ℝ+ ∈ V |
129 | 128 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ+ ∈
V) |
130 | | sseqin2 3779 |
. . . . . . . . . 10
⊢
(ℝ+ ⊆ ℂ ↔ (ℂ ∩
ℝ+) = ℝ+) |
131 | 127, 130 | mpbi 219 |
. . . . . . . . 9
⊢ (ℂ
∩ ℝ+) = ℝ+ |
132 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ℂ) → (𝐹‘𝑓) = (𝐹‘𝑓)) |
133 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷)) = (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷))) |
134 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ℝ+) ∧ 𝑥 = 𝑓) → 𝑥 = 𝑓) |
135 | 134 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ℝ+) ∧ 𝑥 = 𝑓) → (𝑥↑𝐷) = (𝑓↑𝐷)) |
136 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝑓 ∈
ℝ+) |
137 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑓↑𝐷) ∈ V |
138 | 137 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑓↑𝐷) ∈ V) |
139 | 133, 135,
136, 138 | fvmptd 6197 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → ((𝑥 ∈ ℝ+
↦ (𝑥↑𝐷))‘𝑓) = (𝑓↑𝐷)) |
140 | 118, 123,
125, 129, 131, 132, 139 | offval 6802 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘𝑓 / (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷))) = (𝑓 ∈ ℝ+ ↦ ((𝐹‘𝑓) / (𝑓↑𝐷)))) |
141 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑓 → (𝑥↑𝐷) = (𝑓↑𝐷)) |
142 | 141 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷)) = (𝑓 ∈ ℝ+ ↦ (𝑓↑𝐷)) |
143 | 24, 38, 36, 142 | signsplypnf 29953 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹
∘𝑓 / (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷))) ⇝𝑟 𝐵) |
144 | 19, 143 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘𝑓 / (𝑥 ∈ ℝ+
↦ (𝑥↑𝐷))) ⇝𝑟
𝐵) |
145 | 140, 144 | eqbrtrrd 4607 |
. . . . . . 7
⊢ (𝜑 → (𝑓 ∈ ℝ+ ↦ ((𝐹‘𝑓) / (𝑓↑𝐷))) ⇝𝑟 𝐵) |
146 | 116 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝐹:ℂ⟶ℂ) |
147 | 136 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝑓 ∈
ℂ) |
148 | 146, 147 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝐹‘𝑓) ∈ ℂ) |
149 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝐷 ∈
ℕ0) |
150 | 147, 149 | expcld 12870 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑓↑𝐷) ∈ ℂ) |
151 | 136 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝑓 ≠ 0) |
152 | 32 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → 𝐷 ∈
ℤ) |
153 | 147, 151,
152 | expne0d 12876 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → (𝑓↑𝐷) ≠ 0) |
154 | 148, 150,
153 | divcld 10680 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ℝ+) → ((𝐹‘𝑓) / (𝑓↑𝐷)) ∈ ℂ) |
155 | 154 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑓 ∈ ℝ+ ((𝐹‘𝑓) / (𝑓↑𝐷)) ∈ ℂ) |
156 | 126 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ+
⊆ ℝ) |
157 | | 1red 9934 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
158 | 155, 156,
48, 157 | rlim3 14077 |
. . . . . . 7
⊢ (𝜑 → ((𝑓 ∈ ℝ+ ↦ ((𝐹‘𝑓) / (𝑓↑𝐷))) ⇝𝑟 𝐵 ↔ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒))) |
159 | 145, 158 | mpbid 221 |
. . . . . 6
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
160 | | 0lt1 10429 |
. . . . . . . . . 10
⊢ 0 <
1 |
161 | | pnfge 11840 |
. . . . . . . . . . 11
⊢ (+∞
∈ ℝ* → +∞ ≤ +∞) |
162 | 105, 161 | ax-mp 5 |
. . . . . . . . . 10
⊢ +∞
≤ +∞ |
163 | | icossioo 12135 |
. . . . . . . . . 10
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
< 1 ∧ +∞ ≤ +∞)) → (1[,)+∞) ⊆
(0(,)+∞)) |
164 | 104, 105,
160, 162, 163 | mp4an 705 |
. . . . . . . . 9
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
165 | 164, 109 | sseqtri 3600 |
. . . . . . . 8
⊢
(1[,)+∞) ⊆ ℝ+ |
166 | | ssrexv 3630 |
. . . . . . . 8
⊢
((1[,)+∞) ⊆ ℝ+ → (∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒))) |
167 | 165, 166 | ax-mp 5 |
. . . . . . 7
⊢
(∃𝑑 ∈
(1[,)+∞)∀𝑓
∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
168 | 167 | ralimi 2936 |
. . . . . 6
⊢
(∀𝑒 ∈
ℝ+ ∃𝑑 ∈ (1[,)+∞)∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
169 | 159, 168 | syl 17 |
. . . . 5
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
170 | 169 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
171 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → 𝑒 = -𝐵) |
172 | 171 | breq2d 4595 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒 ↔ (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) |
173 | 172 | imbi2d 329 |
. . . . . 6
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵))) |
174 | 173 | rexralbidv 3040 |
. . . . 5
⊢ (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → (∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵))) |
175 | 80, 174 | rspcdv 3285 |
. . . 4
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
(∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵))) |
176 | 170, 175 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < -𝐵)) |
177 | 114, 176 | r19.29a 3060 |
. 2
⊢ ((𝜑 ∧ -𝐵 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ (𝐹‘𝑧) = 0) |
178 | | simplr 788 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → 𝑑 ∈ ℝ+) |
179 | | simpr 476 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) |
180 | 5 | ad2antlr 759 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → 𝑑 ≤ 𝑑) |
181 | 14 | breq1d 4593 |
. . . . . . . 8
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵 ↔ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵)) |
182 | 9, 181 | imbi12d 333 |
. . . . . . 7
⊢ ((𝑑 ∈ ℝ+
∧ 𝑓 = 𝑑) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵) ↔ (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵))) |
183 | 7, 182 | rspcdv 3285 |
. . . . . 6
⊢ (𝑑 ∈ ℝ+
→ (∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵) → (𝑑 ≤ 𝑑 → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵))) |
184 | 178, 179,
180, 183 | syl3c 64 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) |
185 | 48 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
186 | 185 | subidd 10259 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐵 − 𝐵) = 0) |
187 | 186 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → (𝐵 − 𝐵) = 0) |
188 | 19 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐹 ∈
(Poly‘ℝ)) |
189 | 126 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
ℝ+ ⊆ ℝ) |
190 | 189 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ) |
191 | 188, 190 | plyrecld 29952 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝐹‘𝑑) ∈
ℝ) |
192 | 27 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℕ0) |
193 | 190, 192 | reexpcld 12887 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ) |
194 | 190 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℂ) |
195 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ∈
ℝ+) |
196 | 195 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝑑 ≠
0) |
197 | 32 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐷 ∈
ℤ) |
198 | 194, 196,
197 | expne0d 12876 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ≠ 0) |
199 | 191, 193,
198 | redivcld 10732 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((𝐹‘𝑑) / (𝑑↑𝐷)) ∈ ℝ) |
200 | 43 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
201 | 199, 200,
200 | absdifltd 14020 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ ((abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵 ↔ ((𝐵 − 𝐵) < ((𝐹‘𝑑) / (𝑑↑𝐷)) ∧ ((𝐹‘𝑑) / (𝑑↑𝐷)) < (𝐵 + 𝐵)))) |
202 | 201 | simprbda 651 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → (𝐵 − 𝐵) < ((𝐹‘𝑑) / (𝑑↑𝐷))) |
203 | 187, 202 | eqbrtrrd 4607 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → 0 < ((𝐹‘𝑑) / (𝑑↑𝐷))) |
204 | 195, 197 | rpexpcld 12894 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (𝑑↑𝐷) ∈
ℝ+) |
205 | 191, 204 | gt0divd 11785 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (0 < (𝐹‘𝑑) ↔ 0 < ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
206 | 205 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → (0 < (𝐹‘𝑑) ↔ 0 < ((𝐹‘𝑑) / (𝑑↑𝐷)))) |
207 | 203, 206 | mpbird 246 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ (abs‘(((𝐹‘𝑑) / (𝑑↑𝐷)) − 𝐵)) < 𝐵) → 0 < (𝐹‘𝑑)) |
208 | 184, 207 | syldan 486 |
. . . 4
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → 0 < (𝐹‘𝑑)) |
209 | | 0red 9920 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 ∈
ℝ) |
210 | | simplr 788 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝑑 ∈ ℝ+) |
211 | 210 | rpred 11748 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝑑 ∈ ℝ) |
212 | 210 | rpgt0d 11751 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 < 𝑑) |
213 | 37, 211, 67 | sylancr 694 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (0[,]𝑑) ⊆
ℝ) |
214 | 213, 69 | syl6ss 3580 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (0[,]𝑑) ⊆
ℂ) |
215 | 72 | ad3antrrr 762 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝐹 ∈ (ℂ–cn→ℂ)) |
216 | 19 | ad4antr 764 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ 0 < (𝐹‘𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝐹 ∈
(Poly‘ℝ)) |
217 | 213 | sselda 3568 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ 0 < (𝐹‘𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝑥 ∈ ℝ) |
218 | 216, 217 | plyrecld 29952 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝐵 ∈ ℝ+)
∧ 𝑑 ∈
ℝ+) ∧ 0 < (𝐹‘𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → (𝐹‘𝑥) ∈ ℝ) |
219 | 96 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (𝐹‘0) = (𝐶‘0)) |
220 | | simplll 794 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝜑) |
221 | | simpr1 1060 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+
∧ 0 < (𝐹‘𝑑))) → 𝐵 ∈
ℝ+) |
222 | 221 | rpgt0d 11751 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+
∧ 0 < (𝐹‘𝑑))) → 0 < 𝐵) |
223 | 222 | 3anassrs 1282 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 < 𝐵) |
224 | 90, 43, 91 | mul2lt0rgt0 11809 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐴 < 0) |
225 | 220, 223,
224 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 𝐴 < 0) |
226 | 85, 225 | syl5eqbrr 4619 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (𝐶‘0) < 0) |
227 | 219, 226 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (𝐹‘0) < 0) |
228 | | simpr 476 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → 0 < (𝐹‘𝑑)) |
229 | 227, 228 | jca 553 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → ((𝐹‘0) < 0 ∧ 0 < (𝐹‘𝑑))) |
230 | 209, 211,
209, 212, 214, 215, 218, 229 | ivth 23030 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → ∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0) |
231 | 210, 110,
111 | 3syl 18 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → (∃𝑧 ∈ (0(,)𝑑)(𝐹‘𝑧) = 0 → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0)) |
232 | 230, 231 | mpd 15 |
. . . 4
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ 0 < (𝐹‘𝑑)) → ∃𝑧 ∈ ℝ+
(𝐹‘𝑧) = 0) |
233 | 208, 232 | syldan 486 |
. . 3
⊢ ((((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
∧ ∀𝑓 ∈
ℝ+ (𝑑 ≤
𝑓 →
(abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0) |
234 | 169 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒)) |
235 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) → 𝐵 ∈
ℝ+) |
236 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵) |
237 | 236 | breq2d 4595 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → ((abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒 ↔ (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) |
238 | 237 | imbi2d 329 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → ((𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵))) |
239 | 238 | rexralbidv 3040 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → (∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵))) |
240 | 235, 239 | rspcdv 3285 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
(∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑓 ∈ ℝ+
(𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵))) |
241 | 234, 240 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑓 ∈ ℝ+ (𝑑 ≤ 𝑓 → (abs‘(((𝐹‘𝑓) / (𝑓↑𝐷)) − 𝐵)) < 𝐵)) |
242 | 233, 241 | r19.29a 3060 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ (𝐹‘𝑧) = 0) |
243 | | signsply0.2 |
. . . . 5
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
244 | 24, 38 | dgreq0 23825 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹 =
0𝑝 ↔ (𝐶‘𝐷) = 0)) |
245 | 19, 244 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐶‘𝐷) = 0)) |
246 | 245 | necon3bid 2826 |
. . . . 5
⊢ (𝜑 → (𝐹 ≠ 0𝑝 ↔ (𝐶‘𝐷) ≠ 0)) |
247 | 243, 246 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝐶‘𝐷) ≠ 0) |
248 | 36 | neeq1i 2846 |
. . . 4
⊢ (𝐵 ≠ 0 ↔ (𝐶‘𝐷) ≠ 0) |
249 | 247, 248 | sylibr 223 |
. . 3
⊢ (𝜑 → 𝐵 ≠ 0) |
250 | | rpneg 11739 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐵 ∈ ℝ+
↔ ¬ -𝐵 ∈
ℝ+)) |
251 | 250 | biimprd 237 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (¬ -𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ+)) |
252 | 251 | orrd 392 |
. . 3
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (-𝐵 ∈ ℝ+ ∨
𝐵 ∈
ℝ+)) |
253 | 43, 249, 252 | syl2anc 691 |
. 2
⊢ (𝜑 → (-𝐵 ∈ ℝ+ ∨ 𝐵 ∈
ℝ+)) |
254 | 177, 242,
253 | mpjaodan 823 |
1
⊢ (𝜑 → ∃𝑧 ∈ ℝ+ (𝐹‘𝑧) = 0) |