Metamath Proof Explorer

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 ) → ( 𝑀 ↑ 𝑁 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )