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 mulid1d ( 𝐾 ∈ ℕ0 → ( ( 0 ↑ 𝐾 ) · 1 ) = ( 0 ↑ 𝐾 ) )
62 57 61 sylan9eq ( ( 𝑀 ∈ ℕ0𝐾 ∈ ℕ0 ) → ( ( 0 ↑ 𝐾 ) · ( 𝑀 ↑ 0 ) ) = ( 0 ↑ 𝐾 ) )
63 13 nn0cnd ( ( 𝑀 ∈ ℕ0𝐾 ∈ ℕ0 ) → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℂ )
64 63 mulid1d ( ( 𝑀 ∈ ℕ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 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )