Theorem faclbnd4lem2 6894

Description: Lemma for faclbnd4 6897. Use the weak deduction theorem to convert the hypotheses of faclbnd4lem1 6893 to antecedents.

Assertion

Ref	Expression
faclbnd4lem2	|- ((M e. NN0 /\ K e. NN0 /\ N e. NN) -> ((((N - 1)^K) x. (M^(N - 1))) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` (N - 1))) -> ((N^(K + 1)) x. (M^N)) <_ (((2^((K + 1)^2)) x. (M^(M + (K + 1)))) x. (!` N))))

Proof of Theorem faclbnd4lem2

Step	Hyp	Ref	Expression
1		opreq1 3959	. . . . 5 |- (M = if(M e. NN0, M, 1) -> (M^(N - 1)) = (if(M e. NN0, M, 1)^(N - 1)))
2	1	opreq2d 3967	. . . 4 |- (M = if(M e. NN0, M, 1) -> (((N - 1)^K) x. (M^(N - 1))) = (((N - 1)^K) x. (if(M e. NN0, M, 1)^(N - 1))))
3		id 59	. . . . . . 7 |- (M = if(M e. NN0, M, 1) -> M = if(M e. NN0, M, 1))
4		opreq1 3959	. . . . . . 7 |- (M = if(M e. NN0, M, 1) -> (M + K) = (if(M e. NN0, M, 1) + K))
5	3, 4	opreq12d 3969	. . . . . 6 |- (M = if(M e. NN0, M, 1) -> (M^(M + K)) = (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + K)))
6	5	opreq2d 3967	. . . . 5 |- (M = if(M e. NN0, M, 1) -> ((2^(K^2)) x. (M^(M + K))) = ((2^(K^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + K))))
7	6	opreq1d 3966	. . . 4 |- (M = if(M e. NN0, M, 1) -> (((2^(K^2)) x. (M^(M + K))) x. (!` (N - 1))) = (((2^(K^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + K))) x. (!` (N - 1))))
8	2, 7	breq12d 2626	. . 3 |- (M = if(M e. NN0, M, 1) -> ((((N - 1)^K) x. (M^(N - 1))) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` (N - 1))) <-> (((N - 1)^K) x. (if(M e. NN0, M, 1)^(N - 1))) <_ (((2^(K^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + K))) x. (!` (N - 1)))))
9		opreq1 3959	. . . . 5 |- (M = if(M e. NN0, M, 1) -> (M^N) = (if(M e. NN0, M, 1)^N))
10	9	opreq2d 3967	. . . 4 |- (M = if(M e. NN0, M, 1) -> ((N^(K + 1)) x. (M^N)) = ((N^(K + 1)) x. (if(M e. NN0, M, 1)^N)))
11		opreq1 3959	. . . . . . 7 |- (M = if(M e. NN0, M, 1) -> (M + (K + 1)) = (if(M e. NN0, M, 1) + (K + 1)))
12	3, 11	opreq12d 3969	. . . . . 6 |- (M = if(M e. NN0, M, 1) -> (M^(M + (K + 1))) = (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + (K + 1))))
13	12	opreq2d 3967	. . . . 5 |- (M = if(M e. NN0, M, 1) -> ((2^((K + 1)^2)) x. (M^(M + (K + 1)))) = ((2^((K + 1)^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + (K + 1)))))
14	13	opreq1d 3966	. . . 4 |- (M = if(M e. NN0, M, 1) -> (((2^((K + 1)^2)) x. (M^(M + (K + 1)))) x. (!` N)) = (((2^((K + 1)^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + (K + 1)))) x. (!` N)))
15	10, 14	breq12d 2626	. . 3 |- (M = if(M e. NN0, M, 1) -> (((N^(K + 1)) x. (M^N)) <_ (((2^((K + 1)^2)) x. (M^(M + (K + 1)))) x. (!` N)) <-> ((N^(K + 1)) x. (if(M e. NN0, M, 1)^N)) <_ (((2^((K + 1)^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + (K + 1)))) x. (!` N))))
16	8, 15	imbi12d 625	. 2 |- (M = if(M e. NN0, M, 1) -> (((((N - 1)^K) x. (M^(N - 1))) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` (N - 1))) -> ((N^(K + 1)) x. (M^N)) <_ (((2^((K + 1)^2)) x. (M^(M + (K + 1)))) x. (!` N))) <-> ((((N - 1)^K) x. (if(M e. NN0, M, 1)^(N - 1))) <_ (((2^(K^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + K))) x. (!` (N - 1))) -> ((N^(K + 1)) x. (if(M e. NN0, M, 1)^N)) <_ (((2^((K + 1)^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + (K + 1)))) x. (!` N)))))
17		opreq2 3960	. . . . 5 |- (K = if(K e. NN0, K, 1) -> ((N - 1)^K) = ((N - 1)^if(K e. NN0, K, 1)))
18	17	opreq1d 3966	. . . 4 |- (K = if(K e. NN0, K, 1) -> (((N - 1)^K) x. (if(M e. NN0, M, 1)^(N - 1))) = (((N - 1)^if(K e. NN0, K, 1)) x. (if(M e. NN0, M, 1)^(N - 1))))
19		opreq1 3959	. . . . . . 7 |- (K = if(K e. NN0, K, 1) -> (K^2) = (if(K e. NN0, K, 1)^2))
20	19	opreq2d 3967	. . . . . 6 |- (K = if(K e. NN0, K, 1) -> (2^(K^2)) = (2^(if(K e. NN0, K, 1)^2)))
21		opreq2 3960	. . . . . . 7 |- (K = if(K e. NN0, K, 1) -> (if(M e. NN0, M, 1) + K) = (if(M e. NN0, M, 1) + if(K e. NN0, K, 1)))
22	21	opreq2d 3967	. . . . . 6 |- (K = if(K e. NN0, K, 1) -> (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + K)) = (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + if(K e. NN0, K, 1))))
23	20, 22	opreq12d 3969	. . . . 5 |- (K = if(K e. NN0, K, 1) -> ((2^(K^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + K))) = ((2^(if(K e. NN0, K, 1)^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + if(K e. NN0, K, 1)))))
24	23	opreq1d 3966	. . . 4 |- (K = if(K e. NN0, K, 1) -> (((2^(K^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + K))) x. (!` (N - 1))) = (((2^(if(K e. NN0, K, 1)^2)) x. (if(M e. NN0, M, 1)^(if(M e. NN0, M, 1) + if(K e. NN0, K, 1)))) x. (!` (N - 1))))
25	18, 24	breq12d 2626	. . 3 |- (K = if(K e. NN0, K, 1) -> ((((N - 1)^K) x. (if(M e. NN0, M, 1)^(N - 1)