Metamath Proof Explorer

Theorem faclbnd4lem3

Description: Lemma for faclbnd4 . The N = 0 case. (Contributed by NM, 23-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) )
2 0exp ⊢ ( 𝐾 ∈ ℕ → ( 0 ↑ 𝐾 ) = 0 )
3 2 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( 0 ↑ 𝐾 ) = 0 )
4 nnnn0 ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
5 2nn0 ⊢ 2 ∈ ℕ0
6 nn0sqcl ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 ↑ 2 ) ∈ ℕ0 )
7 nn0expcl ⊢ ( ( 2 ∈ ℕ0 ∧ ( 𝐾 ↑ 2 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝐾 ↑ 2 ) ) ∈ ℕ0 )
8 5 6 7 sylancr ⊢ ( 𝐾 ∈ ℕ0 → ( 2 ↑ ( 𝐾 ↑ 2 ) ) ∈ ℕ0 )
9 8 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 2 ↑ ( 𝐾 ↑ 2 ) ) ∈ ℕ0 )
10 nn0addcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 + 𝐾 ) ∈ ℕ0 )
11 nn0expcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ∈ ℕ0 )
12 10 11 syldan ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ∈ ℕ0 )
13 9 12 nn0mulcld ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℕ0 )
14 4 13 sylan2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℕ0 )
15 14 nn0ge0d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → 0 ≤ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) )
16 3 15 eqbrtrd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( 0 ↑ 𝐾 ) ≤ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) )
17 1nn ⊢ 1 ∈ ℕ
18 elnn0 ⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
19 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
20 0nn0 ⊢ 0 ∈ ℕ0
21 nn0addcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( 𝑀 + 0 ) ∈ ℕ0 )
22 19 20 21 sylancl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 + 0 ) ∈ ℕ0 )
23 nnexpcl ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑀 + 0 ) ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑀 + 0 ) ) ∈ ℕ )
24 22 23 mpdan ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 𝑀 + 0 ) ) ∈ ℕ )
25 id ⊢ ( 𝑀 = 0 → 𝑀 = 0 )
26 oveq1 ⊢ ( 𝑀 = 0 → ( 𝑀 + 0 ) = ( 0 + 0 ) )
27 00id ⊢ ( 0 + 0 ) = 0
28 26 27 eqtrdi ⊢ ( 𝑀 = 0 → ( 𝑀 + 0 ) = 0 )
29 25 28 oveq12d ⊢ ( 𝑀 = 0 → ( 𝑀 ↑ ( 𝑀 + 0 ) ) = ( 0 ↑ 0 ) )
30 0exp0e1 ⊢ ( 0 ↑ 0 ) = 1
31 29 30 eqtrdi ⊢ ( 𝑀 = 0 → ( 𝑀 ↑ ( 𝑀 + 0 ) ) = 1 )
32 31 17 eqeltrdi ⊢ ( 𝑀 = 0 → ( 𝑀 ↑ ( 𝑀 + 0 ) ) ∈ ℕ )
33 24 32 jaoi ⊢ ( ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) → ( 𝑀 ↑ ( 𝑀 + 0 ) ) ∈ ℕ )
34 18 33 sylbi ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ↑ ( 𝑀 + 0 ) ) ∈ ℕ )
35 nnmulcl ⊢ ( ( 1 ∈ ℕ ∧ ( 𝑀 ↑ ( 𝑀 + 0 ) ) ∈ ℕ ) → ( 1 · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) ∈ ℕ )
36 17 34 35 sylancr ⊢ ( 𝑀 ∈ ℕ0 → ( 1 · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) ∈ ℕ )
37 36 nnge1d ⊢ ( 𝑀 ∈ ℕ0 → 1 ≤ ( 1 · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) )
38 37 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 = 0 ) → 1 ≤ ( 1 · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) )
39 oveq2 ⊢ ( 𝐾 = 0 → ( 0 ↑ 𝐾 ) = ( 0 ↑ 0 ) )
40 39 30 eqtrdi ⊢ ( 𝐾 = 0 → ( 0 ↑ 𝐾 ) = 1 )
41 sq0i ⊢ ( 𝐾 = 0 → ( 𝐾 ↑ 2 ) = 0 )
42 41 oveq2d ⊢ ( 𝐾 = 0 → ( 2 ↑ ( 𝐾 ↑ 2 ) ) = ( 2 ↑ 0 ) )
43 2cn ⊢ 2 ∈ ℂ
44 exp0 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
45 43 44 ax-mp ⊢ ( 2 ↑ 0 ) = 1
46 42 45 eqtrdi ⊢ ( 𝐾 = 0 → ( 2 ↑ ( 𝐾 ↑ 2 ) ) = 1 )
47 oveq2 ⊢ ( 𝐾 = 0 → ( 𝑀 + 𝐾 ) = ( 𝑀 + 0 ) )
48 47 oveq2d ⊢ ( 𝐾 = 0 → ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) = ( 𝑀 ↑ ( 𝑀 + 0 ) ) )
49 46 48 oveq12d ⊢ ( 𝐾 = 0 → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) = ( 1 · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) )
50 40 49 breq12d ⊢ ( 𝐾 = 0 → ( ( 0 ↑ 𝐾 ) ≤ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ↔ 1 ≤ ( 1 · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) ) )
51 50 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 = 0 ) → ( ( 0 ↑ 𝐾 ) ≤ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ↔ 1 ≤ ( 1 · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) ) )
52 38 51 mpbird ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 = 0 ) → ( 0 ↑ 𝐾 ) ≤ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) )
53 16 52 jaodan ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) ) → ( 0 ↑ 𝐾 ) ≤ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) )
54 1 53 sylan2b ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 0 ↑ 𝐾 ) ≤ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) )
55 nn0cn ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
56 55 exp0d ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ↑ 0 ) = 1 )
57 56 oveq2d ⊢ ( 𝑀 ∈ ℕ0 → ( ( 0 ↑ 𝐾 ) · ( 𝑀 ↑ 0 ) ) = ( ( 0 ↑ 𝐾 ) · 1 ) )
58 nn0expcl ⊢ ( ( 0 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 0 ↑ 𝐾 ) ∈ ℕ0 )
59 20 58 mpan ⊢ ( 𝐾 ∈ ℕ0 → ( 0 ↑ 𝐾 ) ∈ ℕ0 )
60 59 nn0cnd ⊢ ( 𝐾 ∈ ℕ0 → ( 0 ↑ 𝐾 ) ∈ ℂ )
61 60 mulridd ⊢ ( 𝐾 ∈ ℕ0 → ( ( 0 ↑ 𝐾 ) · 1 ) = ( 0 ↑ 𝐾 ) )
62 57 61 sylan9eq ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( 0 ↑ 𝐾 ) · ( 𝑀 ↑ 0 ) ) = ( 0 ↑ 𝐾 ) )
63 13 nn0cnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℂ )
64 63 mulridd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · 1 ) = ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) )
65 54 62 64 3brtr4d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( 0 ↑ 𝐾 ) · ( 𝑀 ↑ 0 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · 1 ) )
66 65 adantr ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑁 = 0 ) → ( ( 0 ↑ 𝐾 ) · ( 𝑀 ↑ 0 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · 1 ) )
67 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 ↑ 𝐾 ) = ( 0 ↑ 𝐾 ) )
68 oveq2 ⊢ ( 𝑁 = 0 → ( 𝑀 ↑ 𝑁 ) = ( 𝑀 ↑ 0 ) )
69 67 68 oveq12d ⊢ ( 𝑁 = 0 → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) = ( ( 0 ↑ 𝐾 ) · ( 𝑀 ↑ 0 ) ) )
70 fveq2 ⊢ ( 𝑁 = 0 → ( ! ‘ 𝑁 ) = ( ! ‘ 0 ) )
71 fac0 ⊢ ( ! ‘ 0 ) = 1
72 70 71 eqtrdi ⊢ ( 𝑁 = 0 → ( ! ‘ 𝑁 ) = 1 )
73 72 oveq2d ⊢ ( 𝑁 = 0 → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) = ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · 1 ) )
74 69 73 breq12d ⊢ ( 𝑁 = 0 → ( ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ↔ ( ( 0 ↑ 𝐾 ) · ( 𝑀 ↑ 0 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · 1 ) ) )
75 74 adantl ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑁 = 0 ) → ( ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ↔ ( ( 0 ↑ 𝐾 ) · ( 𝑀 ↑ 0 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · 1 ) ) )
76 66 75 mpbird ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑁 = 0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )