Theorem faclbnd4

Description: Variant of faclbnd5 providing a non-strict lower bound. (Contributed by NM, 23-Dec-2005)

	Ref	Expression
Assertion	faclbnd4	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2		faclbnd4lem4	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
3	2	3com13	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
4	3	3expa	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
5		faclbnd4lem3	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑁 = 0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
6	4 5	jaodan	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
7	1 6	sylan2b	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
8	7	3impa	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
9	8	3com13	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )