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