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

Metamath Proof Explorer

Theorem faclbnd4

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

Ref Expression
Assertion faclbnd4 ⊢ N ∈ ℕ 0 ∧ K ∈ ℕ 0 ∧ M ∈ ℕ 0 → N K ⁢ M N ≤ 2 K 2 ⁢ M M + K ⁢ N !

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
2 faclbnd4lem4 ⊢ N ∈ ℕ ∧ K ∈ ℕ 0 ∧ M ∈ ℕ 0 → N K ⁢ M N ≤ 2 K 2 ⁢ M M + K ⁢ N !
3 2 3com13 ⊢ M ∈ ℕ 0 ∧ K ∈ ℕ 0 ∧ N ∈ ℕ → N K ⁢ M N ≤ 2 K 2 ⁢ M M + K ⁢ N !
4 3 3expa ⊢ M ∈ ℕ 0 ∧ K ∈ ℕ 0 ∧ N ∈ ℕ → N K ⁢ M N ≤ 2 K 2 ⁢ M M + K ⁢ N !
5 faclbnd4lem3 ⊢ M ∈ ℕ 0 ∧ K ∈ ℕ 0 ∧ N = 0 → N K ⁢ M N ≤ 2 K 2 ⁢ M M + K ⁢ N !
6 4 5 jaodan ⊢ M ∈ ℕ 0 ∧ K ∈ ℕ 0 ∧ N ∈ ℕ ∨ N = 0 → N K ⁢ M N ≤ 2 K 2 ⁢ M M + K ⁢ N !
7 1 6 sylan2b ⊢ M ∈ ℕ 0 ∧ K ∈ ℕ 0 ∧ N ∈ ℕ 0 → N K ⁢ M N ≤ 2 K 2 ⁢ M M + K ⁢ N !
8 7 3impa ⊢ M ∈ ℕ 0 ∧ K ∈ ℕ 0 ∧ N ∈ ℕ 0 → N K ⁢ M N ≤ 2 K 2 ⁢ M M + K ⁢ N !
9 8 3com13 ⊢ N ∈ ℕ 0 ∧ K ∈ ℕ 0 ∧ M ∈ ℕ 0 → N K ⁢ M N ≤ 2 K 2 ⁢ M M + K ⁢ N !