Theorem faclbnd4lem1 7071

Description: Lemma for faclbnd4 7075. 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	nnrei 6018	. . 3 |- N e. RR
3		1re 5524	. . 3 |- 1 e. RR
4		lelttric 5711	. . 3 |- ((N e. RR /\ 1 e. RR) -> (N <_ 1 \/ 1 < N))
5	2, 3, 4	mp2an 700	. 2 |- (N <_ 1 \/ 1 < N)
6	2, 3	letri3i 5663	. . . . . 6 |- (N = 1 <-> (N <_ 1 /\ 1 <_ N))
7		nnge1 6030	. . . . . . 7 |- (N e. NN -> 1 <_ N)
8	1, 7	ax-mp 7	. . . . . 6 |- 1 <_ N
9	6, 8	mpbiran2 732	. . . . 5 |- (N = 1 <-> N <_ 1)
10		0re 5529	. . . . . . . . . . 11 |- 0 e. RR
11		lt01 5769	. . . . . . . . . . 11 |- 0 < 1
12	10, 3, 11	ltleii 5670	. . . . . . . . . 10 |- 0 <_ 1
13	3, 12	pm3.2i 283	. . . . . . . . 9 |- (1 e. RR /\ 0 <_ 1)
14		2re 6067	. . . . . . . . . 10 |- 2 e. RR
15		faclbnd4lem1.2	. . . . . . . . . . . . 13 |- K e. NN0
16		1nn 6021	. . . . . . . . . . . . 13 |- 1 e. NN
17		nn0nnaddcl 6236	. . . . . . . . . . . . 13 |- ((K e. NN0 /\ 1 e. NN) -> (K + 1) e. NN)
18	15, 16, 17	mp2an 700	. . . . . . . . . . . 12 |- (K + 1) e. NN
19	18	nnnn0i 6217	. . . . . . . . . . 11 |- (K + 1) e. NN0
20		2nn0 6225	. . . . . . . . . . 11 |- 2 e. NN0
21		nn0expcl 6700	. . . . . . . . . . 11 |- (((K + 1) e. NN0 /\ 2 e. NN0) -> ((K + 1)^2) e. NN0)
22	19, 20, 21	mp2an 700	. . . . . . . . . 10 |- ((K + 1)^2) e. NN0
23		reexpcl 6703	. . . . . . . . . 10 |- ((2 e. RR /\ ((K + 1)^2) e. NN0) -> (2^((K + 1)^2)) e. RR)
24	14, 22, 23	mp2an 700	. . . . . . . . 9 |- (2^((K + 1)^2)) e. RR
25	13, 24	pm3.2i 283	. . . . . . . 8 |- ((1 e. RR /\ 0 <_ 1) /\ (2^((K + 1)^2)) e. RR)
26		faclbnd4lem1.3	. . . . . . . . . . 11 |- M e. NN0
27	26	nn0rei 6220	. . . . . . . . . 10 |- M e. RR
28	26	nn0ge0i 6228	. . . . . . . . . 10 |- 0 <_ M
29	27, 28	pm3.2i 283	. . . . . . . . 9 |- (M e. RR /\ 0 <_ M)
30		nn0nnaddcl 6236	. . . . . . . . . . . . 13 |- ((M e. NN0 /\ (K + 1) e. NN) -> (M + (K + 1)) e. NN)
31	26, 18, 30	mp2an 700	. . . . . . . . . . . 12 |- (M + (K + 1)) e. NN
32	31	nnnn0i 6217	. . . . . . . . . . 11 |- (M + (K + 1)) e. NN0
33		nn0expcl 6700	. . . . . . . . . . 11 |- ((M e. NN0 /\ (M + (K + 1)) e. NN0) -> (M^(M + (K + 1))) e. NN0)
34	26, 32, 33	mp2an 700	. . . . . . . . . 10 |- (M^(M + (K + 1))) e. NN0
35	34	nn0rei 6220	. . . . . . . . 9 |- (M^(M + (K + 1))) e. RR
36	29, 35	pm3.2i 283	. . . . . . . 8 |- ((M e. RR /\ 0 <_ M) /\ (M^(M + (K + 1))) e. RR)
37	25, 36	pm3.2i 283	. . . . . . 7 |- (((1 e. RR /\ 0 <_ 1) /\ (2^((K + 1)^2)) e. RR) /\ ((M e. RR /\ 0 <_ M) /\ (M^(M + (K + 1))) e. RR))
38		2cn 6068	. . . . . . . . . 10 |- 2 e. CC
39		exp0 6694	. . . . . . . . . 10 |- (2 e. CC -> (2^0) = 1)
40	38, 39	ax-mp 7	. . . . . . . . 9 |- (2^0) = 1
41		0nn0 6223	. . . . . . . . . . 11 |- 0 e. NN0
42	14, 41, 22	3pm3.2i 821	. . . . . . . . . 10 |- (2 e. RR /\ 0 e. NN0 /\ ((K + 1)^2) e. NN0)
43		1lt2 6116	. . . . . . . . . . . 12 |- 1 < 2
44	3, 14, 43	ltleii 5670	. . . . . . . . . . 11 |- 1 <_ 2
45	22	nn0ge0i 6228	. . . . . . . . . . 11 |- 0 <_ ((K + 1)^2)
46	44, 45	pm3.2i 283	. . . . . . . . . 10 |- (1 <_ 2 /\ 0 <_ ((K + 1)^2))
47		expwordi 6725	. . . . . . . . . 10 |- (((2 e. RR /\ 0 e. NN0 /\ ((K + 1)^2) e. NN0) /\ (1 <_ 2 /\ 0 <_ ((K + 1)^2))) -> (2^0) <_ (2^((K + 1)^2)))
48	42, 46, 47	mp2an 700	. . . . . . . . 9 |- (2^0) <_ (2^((K + 1)^2))
49	40, 48	eqbrtrri 2686	. . . . . . . 8 |- 1 <_ (2^((K + 1)^2))
50		elnn0 6211	. . . . . . . . . 10 |- (M e. NN0 <-> (M e. NN \/ M = 0))
51		nncn 6017	. . . . . . . . . . . . 13 |- (M e. NN -> M e. CC)
52		exp1 6696	. . . . . . . . . . . . 13 |- (M e. CC -> (M^1) = M)
53	51, 52	syl 10	. . . . . . . . . . . 12 |- (M e. NN -> (M^1) = M)
54		nnge1 6030	. . . . . . . . . . . . 13 |- (M e. NN -> 1 <_ M)
55		nnge1 6030	. . . . . . . . . . . . . . 15 |- ((M + (K + 1)) e. NN -> 1 <_ (M + (K + 1)))
56	31, 55	ax-mp 7	. . . . . . . . . . . . . 14 |- 1 <_ (M + (K + 1))
57		1nn0 6224	. . . . . . . . . . . . . . . 16 |- 1 e. NN0
58	27, 57, 32	3pm3.2i 821	. . . . . . . . . . . . . . 15 |- (M e. RR /\ 1 e. NN0 /\ (M + (K + 1)) e. NN0)
59		expwordi 6725	. . . . . . . . . . . . . . 15 |- (((M e. RR /\ 1 e. NN0 /\ (M + (K + 1)) e. NN0) /\ (1 <_ M /\ 1 <_ (M + (K + 1)))) -> (M^1) <_ (M^(M + (K + 1))))
60	58, 59	mpan 698	. . . . . . . . . . . . . 14 |- ((1 <_ M /\ 1 <_ (M + (K + 1))) -> (M^1) <_ (M^(M + (K + 1))))
61	56, 60	mpan2 699	. . . . . . . . . . . . 13 |- (1 <_ M -> (M^1) <_ (M^(M + (K + 1))))
62	54, 61	syl 10	. . . . . . . . . . . 12 |- (M e. NN -> (M^1) <_ (M^(M + (K + 1))))
63	53, 62	eqbrtrrd 2687	. . . . . . . . . . 11 |- (M e. NN -> M <_ (M^(M + (K + 1))))
64	34	nn0ge0i 6228	. . . . . . . . . . . 12 |- 0 <_ (M^(M + (K + 1)))
65		breq1 2672	. . . . . . . . . . . 12 |- (M = 0 -> (M <_ (M^(M + (K + 1))) <-> 0 <_ (M^(M + (K + 1)))))
66	64, 65	mpbiri 192	. . . . . . . . . . 11 |- (M = 0 -> M <_ (M^(M + (K + 1))))
67	63, 66	jaoi 339	. . . . . . . . . 10 |- ((M e. NN \/ M = 0) -> M <_ (M^(M + (K + 1))))
68	50, 67	sylbi 197	. . . . . . . . 9 |- (M e. NN0 -> M <_ (M^(M + (K + 1))))
69	26, 68	ax-mp 7	. . . . . . . 8 |- M <_ (M^(M + (K + 1)))
70	49, 69	pm3.2i 283	. . . . . . 7 |- (1 <_ (2^((K + 1)^2)) /\ M <_ (M^(M + (K + 1))))
71		lemul12a 5929	. . . . . . 7 |- ((((1 e. RR /\ 0 <_ 1) /\ (2^((K + 1)^2)) e. RR) /\ ((M e. RR /\ 0 <_ M) /\ (M^(M + (K + 1))) e. RR)) -> ((1 <_ (2^((K + 1)^2)) /\ M <_ (M^(M + (K + 1)))) -> (1 x. M) <_ ((2^((K + 1)^2)) x. (M^(M + (K + 1))))))
72	37, 70, 71	mp2 43	. . . . . 6 |- (1 x. M) <_ ((2^((K + 1)^2)) x. (M^(M + (K + 1))))
73		opreq1 4044	. . . . . . . . 9 |- (N = 1 -> (N^(K + 1)) = (1^(K + 1)))
74		1exp 6707	. . . . . . . . . 10 |- ((K + 1) e. NN0 -> (1^(K + 1)) = 1)
75	19, 74	ax-mp 7	. . . . . . . . 9 |- (1^(K + 1)) = 1
76	73, 75	syl6eq 1560	. . . . . . . 8 |- (N = 1 -> (N^(K + 1)) = 1)
77		opreq2 4045	. . . . . . . . 9 |- (N = 1 -> (M^N) = (M^1))
78	26	nn0cni 6221	. . . . . . . . . 10 |- M e. CC
79	78, 52	ax-mp 7	. . . . . . . . 9 |- (M^1) = M
80	77, 79	syl6eq 1560	. . . . . . . 8 |- (N = 1 -> (M^N) = M)
81	76, 80	opreq12d 4054	. . . . . . 7 |- (N = 1 -> ((N^(K + 1)) x. (M^N)) = (1 x. M))
82		fveq2 3800	. . . . . . . . . 10 |- (N = 1 -> (!` N) = (!` 1))
83		fac1 7058	. . . . . . . . . 10 |- (!` 1) = 1
84	82, 83	syl6eq 1560	. . . . . . . . 9 |- (N = 1 -> (!` N) = 1)
85	84	opreq2d 4052	. . . . . . . 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	24	recni 5403	. . . . . . . . . 10 |- (2^((K + 1)^2)) e. CC
87	34	nn0cni 6221	. . . . . . . . . 10 |- (M^(M + (K + 1))) e. CC
88	86, 87	mulcli 5410	. . . . . . . . 9 |- ((2^((K + 1)^2)) x. (M^(M + (K + 1)))) e. CC
89	88	mulid1i 5421	. . . . . . . 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 1560	. . . . . . 7 |- (N = 1 -> (((2^((K + 1)^2)