Theorem faclbnd4lem3 6887

Description: Lemma for faclbnd4 6889. The N = 0 case.

Assertion

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

Proof of Theorem faclbnd4lem3

Step	Hyp	Ref	Expression
1		0expt 6521	. . . . . . . 8 |- (K e. NN -> (0^K) = 0)
2	1	adantl 388	. . . . . . 7 |- ((M e. NN0 /\ K e. NN) -> (0^K) = 0)
3		nn0mulclt 6070	. . . . . . . . . 10 |- (((2^(K^2)) e. NN0 /\ (M^(M + K)) e. NN0) -> ((2^(K^2)) x. (M^(M + K))) e. NN0)
4		2nn0 6062	. . . . . . . . . . . . 13 |- 2 e. NN0
5		nn0expclt 6509	. . . . . . . . . . . . 13 |- ((K e. NN0 /\ 2 e. NN0) -> (K^2) e. NN0)
6	4, 5	mpan2 694	. . . . . . . . . . . 12 |- (K e. NN0 -> (K^2) e. NN0)
7		nn0expclt 6509	. . . . . . . . . . . . 13 |- ((2 e. NN0 /\ (K^2) e. NN0) -> (2^(K^2)) e. NN0)
8	4, 7	mpan 693	. . . . . . . . . . . 12 |- ((K^2) e. NN0 -> (2^(K^2)) e. NN0)
9	6, 8	syl 10	. . . . . . . . . . 11 |- (K e. NN0 -> (2^(K^2)) e. NN0)
10	9	adantl 388	. . . . . . . . . 10 |- ((M e. NN0 /\ K e. NN0) -> (2^(K^2)) e. NN0)
11		nn0addclt 6067	. . . . . . . . . . 11 |- ((M e. NN0 /\ K e. NN0) -> (M + K) e. NN0)
12		nn0expclt 6509	. . . . . . . . . . 11 |- ((M e. NN0 /\ (M + K) e. NN0) -> (M^(M + K)) e. NN0)
13	11, 12	syldan 467	. . . . . . . . . 10 |- ((M e. NN0 /\ K e. NN0) -> (M^(M + K)) e. NN0)
14	3, 10, 13	sylanc 471	. . . . . . . . 9 |- ((M e. NN0 /\ K e. NN0) -> ((2^(K^2)) x. (M^(M + K))) e. NN0)
15		nnnn0t 6053	. . . . . . . . 9 |- (K e. NN -> K e. NN0)
16	14, 15	sylan2 451	. . . . . . . 8 |- ((M e. NN0 /\ K e. NN) -> ((2^(K^2)) x. (M^(M + K))) e. NN0)
17		nn0ge0t 6064	. . . . . . . 8 |- (((2^(K^2)) x. (M^(M + K))) e. NN0 -> 0 <_ ((2^(K^2)) x. (M^(M + K))))
18	16, 17	syl 10	. . . . . . 7 |- ((M e. NN0 /\ K e. NN) -> 0 <_ ((2^(K^2)) x. (M^(M + K))))
19	2, 18	eqbrtrd 2625	. . . . . 6 |- ((M e. NN0 /\ K e. NN) -> (0^K) <_ ((2^(K^2)) x. (M^(M + K))))
20		elnn0 6048	. . . . . . . . . 10 |- (M e. NN0 <-> (M e. NN \/ M = 0))
21		nnnn0t 6053	. . . . . . . . . . . . 13 |- (M e. NN -> M e. NN0)
22		0nn0 6060	. . . . . . . . . . . . . 14 |- 0 e. NN0
23		nn0addclt 6067	. . . . . . . . . . . . . 14 |- ((M e. NN0 /\ 0 e. NN0) -> (M + 0) e. NN0)
24	22, 23	mpan2 694	. . . . . . . . . . . . 13 |- (M e. NN0 -> (M + 0) e. NN0)
25	21, 24	syl 10	. . . . . . . . . . . 12 |- (M e. NN -> (M + 0) e. NN0)
26		nnexpclt 6508	. . . . . . . . . . . 12 |- ((M e. NN /\ (M + 0) e. NN0) -> (M^(M + 0)) e. NN)
27	25, 26	mpdan 702	. . . . . . . . . . 11 |- (M e. NN -> (M^(M + 0)) e. NN)
28		id 59	. . . . . . . . . . . . . 14 |- (M = 0 -> M = 0)
29		opreq1 3953	. . . . . . . . . . . . . . 15 |- (M = 0 -> (M + 0) = (0 + 0))
30		0cn 5300	. . . . . . . . . . . . . . . 16 |- 0 e. CC
31	30	addid1 5302	. . . . . . . . . . . . . . 15 |- (0 + 0) = 0
32	29, 31	syl6eq 1515	. . . . . . . . . . . . . 14 |- (M = 0 -> (M + 0) = 0)
33	28, 32	opreq12d 3963	. . . . . . . . . . . . 13 |- (M = 0 -> (M^(M + 0)) = (0^0))
34		exp0t 6503	. . . . . . . . . . . . . 14 |- (0 e. CC -> (0^0) = 1)
35	30, 34	ax-mp 7	. . . . . . . . . . . . 13 |- (0^0) = 1
36	33, 35	syl6eq 1515	. . . . . . . . . . . 12 |- (M = 0 -> (M^(M + 0)) = 1)
37		1nn 5882	. . . . . . . . . . . 12 |- 1 e. NN
38	36, 37	syl6eqel 1548	. . . . . . . . . . 11 |- (M = 0 -> (M^(M + 0)) e. NN)
39	27, 38	jaoi 341	. . . . . . . . . 10 |- ((M e. NN \/ M = 0) -> (M^(M + 0)) e. NN)
40	20, 39	sylbi 199	. . . . . . . . 9 |- (M e. NN0 -> (M^(M + 0)) e. NN)
41		nnmulclt 5889	. . . . . . . . . 10 |- ((1 e. NN /\ (M^(M + 0)) e. NN) -> (1 x. (M^(M + 0))) e. NN)
42	37, 41	mpan 693	. . . . . . . . 9 |- ((M^(M + 0)) e. NN -> (1 x. (M^(M + 0))) e. NN)
43		nnge1t 5891	. . . . . . . . 9 |- ((1 x. (M^(M + 0))) e. NN -> 1 <_ (1 x. (M^(M + 0))))
44	40, 42, 43	3syl 20	. . . . . . . 8 |- (M e. NN0 -> 1 <_ (1 x. (M^(M + 0))))
45	44	adantr 389	. . . . . . 7 |- ((M e. NN0 /\ K = 0) -> 1 <_ (1 x. (M^(M + 0))))
46		opreq2 3954	. . . . . . . . . 10 |- (K = 0 -> (0^K) = (0^0))
47	46, 35	syl6eq 1515	. . . . . . . . 9 |- (K = 0 -> (0^K) = 1)
48		sq0i 6567	. . . . . . . . . . . 12 |- (K = 0 -> (K^2) = 0)
49	48	opreq2d 3961	. . . . . . . . . . 11 |- (K = 0 -> (2^(K^2)) = (2^0))
50		2cn 5927	. . . . . . . . . . . 12 |- 2 e. CC
51		exp0t 6503	. . . . . . . . . . . 12 |- (2 e. CC -> (2^0) = 1)
52	50, 51	ax-mp 7	. . . . . . . . . . 11 |- (2^0) = 1
53	49, 52	syl6eq 1515	. . . . . . . . . 10 |- (K = 0 -> (2^(K^2)) = 1)
54		opreq2 3954	. . . . . . . . . . 11 |- (K = 0 -> (M + K) = (M + 0))
55	54	opreq2d 3961	. . . . . . . . . 10 |- (K = 0 -> (M^(M + K)) = (M^(M + 0)))
56	53, 55	opreq12d 3963	. . . . . . . . 9 |- (K = 0 -> ((2^(K^2)) x. (M^(M + K))) = (1 x. (M^(M + 0))))
57	47, 56	breq12d 2621	. . . . . . . 8 |- (K = 0 -> ((0^K) <_ ((2^(K^2)) x. (M^(M + K))) <-> 1 <_ (1 x. (M^(M + 0)))))
58	57	adantl 388	. . . . . . 7 |- ((M e. NN0 /\ K = 0) -> ((0^K) <_ ((2^(K^2)) x. (M^(M + K))) <-> 1 <_ (1 x. (M^(M + 0)))))
59	45, 58	mpbird 196	. . . . . 6 |- ((M e. NN0 /\ K = 0) -> (0^K) <_ ((2^(K^2)) x. (M^(M + K))))
60	19, 59	jaodan 426	. . . . 5 |- ((M e. NN0 /\ (K e. NN \/ K = 0)) -> (0^K) <_ ((2^(K^2)) x. (M^(M + K))))
61		elnn0 6048	. . . . 5 |- (K e. NN0 <-> (K e. NN \/ K = 0))
62	60, 61	sylan2b 452	. . . 4 |- ((M e. NN0 /\ K e. NN0) -> (0^K) <_ ((2^(K^2)) x. (M^(M + K))))
63		nn0cnt 6056	. . . . . . 7 |- (M e. NN0 -> M e. CC)
64		exp0t 6503	. . . . . . 7 |- (M e. CC -> (M^0) = 1)
65	63, 64	syl 10	. . . . . 6 |- (M e. NN0 -> (M^0) = 1)
66	65	opreq2d 3961	. . . . 5 |- (M e. NN0 -> ((0^K) x. (M^0)) = ((0^K) x. 1))
67		nn0expclt 6509	. . . . . . 7 |- ((0 e. NN0 /\ K e. NN0) -> (0^K) e. NN0)
68	22, 67	mpan 693	. . . . . 6 |- (K e. NN0 -> (0^K) e. NN0)
69		nn0cnt 6056	. . . . . 6 |- ((0^K) e. NN0 -> (0^K) e. CC)
70		ax1id 5254	. . . . . 6 |- ((0^K) e. CC -> ((0^K) x. 1) = (0^K))
71	68, 69, 70	3syl 20	. . . . 5 |- (K e. NN0 -> ((0^K) x. 1) = (0^K))
72	66, 71	sylan9eq 1519	. . . 4 |- ((M e. NN0 /\ K e. NN0) -> ((0^K) x. (M^0)) = (0^K))
73		nn0cnt 6056	. . . . 5 |- (((2^(K^2)) x. (M^(M + K))) e. NN0 -> ((2^(K^2)) x. (M^(M + K))) e. CC)
74		ax1id 5254	. . . . 5 |- (((2^(K^2)) x. (M^(M + K))) e. CC -> (((2^(K^2)) x. (M^(M + K))) x. 1) = ((2^(K^2)) x. (M^(M + K))))
75	14, 73, 74	3syl 20	. . . 4 |- ((M e. NN0 /\ K e. NN0) -> (((2^(K^2)) x. (M^(M + K))) x. 1) = ((2^(K^2)) x. (M^(M + K))))
76	62, 72, 75	3brtr4d 2635	. . 3 |- ((M e. NN0 /\ K e. NN0) -> ((0^K) x. (M^0)) <_ (((2^(K^2)) x. (M^(M + K))) x. 1))
77	76	adantr 389	. 2 |- (((M e. NN0 /\ K e. NN0) /\ N = 0) -> ((0^K) x. (M^0)) <_ (((2^(K^2))