This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem faclbnd5

Description: The factorial function grows faster than powers and exponentiations. If we consider K and M to be constants, the right-hand side of the inequality is a constant times N -factorial. (Contributed by NM, 24-Dec-2005)

Ref Expression
Assertion faclbnd5 ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) < ( ( 2 · ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ) · ( ! ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
2 reexpcl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 ↑ 𝐾 ) ∈ ℝ )
3 1 2 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 ↑ 𝐾 ) ∈ ℝ )
4 3 ancoms ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ↑ 𝐾 ) ∈ ℝ )
5 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
6 reexpcl ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ∈ ℝ )
7 5 6 sylan ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ∈ ℝ )
8 remulcl ⊢ ( ( ( 𝑁 ↑ 𝐾 ) ∈ ℝ ∧ ( 𝑀 ↑ 𝑁 ) ∈ ℝ ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ∈ ℝ )
9 4 7 8 syl2an ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ∈ ℝ )
10 9 anandirs ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ∈ ℝ )
11 2nn ⊢ 2 ∈ ℕ
12 nn0sqcl ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 ↑ 2 ) ∈ ℕ0 )
13 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ ( 𝐾 ↑ 2 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝐾 ↑ 2 ) ) ∈ ℕ )
14 11 12 13 sylancr ⊢ ( 𝐾 ∈ ℕ0 → ( 2 ↑ ( 𝐾 ↑ 2 ) ) ∈ ℕ )
15 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
16 nn0addcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 + 𝐾 ) ∈ ℕ0 )
17 16 ancoms ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 𝐾 ) ∈ ℕ0 )
18 15 17 sylan2 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( 𝑀 + 𝐾 ) ∈ ℕ0 )
19 nnexpcl ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑀 + 𝐾 ) ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ∈ ℕ )
20 18 19 sylan2 ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ) → ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ∈ ℕ )
21 20 anabss7 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ∈ ℕ )
22 nnmulcl ⊢ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) ∈ ℕ ∧ ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ∈ ℕ ) → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℕ )
23 14 21 22 syl2an2r ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℕ )
24 23 nnred ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℝ )
25 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
26 25 nnred ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℝ )
27 remulcl ⊢ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℝ ∧ ( ! ‘ 𝑁 ) ∈ ℝ ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℝ )
28 24 26 27 syl2an ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℝ )
29 2re ⊢ 2 ∈ ℝ
30 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℝ ) → ( 2 · ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) ∈ ℝ )
31 29 28 30 sylancr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) ∈ ℝ )
32 faclbnd4 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
33 15 32 syl3an3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
34 33 3coml ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
35 34 3expa ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
36 1lt2 ⊢ 1 < 2
37 nnmulcl ⊢ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℕ ∧ ( ! ‘ 𝑁 ) ∈ ℕ ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℕ )
38 23 25 37 syl2an ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℕ )
39 38 nngt0d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 0 < ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
40 ltmulgt12 ⊢ ( ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) → ( 1 < 2 ↔ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) < ( 2 · ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) ) )
41 29 40 mp3an2 ⊢ ( ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℝ ∧ 0 < ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) → ( 1 < 2 ↔ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) < ( 2 · ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) ) )
42 28 39 41 syl2anc ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 1 < 2 ↔ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) < ( 2 · ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) ) )
43 36 42 mpbii ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) < ( 2 · ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
44 10 28 31 35 43 lelttrd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) < ( 2 · ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
45 2cn ⊢ 2 ∈ ℂ
46 23 nncnd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℂ )
47 25 nncnd ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℂ )
48 mulass ⊢ ( ( 2 ∈ ℂ ∧ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℂ ∧ ( ! ‘ 𝑁 ) ∈ ℂ ) → ( ( 2 · ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( 2 · ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
49 45 46 47 48 mp3an3an ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 · ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( 2 · ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
50 44 49 breqtrrd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) < ( ( 2 · ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ) · ( ! ‘ 𝑁 ) ) )
51 50 3impa ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) < ( ( 2 · ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ) · ( ! ‘ 𝑁 ) ) )
52 51 3comr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) < ( ( 2 · ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ) · ( ! ‘ 𝑁 ) ) )