Step | Hyp | Ref
| Expression |
1 | | ftalem.1 |
. . 3
⊢ 𝐴 = (coeff‘𝐹) |
2 | | ftalem.2 |
. . 3
⊢ 𝑁 = (deg‘𝐹) |
3 | | ftalem.3 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
4 | | ftalem.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | 1 | coef3 23988 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
6 | 3, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
7 | 4 | nnnn0d 11351 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
8 | 6, 7 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐴‘𝑁) ∈ ℂ) |
9 | 4 | nnne0d 11065 |
. . . . . 6
⊢ (𝜑 → 𝑁 ≠ 0) |
10 | 2, 1 | dgreq0 24021 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0)) |
11 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
(deg‘0𝑝)) |
12 | | dgr0 24018 |
. . . . . . . . . . 11
⊢
(deg‘0𝑝) = 0 |
13 | 11, 12 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
0) |
14 | 2, 13 | syl5eq 2668 |
. . . . . . . . 9
⊢ (𝐹 = 0𝑝 →
𝑁 = 0) |
15 | 10, 14 | syl6bir 244 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘𝑆) → ((𝐴‘𝑁) = 0 → 𝑁 = 0)) |
16 | 3, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐴‘𝑁) = 0 → 𝑁 = 0)) |
17 | 16 | necon3d 2815 |
. . . . . 6
⊢ (𝜑 → (𝑁 ≠ 0 → (𝐴‘𝑁) ≠ 0)) |
18 | 9, 17 | mpd 15 |
. . . . 5
⊢ (𝜑 → (𝐴‘𝑁) ≠ 0) |
19 | 8, 18 | absrpcld 14187 |
. . . 4
⊢ (𝜑 → (abs‘(𝐴‘𝑁)) ∈
ℝ+) |
20 | 19 | rphalfcld 11884 |
. . 3
⊢ (𝜑 → ((abs‘(𝐴‘𝑁)) / 2) ∈
ℝ+) |
21 | | fveq2 6191 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘)) |
22 | 21 | fveq2d 6195 |
. . . . 5
⊢ (𝑛 = 𝑘 → (abs‘(𝐴‘𝑛)) = (abs‘(𝐴‘𝑘))) |
23 | 22 | cbvsumv 14426 |
. . . 4
⊢
Σ𝑛 ∈
(0...(𝑁 −
1))(abs‘(𝐴‘𝑛)) = Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) |
24 | 23 | oveq1i 6660 |
. . 3
⊢
(Σ𝑛 ∈
(0...(𝑁 −
1))(abs‘(𝐴‘𝑛)) / ((abs‘(𝐴‘𝑁)) / 2)) = (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / ((abs‘(𝐴‘𝑁)) / 2)) |
25 | 1, 2, 3, 4, 20, 24 | ftalem1 24799 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ ℝ ∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))) |
26 | | ftalem2.5 |
. . . . . 6
⊢ 𝑈 = if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)) |
27 | | ftalem2.6 |
. . . . . . . . 9
⊢ 𝑇 = ((abs‘(𝐹‘0)) / ((abs‘(𝐴‘𝑁)) / 2)) |
28 | | plyf 23954 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
29 | 3, 28 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
30 | | 0cn 10032 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
31 | | ffvelrn 6357 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℂ⟶ℂ ∧ 0
∈ ℂ) → (𝐹‘0) ∈ ℂ) |
32 | 29, 30, 31 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘0) ∈ ℂ) |
33 | 32 | abscld 14175 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝐹‘0)) ∈
ℝ) |
34 | 33, 20 | rerpdivcld 11903 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘(𝐹‘0)) / ((abs‘(𝐴‘𝑁)) / 2)) ∈ ℝ) |
35 | 27, 34 | syl5eqel 2705 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ ℝ) |
36 | 35 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑇 ∈ ℝ) |
37 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℝ) |
38 | | 1re 10039 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
39 | | ifcl 4130 |
. . . . . . . 8
⊢ ((𝑠 ∈ ℝ ∧ 1 ∈
ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ∈ ℝ) |
40 | 37, 38, 39 | sylancl 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ∈ ℝ) |
41 | 36, 40 | ifcld 4131 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)) ∈ ℝ) |
42 | 26, 41 | syl5eqel 2705 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑈 ∈ ℝ) |
43 | | 0red 10041 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 0 ∈
ℝ) |
44 | | 1red 10055 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 1 ∈
ℝ) |
45 | | 0lt1 10550 |
. . . . . . 7
⊢ 0 <
1 |
46 | 45 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 0 <
1) |
47 | | max1 12016 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 𝑠
∈ ℝ) → 1 ≤ if(1 ≤ 𝑠, 𝑠, 1)) |
48 | 38, 37, 47 | sylancr 695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 1 ≤ if(1 ≤
𝑠, 𝑠, 1)) |
49 | | max1 12016 |
. . . . . . . . 9
⊢ ((if(1
≤ 𝑠, 𝑠, 1) ∈ ℝ ∧ 𝑇 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1))) |
50 | 40, 36, 49 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1))) |
51 | 50, 26 | syl6breqr 4695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑈) |
52 | 44, 40, 42, 48, 51 | letrd 10194 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 1 ≤ 𝑈) |
53 | 43, 44, 42, 46, 52 | ltletrd 10197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 0 < 𝑈) |
54 | 42, 53 | elrpd 11869 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑈 ∈
ℝ+) |
55 | | max2 12018 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 𝑠
∈ ℝ) → 𝑠
≤ if(1 ≤ 𝑠, 𝑠, 1)) |
56 | 38, 37, 55 | sylancr 695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑠 ≤ if(1 ≤ 𝑠, 𝑠, 1)) |
57 | 37, 40, 42, 56, 51 | letrd 10194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑠 ≤ 𝑈) |
58 | 57 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → 𝑠 ≤ 𝑈) |
59 | 37 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → 𝑠 ∈ ℝ) |
60 | 42 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → 𝑈 ∈ ℝ) |
61 | | abscl 14018 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(abs‘𝑥) ∈
ℝ) |
62 | 61 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → (abs‘𝑥) ∈
ℝ) |
63 | | lelttr 10128 |
. . . . . . . . 9
⊢ ((𝑠 ∈ ℝ ∧ 𝑈 ∈ ℝ ∧
(abs‘𝑥) ∈
ℝ) → ((𝑠 ≤
𝑈 ∧ 𝑈 < (abs‘𝑥)) → 𝑠 < (abs‘𝑥))) |
64 | 59, 60, 62, 63 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑠 ≤ 𝑈 ∧ 𝑈 < (abs‘𝑥)) → 𝑠 < (abs‘𝑥))) |
65 | 58, 64 | mpand 711 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → (𝑈 < (abs‘𝑥) → 𝑠 < (abs‘𝑥))) |
66 | 65 | imim1d 82 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑠 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → (𝑈 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))))) |
67 | 29 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝐹:ℂ⟶ℂ) |
68 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑥 ∈ ℂ) |
69 | 67, 68 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (𝐹‘𝑥) ∈ ℂ) |
70 | 8 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (𝐴‘𝑁) ∈ ℂ) |
71 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑁 ∈
ℕ0) |
72 | 68, 71 | expcld 13008 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (𝑥↑𝑁) ∈ ℂ) |
73 | 70, 72 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((𝐴‘𝑁) · (𝑥↑𝑁)) ∈ ℂ) |
74 | 69, 73 | subcld 10392 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))) ∈ ℂ) |
75 | 74 | abscld 14175 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) ∈ ℝ) |
76 | 73 | abscld 14175 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) ∈ ℝ) |
77 | 76 | rehalfcld 11279 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) ∈ ℝ) |
78 | 75, 77, 76 | ltsub2d 10637 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) ↔ ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))))) |
79 | 70, 72 | absmuld 14193 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) = ((abs‘(𝐴‘𝑁)) · (abs‘(𝑥↑𝑁)))) |
80 | 68, 71 | absexpd 14191 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝑥↑𝑁)) = ((abs‘𝑥)↑𝑁)) |
81 | 80 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐴‘𝑁)) · (abs‘(𝑥↑𝑁))) = ((abs‘(𝐴‘𝑁)) · ((abs‘𝑥)↑𝑁))) |
82 | 79, 81 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) = ((abs‘(𝐴‘𝑁)) · ((abs‘𝑥)↑𝑁))) |
83 | 82 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) = (((abs‘(𝐴‘𝑁)) · ((abs‘𝑥)↑𝑁)) / 2)) |
84 | 70 | abscld 14175 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐴‘𝑁)) ∈ ℝ) |
85 | 84 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐴‘𝑁)) ∈ ℂ) |
86 | 62 | adantrr 753 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘𝑥) ∈ ℝ) |
87 | 86, 71 | reexpcld 13025 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) ∈ ℝ) |
88 | 87 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) ∈ ℂ) |
89 | | 2cnd 11093 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 2 ∈ ℂ) |
90 | | 2ne0 11113 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
91 | 90 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 2 ≠ 0) |
92 | 85, 88, 89, 91 | div23d 10838 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴‘𝑁)) · ((abs‘𝑥)↑𝑁)) / 2) = (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) |
93 | 83, 92 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) = (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) |
94 | 93 | breq2d 4665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) ↔ (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))) |
95 | 76 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) ∈ ℂ) |
96 | 95 | 2halvesd 11278 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) + ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) = (abs‘((𝐴‘𝑁) · (𝑥↑𝑁)))) |
97 | 96 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) + ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) − ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) = ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2))) |
98 | 77 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) ∈ ℂ) |
99 | 98, 98 | pncand 10393 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) + ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) − ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) = ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) |
100 | 97, 99 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) = ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) |
101 | 100 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))) ↔ ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))))) |
102 | 78, 94, 101 | 3bitr3d 298 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) ↔ ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))))) |
103 | 73, 69 | subcld 10392 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((𝐴‘𝑁) · (𝑥↑𝑁)) − (𝐹‘𝑥)) ∈ ℂ) |
104 | 73, 103 | abs2difd 14196 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘(((𝐴‘𝑁) · (𝑥↑𝑁)) − (𝐹‘𝑥)))) ≤ (abs‘(((𝐴‘𝑁) · (𝑥↑𝑁)) − (((𝐴‘𝑁) · (𝑥↑𝑁)) − (𝐹‘𝑥))))) |
105 | 73, 69 | abssubd 14192 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(((𝐴‘𝑁) · (𝑥↑𝑁)) − (𝐹‘𝑥))) = (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))) |
106 | 105 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘(((𝐴‘𝑁) · (𝑥↑𝑁)) − (𝐹‘𝑥)))) = ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))))) |
107 | 73, 69 | nncand 10397 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((𝐴‘𝑁) · (𝑥↑𝑁)) − (((𝐴‘𝑁) · (𝑥↑𝑁)) − (𝐹‘𝑥))) = (𝐹‘𝑥)) |
108 | 107 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(((𝐴‘𝑁) · (𝑥↑𝑁)) − (((𝐴‘𝑁) · (𝑥↑𝑁)) − (𝐹‘𝑥)))) = (abs‘(𝐹‘𝑥))) |
109 | 104, 106,
108 | 3brtr3d 4684 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))) ≤ (abs‘(𝐹‘𝑥))) |
110 | 76, 75 | resubcld 10458 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))) ∈ ℝ) |
111 | 69 | abscld 14175 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
112 | | ltletr 10129 |
. . . . . . . . . . . 12
⊢
((((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) ∈ ℝ ∧
((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))) ∈ ℝ ∧ (abs‘(𝐹‘𝑥)) ∈ ℝ) →
((((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))) ∧ ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))) ≤ (abs‘(𝐹‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < (abs‘(𝐹‘𝑥)))) |
113 | 77, 110, 111, 112 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))) ∧ ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))) ≤ (abs‘(𝐹‘𝑥))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < (abs‘(𝐹‘𝑥)))) |
114 | 109, 113 | mpan2d 710 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) − (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))))) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < (abs‘(𝐹‘𝑥)))) |
115 | 102, 114 | sylbid 230 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) → ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < (abs‘(𝐹‘𝑥)))) |
116 | 33 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) ∈ ℝ) |
117 | 20 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐴‘𝑁)) / 2) ∈
ℝ+) |
118 | 117 | rpred 11872 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐴‘𝑁)) / 2) ∈ ℝ) |
119 | 118, 86 | remulcld 10070 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴‘𝑁)) / 2) · (abs‘𝑥)) ∈
ℝ) |
120 | 93, 77 | eqeltrrd 2702 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) ∈ ℝ) |
121 | 36 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑇 ∈ ℝ) |
122 | 42 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑈 ∈ ℝ) |
123 | | max2 12018 |
. . . . . . . . . . . . . . . . . 18
⊢ ((if(1
≤ 𝑠, 𝑠, 1) ∈ ℝ ∧ 𝑇 ∈ ℝ) → 𝑇 ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1))) |
124 | 40, 36, 123 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑇 ≤ if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1))) |
125 | 124, 26 | syl6breqr 4695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑇 ≤ 𝑈) |
126 | 125 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑇 ≤ 𝑈) |
127 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑈 < (abs‘𝑥)) |
128 | 121, 122,
86, 126, 127 | lelttrd 10195 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑇 < (abs‘𝑥)) |
129 | 27, 128 | syl5eqbrr 4689 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘(𝐹‘0)) / ((abs‘(𝐴‘𝑁)) / 2)) < (abs‘𝑥)) |
130 | 116, 86, 117 | ltdivmuld 11923 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐹‘0)) / ((abs‘(𝐴‘𝑁)) / 2)) < (abs‘𝑥) ↔ (abs‘(𝐹‘0)) < (((abs‘(𝐴‘𝑁)) / 2) · (abs‘𝑥)))) |
131 | 129, 130 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) < (((abs‘(𝐴‘𝑁)) / 2) · (abs‘𝑥))) |
132 | 86 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘𝑥) ∈ ℂ) |
133 | 132 | exp1d 13003 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑1) = (abs‘𝑥)) |
134 | | 1red 10055 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 ∈ ℝ) |
135 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 ≤ 𝑈) |
136 | 134, 122,
86, 135, 127 | lelttrd 10195 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 < (abs‘𝑥)) |
137 | 134, 86, 136 | ltled 10185 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 1 ≤ (abs‘𝑥)) |
138 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑁 ∈ ℕ) |
139 | | nnuz 11723 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
140 | 138, 139 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → 𝑁 ∈
(ℤ≥‘1)) |
141 | 86, 137, 140 | leexp2ad 13041 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥)↑1) ≤ ((abs‘𝑥)↑𝑁)) |
142 | 133, 141 | eqbrtrrd 4677 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘𝑥) ≤ ((abs‘𝑥)↑𝑁)) |
143 | 86, 87, 117 | lemul2d 11916 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘𝑥) ≤ ((abs‘𝑥)↑𝑁) ↔ (((abs‘(𝐴‘𝑁)) / 2) · (abs‘𝑥)) ≤ (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁)))) |
144 | 142, 143 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐴‘𝑁)) / 2) · (abs‘𝑥)) ≤ (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) |
145 | 116, 119,
120, 131, 144 | ltletrd 10197 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) |
146 | 145, 93 | breqtrrd 4681 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (abs‘(𝐹‘0)) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2)) |
147 | | lttr 10114 |
. . . . . . . . . . 11
⊢
(((abs‘(𝐹‘0)) ∈ ℝ ∧
((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) ∈ ℝ ∧
(abs‘(𝐹‘𝑥)) ∈ ℝ) →
(((abs‘(𝐹‘0))
< ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) ∧ ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < (abs‘(𝐹‘𝑥))) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥)))) |
148 | 116, 77, 111, 147 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘(𝐹‘0)) < ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) ∧ ((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < (abs‘(𝐹‘𝑥))) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥)))) |
149 | 146, 148 | mpand 711 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → (((abs‘((𝐴‘𝑁) · (𝑥↑𝑁))) / 2) < (abs‘(𝐹‘𝑥)) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥)))) |
150 | 115, 149 | syld 47 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑈 < (abs‘𝑥))) → ((abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥)))) |
151 | 150 | expr 643 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → (𝑈 < (abs‘𝑥) → ((abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁)) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))))) |
152 | 151 | a2d 29 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑈 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))))) |
153 | 66, 152 | syld 47 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℂ) → ((𝑠 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))))) |
154 | 153 | ralimdva 2962 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → (∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → ∀𝑥 ∈ ℂ (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))))) |
155 | | breq1 4656 |
. . . . . . 7
⊢ (𝑟 = 𝑈 → (𝑟 < (abs‘𝑥) ↔ 𝑈 < (abs‘𝑥))) |
156 | 155 | imbi1d 331 |
. . . . . 6
⊢ (𝑟 = 𝑈 → ((𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))) ↔ (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))))) |
157 | 156 | ralbidv 2986 |
. . . . 5
⊢ (𝑟 = 𝑈 → (∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))) ↔ ∀𝑥 ∈ ℂ (𝑈 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))))) |
158 | 157 | rspcev 3309 |
. . . 4
⊢ ((𝑈 ∈ ℝ+
∧ ∀𝑥 ∈
ℂ (𝑈 <
(abs‘𝑥) →
(abs‘(𝐹‘0))
< (abs‘(𝐹‘𝑥)))) → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) <
(abs‘(𝐹‘𝑥)))) |
159 | 54, 154, 158 | syl6an 568 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → (∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) <
(abs‘(𝐹‘𝑥))))) |
160 | 159 | rexlimdva 3031 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ ℝ ∀𝑥 ∈ ℂ (𝑠 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (((abs‘(𝐴‘𝑁)) / 2) · ((abs‘𝑥)↑𝑁))) → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) <
(abs‘(𝐹‘𝑥))))) |
161 | 25, 160 | mpd 15 |
1
⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) <
(abs‘(𝐹‘𝑥)))) |