This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fltnltalem

Description: Lemma for fltnlta . A lower bound for A based on pwdif . (Contributed by Steven Nguyen, 22-Aug-2023)

Ref Expression
Hypotheses fltltc.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
fltltc.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
fltltc.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
fltltc.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
fltltc.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
Assertion fltnltalem ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) < ( 𝐴 ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fltltc.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 fltltc.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 fltltc.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 fltltc.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
5 fltltc.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
6 3 nnred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
7 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
8 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
9 4 7 8 3syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
10 6 9 reexpcld ⊢ ( 𝜑 → ( 𝐶 ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
11 9 nn0red ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
12 2 nnred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
13 12 9 reexpcld ⊢ ( 𝜑 → ( 𝐵 ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
14 11 13 remulcld ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
15 10 14 readdcld ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ∈ ℝ )
16 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
17 16 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ Fin )
18 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ∈ ℝ )
19 elfzonn0 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ℕ0 )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
21 18 20 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐶 ↑ 𝑘 ) ∈ ℝ )
22 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ℝ )
23 fzonnsub ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ )
25 nnm1nn0 ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℕ → ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℕ0 )
26 24 25 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℕ0 )
27 22 26 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ∈ ℝ )
28 21 27 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ∈ ℝ )
29 17 28 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ∈ ℝ )
30 1 2 3 4 5 fltltc ⊢ ( 𝜑 → 𝐵 < 𝐶 )
31 difrp ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐶 ↔ ( 𝐶 − 𝐵 ) ∈ ℝ+ ) )
32 12 6 31 syl2anc ⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ ( 𝐶 − 𝐵 ) ∈ ℝ+ ) )
33 30 32 mpbid ⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℝ+ )
34 fzofi ⊢ ( 0 ..^ ( 𝑁 − 1 ) ) ∈ Fin
35 34 a1i ⊢ ( 𝜑 → ( 0 ..^ ( 𝑁 − 1 ) ) ∈ Fin )
36 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝐶 ∈ ℝ )
37 elfzonn0 ⊢ ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ0 )
39 36 38 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝐶 ↑ 𝑘 ) ∈ ℝ )
40 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝐵 ∈ ℝ )
41 fzonnsub ⊢ ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) − 𝑘 ) ∈ ℕ )
42 41 nnnn0d ⊢ ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) − 𝑘 ) ∈ ℕ0 )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) − 𝑘 ) ∈ ℕ0 )
44 40 43 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ∈ ℝ )
45 39 44 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ∈ ℝ )
46 35 45 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ∈ ℝ )
47 fzofi ⊢ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ∈ Fin
48 47 a1i ⊢ ( 𝜑 → ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ∈ Fin )
49 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝐵 ∈ ℝ )
50 elfzonn0 ⊢ ( 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) → 𝑘 ∈ ℕ0 )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝑘 ∈ ℕ0 )
52 49 51 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( 𝐵 ↑ 𝑘 ) ∈ ℝ )
53 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) )
54 1nn0 ⊢ 1 ∈ ℕ0
55 elfzoext ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ∧ 1 ∈ ℕ0 ) → 𝑘 ∈ ( 0 ..^ ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) ) )
56 53 54 55 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝑘 ∈ ( 0 ..^ ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) ) )
57 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
58 4 7 57 3syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
59 58 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
60 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
61 59 60 subcld ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℂ )
62 61 60 npcand ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) = ( 𝑁 − 1 ) )
63 62 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) ) = ( 0 ..^ ( 𝑁 − 1 ) ) )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( 0 ..^ ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) ) = ( 0 ..^ ( 𝑁 − 1 ) ) )
65 56 64 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
66 65 42 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( ( 𝑁 − 1 ) − 𝑘 ) ∈ ℕ0 )
67 49 66 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ∈ ℝ )
68 52 67 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ∈ ℝ )
69 48 68 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ∈ ℝ )
70 sub1m1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − 2 ) )
71 59 70 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − 2 ) )
72 uz3m2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )
73 4 72 syl ⊢ ( 𝜑 → ( 𝑁 − 2 ) ∈ ℕ )
74 71 73 eqeltrd ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) − 1 ) ∈ ℕ )
75 74 nnnn0d ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) − 1 ) ∈ ℕ0 )
76 12 75 reexpcld ⊢ ( 𝜑 → ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) ∈ ℝ )
77 76 12 remulcld ⊢ ( 𝜑 → ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ∈ ℝ )
78 69 77 readdcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) ∈ ℝ )
79 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝐶 ∈ ℝ )
80 79 51 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( 𝐶 ↑ 𝑘 ) ∈ ℝ )
81 80 67 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ∈ ℝ )
82 48 81 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ∈ ℝ )
83 6 75 reexpcld ⊢ ( 𝜑 → ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) ∈ ℝ )
84 83 12 remulcld ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ∈ ℝ )
85 82 84 readdcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) ∈ ℝ )
86 2 nncnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
87 uzuzle23 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
88 4 87 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
89 uz2m1nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ )
90 88 89 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ )
91 expm1t ⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ ) → ( 𝐵 ↑ ( 𝑁 − 1 ) ) = ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) )
92 86 90 91 syl2anc ⊢ ( 𝜑 → ( 𝐵 ↑ ( 𝑁 − 1 ) ) = ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) )
93 92 eqcomd ⊢ ( 𝜑 → ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) = ( 𝐵 ↑ ( 𝑁 − 1 ) ) )
94 93 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝑁 − 1 ) − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) + ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) = ( ( ( ( 𝑁 − 1 ) − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) + ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
95 61 60 subcld ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) − 1 ) ∈ ℂ )
96 86 9 expcld ⊢ ( 𝜑 → ( 𝐵 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
97 95 96 adddirp1d ⊢ ( 𝜑 → ( ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) = ( ( ( ( 𝑁 − 1 ) − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) + ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
98 62 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) = ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
99 94 97 98 3eqtr2rd ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) = ( ( ( ( 𝑁 − 1 ) − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) + ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) )
100 14 99 eqled ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( ( 𝑁 − 1 ) − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) + ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) )
101 37 nn0cnd ⊢ ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝑘 ∈ ℂ )
102 65 101 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝑘 ∈ ℂ )
103 61 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℂ )
104 102 103 pncan3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( 𝑘 + ( ( 𝑁 − 1 ) − 𝑘 ) ) = ( 𝑁 − 1 ) )
105 104 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( 𝐵 ↑ ( 𝑘 + ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( 𝐵 ↑ ( 𝑁 − 1 ) ) )
106 105 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( 𝐵 ↑ ( 𝑘 + ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( 𝐵 ↑ ( 𝑁 − 1 ) ) )
107 86 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝐵 ∈ ℂ )
108 107 66 51 expaddd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( 𝐵 ↑ ( 𝑘 + ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
109 108 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( 𝐵 ↑ ( 𝑘 + ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
110 fsumconst ⊢ ( ( ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ∈ Fin ∧ ( 𝐵 ↑ ( 𝑁 − 1 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( 𝐵 ↑ ( 𝑁 − 1 ) ) = ( ( ♯ ‘ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
111 48 96 110 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( 𝐵 ↑ ( 𝑁 − 1 ) ) = ( ( ♯ ‘ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
112 hashfzo0 ⊢ ( ( ( 𝑁 − 1 ) − 1 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) = ( ( 𝑁 − 1 ) − 1 ) )
113 75 112 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) = ( ( 𝑁 − 1 ) − 1 ) )
114 113 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) = ( ( ( 𝑁 − 1 ) − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
115 111 114 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( 𝐵 ↑ ( 𝑁 − 1 ) ) = ( ( ( 𝑁 − 1 ) − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
116 106 109 115 3eqtr3d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( ( ( 𝑁 − 1 ) − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
117 116 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) = ( ( ( ( 𝑁 − 1 ) − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) + ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) )
118 100 117 breqtrrd ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ≤ ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) )
119 2 nnrpd ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
120 119 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝐵 )
121 120 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 0 ≤ 𝐵 )
122 49 66 121 expge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 0 ≤ ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) )
123 12 6 30 ltled ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
124 123 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → 𝐵 ≤ 𝐶 )
125 leexp1a ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( 𝐵 ↑ 𝑘 ) ≤ ( 𝐶 ↑ 𝑘 ) )
126 49 79 51 121 124 125 syl32anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( 𝐵 ↑ 𝑘 ) ≤ ( 𝐶 ↑ 𝑘 ) )
127 52 80 67 122 126 lemul1ad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ) → ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ≤ ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
128 48 68 81 127 fsumle ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
129 3 nnrpd ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
130 119 129 74 30 ltexp1dd ⊢ ( 𝜑 → ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) < ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) )
131 76 83 119 130 ltmul1dd ⊢ ( 𝜑 → ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) < ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) )
132 69 77 82 84 128 131 leltaddd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐵 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) < ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) )
133 14 78 85 118 132 lelttrd ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) < ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) )
134 61 60 nncand ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) − ( ( 𝑁 − 1 ) − 1 ) ) = 1 )
135 134 oveq2d ⊢ ( 𝜑 → ( 𝐵 ↑ ( ( 𝑁 − 1 ) − ( ( 𝑁 − 1 ) − 1 ) ) ) = ( 𝐵 ↑ 1 ) )
136 86 exp1d ⊢ ( 𝜑 → ( 𝐵 ↑ 1 ) = 𝐵 )
137 135 136 eqtrd ⊢ ( 𝜑 → ( 𝐵 ↑ ( ( 𝑁 − 1 ) − ( ( 𝑁 − 1 ) − 1 ) ) ) = 𝐵 )
138 137 oveq2d ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − ( ( 𝑁 − 1 ) − 1 ) ) ) ) = ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) )
139 138 oveq2d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − ( ( 𝑁 − 1 ) − 1 ) ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · 𝐵 ) ) )
140 133 139 breqtrrd ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) < ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − ( ( 𝑁 − 1 ) − 1 ) ) ) ) ) )
141 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
142 141 peano2zd ⊢ ( 𝜑 → ( 0 + 1 ) ∈ ℤ )
143 0cn ⊢ 0 ∈ ℂ
144 ax-1cn ⊢ 1 ∈ ℂ
145 143 144 144 addassi ⊢ ( ( 0 + 1 ) + 1 ) = ( 0 + ( 1 + 1 ) )
146 144 144 addcli ⊢ ( 1 + 1 ) ∈ ℂ
147 146 addlidi ⊢ ( 0 + ( 1 + 1 ) ) = ( 1 + 1 )
148 1p1e2 ⊢ ( 1 + 1 ) = 2
149 145 147 148 3eqtri ⊢ ( ( 0 + 1 ) + 1 ) = 2
150 149 a1i ⊢ ( 𝜑 → ( ( 0 + 1 ) + 1 ) = 2 )
151 150 fveq2d ⊢ ( 𝜑 → ( ℤ≥ ‘ ( ( 0 + 1 ) + 1 ) ) = ( ℤ≥ ‘ 2 ) )
152 88 151 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( ( 0 + 1 ) + 1 ) ) )
153 eluzp1m1 ⊢ ( ( ( 0 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( ( 0 + 1 ) + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
154 142 152 153 syl2anc ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
155 eluzp1m1 ⊢ ( ( 0 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( ( 𝑁 − 1 ) − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
156 141 154 155 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
157 3 nncnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
158 157 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝐶 ∈ ℂ )
159 158 38 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝐶 ↑ 𝑘 ) ∈ ℂ )
160 86 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝐵 ∈ ℂ )
161 160 43 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ∈ ℂ )
162 159 161 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ∈ ℂ )
163 oveq2 ⊢ ( 𝑘 = ( ( 𝑁 − 1 ) − 1 ) → ( 𝐶 ↑ 𝑘 ) = ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) )
164 oveq2 ⊢ ( 𝑘 = ( ( 𝑁 − 1 ) − 1 ) → ( ( 𝑁 − 1 ) − 𝑘 ) = ( ( 𝑁 − 1 ) − ( ( 𝑁 − 1 ) − 1 ) ) )
165 164 oveq2d ⊢ ( 𝑘 = ( ( 𝑁 − 1 ) − 1 ) → ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) = ( 𝐵 ↑ ( ( 𝑁 − 1 ) − ( ( 𝑁 − 1 ) − 1 ) ) ) )
166 163 165 oveq12d ⊢ ( 𝑘 = ( ( 𝑁 − 1 ) − 1 ) → ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − ( ( 𝑁 − 1 ) − 1 ) ) ) ) )
167 9 nn0zd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
168 156 162 166 167 fzosumm1 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ..^ ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − ( ( 𝑁 − 1 ) − 1 ) ) ) ) ) )
169 140 168 breqtrrd ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) < Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
170 14 46 10 169 ltadd2dd ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) < ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ) )
171 35 162 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ∈ ℂ )
172 157 9 expcld ⊢ ( 𝜑 → ( 𝐶 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
173 171 172 addcomd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( 𝐶 ↑ ( 𝑁 − 1 ) ) ) = ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ) )
174 170 173 breqtrrd ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) < ( Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( 𝐶 ↑ ( 𝑁 − 1 ) ) ) )
175 59 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℂ )
176 101 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℂ )
177 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 1 ∈ ℂ )
178 175 176 177 sub32d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 𝑘 ) − 1 ) = ( ( 𝑁 − 1 ) − 𝑘 ) )
179 178 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) = ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) )
180 179 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
181 180 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
182 59 59 60 nnncand ⊢ ( 𝜑 → ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) = ( 𝑁 − 𝑁 ) )
183 59 subidd ⊢ ( 𝜑 → ( 𝑁 − 𝑁 ) = 0 )
184 182 183 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) = 0 )
185 184 oveq2d ⊢ ( 𝜑 → ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) = ( 𝐵 ↑ 0 ) )
186 86 exp0d ⊢ ( 𝜑 → ( 𝐵 ↑ 0 ) = 1 )
187 185 186 eqtrd ⊢ ( 𝜑 → ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) = 1 )
188 187 oveq2d ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) = ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) · 1 ) )
189 10 recnd ⊢ ( 𝜑 → ( 𝐶 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
190 189 mulridd ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) · 1 ) = ( 𝐶 ↑ ( 𝑁 − 1 ) ) )
191 188 190 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) = ( 𝐶 ↑ ( 𝑁 − 1 ) ) )
192 181 191 oveq12d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) + ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( 𝐶 ↑ ( 𝑁 − 1 ) ) ) )
193 174 192 breqtrrd ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) < ( Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) + ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) ) )
194 elnn0uz ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 ↔ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
195 9 194 sylib ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
196 157 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ∈ ℂ )
197 196 20 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐶 ↑ 𝑘 ) ∈ ℂ )
198 86 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ℂ )
199 198 26 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ∈ ℂ )
200 197 199 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ∈ ℂ )
201 oveq2 ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( 𝐶 ↑ 𝑘 ) = ( 𝐶 ↑ ( 𝑁 − 1 ) ) )
202 oveq2 ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( 𝑁 − 𝑘 ) = ( 𝑁 − ( 𝑁 − 1 ) ) )
203 202 oveq1d ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( ( 𝑁 − 𝑘 ) − 1 ) = ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) )
204 203 oveq2d ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) = ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) )
205 201 204 oveq12d ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) )
206 58 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
207 195 200 205 206 fzosumm1 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( Σ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) + ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) · ( 𝐵 ↑ ( ( 𝑁 − ( 𝑁 − 1 ) ) − 1 ) ) ) ) )
208 193 207 breqtrrd ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) < Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) )
209 15 29 33 208 ltmul2dd ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) < ( ( 𝐶 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )
210 pwdif ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐶 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )
211 58 157 86 210 syl3anc ⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐶 − 𝐵 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐶 ↑ 𝑘 ) · ( 𝐵 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )
212 209 211 breqtrrd ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) < ( ( 𝐶 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) )
213 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
214 213 58 expcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
215 86 58 expcld ⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) ∈ ℂ )
216 214 215 5 mvlraddd ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) = ( ( 𝐶 ↑ 𝑁 ) − ( 𝐵 ↑ 𝑁 ) ) )
217 212 216 breqtrrd ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) < ( 𝐴 ↑ 𝑁 ) )