Theorem faclbnd3

Description: A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005)

	Ref	Expression
Assertion	faclbnd3	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
2		nnre	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
3	2	adantr	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
4		nnge1	⊢ ( 𝑀 ∈ ℕ → 1 ≤ 𝑀 )
5	4	adantr	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 1 ≤ 𝑀 )
6		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
7	6	adantl	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
8		uzid	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
9		peano2uz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
10	7 8 9	3syl	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
11	3 5 10	leexp2ad	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ≤ ( 𝑀 ↑ ( 𝑁 + 1 ) ) )
12		nnnn0	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
13		faclbnd	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )
14	12 13	sylan	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )
15		nn0re	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
16		reexpcl	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ∈ ℝ )
17	15 16	sylan	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ∈ ℝ )
18		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
19		reexpcl	⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ∈ ℝ )
20	15 18 19	syl2an	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ∈ ℝ )
21		reexpcl	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑀 ) ∈ ℝ )
22	15 21	mpancom	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ↑ 𝑀 ) ∈ ℝ )
23		faccl	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
24	23	nnred	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℝ )
25		remulcl	⊢ ( ( ( 𝑀 ↑ 𝑀 ) ∈ ℝ ∧ ( ! ‘ 𝑁 ) ∈ ℝ ) → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ∈ ℝ )
26	22 24 25	syl2an	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ∈ ℝ )
27		letr	⊢ ( ( ( 𝑀 ↑ 𝑁 ) ∈ ℝ ∧ ( 𝑀 ↑ ( 𝑁 + 1 ) ) ∈ ℝ ∧ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ∈ ℝ ) → ( ( ( 𝑀 ↑ 𝑁 ) ≤ ( 𝑀 ↑ ( 𝑁 + 1 ) ) ∧ ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ) → ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ) )
28	17 20 26 27	syl3anc	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑀 ↑ 𝑁 ) ≤ ( 𝑀 ↑ ( 𝑁 + 1 ) ) ∧ ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ) → ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ) )
29	12 28	sylan	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑀 ↑ 𝑁 ) ≤ ( 𝑀 ↑ ( 𝑁 + 1 ) ) ∧ ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ) → ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ) )
30	11 14 29	mp2and	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )
31		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
32		0exp	⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) = 0 )
33		0le1	⊢ 0 ≤ 1
34	32 33	eqbrtrdi	⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) ≤ 1 )
35		oveq2	⊢ ( 𝑁 = 0 → ( 0 ↑ 𝑁 ) = ( 0 ↑ 0 ) )
36		0exp0e1	⊢ ( 0 ↑ 0 ) = 1
37		1le1	⊢ 1 ≤ 1
38	36 37	eqbrtri	⊢ ( 0 ↑ 0 ) ≤ 1
39	35 38	eqbrtrdi	⊢ ( 𝑁 = 0 → ( 0 ↑ 𝑁 ) ≤ 1 )
40	34 39	jaoi	⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 0 ↑ 𝑁 ) ≤ 1 )
41	31 40	sylbi	⊢ ( 𝑁 ∈ ℕ0 → ( 0 ↑ 𝑁 ) ≤ 1 )
42		1nn	⊢ 1 ∈ ℕ
43		nnmulcl	⊢ ( ( 1 ∈ ℕ ∧ ( ! ‘ 𝑁 ) ∈ ℕ ) → ( 1 · ( ! ‘ 𝑁 ) ) ∈ ℕ )
44	42 23 43	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( 1 · ( ! ‘ 𝑁 ) ) ∈ ℕ )
45	44	nnge1d	⊢ ( 𝑁 ∈ ℕ0 → 1 ≤ ( 1 · ( ! ‘ 𝑁 ) ) )
46		0re	⊢ 0 ∈ ℝ
47		reexpcl	⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 0 ↑ 𝑁 ) ∈ ℝ )
48	46 47	mpan	⊢ ( 𝑁 ∈ ℕ0 → ( 0 ↑ 𝑁 ) ∈ ℝ )
49		1re	⊢ 1 ∈ ℝ
50		remulcl	⊢ ( ( 1 ∈ ℝ ∧ ( ! ‘ 𝑁 ) ∈ ℝ ) → ( 1 · ( ! ‘ 𝑁 ) ) ∈ ℝ )
51	49 24 50	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( 1 · ( ! ‘ 𝑁 ) ) ∈ ℝ )
52		letr	⊢ ( ( ( 0 ↑ 𝑁 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 1 · ( ! ‘ 𝑁 ) ) ∈ ℝ ) → ( ( ( 0 ↑ 𝑁 ) ≤ 1 ∧ 1 ≤ ( 1 · ( ! ‘ 𝑁 ) ) ) → ( 0 ↑ 𝑁 ) ≤ ( 1 · ( ! ‘ 𝑁 ) ) ) )
53	49 52	mp3an2	⊢ ( ( ( 0 ↑ 𝑁 ) ∈ ℝ ∧ ( 1 · ( ! ‘ 𝑁 ) ) ∈ ℝ ) → ( ( ( 0 ↑ 𝑁 ) ≤ 1 ∧ 1 ≤ ( 1 · ( ! ‘ 𝑁 ) ) ) → ( 0 ↑ 𝑁 ) ≤ ( 1 · ( ! ‘ 𝑁 ) ) ) )
54	48 51 53	syl2anc	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 0 ↑ 𝑁 ) ≤ 1 ∧ 1 ≤ ( 1 · ( ! ‘ 𝑁 ) ) ) → ( 0 ↑ 𝑁 ) ≤ ( 1 · ( ! ‘ 𝑁 ) ) ) )
55	41 45 54	mp2and	⊢ ( 𝑁 ∈ ℕ0 → ( 0 ↑ 𝑁 ) ≤ ( 1 · ( ! ‘ 𝑁 ) ) )
56	55	adantl	⊢ ( ( 𝑀 = 0 ∧ 𝑁 ∈ ℕ0 ) → ( 0 ↑ 𝑁 ) ≤ ( 1 · ( ! ‘ 𝑁 ) ) )
57		oveq1	⊢ ( 𝑀 = 0 → ( 𝑀 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
58		oveq12	⊢ ( ( 𝑀 = 0 ∧ 𝑀 = 0 ) → ( 𝑀 ↑ 𝑀 ) = ( 0 ↑ 0 ) )
59	58	anidms	⊢ ( 𝑀 = 0 → ( 𝑀 ↑ 𝑀 ) = ( 0 ↑ 0 ) )
60	59 36	eqtrdi	⊢ ( 𝑀 = 0 → ( 𝑀 ↑ 𝑀 ) = 1 )
61	60	oveq1d	⊢ ( 𝑀 = 0 → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) = ( 1 · ( ! ‘ 𝑁 ) ) )
62	57 61	breq12d	⊢ ( 𝑀 = 0 → ( ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ↔ ( 0 ↑ 𝑁 ) ≤ ( 1 · ( ! ‘ 𝑁 ) ) ) )
63	62	adantr	⊢ ( ( 𝑀 = 0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ↔ ( 0 ↑ 𝑁 ) ≤ ( 1 · ( ! ‘ 𝑁 ) ) ) )
64	56 63	mpbird	⊢ ( ( 𝑀 = 0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )
65	30 64	jaoian	⊢ ( ( ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )
66	1 65	sylanb	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )