Theorem faclbnd4lem4 7074

Description: Lemma for faclbnd4 7075. 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 4044	. . . . . 6 |- (n = N -> (n^K) = (N^K))
2		opreq2 4045	. . . . . 6 |- (n = N -> (M^n) = (M^N))
3	1, 2	opreq12d 4054	. . . . 5 |- (n = N -> ((n^K) x. (M^n)) = ((N^K) x. (M^N)))
4		fveq2 3800	. . . . . 6 |- (n = N -> (!` n) = (!` N))
5	4	opreq2d 4052	. . . . 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 2681	. . . 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 1913	. . 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 7073	. . . . . . . . . . . . . 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		nnge1 6030	. . . . . . . . . . . . . . . . 17 |- (n e. NN -> 1 <_ n)
10	9	adantr 389	. . . . . . . . . . . . . . . 16 |- ((n e. NN /\ n <_ 1) -> 1 <_ n)
11		nnre 6016	. . . . . . . . . . . . . . . . . . 19 |- (n e. NN -> n e. RR)
12		1re 5524	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. RR
13		letri3 5606	. . . . . . . . . . . . . . . . . . . 20 |- ((n e. RR /\ 1 e. RR) -> (n = 1 <-> (n <_ 1 /\ 1 <_ n)))
14	12, 13	mpan2 699	. . . . . . . . . . . . . . . . . . 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 443	. . . . . . . . . . . . . . . 16 |- (((n e. NN /\ n <_ 1) /\ 1 <_ n) -> n = 1)
18	10, 17	mpdan 707	. . . . . . . . . . . . . . 15 |- ((n e. NN /\ n <_ 1) -> n = 1)
19		opreq1 4044	. . . . . . . . . . . . . . . 16 |- (n = 1 -> (n - 1) = (1 - 1))
20		ax1cn 5358	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
21	20	subidi 5480	. . . . . . . . . . . . . . . 16 |- (1 - 1) = 0
22	19, 21	syl6eq 1560	. . . . . . . . . . . . . . 15 |- (n = 1 -> (n - 1) = 0)
23	18, 22	syl 10	. . . . . . . . . . . . . 14 |- ((n e. NN /\ n <_ 1) -> (n - 1) = 0)
24	8, 23	sylan2 453	. . . . . . . . . . . . 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 6021	. . . . . . . . . . . . . . . 16 |- 1 e. NN
27		nnsub 6045	. . . . . . . . . . . . . . . 16 |- ((1 e. NN /\ n e. NN) -> (1 < n <-> (n - 1) e. NN))
28	26, 27	mpan 698	. . . . . . . . . . . . . . 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 4044	. . . . . . . . . . . . . . . . 17 |- (m = (n - 1) -> (m^j) = ((n - 1)^j))
31		opreq2 4045	. . . . . . . . . . . . . . . . 17 |- (m = (n - 1) -> (M^m) = (M^(n - 1)))
32	30, 31	opreq12d 4054	. . . . . . . . . . . . . . . 16 |- (m = (n - 1) -> ((m^j) x. (M^m)) = (((n - 1)^j) x. (M^(n - 1))))
33		fveq2 3800	. . . . . . . . . . . . . . . . 17 |- (m = (n - 1) -> (!` m) = (!` (n - 1)))
34	33	opreq2d 4052	. . . . . . . . . . . . . . . 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 2681	. . . . . . . . . . . . . . 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 1911	. . . . . . . . . . . . . 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		lelttric 5711	. . . . . . . . . . . . . . 15 |- ((n e. RR /\ 1 e. RR) -> (n <_ 1 \/ 1 < n))
41	12, 40	mpan2 699	. . . . . . . . . . . . . 14 |- (n e. RR -> (n <_ 1 \/ 1 < n))
42	11, 41	syl 10	. . . . . . . . . . . . 13 |- (n e. NN -> (n <_ 1 \/ 1 < n))
43	42	ancli 294	. . . . . . . . . . . 12 |- (n e. NN -> (n e. NN /\ (n <_ 1 \/ 1 < n)))
44		andi 606	. . . . . . . . . . . 12 |- ((n e. NN /\ (n <_ 1 \/ 1 < n)) <-> ((n e. NN /\ n <_ 1) \/ (n e. NN /\ 1 < n)))
45	43, 44	sylib 196	. . . . . . . . . . 11 |- (n e. NN -> ((n e. NN /\ n <_ 1) \/ (n e. NN /\ 1 < n)))
46	39, 45	sylan2 453	. . . . . . . . . 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 -