Metamath Proof Explorer

Theorem facubnd

Description: An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016)

Ref Expression
Assertion facubnd ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ≤ ( 𝑁 ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑚 = 0 → ( ! ‘ 𝑚 ) = ( ! ‘ 0 ) )
2 fac0 ⊢ ( ! ‘ 0 ) = 1
3 1 2 eqtrdi ⊢ ( 𝑚 = 0 → ( ! ‘ 𝑚 ) = 1 )
4 id ⊢ ( 𝑚 = 0 → 𝑚 = 0 )
5 4 4 oveq12d ⊢ ( 𝑚 = 0 → ( 𝑚 ↑ 𝑚 ) = ( 0 ↑ 0 ) )
6 0exp0e1 ⊢ ( 0 ↑ 0 ) = 1
7 5 6 eqtrdi ⊢ ( 𝑚 = 0 → ( 𝑚 ↑ 𝑚 ) = 1 )
8 3 7 breq12d ⊢ ( 𝑚 = 0 → ( ( ! ‘ 𝑚 ) ≤ ( 𝑚 ↑ 𝑚 ) ↔ 1 ≤ 1 ) )
9 fveq2 ⊢ ( 𝑚 = 𝑘 → ( ! ‘ 𝑚 ) = ( ! ‘ 𝑘 ) )
10 id ⊢ ( 𝑚 = 𝑘 → 𝑚 = 𝑘 )
11 10 10 oveq12d ⊢ ( 𝑚 = 𝑘 → ( 𝑚 ↑ 𝑚 ) = ( 𝑘 ↑ 𝑘 ) )
12 9 11 breq12d ⊢ ( 𝑚 = 𝑘 → ( ( ! ‘ 𝑚 ) ≤ ( 𝑚 ↑ 𝑚 ) ↔ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) )
13 fveq2 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ! ‘ 𝑚 ) = ( ! ‘ ( 𝑘 + 1 ) ) )
14 id ⊢ ( 𝑚 = ( 𝑘 + 1 ) → 𝑚 = ( 𝑘 + 1 ) )
15 14 14 oveq12d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 𝑚 ↑ 𝑚 ) = ( ( 𝑘 + 1 ) ↑ ( 𝑘 + 1 ) ) )
16 13 15 breq12d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( ! ‘ 𝑚 ) ≤ ( 𝑚 ↑ 𝑚 ) ↔ ( ! ‘ ( 𝑘 + 1 ) ) ≤ ( ( 𝑘 + 1 ) ↑ ( 𝑘 + 1 ) ) ) )
17 fveq2 ⊢ ( 𝑚 = 𝑁 → ( ! ‘ 𝑚 ) = ( ! ‘ 𝑁 ) )
18 id ⊢ ( 𝑚 = 𝑁 → 𝑚 = 𝑁 )
19 18 18 oveq12d ⊢ ( 𝑚 = 𝑁 → ( 𝑚 ↑ 𝑚 ) = ( 𝑁 ↑ 𝑁 ) )
20 17 19 breq12d ⊢ ( 𝑚 = 𝑁 → ( ( ! ‘ 𝑚 ) ≤ ( 𝑚 ↑ 𝑚 ) ↔ ( ! ‘ 𝑁 ) ≤ ( 𝑁 ↑ 𝑁 ) ) )
21 1le1 ⊢ 1 ≤ 1
22 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
23 22 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
24 23 nnred ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( ! ‘ 𝑘 ) ∈ ℝ )
25 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
26 25 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → 𝑘 ∈ ℝ )
27 simpl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → 𝑘 ∈ ℕ0 )
28 26 27 reexpcld ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( 𝑘 ↑ 𝑘 ) ∈ ℝ )
29 nn0p1nn ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ )
30 29 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( 𝑘 + 1 ) ∈ ℕ )
31 30 nnred ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
32 31 27 reexpcld ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( ( 𝑘 + 1 ) ↑ 𝑘 ) ∈ ℝ )
33 simpr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) )
34 nn0ge0 ⊢ ( 𝑘 ∈ ℕ0 → 0 ≤ 𝑘 )
35 34 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → 0 ≤ 𝑘 )
36 26 lep1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → 𝑘 ≤ ( 𝑘 + 1 ) )
37 leexp1a ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 0 ≤ 𝑘 ∧ 𝑘 ≤ ( 𝑘 + 1 ) ) ) → ( 𝑘 ↑ 𝑘 ) ≤ ( ( 𝑘 + 1 ) ↑ 𝑘 ) )
38 26 31 27 35 36 37 syl32anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( 𝑘 ↑ 𝑘 ) ≤ ( ( 𝑘 + 1 ) ↑ 𝑘 ) )
39 24 28 32 33 38 letrd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( ! ‘ 𝑘 ) ≤ ( ( 𝑘 + 1 ) ↑ 𝑘 ) )
40 30 nngt0d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → 0 < ( 𝑘 + 1 ) )
41 lemul1 ⊢ ( ( ( ! ‘ 𝑘 ) ∈ ℝ ∧ ( ( 𝑘 + 1 ) ↑ 𝑘 ) ∈ ℝ ∧ ( ( 𝑘 + 1 ) ∈ ℝ ∧ 0 < ( 𝑘 + 1 ) ) ) → ( ( ! ‘ 𝑘 ) ≤ ( ( 𝑘 + 1 ) ↑ 𝑘 ) ↔ ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ≤ ( ( ( 𝑘 + 1 ) ↑ 𝑘 ) · ( 𝑘 + 1 ) ) ) )
42 24 32 31 40 41 syl112anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( ( ! ‘ 𝑘 ) ≤ ( ( 𝑘 + 1 ) ↑ 𝑘 ) ↔ ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ≤ ( ( ( 𝑘 + 1 ) ↑ 𝑘 ) · ( 𝑘 + 1 ) ) ) )
43 39 42 mpbid ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ≤ ( ( ( 𝑘 + 1 ) ↑ 𝑘 ) · ( 𝑘 + 1 ) ) )
44 facp1 ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
45 44 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
46 30 nncnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( 𝑘 + 1 ) ∈ ℂ )
47 46 27 expp1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( ( 𝑘 + 1 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( 𝑘 + 1 ) ↑ 𝑘 ) · ( 𝑘 + 1 ) ) )
48 43 45 47 3brtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) ) → ( ! ‘ ( 𝑘 + 1 ) ) ≤ ( ( 𝑘 + 1 ) ↑ ( 𝑘 + 1 ) ) )
49 48 ex ⊢ ( 𝑘 ∈ ℕ0 → ( ( ! ‘ 𝑘 ) ≤ ( 𝑘 ↑ 𝑘 ) → ( ! ‘ ( 𝑘 + 1 ) ) ≤ ( ( 𝑘 + 1 ) ↑ ( 𝑘 + 1 ) ) ) )
50 8 12 16 20 21 49 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ≤ ( 𝑁 ↑ 𝑁 ) )