Theorem faclbnd3 6884

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 6534	. . . . 5 |- (((M e. RR /\ N e. NN0 /\ (N + 1) e. NN0) /\ (1 <_ M /\ N <_ (N + 1))) -> (M^N) <_ (M^(N + 1)))
2		nnret 5877	. . . . . . 7 |- (M e. NN -> M e. RR)
3	2	adantr 389	. . . . . 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 6071	. . . . . . 7 |- (N e. NN0 -> (N + 1) e. NN0)
6	5	adantl 388	. . . . . 6 |- ((M e. NN /\ N e. NN0) -> (N + 1) e. NN0)
7	3, 4, 6	3jca 817	. . . . 5 |- ((M e. NN /\ N e. NN0) -> (M e. RR /\ N e. NN0 /\ (N + 1) e. NN0))
8		nnge1t 5891	. . . . . 6 |- (M e. NN -> 1 <_ M)
9		letrp1t 5772	. . . . . . 7 |- ((N e. RR /\ N e. RR /\ N <_ N) -> N <_ (N + 1))
10		nn0ret 6055	. . . . . . 7 |- (N e. NN0 -> N e. RR)
11		leidt 5504	. . . . . . . 8 |- (N e. RR -> N <_ N)
12	10, 11	syl 10	. . . . . . 7 |- (N e. NN0 -> N <_ N)
13	9, 10, 10, 12	syl3anc 856	. . . . . 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 471	. . . 4 |- ((M e. NN /\ N e. NN0) -> (M^N) <_ (M^(N + 1)))
16		faclbnd 6882	. . . . 5 |- ((M e. NN0 /\ N e. NN0) -> (M^(N + 1)) <_ ((M^M) x. (!` N)))
17		nnnn0t 6053	. . . . 5 |- (M e. NN -> M e. NN0)
18	16, 17	sylan 448	. . . 4 |- ((M e. NN /\ N e. NN0) -> (M^(N + 1)) <_ ((M^M) x. (!` N)))
19		letrt 5498	. . . . . 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 6512	. . . . . . 7 |- ((M e. RR /\ N e. NN0) -> (M^N) e. RR)
21		nn0ret 6055	. . . . . . 7 |- (M e. NN0 -> M e. RR)
22	20, 21	sylan 448	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (M^N) e. RR)
23		reexpclt 6512	. . . . . . 7 |- ((M e. RR /\ (N + 1) e. NN0) -> (M^(N + 1)) e. RR)
24	23, 21, 5	syl2an 454	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (M^(N + 1)) e. RR)
25		axmulrcl 5246	. . . . . . 7 |- (((M^M) e. RR /\ (!` N) e. RR) -> ((M^M) x. (!` N)) e. RR)
26		reexpclt 6512	. . . . . . . 8 |- ((M e. RR /\ M e. NN0) -> (M^M) e. RR)
27	21, 26	mpancom 703	. . . . . . 7 |- (M e. NN0 -> (M^M) e. RR)
28		facclt 6877	. . . . . . . 8 |- (N e. NN0 -> (!` N) e. NN)
29		nnret 5877	. . . . . . . 8 |- ((!` N) e. NN -> (!` N) e. RR)
30	28, 29	syl 10	. . . . . . 7 |- (N e. NN0 -> (!` N) e. RR)
31	25, 27, 30	syl2an 454	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> ((M^M) x. (!` N)) e. RR)
32	19, 22, 24, 31	syl3anc 856	. . . . 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 448	. . . 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 701	. . 3 |- ((M e. NN /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))
35		elnn0 6048	. . . . . . 7 |- (N e. NN0 <-> (N e. NN \/ N = 0))
36		0expt 6521	. . . . . . . . 9 |- (N e. NN -> (0^N) = 0)
37		0re 5412	. . . . . . . . . 10 |- 0 e. RR
38		1re 5407	. . . . . . . . . 10 |- 1 e. RR
39		lt01 5653	. . . . . . . . . 10 |- 0 < 1
40	37, 38, 39	ltlei 5554	. . . . . . . . 9 |- 0 <_ 1
41	36, 40	syl6eqbr 2642	. . . . . . . 8 |- (N e. NN -> (0^N) <_ 1)
42		opreq2 3954	. . . . . . . . 9 |- (N = 0 -> (0^N) = (0^0))
43		0cn 5300	. . . . . . . . . . 11 |- 0 e. CC
44		exp0t 6503	. . . . . . . . . . 11 |- (0 e. CC -> (0^0) = 1)
45	43, 44	ax-mp 7	. . . . . . . . . 10 |- (0^0) = 1
46	38	leid 5584	. . . . . . . . . 10 |- 1 <_ 1
47	45, 46	eqbrtr 2624	. . . . . . . . 9 |- (0^0) <_ 1
48	42, 47	syl6eqbr 2642	. . . . . . . 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 5882	. . . . . . . . 9 |- 1 e. NN
52		nnmulclt 5889	. . . . . . . . 9 |- ((1 e. NN /\ (!` N) e. NN) -> (1 x. (!` N)) e. NN)
53	51, 52	mpan 693	. . . . . . . 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 5891	. . . . . . 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 5498	. . . . . . . 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 901	. . . . . . 7 |- (((0^N) e. RR /\ (1 x. (!` N)) e. RR) -> (((0^N) <_ 1 /\ 1 <_ (1 x. (!` N))) -> (0^N) <_ (1 x. (!` N))))
59		reexpclt 6512	. . . . . . . 8 |- ((0 e. RR /\ N e. NN0) -> (0^N) e. RR)
60	37, 59	mpan 693	. . . . . . 7 |- (N e. NN0 -> (0^N) e. RR)
61		axmulrcl 5246	. . . . . . . . 9 |- ((1 e. RR /\ (!` N) e. RR) -> (1 x. (!` N)) e. RR)
62	38, 61	mpan 693	. . . . . . . 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 471	. . . . . 6 |- (N e. NN0 -> (((0^N) <_ 1 /\ 1 <_ (1 x. (!` N))) -> (0^N) <_ (1 x. (!` N))))
65	50, 56, 64	mp2and 701	. . . . 5 |- (N e. NN0 -> (0^N) <_ (1 x. (!` N)))
66	65	adantl 388	. . . 4 |- ((M = 0 /\ N e. NN0) -> (0^N) <_ (1 x. (!` N)))
67		opreq1 3953	. . . . . 6 |- (M = 0 -> (M^N) = (0^N))
68		opreq12 3955	. . . . . . . . 9 |- ((M = 0 /\ M = 0) -> (M^M) = (0^0))
69	68	anidms 434	. . . . . . . 8 |- (M = 0 -> (M^M) = (0^0))
70	69, 45	syl6eq 1515	. . . . . . 7 |- (M = 0 -> (M^M) = 1)
71	70	opreq1d 3960	. . . . . 6 |- (M = 0 -> ((M^M) x. (!` N)) = (1 x. (!` N)))
72	67, 71	breq12d 2621	. . . . 5 |- (M = 0 -> ((M^N) <_ ((M^M) x. (!` N)) <-> (0^N) <_ (1 x. (!` N))))
73	72	adantr 389	. . . 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 425	. 2 |- (((M e. NN \/ M = 0) /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))
76		elnn0 6048	. 2 |- (M e. NN0 <-> (M e. NN \/ M = 0))
77	75, 76	sylanb 449	1 |- ((M e. NN0 /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   /\ w3a 773   = wceq 953   e. wcel 955   class class class wbr 2609  ` cfv 3172  (class class class)co 3948  CCcc 5204  RRcr 5205  0cc0 5206  1c1 5207   + caddc 5209   x. cmul 5211   <_ cle 5267  NNcn 5268  NN0cn0 5269  ^cexp 6500  !cfa 6868

This theorem is referenced by:  faclbnd4lem4 6888

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17