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	$⊢ φ \to A \in ℕ$
	fltltc.b	$⊢ φ \to B \in ℕ$
	fltltc.c	$⊢ φ \to C \in ℕ$
	fltltc.n	$⊢ φ \to N \in ℤ_{\geq 3}$
	fltltc.1	$⊢ φ \to A^{N} + B^{N} = C^{N}$
Assertion	fltnltalem	$⊢ φ \to (C - B) (C^{N - 1} + (N - 1) B^{N - 1}) < A^{N}$

Proof

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

Metamath Proof Explorer

Theorem fltnltalem

Proof