Step | Hyp | Ref
| Expression |
1 | | fltltc.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℕ) |
2 | 1 | nnred 11971 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
3 | | fltltc.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) |
4 | | eluzge3nn 12612 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
5 | | nnm1nn0 12257 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
6 | 3, 4, 5 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
7 | 2, 6 | reexpcld 13862 |
. . . . 5
⊢ (𝜑 → (𝐶↑(𝑁 − 1)) ∈
ℝ) |
8 | 6 | nn0red 12277 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
9 | | fltltc.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℕ) |
10 | 9 | nnred 11971 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
11 | 10, 6 | reexpcld 13862 |
. . . . . 6
⊢ (𝜑 → (𝐵↑(𝑁 − 1)) ∈
ℝ) |
12 | 8, 11 | remulcld 10989 |
. . . . 5
⊢ (𝜑 → ((𝑁 − 1) · (𝐵↑(𝑁 − 1))) ∈
ℝ) |
13 | 7, 12 | readdcld 10988 |
. . . 4
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1)))) ∈
ℝ) |
14 | | fzofi 13675 |
. . . . . 6
⊢
(0..^𝑁) ∈
Fin |
15 | 14 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0..^𝑁) ∈ Fin) |
16 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ) |
17 | | elfzonn0 13413 |
. . . . . . . 8
⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ ℕ0) |
18 | 17 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ ℕ0) |
19 | 16, 18 | reexpcld 13862 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (𝐶↑𝑘) ∈ ℝ) |
20 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ) |
21 | | fzonnsub 13393 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0..^𝑁) → (𝑁 − 𝑘) ∈ ℕ) |
22 | 21 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (𝑁 − 𝑘) ∈ ℕ) |
23 | | nnm1nn0 12257 |
. . . . . . . 8
⊢ ((𝑁 − 𝑘) ∈ ℕ → ((𝑁 − 𝑘) − 1) ∈
ℕ0) |
24 | 22, 23 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → ((𝑁 − 𝑘) − 1) ∈
ℕ0) |
25 | 20, 24 | reexpcld 13862 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈
ℝ) |
26 | 19, 25 | remulcld 10989 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈
ℝ) |
27 | 15, 26 | fsumrecl 15427 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (0..^𝑁)((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈
ℝ) |
28 | | fltltc.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℕ) |
29 | | fltltc.1 |
. . . . . 6
⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) |
30 | 28, 9, 1, 3, 29 | fltltc 40478 |
. . . . 5
⊢ (𝜑 → 𝐵 < 𝐶) |
31 | | difrp 12750 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 ↔ (𝐶 − 𝐵) ∈
ℝ+)) |
32 | 10, 2, 31 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐶 − 𝐵) ∈
ℝ+)) |
33 | 30, 32 | mpbid 231 |
. . . 4
⊢ (𝜑 → (𝐶 − 𝐵) ∈
ℝ+) |
34 | | fzofi 13675 |
. . . . . . . . . 10
⊢
(0..^(𝑁 − 1))
∈ Fin |
35 | 34 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(𝑁 − 1)) ∈ Fin) |
36 | 2 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → 𝐶 ∈ ℝ) |
37 | | elfzonn0 13413 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0..^(𝑁 − 1)) → 𝑘 ∈ ℕ0) |
38 | 37 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → 𝑘 ∈ ℕ0) |
39 | 36, 38 | reexpcld 13862 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → (𝐶↑𝑘) ∈ ℝ) |
40 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → 𝐵 ∈ ℝ) |
41 | | fzonnsub 13393 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0..^(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ) |
42 | 41 | nnnn0d 12276 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0..^(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈
ℕ0) |
43 | 42 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → ((𝑁 − 1) − 𝑘) ∈
ℕ0) |
44 | 40, 43 | reexpcld 13862 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → (𝐵↑((𝑁 − 1) − 𝑘)) ∈ ℝ) |
45 | 39, 44 | remulcld 10989 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → ((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) ∈ ℝ) |
46 | 35, 45 | fsumrecl 15427 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) ∈ ℝ) |
47 | | fzofi 13675 |
. . . . . . . . . . . . . 14
⊢
(0..^((𝑁 − 1)
− 1)) ∈ Fin |
48 | 47 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0..^((𝑁 − 1) − 1)) ∈
Fin) |
49 | 10 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 𝐵 ∈
ℝ) |
50 | | elfzonn0 13413 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0..^((𝑁 − 1) − 1)) → 𝑘 ∈
ℕ0) |
51 | 50 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 𝑘 ∈
ℕ0) |
52 | 49, 51 | reexpcld 13862 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → (𝐵↑𝑘) ∈ ℝ) |
53 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 𝑘 ∈ (0..^((𝑁 − 1) − 1))) |
54 | | 1nn0 12232 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ0 |
55 | | elfzoext 13425 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ (0..^((𝑁 − 1) − 1)) ∧ 1 ∈
ℕ0) → 𝑘 ∈ (0..^(((𝑁 − 1) − 1) +
1))) |
56 | 53, 54, 55 | sylancl 585 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 𝑘 ∈ (0..^(((𝑁 − 1) − 1) +
1))) |
57 | | nnnn0 12223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
58 | 3, 4, 57 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
59 | 58 | nn0cnd 12278 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ ℂ) |
60 | | 1cnd 10954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ∈
ℂ) |
61 | 59, 60 | subcld 11315 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
62 | 61, 60 | npcand 11319 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1)) |
63 | 62 | oveq2d 7284 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (0..^(((𝑁 − 1) − 1) + 1)) = (0..^(𝑁 − 1))) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) →
(0..^(((𝑁 − 1)
− 1) + 1)) = (0..^(𝑁
− 1))) |
65 | 56, 64 | eleqtrd 2842 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 𝑘 ∈ (0..^(𝑁 − 1))) |
66 | 65, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → ((𝑁 − 1) − 𝑘) ∈
ℕ0) |
67 | 49, 66 | reexpcld 13862 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → (𝐵↑((𝑁 − 1) − 𝑘)) ∈ ℝ) |
68 | 52, 67 | remulcld 10989 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → ((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) ∈ ℝ) |
69 | 48, 68 | fsumrecl 15427 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) ∈ ℝ) |
70 | | sub1m1 12208 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
71 | 59, 70 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
72 | | uz3m2nn 12613 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
73 | 3, 72 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 2) ∈ ℕ) |
74 | 71, 73 | eqeltrd 2840 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 − 1) − 1) ∈
ℕ) |
75 | 74 | nnnn0d 12276 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) − 1) ∈
ℕ0) |
76 | 10, 75 | reexpcld 13862 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵↑((𝑁 − 1) − 1)) ∈
ℝ) |
77 | 76, 10 | remulcld 10989 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵↑((𝑁 − 1) − 1)) · 𝐵) ∈
ℝ) |
78 | 69, 77 | readdcld 10988 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐵↑((𝑁 − 1) − 1)) · 𝐵)) ∈
ℝ) |
79 | 2 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 𝐶 ∈
ℝ) |
80 | 79, 51 | reexpcld 13862 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → (𝐶↑𝑘) ∈ ℝ) |
81 | 80, 67 | remulcld 10989 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → ((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) ∈ ℝ) |
82 | 48, 81 | fsumrecl 15427 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) ∈ ℝ) |
83 | 2, 75 | reexpcld 13862 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶↑((𝑁 − 1) − 1)) ∈
ℝ) |
84 | 83, 10 | remulcld 10989 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶↑((𝑁 − 1) − 1)) · 𝐵) ∈
ℝ) |
85 | 82, 84 | readdcld 10988 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐶↑((𝑁 − 1) − 1)) · 𝐵)) ∈
ℝ) |
86 | 9 | nncnd 11972 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ ℂ) |
87 | | uzuzle23 12611 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
88 | 3, 87 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) |
89 | | uz2m1nn 12645 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 1) ∈ ℕ) |
91 | | expm1t 13792 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ)
→ (𝐵↑(𝑁 − 1)) = ((𝐵↑((𝑁 − 1) − 1)) · 𝐵)) |
92 | 86, 90, 91 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵↑(𝑁 − 1)) = ((𝐵↑((𝑁 − 1) − 1)) · 𝐵)) |
93 | 92 | eqcomd 2745 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵↑((𝑁 − 1) − 1)) · 𝐵) = (𝐵↑(𝑁 − 1))) |
94 | 93 | oveq2d 7284 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝑁 − 1) − 1) · (𝐵↑(𝑁 − 1))) + ((𝐵↑((𝑁 − 1) − 1)) · 𝐵)) = ((((𝑁 − 1) − 1) · (𝐵↑(𝑁 − 1))) + (𝐵↑(𝑁 − 1)))) |
95 | 61, 60 | subcld 11315 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 − 1) − 1) ∈
ℂ) |
96 | 86, 6 | expcld 13845 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵↑(𝑁 − 1)) ∈
ℂ) |
97 | 95, 96 | adddirp1d 10985 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝑁 − 1) − 1) + 1) · (𝐵↑(𝑁 − 1))) = ((((𝑁 − 1) − 1) · (𝐵↑(𝑁 − 1))) + (𝐵↑(𝑁 − 1)))) |
98 | 62 | oveq1d 7283 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝑁 − 1) − 1) + 1) · (𝐵↑(𝑁 − 1))) = ((𝑁 − 1) · (𝐵↑(𝑁 − 1)))) |
99 | 94, 97, 98 | 3eqtr2rd 2786 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 − 1) · (𝐵↑(𝑁 − 1))) = ((((𝑁 − 1) − 1) · (𝐵↑(𝑁 − 1))) + ((𝐵↑((𝑁 − 1) − 1)) · 𝐵))) |
100 | 12, 99 | eqled 11061 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) · (𝐵↑(𝑁 − 1))) ≤ ((((𝑁 − 1) − 1) · (𝐵↑(𝑁 − 1))) + ((𝐵↑((𝑁 − 1) − 1)) · 𝐵))) |
101 | 37 | nn0cnd 12278 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (0..^(𝑁 − 1)) → 𝑘 ∈ ℂ) |
102 | 65, 101 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 𝑘 ∈
ℂ) |
103 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → (𝑁 − 1) ∈
ℂ) |
104 | 102, 103 | pncan3d 11318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → (𝑘 + ((𝑁 − 1) − 𝑘)) = (𝑁 − 1)) |
105 | 104 | oveq2d 7284 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → (𝐵↑(𝑘 + ((𝑁 − 1) − 𝑘))) = (𝐵↑(𝑁 − 1))) |
106 | 105 | sumeq2dv 15396 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))(𝐵↑(𝑘 + ((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))(𝐵↑(𝑁 − 1))) |
107 | 86 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 𝐵 ∈
ℂ) |
108 | 107, 66, 51 | expaddd 13847 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → (𝐵↑(𝑘 + ((𝑁 − 1) − 𝑘))) = ((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘)))) |
109 | 108 | sumeq2dv 15396 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))(𝐵↑(𝑘 + ((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘)))) |
110 | | fsumconst 15483 |
. . . . . . . . . . . . . . . 16
⊢
(((0..^((𝑁 −
1) − 1)) ∈ Fin ∧ (𝐵↑(𝑁 − 1)) ∈ ℂ) →
Σ𝑘 ∈
(0..^((𝑁 − 1) −
1))(𝐵↑(𝑁 − 1)) =
((♯‘(0..^((𝑁
− 1) − 1))) · (𝐵↑(𝑁 − 1)))) |
111 | 48, 96, 110 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))(𝐵↑(𝑁 − 1)) = ((♯‘(0..^((𝑁 − 1) − 1)))
· (𝐵↑(𝑁 − 1)))) |
112 | | hashfzo0 14126 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 − 1) − 1) ∈
ℕ0 → (♯‘(0..^((𝑁 − 1) − 1))) = ((𝑁 − 1) −
1)) |
113 | 75, 112 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(♯‘(0..^((𝑁
− 1) − 1))) = ((𝑁 − 1) − 1)) |
114 | 113 | oveq1d 7283 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
((♯‘(0..^((𝑁
− 1) − 1))) · (𝐵↑(𝑁 − 1))) = (((𝑁 − 1) − 1) · (𝐵↑(𝑁 − 1)))) |
115 | 111, 114 | eqtrd 2779 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))(𝐵↑(𝑁 − 1)) = (((𝑁 − 1) − 1) · (𝐵↑(𝑁 − 1)))) |
116 | 106, 109,
115 | 3eqtr3d 2787 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) = (((𝑁 − 1) − 1) · (𝐵↑(𝑁 − 1)))) |
117 | 116 | oveq1d 7283 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐵↑((𝑁 − 1) − 1)) · 𝐵)) = ((((𝑁 − 1) − 1) · (𝐵↑(𝑁 − 1))) + ((𝐵↑((𝑁 − 1) − 1)) · 𝐵))) |
118 | 100, 117 | breqtrrd 5106 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) · (𝐵↑(𝑁 − 1))) ≤ (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐵↑((𝑁 − 1) − 1)) · 𝐵))) |
119 | 9 | nnrpd 12752 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
120 | 119 | rpge0d 12758 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ 𝐵) |
121 | 120 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 0 ≤ 𝐵) |
122 | 49, 66, 121 | expge0d 13863 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 0 ≤
(𝐵↑((𝑁 − 1) − 𝑘))) |
123 | 10, 2, 30 | ltled 11106 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ≤ 𝐶) |
124 | 123 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → 𝐵 ≤ 𝐶) |
125 | | leexp1a 13874 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
∧ (0 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → (𝐵↑𝑘) ≤ (𝐶↑𝑘)) |
126 | 49, 79, 51, 121, 124, 125 | syl32anc 1376 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → (𝐵↑𝑘) ≤ (𝐶↑𝑘)) |
127 | 52, 80, 67, 122, 126 | lemul1ad 11897 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^((𝑁 − 1) − 1))) → ((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) ≤ ((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘)))) |
128 | 48, 68, 81, 127 | fsumle 15492 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) ≤ Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘)))) |
129 | 1 | nnrpd 12752 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
130 | 119, 129,
74, 30 | ltexp1dd 40303 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵↑((𝑁 − 1) − 1)) < (𝐶↑((𝑁 − 1) − 1))) |
131 | 76, 83, 119, 130 | ltmul1dd 12809 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵↑((𝑁 − 1) − 1)) · 𝐵) < ((𝐶↑((𝑁 − 1) − 1)) · 𝐵)) |
132 | 69, 77, 82, 84, 128, 131 | leltaddd 11580 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐵↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐵↑((𝑁 − 1) − 1)) · 𝐵)) < (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐶↑((𝑁 − 1) − 1)) · 𝐵))) |
133 | 12, 78, 85, 118, 132 | lelttrd 11116 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − 1) · (𝐵↑(𝑁 − 1))) < (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐶↑((𝑁 − 1) − 1)) · 𝐵))) |
134 | 61, 60 | nncand 11320 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) − ((𝑁 − 1) − 1)) =
1) |
135 | 134 | oveq2d 7284 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵↑((𝑁 − 1) − ((𝑁 − 1) − 1))) = (𝐵↑1)) |
136 | 86 | exp1d 13840 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵↑1) = 𝐵) |
137 | 135, 136 | eqtrd 2779 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵↑((𝑁 − 1) − ((𝑁 − 1) − 1))) = 𝐵) |
138 | 137 | oveq2d 7284 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶↑((𝑁 − 1) − 1)) · (𝐵↑((𝑁 − 1) − ((𝑁 − 1) − 1)))) = ((𝐶↑((𝑁 − 1) − 1)) · 𝐵)) |
139 | 138 | oveq2d 7284 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐶↑((𝑁 − 1) − 1)) · (𝐵↑((𝑁 − 1) − ((𝑁 − 1) − 1))))) = (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐶↑((𝑁 − 1) − 1)) · 𝐵))) |
140 | 133, 139 | breqtrrd 5106 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) · (𝐵↑(𝑁 − 1))) < (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐶↑((𝑁 − 1) − 1)) · (𝐵↑((𝑁 − 1) − ((𝑁 − 1) − 1)))))) |
141 | | 0zd 12314 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℤ) |
142 | 141 | peano2zd 12411 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 + 1) ∈
ℤ) |
143 | | 0cn 10951 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℂ |
144 | | ax-1cn 10913 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
145 | 143, 144,
144 | addassi 10969 |
. . . . . . . . . . . . . . . 16
⊢ ((0 + 1)
+ 1) = (0 + (1 + 1)) |
146 | 144, 144 | addcli 10965 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + 1)
∈ ℂ |
147 | 146 | addid2i 11146 |
. . . . . . . . . . . . . . . 16
⊢ (0 + (1 +
1)) = (1 + 1) |
148 | | 1p1e2 12081 |
. . . . . . . . . . . . . . . 16
⊢ (1 + 1) =
2 |
149 | 145, 147,
148 | 3eqtri 2771 |
. . . . . . . . . . . . . . 15
⊢ ((0 + 1)
+ 1) = 2 |
150 | 149 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((0 + 1) + 1) =
2) |
151 | 150 | fveq2d 6772 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘((0 + 1) + 1)) =
(ℤ≥‘2)) |
152 | 88, 151 | eleqtrrd 2843 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘((0 +
1) + 1))) |
153 | | eluzp1m1 12590 |
. . . . . . . . . . . 12
⊢ (((0 + 1)
∈ ℤ ∧ 𝑁
∈ (ℤ≥‘((0 + 1) + 1))) → (𝑁 − 1) ∈
(ℤ≥‘(0 + 1))) |
154 | 142, 152,
153 | syl2anc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘(0 + 1))) |
155 | | eluzp1m1 12590 |
. . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ (𝑁
− 1) ∈ (ℤ≥‘(0 + 1))) → ((𝑁 − 1) − 1) ∈
(ℤ≥‘0)) |
156 | 141, 154,
155 | syl2anc 583 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − 1) − 1) ∈
(ℤ≥‘0)) |
157 | 1 | nncnd 11972 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℂ) |
158 | 157 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → 𝐶 ∈ ℂ) |
159 | 158, 38 | expcld 13845 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → (𝐶↑𝑘) ∈ ℂ) |
160 | 86 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → 𝐵 ∈ ℂ) |
161 | 160, 43 | expcld 13845 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → (𝐵↑((𝑁 − 1) − 𝑘)) ∈ ℂ) |
162 | 159, 161 | mulcld 10979 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → ((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) ∈ ℂ) |
163 | | oveq2 7276 |
. . . . . . . . . . 11
⊢ (𝑘 = ((𝑁 − 1) − 1) → (𝐶↑𝑘) = (𝐶↑((𝑁 − 1) − 1))) |
164 | | oveq2 7276 |
. . . . . . . . . . . 12
⊢ (𝑘 = ((𝑁 − 1) − 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − ((𝑁 − 1) − 1))) |
165 | 164 | oveq2d 7284 |
. . . . . . . . . . 11
⊢ (𝑘 = ((𝑁 − 1) − 1) → (𝐵↑((𝑁 − 1) − 𝑘)) = (𝐵↑((𝑁 − 1) − ((𝑁 − 1) − 1)))) |
166 | 163, 165 | oveq12d 7286 |
. . . . . . . . . 10
⊢ (𝑘 = ((𝑁 − 1) − 1) → ((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) = ((𝐶↑((𝑁 − 1) − 1)) · (𝐵↑((𝑁 − 1) − ((𝑁 − 1) − 1))))) |
167 | 6 | nn0zd 12406 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
168 | 156, 162,
166, 167 | fzosumm1 40198 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0..^((𝑁 − 1) − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + ((𝐶↑((𝑁 − 1) − 1)) · (𝐵↑((𝑁 − 1) − ((𝑁 − 1) − 1)))))) |
169 | 140, 168 | breqtrrd 5106 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 1) · (𝐵↑(𝑁 − 1))) < Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘)))) |
170 | 12, 46, 7, 169 | ltadd2dd 11117 |
. . . . . . 7
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1)))) < ((𝐶↑(𝑁 − 1)) + Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))))) |
171 | 35, 162 | fsumcl 15426 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) ∈ ℂ) |
172 | 157, 6 | expcld 13845 |
. . . . . . . 8
⊢ (𝜑 → (𝐶↑(𝑁 − 1)) ∈
ℂ) |
173 | 171, 172 | addcomd 11160 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + (𝐶↑(𝑁 − 1))) = ((𝐶↑(𝑁 − 1)) + Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))))) |
174 | 170, 173 | breqtrrd 5106 |
. . . . . 6
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1)))) < (Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + (𝐶↑(𝑁 − 1)))) |
175 | 59 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ ℂ) |
176 | 101 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → 𝑘 ∈ ℂ) |
177 | | 1cnd 10954 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → 1 ∈
ℂ) |
178 | 175, 176,
177 | sub32d 11347 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → ((𝑁 − 𝑘) − 1) = ((𝑁 − 1) − 𝑘)) |
179 | 178 | oveq2d 7284 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − 1) − 𝑘))) |
180 | 179 | oveq2d 7284 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(𝑁 − 1))) → ((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘)))) |
181 | 180 | sumeq2dv 15396 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘)))) |
182 | 59, 59, 60 | nnncand 11348 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − (𝑁 − 1)) − 1) = (𝑁 − 𝑁)) |
183 | 59 | subidd 11303 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − 𝑁) = 0) |
184 | 182, 183 | eqtrd 2779 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − (𝑁 − 1)) − 1) =
0) |
185 | 184 | oveq2d 7284 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) = (𝐵↑0)) |
186 | 86 | exp0d 13839 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵↑0) = 1) |
187 | 185, 186 | eqtrd 2779 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵↑((𝑁 − (𝑁 − 1)) − 1)) =
1) |
188 | 187 | oveq2d 7284 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = ((𝐶↑(𝑁 − 1)) · 1)) |
189 | 7 | recnd 10987 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶↑(𝑁 − 1)) ∈
ℂ) |
190 | 189 | mulid1d 10976 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) · 1) = (𝐶↑(𝑁 − 1))) |
191 | 188, 190 | eqtrd 2779 |
. . . . . . 7
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) = (𝐶↑(𝑁 − 1))) |
192 | 181, 191 | oveq12d 7286 |
. . . . . 6
⊢ (𝜑 → (Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐶↑(𝑁 − 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) = (Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 1) − 𝑘))) + (𝐶↑(𝑁 − 1)))) |
193 | 174, 192 | breqtrrd 5106 |
. . . . 5
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1)))) < (Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐶↑(𝑁 − 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))))) |
194 | | elnn0uz 12605 |
. . . . . . 7
⊢ ((𝑁 − 1) ∈
ℕ0 ↔ (𝑁 − 1) ∈
(ℤ≥‘0)) |
195 | 6, 194 | sylib 217 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘0)) |
196 | 157 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝐶 ∈ ℂ) |
197 | 196, 18 | expcld 13845 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (𝐶↑𝑘) ∈ ℂ) |
198 | 86 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝐵 ∈ ℂ) |
199 | 198, 24 | expcld 13845 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵↑((𝑁 − 𝑘) − 1)) ∈
ℂ) |
200 | 197, 199 | mulcld 10979 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) ∈
ℂ) |
201 | | oveq2 7276 |
. . . . . . 7
⊢ (𝑘 = (𝑁 − 1) → (𝐶↑𝑘) = (𝐶↑(𝑁 − 1))) |
202 | | oveq2 7276 |
. . . . . . . . 9
⊢ (𝑘 = (𝑁 − 1) → (𝑁 − 𝑘) = (𝑁 − (𝑁 − 1))) |
203 | 202 | oveq1d 7283 |
. . . . . . . 8
⊢ (𝑘 = (𝑁 − 1) → ((𝑁 − 𝑘) − 1) = ((𝑁 − (𝑁 − 1)) − 1)) |
204 | 203 | oveq2d 7284 |
. . . . . . 7
⊢ (𝑘 = (𝑁 − 1) → (𝐵↑((𝑁 − 𝑘) − 1)) = (𝐵↑((𝑁 − (𝑁 − 1)) − 1))) |
205 | 201, 204 | oveq12d 7286 |
. . . . . 6
⊢ (𝑘 = (𝑁 − 1) → ((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = ((𝐶↑(𝑁 − 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1)))) |
206 | 58 | nn0zd 12406 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
207 | 195, 200,
205, 206 | fzosumm1 40198 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0..^𝑁)((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) = (Σ𝑘 ∈ (0..^(𝑁 − 1))((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))) + ((𝐶↑(𝑁 − 1)) · (𝐵↑((𝑁 − (𝑁 − 1)) − 1))))) |
208 | 193, 207 | breqtrrd 5106 |
. . . 4
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1)))) < Σ𝑘 ∈ (0..^𝑁)((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1)))) |
209 | 13, 27, 33, 208 | ltmul2dd 12810 |
. . 3
⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < ((𝐶 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) |
210 | | pwdif 15561 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐶 ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ ((𝐶↑𝑁) − (𝐵↑𝑁)) = ((𝐶 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) |
211 | 58, 157, 86, 210 | syl3anc 1369 |
. . 3
⊢ (𝜑 → ((𝐶↑𝑁) − (𝐵↑𝑁)) = ((𝐶 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐶↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) |
212 | 209, 211 | breqtrrd 5106 |
. 2
⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < ((𝐶↑𝑁) − (𝐵↑𝑁))) |
213 | 28 | nncnd 11972 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℂ) |
214 | 213, 58 | expcld 13845 |
. . 3
⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ) |
215 | 86, 58 | expcld 13845 |
. . 3
⊢ (𝜑 → (𝐵↑𝑁) ∈ ℂ) |
216 | 214, 215,
29 | mvlraddd 11368 |
. 2
⊢ (𝜑 → (𝐴↑𝑁) = ((𝐶↑𝑁) − (𝐵↑𝑁))) |
217 | 212, 216 | breqtrrd 5106 |
1
⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < (𝐴↑𝑁)) |