Theorem faclbnd4lem4 6896

Description: Lemma for faclbnd4 6897. Prove the 0 < N case by induction on K.

Assertion

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

Proof of Theorem faclbnd4lem4

Step	Hyp	Ref	Expression
1		opreq1 3959	. . . . . 6 |- (n = N -> (n^K) = (N^K))
2		opreq2 3960	. . . . . 6 |- (n = N -> (M^n) = (M^N))
3	1, 2	opreq12d 3969	. . . . 5 |- (n = N -> ((n^K) x. (M^n)) = ((N^K) x. (M^N)))
4		fveq2 3715	. . . . . 6 |- (n = N -> (!` n) = (!` N))
5	4	opreq2d 3967	. . . . 5 |- (n = N -> (((2^(K^2)) x. (M^(M + K))) x. (!` n)) = (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
6	3, 5	breq12d 2626	. . . 4 |- (n = N -> (((n^K) x. (M^n)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` n)) <-> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N))))
7	6	rcla4va 1871	. . 3 |- ((N e. NN /\ A.n e. NN ((n^K) x. (M^n)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` n))) -> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
8		faclbnd4lem3 6895	. . . . . . . . . . . . . 14 |- (((M e. NN0 /\ j e. NN0) /\ (n - 1) = 0) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1))))
9		nnge1t 5899	. . . . . . . . . . . . . . . . 17 |- (n e. NN -> 1 <_ n)
10	9	adantr 389	. . . . . . . . . . . . . . . 16 |- ((n e. NN /\ n <_ 1) -> 1 <_ n)
11		nnret 5885	. . . . . . . . . . . . . . . . . . 19 |- (n e. NN -> n e. RR)
12		1re 5415	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. RR
13		letri3t 5498	. . . . . . . . . . . . . . . . . . . 20 |- ((n e. RR /\ 1 e. RR) -> (n = 1 <-> (n <_ 1 /\ 1 <_ n)))
14	12, 13	mpan2 695	. . . . . . . . . . . . . . . . . . 19 |- (n e. RR -> (n = 1 <-> (n <_ 1 /\ 1 <_ n)))
15	11, 14	syl 10	. . . . . . . . . . . . . . . . . 18 |- (n e. NN -> (n = 1 <-> (n <_ 1 /\ 1 <_ n)))
16	15	biimpar 417	. . . . . . . . . . . . . . . . 17 |- ((n e. NN /\ (n <_ 1 /\ 1 <_ n)) -> n = 1)
17	16	anassrs 441	. . . . . . . . . . . . . . . 16 |- (((n e. NN /\ n <_ 1) /\ 1 <_ n) -> n = 1)
18	10, 17	mpdan 703	. . . . . . . . . . . . . . 15 |- ((n e. NN /\ n <_ 1) -> n = 1)
19		opreq1 3959	. . . . . . . . . . . . . . . 16 |- (n = 1 -> (n - 1) = (1 - 1))
20		ax1cn 5249	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
21	20	subid 5371	. . . . . . . . . . . . . . . 16 |- (1 - 1) = 0
22	19, 21	syl6eq 1520	. . . . . . . . . . . . . . 15 |- (n = 1 -> (n - 1) = 0)
23	18, 22	syl 10	. . . . . . . . . . . . . 14 |- ((n e. NN /\ n <_ 1) -> (n - 1) = 0)
24	8, 23	sylan2 451	. . . . . . . . . . . . 13 |- (((M e. NN0 /\ j e. NN0) /\ (n e. NN /\ n <_ 1)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1))))
25	24	a1d 12	. . . . . . . . . . . 12 |- (((M e. NN0 /\ j e. NN0) /\ (n e. NN /\ n <_ 1)) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
26		1nn 5890	. . . . . . . . . . . . . . . 16 |- 1 e. NN
27		nnsubt 5912	. . . . . . . . . . . . . . . 16 |- ((1 e. NN /\ n e. NN) -> (1 < n <-> (n - 1) e. NN))
28	26, 27	mpan 694	. . . . . . . . . . . . . . 15 |- (n e. NN -> (1 < n <-> (n - 1) e. NN))
29	28	biimpa 416	. . . . . . . . . . . . . 14 |- ((n e. NN /\ 1 < n) -> (n - 1) e. NN)
30		opreq1 3959	. . . . . . . . . . . . . . . . 17 |- (m = (n - 1) -> (m^j) = ((n - 1)^j))
31		opreq2 3960	. . . . . . . . . . . . . . . . 17 |- (m = (n - 1) -> (M^m) = (M^(n - 1)))
32	30, 31	opreq12d 3969	. . . . . . . . . . . . . . . 16 |- (m = (n - 1) -> ((m^j) x. (M^m)) = (((n - 1)^j) x. (M^(n - 1))))
33		fveq2 3715	. . . . . . . . . . . . . . . . 17 |- (m = (n - 1) -> (!` m) = (!` (n - 1)))
34	33	opreq2d 3967	. . . . . . . . . . . . . . . 16 |- (m = (n - 1) -> (((2^(j^2)) x. (M^(M + j))) x. (!` m)) = (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1))))
35	32, 34	breq12d 2626	. . . . . . . . . . . . . . 15 |- (m = (n - 1) -> (((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) <-> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
36	35	rcla4v 1869	. . . . . . . . . . . . . 14 |- ((n - 1) e. NN -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
37	29, 36	syl 10	. . . . . . . . . . . . 13 |- ((n e. NN /\ 1 < n) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
38	37	adantl 388	. . . . . . . . . . . 12 |- (((M e. NN0 /\ j e. NN0) /\ (n e. NN /\ 1 < n)) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
39	25, 38	jaodan 426	. . . . . . . . . . 11 |- (((M e. NN0 /\ j e. NN0) /\ ((n e. NN /\ n <_ 1) \/ (n e. NN /\ 1 < n))) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
40		lelttrit 5604	. . . . . . . . . . . . . . 15 |- ((n e. RR /\ 1 e. RR) -> (n <_ 1 \/ 1 < n))
41	12, 40	mpan2 695	. . . . . . . . . . . . . 14 |- (n e. RR -> (n <_ 1 \/ 1 < n))
42	11, 41	syl 10	. . . . . . . . . . . . 13 |- (n e. NN -> (n <_ 1 \/ 1 < n))
43	42	ancli 296	. . . . . . . . . . . 12 |- (n e. NN -> (n e. NN /\ (n <_ 1 \/ 1 < n)))
44		andi 603	. . . . . . . . . . . 12 |- ((n e. NN /\ (n <_ 1 \/ 1 < n)) <-> ((n e. NN /\ n <_ 1) \/ (n e. NN /\ 1 < n)))
45	43, 44	sylib 198	. . . . . . . . . . 11 |- (n e. NN -> ((n e. NN /\ n <_ 1) \/ (n e. NN /\ 1 < n)))
46	39, 45	sylan2 451	. . . . . . . . . 10 |- (((M e. NN0 /\ j e. NN0) /\ n e. NN) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1