Theorem faclbnd3 6947

Description: A lower bound for the factorial function.

Assertion

Ref	Expression
faclbnd3	|- ((M e. NN0 /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))

Proof of Theorem faclbnd3

Step	Hyp	Ref	Expression
1		expwordit 6604	. . . . 5 |- (((M e. RR /\ N e. NN0 /\ (N + 1) e. NN0) /\ (1 <_ M /\ N <_ (N + 1))) -> (M^N) <_ (M^(N + 1)))
2		nnret 5931	. . . . . . 7 |- (M e. NN -> M e. RR)
3	2	adantr 391	. . . . . 6 |- ((M e. NN /\ N e. NN0) -> M e. RR)
4		pm3.27 323	. . . . . 6 |- ((M e. NN /\ N e. NN0) -> N e. NN0)
5		peano2nn0 6126	. . . . . . 7 |- (N e. NN0 -> (N + 1) e. NN0)
6	5	adantl 390	. . . . . 6 |- ((M e. NN /\ N e. NN0) -> (N + 1) e. NN0)
7	3, 4, 6	3jca 821	. . . . 5 |- ((M e. NN /\ N e. NN0) -> (M e. RR /\ N e. NN0 /\ (N + 1) e. NN0))
8		nnge1t 5945	. . . . . 6 |- (M e. NN -> 1 <_ M)
9		letrp1t 5818	. . . . . . 7 |- ((N e. RR /\ N e. RR /\ N <_ N) -> N <_ (N + 1))
10		nn0ret 6110	. . . . . . 7 |- (N e. NN0 -> N e. RR)
11		leidt 5543	. . . . . . . 8 |- (N e. RR -> N <_ N)
12	10, 11	syl 10	. . . . . . 7 |- (N e. NN0 -> N <_ N)
13	9, 10, 10, 12	syl3anc 860	. . . . . 6 |- (N e. NN0 -> N <_ (N + 1))
14	8, 13	anim12i 333	. . . . 5 |- ((M e. NN /\ N e. NN0) -> (1 <_ M /\ N <_ (N + 1)))
15	1, 7, 14	sylanc 473	. . . 4 |- ((M e. NN /\ N e. NN0) -> (M^N) <_ (M^(N + 1)))
16		faclbnd 6945	. . . . 5 |- ((M e. NN0 /\ N e. NN0) -> (M^(N + 1)) <_ ((M^M) x. (!` N)))
17		nnnn0t 6108	. . . . 5 |- (M e. NN -> M e. NN0)
18	16, 17	sylan 450	. . . 4 |- ((M e. NN /\ N e. NN0) -> (M^(N + 1)) <_ ((M^M) x. (!` N)))
19		letrt 5537	. . . . . 6 |- (((M^N) e. RR /\ (M^(N + 1)) e. RR /\ ((M^M) x. (!` N)) e. RR) -> (((M^N) <_ (M^(N + 1)) /\ (M^(N + 1)) <_ ((M^M) x. (!` N))) -> (M^N) <_ ((M^M) x. (!` N))))
20		reexpclt 6581	. . . . . . 7 |- ((M e. RR /\ N e. NN0) -> (M^N) e. RR)
21		nn0ret 6110	. . . . . . 7 |- (M e. NN0 -> M e. RR)
22	20, 21	sylan 450	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (M^N) e. RR)
23		reexpclt 6581	. . . . . . 7 |- ((M e. RR /\ (N + 1) e. NN0) -> (M^(N + 1)) e. RR)
24	23, 21, 5	syl2an 456	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (M^(N + 1)) e. RR)
25		axmulrcl 5286	. . . . . . 7 |- (((M^M) e. RR /\ (!` N) e. RR) -> ((M^M) x. (!` N)) e. RR)
26		reexpclt 6581	. . . . . . . 8 |- ((M e. RR /\ M e. NN0) -> (M^M) e. RR)
27	21, 26	mpancom 707	. . . . . . 7 |- (M e. NN0 -> (M^M) e. RR)
28		facclt 6940	. . . . . . . 8 |- (N e. NN0 -> (!` N) e. NN)
29		nnret 5931	. . . . . . . 8 |- ((!` N) e. NN -> (!` N) e. RR)
30	28, 29	syl 10	. . . . . . 7 |- (N e. NN0 -> (!` N) e. RR)
31	25, 27, 30	syl2an 456	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> ((M^M) x. (!` N)) e. RR)
32	19, 22, 24, 31	syl3anc 860	. . . . 5 |- ((M e. NN0 /\ N e. NN0) -> (((M^N) <_ (M^(N + 1)) /\ (M^(N + 1)) <_ ((M^M) x. (!` N))) -> (M^N) <_ ((M^M) x. (!` N))))
33	32, 17	sylan 450	. . . 4 |- ((M e. NN /\ N e. NN0) -> (((M^N) <_ (M^(N + 1)) /\ (M^(N + 1)) <_ ((M^M) x. (!` N))) -> (M^N) <_ ((M^M) x. (!` N))))
34	15, 18, 33	mp2and 705	. . 3 |- ((M e. NN /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))
35		elnn0 6103	. . . . . . 7 |- (N e. NN0 <-> (N e. NN \/ N = 0))
36		0expt 6591	. . . . . . . . 9 |- (N e. NN -> (0^N) = 0)
37		0re 5452	. . . . . . . . . 10 |- 0 e. RR
38		1re 5447	. . . . . . . . . 10 |- 1 e. RR
39		lt01 5692	. . . . . . . . . 10 |- 0 < 1
40	37, 38, 39	ltlei 5593	. . . . . . . . 9 |- 0 <_ 1
41	36, 40	syl6eqbr 2657	. . . . . . . 8 |- (N e. NN -> (0^N) <_ 1)
42		opreq2 3975	. . . . . . . . 9 |- (N = 0 -> (0^N) = (0^0))
43		0cn 5340	. . . . . . . . . . 11 |- 0 e. CC
44		exp0t 6572	. . . . . . . . . . 11 |- (0 e. CC -> (0^0) = 1)
45	43, 44	ax-mp 7	. . . . . . . . . 10 |- (0^0) = 1
46	38	leid 5622	. . . . . . . . . 10 |- 1 <_ 1
47	45, 46	eqbrtr 2639	. . . . . . . . 9 |- (0^0) <_ 1
48	42, 47	syl6eqbr 2657	. . . . . . . 8 |- (N = 0 -> (0^N) <_ 1)
49	41, 48	jaoi 341	. . . . . . 7 |- ((N e. NN \/ N = 0) -> (0^N) <_ 1)
50	35, 49	sylbi 199	. . . . . 6 |- (N e. NN0 -> (0^N) <_ 1)
51		1nn 5936	. . . . . . . . 9 |- 1 e. NN
52		nnmulclt 5943	. . . . . . . . 9 |- ((1 e. NN /\ (!` N) e. NN) -> (1 x. (!` N)) e. NN)
53	51, 52	mpan 697	. . . . . . . 8 |- ((!` N) e. NN -> (1 x. (!` N)) e. NN)
54	28, 53	syl 10	. . . . . . 7 |- (N e. NN0 -> (1 x. (!` N)) e. NN)
55		nnge1t 5945	. . . . . . 7 |- ((1 x. (!` N)) e. NN -> 1 <_ (1 x. (!` N)))
56	54, 55	syl 10	. . . . . 6 |- (N e. NN0 -> 1 <_ (1 x. (!` N)))
57		letrt 5537	. . . . . . . 8 |- (((0^N) e. RR /\ 1 e. RR /\ (1 x. (!` N)) e. RR) -> (((0^N) <_ 1 /\ 1 <_ (1 x. (!` N))) -> (0^N) <_ (1 x. (!` N))))
58	38, 57	mp3an2 906	. . . . . . 7 |- (((0^N) e. RR /\ (1 x. (!` N)) e. RR) -> (((0^N) <_ 1 /\ 1 <_ (1 x. (!` N))) -> (0^N) <_ (1 x. (!` N))))
59		reexpclt 6581	. . . . . . . 8 |- ((0 e. RR /\ N e. NN0) -> (0^N) e. RR)
60	37, 59	mpan 697	. . . . . . 7 |- (N e. NN0 -> (0^N) e. RR)
61		axmulrcl 5286	. . . . . . . . 9 |- ((1 e. RR /\ (!` N) e. RR) -> (1 x. (!` N)) e. RR)
62	38, 61	mpan 697	. . . . . . . 8 |- ((!` N) e. RR -> (1 x. (!` N)) e. RR)
63	30, 62	syl 10	. . . . . . 7 |- (N e. NN0 -> (1 x. (!` N)) e. RR)
64	58, 60, 63	sylanc 473	. . . . . 6 |- (N e. NN0 -> (((0^N) <_ 1 /\ 1 <_ (1 x. (!` N))) -> (0^N) <_ (1 x. (!` N))))
65	50, 56, 64	mp2and 705	. . . . 5 |- (N e. NN0 -> (0^N) <_ (1 x. (!` N)))
66	65	adantl 390	. . . 4 |- ((M = 0 /\ N e. NN0) -> (0^N) <_ (1 x. (!` N)))
67		opreq1 3974	. . . . . 6 |- (M = 0 -> (M^N) = (0^N))
68		opreq12 3976	. . . . . . . . 9 |- ((M = 0 /\ M = 0) -> (M^M) = (0^0))
69	68	anidms 436	. . . . . . . 8 |- (M = 0 -> (M^M) = (0^0))
70	69, 45	syl6eq 1526	. . . . . . 7 |- (M = 0 -> (M^M) = 1)
71	70	opreq1d 3981	. . . . . 6 |- (M = 0 -> ((M^M) x. (!` N)) = (1 x. (!` N)))
72	67, 71	breq12d 2636	. . . . 5 |- (M = 0 -> ((M^N) <_ ((M^M) x. (!` N)) <-> (0^N) <_ (1 x. (!` N))))
73	72	adantr 391	. . . 4 |- ((M = 0 /\ N e. NN0) -> ((M^N) <_ ((M^M) x. (!` N)) <-> (0^N) <_ (1 x. (!` N))))
74	66, 73	mpbird 196	. . 3 |- ((M = 0 /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))
75	34, 74	jaoian 427	. 2 |- (((M e. NN \/ M = 0) /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))
76		elnn0 6103	. 2 |- (M e. NN0 <-> (M e. NN \/ M = 0))
77	75, 76	sylanb 451	1 |- ((M e. NN0 /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   /\ w3a 777   = wceq 958   e. wcel 960   class class class wbr 2624  ` cfv 3188  (class class class)co 3969  CCcc 5244  RRcr 5245  0cc0 5246  1c1 5247   + caddc 5249   x. cmul 5251   <_ cle 5307  NNcn 5308  NN0cn0 5309  ^cexp 6569  !cfa 6931

This theorem is referenced by:  faclbnd4lem4 6951

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14