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 
|- ( ph -> A e. NN )
fltltc.b 
|- ( ph -> B e. NN )
fltltc.c 
|- ( ph -> C e. NN )
fltltc.n 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
fltltc.1 
|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
Assertion fltnltalem 
|- ( ph -> ( ( C - B ) x. ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) < ( A ^ N ) )

Proof

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