Theorem faclbnd4lem1 6885

Description: Lemma for faclbnd4 6889. Prepare the induction step. Warning: The HTML proof page is 0.6 megabyte in size.

Hypotheses

Ref	Expression
faclbnd4lem1.1	|- N e. NN
faclbnd4lem1.2	|- K e. NN0
faclbnd4lem1.3	|- M e. NN0

Assertion

Ref	Expression
faclbnd4lem1	|- ((((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 faclbnd4lem1

Step	Hyp	Ref	Expression
1		faclbnd4lem1.1	. . . 4 |- N e. NN
2	1	nnre 5879	. . 3 |- N e. RR
3		1re 5407	. . 3 |- 1 e. RR
4		lelttrit 5596	. . 3 |- ((N e. RR /\ 1 e. RR) -> (N <_ 1 \/ 1 < N))
5	2, 3, 4	mp2an 695	. 2 |- (N <_ 1 \/ 1 < N)
6	2, 3	letri3 5547	. . . . . 6 |- (N = 1 <-> (N <_ 1 /\ 1 <_ N))
7		nnge1t 5891	. . . . . . 7 |- (N e. NN -> 1 <_ N)
8	1, 7	ax-mp 7	. . . . . 6 |- 1 <_ N
9	6, 8	mpbiran2 727	. . . . 5 |- (N = 1 <-> N <_ 1)
10		2re 5926	. . . . . . . . . 10 |- 2 e. RR
11		faclbnd4lem1.2	. . . . . . . . . . . . 13 |- K e. NN0
12		1nn 5882	. . . . . . . . . . . . 13 |- 1 e. NN
13		nn0nnaddclt 6073	. . . . . . . . . . . . 13 |- ((K e. NN0 /\ 1 e. NN) -> (K + 1) e. NN)
14	11, 12, 13	mp2an 695	. . . . . . . . . . . 12 |- (K + 1) e. NN
15	14	nnnn0 6054	. . . . . . . . . . 11 |- (K + 1) e. NN0
16		2nn0 6062	. . . . . . . . . . 11 |- 2 e. NN0
17		nn0expclt 6509	. . . . . . . . . . 11 |- (((K + 1) e. NN0 /\ 2 e. NN0) -> ((K + 1)^2) e. NN0)
18	15, 16, 17	mp2an 695	. . . . . . . . . 10 |- ((K + 1)^2) e. NN0
19		reexpclt 6512	. . . . . . . . . 10 |- ((2 e. RR /\ ((K + 1)^2) e. NN0) -> (2^((K + 1)^2)) e. RR)
20	10, 18, 19	mp2an 695	. . . . . . . . 9 |- (2^((K + 1)^2)) e. RR
21	3, 20	pm3.2i 285	. . . . . . . 8 |- (1 e. RR /\ (2^((K + 1)^2)) e. RR)
22		0re 5412	. . . . . . . . . 10 |- 0 e. RR
23		lt01 5653	. . . . . . . . . 10 |- 0 < 1
24	22, 3, 23	ltlei 5554	. . . . . . . . 9 |- 0 <_ 1
25		2cn 5927	. . . . . . . . . . 11 |- 2 e. CC
26		exp0t 6503	. . . . . . . . . . 11 |- (2 e. CC -> (2^0) = 1)
27	25, 26	ax-mp 7	. . . . . . . . . 10 |- (2^0) = 1
28		0nn0 6060	. . . . . . . . . . . 12 |- 0 e. NN0
29	10, 28, 18	3pm3.2i 816	. . . . . . . . . . 11 |- (2 e. RR /\ 0 e. NN0 /\ ((K + 1)^2) e. NN0)
30		1lt2 5975	. . . . . . . . . . . . 13 |- 1 < 2
31	3, 10, 30	ltlei 5554	. . . . . . . . . . . 12 |- 1 <_ 2
32	18	nn0ge0 6065	. . . . . . . . . . . 12 |- 0 <_ ((K + 1)^2)
33	31, 32	pm3.2i 285	. . . . . . . . . . 11 |- (1 <_ 2 /\ 0 <_ ((K + 1)^2))
34		expwordit 6534	. . . . . . . . . . 11 |- (((2 e. RR /\ 0 e. NN0 /\ ((K + 1)^2) e. NN0) /\ (1 <_ 2 /\ 0 <_ ((K + 1)^2))) -> (2^0) <_ (2^((K + 1)^2)))
35	29, 33, 34	mp2an 695	. . . . . . . . . 10 |- (2^0) <_ (2^((K + 1)^2))
36	27, 35	eqbrtrr 2626	. . . . . . . . 9 |- 1 <_ (2^((K + 1)^2))
37	24, 36	pm3.2i 285	. . . . . . . 8 |- (0 <_ 1 /\ 1 <_ (2^((K + 1)^2)))
38	21, 37	pm3.2i 285	. . . . . . 7 |- ((1 e. RR /\ (2^((K + 1)^2)) e. RR) /\ (0 <_ 1 /\ 1 <_ (2^((K + 1)^2))))
39		faclbnd4lem1.3	. . . . . . . . . 10 |- M e. NN0
40	39	nn0re 6057	. . . . . . . . 9 |- M e. RR
41		nn0nnaddclt 6073	. . . . . . . . . . . . 13 |- ((M e. NN0 /\ (K + 1) e. NN) -> (M + (K + 1)) e. NN)
42	39, 14, 41	mp2an 695	. . . . . . . . . . . 12 |- (M + (K + 1)) e. NN
43	42	nnnn0 6054	. . . . . . . . . . 11 |- (M + (K + 1)) e. NN0
44		nn0expclt 6509	. . . . . . . . . . 11 |- ((M e. NN0 /\ (M + (K + 1)) e. NN0) -> (M^(M + (K + 1))) e. NN0)
45	39, 43, 44	mp2an 695	. . . . . . . . . 10 |- (M^(M + (K + 1))) e. NN0
46	45	nn0re 6057	. . . . . . . . 9 |- (M^(M + (K + 1))) e. RR
47	40, 46	pm3.2i 285	. . . . . . . 8 |- (M e. RR /\ (M^(M + (K + 1))) e. RR)
48	39	nn0ge0 6065	. . . . . . . . 9 |- 0 <_ M
49		elnn0 6048	. . . . . . . . . . 11 |- (M e. NN0 <-> (M e. NN \/ M = 0))
50		nncnt 5878	. . . . . . . . . . . . . 14 |- (M e. NN -> M e. CC)
51		exp1t 6505	. . . . . . . . . . . . . 14 |- (M e. CC -> (M^1) = M)
52	50, 51	syl 10	. . . . . . . . . . . . 13 |- (M e. NN -> (M^1) = M)
53		nnge1t 5891	. . . . . . . . . . . . . 14 |- (M e. NN -> 1 <_ M)
54		nnge1t 5891	. . . . . . . . . . . . . . . 16 |- ((M + (K + 1)) e. NN -> 1 <_ (M + (K + 1)))
55	42, 54	ax-mp 7	. . . . . . . . . . . . . . 15 |- 1 <_ (M + (K + 1))
56		1nn0 6061	. . . . . . . . . . . . . . . . 17 |- 1 e. NN0
57	40, 56, 43	3pm3.2i 816	. . . . . . . . . . . . . . . 16 |- (M e. RR /\ 1 e. NN0 /\ (M + (K + 1)) e. NN0)
58		expwordit 6534	. . . . . . . . . . . . . . . 16 |- (((M e. RR /\ 1 e. NN0 /\ (M + (K + 1)) e. NN0) /\ (1 <_ M /\ 1 <_ (M + (K + 1)))) -> (M^1) <_ (M^(M + (K + 1))))
59	57, 58	mpan 693	. . . . . . . . . . . . . . 15 |- ((1 <_ M /\ 1 <_ (M + (K + 1))) -> (M^1) <_ (M^(M + (K + 1))))
60	55, 59	mpan2 694	. . . . . . . . . . . . . 14 |- (1 <_ M -> (M^1) <_ (M^(M + (K + 1))))
61	53, 60	syl 10	. . . . . . . . . . . . 13 |- (M e. NN -> (M^1) <_ (M^(M + (K + 1))))
62	52, 61	eqbrtrrd 2627	. . . . . . . . . . . 12 |- (M e. NN -> M <_ (M^(M + (K + 1))))
63	45	nn0ge0 6065	. . . . . . . . . . . . 13 |- 0 <_ (M^(M + (K + 1)))
64		breq1 2612	. . . . . . . . . . . . 13 |- (M = 0 -> (M <_ (M^(M + (K + 1))) <-> 0 <_ (M^(M + (K + 1)))))
65	63, 64	mpbiri 194	. . . . . . . . . . . 12 |- (M = 0 -> M <_ (M^(M + (K + 1))))
66	62, 65	jaoi 341	. . . . . . . . . . 11 |- ((M e. NN \/ M = 0) -> M <_ (M^(M + (K + 1))))
67	49, 66	sylbi 199	. . . . . . . . . 10 |- (M e. NN0 -> M <_ (M^(M + (K + 1))))
68	39, 67	ax-mp 7	. . . . . . . . 9 |- M <_ (M^(M + (K + 1)))
69	48, 68	pm3.2i 285	. . . . . . . 8 |- (0 <_ M /\ M <_ (M^(M + (K + 1))))
70	47, 69	pm3.2i 285	. . . . . . 7 |- ((M e. RR /\ (M^(M + (K + 1))) e. RR) /\ (0 <_ M /\ M <_ (M^(M + (K + 1)))))
71		lemul12itOLD 5799	. . . . . . 7 |- ((((1 e. RR /\ (2^((K + 1)^2)) e. RR) /\ (0 <_ 1 /\ 1 <_ (2^((K + 1)^2)))) /\ ((M e. RR /\ (M^(M + (K + 1))) e. RR) /\ (0 <_ M /\ M <_ (M^(M + (K + 1)))))) -> (1 x. M) <_ ((2^((K + 1)^2)) x. (M^(M + (K + 1)))))
72	38, 70, 71	mp2an 695	. . . . . 6 |- (1 x. M) <_ ((2^((K + 1)^2)) x. (M^(M + (K + 1))))
73		opreq1 3953	. . . . . . . . 9 |- (N = 1 -> (N^(K + 1)) = (1^(K + 1)))
74		1expt 6516	. . . . . . . . . 10 |- ((K + 1) e. NN0 -> (1^(K + 1)) = 1)
75	15, 74	ax-mp 7	. . . . . . . . 9 |- (1^(K + 1)) = 1
76	73, 75	syl6eq 1515	. . . . . . . 8 |- (N = 1 -> (N^(K + 1)) = 1)
77		opreq2 3954	. . . . . . . . 9 |- (N = 1 -> (M^N) = (M^1))
78	39	nn0cn 6058	. . . . . . . . . 10 |- M e. CC
79	78, 51	ax-mp 7	. . . . . . . . 9 |- (M^1) = M
80	77, 79	syl6eq 1515	. . . . . . . 8 |- (N = 1 -> (M^N) = M)
81	76, 80	opreq12d 3963	. . . . . . 7 |- (N = 1 -> ((N^(K + 1)) x. (M^N)) = (1 x. M))
82		fveq2 3709	. . . . . . . . . 10 |- (N = 1 -> (!` N) = (!` 1))
83		fac1 6872	. . . . . . . . . 10 |- (!` 1) = 1
84	82, 83	syl6eq 1515	. . . . . . . . 9 |- (N = 1 -> (!` N) = 1)
85	84	opreq2d 3961	. . . . . . . 8 |- (N = 1 -> (((2^((K + 1)^2)) x. (M^(M + (K + 1)))) x. (!` N)) = (((2^((K + 1)^2)) x. (M^(M + (K + 1)))) x. 1))
86	20	recn 5286	. . . . . . . . . 10 |- (2^((K + 1)^2)) e. CC
87	45	nn0cn 6058	. . . . . . . . . 10 |- (M^(M + (K + 1))) e. CC
88	86, 87	mulcl 5293	. . . . . . . . 9 |- ((2^((K + 1)^2)) x. (M^(M + (K + 1)))) e. CC
89	88	mulid1 5304	. . . . . . . 8 |- (((2^((K + 1)^2)) x. (M^(M + (K + 1)))) x. 1) = ((2^((K + 1)^2)) x. (M^(M + (K + 1))))
90	85, 89	syl6eq 1515	. . . . . . 7 |- (N = 1 -> ((