Metamath Proof Explorer

Theorem faclbnd6

Description: Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007)

Ref Expression
Assertion faclbnd6 ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑀 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑚 = 0 → ( ( 𝑁 + 1 ) ↑ 𝑚 ) = ( ( 𝑁 + 1 ) ↑ 0 ) )
2 1 oveq2d ⊢ ( 𝑚 = 0 → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑚 ) ) = ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 0 ) ) )
3 oveq2 ⊢ ( 𝑚 = 0 → ( 𝑁 + 𝑚 ) = ( 𝑁 + 0 ) )
4 3 fveq2d ⊢ ( 𝑚 = 0 → ( ! ‘ ( 𝑁 + 𝑚 ) ) = ( ! ‘ ( 𝑁 + 0 ) ) )
5 2 4 breq12d ⊢ ( 𝑚 = 0 → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑚 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑚 ) ) ↔ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 0 ) ) ≤ ( ! ‘ ( 𝑁 + 0 ) ) ) )
6 oveq2 ⊢ ( 𝑚 = 𝑘 → ( ( 𝑁 + 1 ) ↑ 𝑚 ) = ( ( 𝑁 + 1 ) ↑ 𝑘 ) )
7 6 oveq2d ⊢ ( 𝑚 = 𝑘 → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑚 ) ) = ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) )
8 oveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝑁 + 𝑚 ) = ( 𝑁 + 𝑘 ) )
9 8 fveq2d ⊢ ( 𝑚 = 𝑘 → ( ! ‘ ( 𝑁 + 𝑚 ) ) = ( ! ‘ ( 𝑁 + 𝑘 ) ) )
10 7 9 breq12d ⊢ ( 𝑚 = 𝑘 → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑚 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑚 ) ) ↔ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑘 ) ) ) )
11 oveq2 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( 𝑁 + 1 ) ↑ 𝑚 ) = ( ( 𝑁 + 1 ) ↑ ( 𝑘 + 1 ) ) )
12 11 oveq2d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑚 ) ) = ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ ( 𝑘 + 1 ) ) ) )
13 oveq2 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 𝑁 + 𝑚 ) = ( 𝑁 + ( 𝑘 + 1 ) ) )
14 13 fveq2d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ! ‘ ( 𝑁 + 𝑚 ) ) = ( ! ‘ ( 𝑁 + ( 𝑘 + 1 ) ) ) )
15 12 14 breq12d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑚 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑚 ) ) ↔ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ ( 𝑘 + 1 ) ) ) ≤ ( ! ‘ ( 𝑁 + ( 𝑘 + 1 ) ) ) ) )
16 oveq2 ⊢ ( 𝑚 = 𝑀 → ( ( 𝑁 + 1 ) ↑ 𝑚 ) = ( ( 𝑁 + 1 ) ↑ 𝑀 ) )
17 16 oveq2d ⊢ ( 𝑚 = 𝑀 → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑚 ) ) = ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑀 ) ) )
18 oveq2 ⊢ ( 𝑚 = 𝑀 → ( 𝑁 + 𝑚 ) = ( 𝑁 + 𝑀 ) )
19 18 fveq2d ⊢ ( 𝑚 = 𝑀 → ( ! ‘ ( 𝑁 + 𝑚 ) ) = ( ! ‘ ( 𝑁 + 𝑀 ) ) )
20 17 19 breq12d ⊢ ( 𝑚 = 𝑀 → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑚 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑚 ) ) ↔ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑀 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑀 ) ) ) )
21 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
22 21 nnred ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℝ )
23 22 leidd ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ≤ ( ! ‘ 𝑁 ) )
24 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
25 peano2cn ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 + 1 ) ∈ ℂ )
26 24 25 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
27 26 exp0d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) ↑ 0 ) = 1 )
28 27 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 0 ) ) = ( ( ! ‘ 𝑁 ) · 1 ) )
29 21 nncnd ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℂ )
30 29 mulridd ⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) · 1 ) = ( ! ‘ 𝑁 ) )
31 28 30 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 0 ) ) = ( ! ‘ 𝑁 ) )
32 24 addridd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 0 ) = 𝑁 )
33 32 fveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( 𝑁 + 0 ) ) = ( ! ‘ 𝑁 ) )
34 23 31 33 3brtr4d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 0 ) ) ≤ ( ! ‘ ( 𝑁 + 0 ) ) )
35 22 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑁 ) ∈ ℝ )
36 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
37 36 nn0red ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ )
38 reexpcl ⊢ ( ( ( 𝑁 + 1 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) ↑ 𝑘 ) ∈ ℝ )
39 37 38 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) ↑ 𝑘 ) ∈ ℝ )
40 35 39 remulcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ∈ ℝ )
41 nnnn0 ⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℕ0 )
42 41 nn0ge0d ⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → 0 ≤ ( ! ‘ 𝑁 ) )
43 21 42 syl ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ ( ! ‘ 𝑁 ) )
44 43 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ ( ! ‘ 𝑁 ) )
45 37 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℝ )
46 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
47 36 nn0ge0d ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ ( 𝑁 + 1 ) )
48 47 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ ( 𝑁 + 1 ) )
49 45 46 48 expge0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ ( ( 𝑁 + 1 ) ↑ 𝑘 ) )
50 35 39 44 49 mulge0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) )
51 40 50 jca ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ∈ ℝ ∧ 0 ≤ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ) )
52 nn0addcl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + 𝑘 ) ∈ ℕ0 )
53 52 faccld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ ( 𝑁 + 𝑘 ) ) ∈ ℕ )
54 53 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ ( 𝑁 + 𝑘 ) ) ∈ ℝ )
55 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
56 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
57 56 nn0red ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℝ )
58 readdcl ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ℝ )
59 55 57 58 syl2an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ℝ )
60 45 48 59 jca31 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) ∈ ℝ ∧ 0 ≤ ( 𝑁 + 1 ) ) ∧ ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ℝ ) )
61 51 54 60 jca31 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ∈ ℝ ∧ 0 ≤ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ) ∧ ( ! ‘ ( 𝑁 + 𝑘 ) ) ∈ ℝ ) ∧ ( ( ( 𝑁 + 1 ) ∈ ℝ ∧ 0 ≤ ( 𝑁 + 1 ) ) ∧ ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ℝ ) ) )
62 61 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑘 ) ) ) → ( ( ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ∈ ℝ ∧ 0 ≤ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ) ∧ ( ! ‘ ( 𝑁 + 𝑘 ) ) ∈ ℝ ) ∧ ( ( ( 𝑁 + 1 ) ∈ ℝ ∧ 0 ≤ ( 𝑁 + 1 ) ) ∧ ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ℝ ) ) )
63 32 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + 0 ) = 𝑁 )
64 nn0ge0 ⊢ ( 𝑘 ∈ ℕ0 → 0 ≤ 𝑘 )
65 64 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ 𝑘 )
66 0re ⊢ 0 ∈ ℝ
67 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
68 67 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
69 55 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
70 leadd2 ⊢ ( ( 0 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 ≤ 𝑘 ↔ ( 𝑁 + 0 ) ≤ ( 𝑁 + 𝑘 ) ) )
71 66 68 69 70 mp3an2i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 0 ≤ 𝑘 ↔ ( 𝑁 + 0 ) ≤ ( 𝑁 + 𝑘 ) ) )
72 65 71 mpbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + 0 ) ≤ ( 𝑁 + 𝑘 ) )
73 63 72 eqbrtrrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ≤ ( 𝑁 + 𝑘 ) )
74 52 nn0red ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + 𝑘 ) ∈ ℝ )
75 1re ⊢ 1 ∈ ℝ
76 leadd1 ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 + 𝑘 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑁 ≤ ( 𝑁 + 𝑘 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 𝑘 ) + 1 ) ) )
77 75 76 mp3an3 ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 + 𝑘 ) ∈ ℝ ) → ( 𝑁 ≤ ( 𝑁 + 𝑘 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 𝑘 ) + 1 ) ) )
78 69 74 77 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ≤ ( 𝑁 + 𝑘 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 𝑘 ) + 1 ) ) )
79 73 78 mpbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 𝑘 ) + 1 ) )
80 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
81 ax-1cn ⊢ 1 ∈ ℂ
82 addass ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 𝑘 ) + 1 ) = ( 𝑁 + ( 𝑘 + 1 ) ) )
83 81 82 mp3an3 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑁 + 𝑘 ) + 1 ) = ( 𝑁 + ( 𝑘 + 1 ) ) )
84 24 80 83 syl2an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 𝑘 ) + 1 ) = ( 𝑁 + ( 𝑘 + 1 ) ) )
85 79 84 breqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( 𝑁 + ( 𝑘 + 1 ) ) )
86 85 anim1ci ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑘 ) ) ) → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑘 ) ) ∧ ( 𝑁 + 1 ) ≤ ( 𝑁 + ( 𝑘 + 1 ) ) ) )
87 lemul12a ⊢ ( ( ( ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ∈ ℝ ∧ 0 ≤ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ) ∧ ( ! ‘ ( 𝑁 + 𝑘 ) ) ∈ ℝ ) ∧ ( ( ( 𝑁 + 1 ) ∈ ℝ ∧ 0 ≤ ( 𝑁 + 1 ) ) ∧ ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ℝ ) ) → ( ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑘 ) ) ∧ ( 𝑁 + 1 ) ≤ ( 𝑁 + ( 𝑘 + 1 ) ) ) → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) · ( 𝑁 + 1 ) ) ≤ ( ( ! ‘ ( 𝑁 + 𝑘 ) ) · ( 𝑁 + ( 𝑘 + 1 ) ) ) ) )
88 62 86 87 sylc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑘 ) ) ) → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) · ( 𝑁 + 1 ) ) ≤ ( ( ! ‘ ( 𝑁 + 𝑘 ) ) · ( 𝑁 + ( 𝑘 + 1 ) ) ) )
89 expp1 ⊢ ( ( ( 𝑁 + 1 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( 𝑁 + 1 ) ↑ 𝑘 ) · ( 𝑁 + 1 ) ) )
90 26 89 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( 𝑁 + 1 ) ↑ 𝑘 ) · ( 𝑁 + 1 ) ) )
91 90 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ ( 𝑘 + 1 ) ) ) = ( ( ! ‘ 𝑁 ) · ( ( ( 𝑁 + 1 ) ↑ 𝑘 ) · ( 𝑁 + 1 ) ) ) )
92 29 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑁 ) ∈ ℂ )
93 expcl ⊢ ( ( ( 𝑁 + 1 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) ↑ 𝑘 ) ∈ ℂ )
94 26 93 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) ↑ 𝑘 ) ∈ ℂ )
95 26 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℂ )
96 92 94 95 mulassd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) · ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( ( ( 𝑁 + 1 ) ↑ 𝑘 ) · ( 𝑁 + 1 ) ) ) )
97 91 96 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ ( 𝑘 + 1 ) ) ) = ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) · ( 𝑁 + 1 ) ) )
98 97 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑘 ) ) ) → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ ( 𝑘 + 1 ) ) ) = ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) · ( 𝑁 + 1 ) ) )
99 facp1 ⊢ ( ( 𝑁 + 𝑘 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑁 + 𝑘 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 + 𝑘 ) ) · ( ( 𝑁 + 𝑘 ) + 1 ) ) )
100 52 99 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ ( ( 𝑁 + 𝑘 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 + 𝑘 ) ) · ( ( 𝑁 + 𝑘 ) + 1 ) ) )
101 84 fveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ ( ( 𝑁 + 𝑘 ) + 1 ) ) = ( ! ‘ ( 𝑁 + ( 𝑘 + 1 ) ) ) )
102 84 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ! ‘ ( 𝑁 + 𝑘 ) ) · ( ( 𝑁 + 𝑘 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 + 𝑘 ) ) · ( 𝑁 + ( 𝑘 + 1 ) ) ) )
103 100 101 102 3eqtr3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ ( 𝑁 + ( 𝑘 + 1 ) ) ) = ( ( ! ‘ ( 𝑁 + 𝑘 ) ) · ( 𝑁 + ( 𝑘 + 1 ) ) ) )
104 103 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑘 ) ) ) → ( ! ‘ ( 𝑁 + ( 𝑘 + 1 ) ) ) = ( ( ! ‘ ( 𝑁 + 𝑘 ) ) · ( 𝑁 + ( 𝑘 + 1 ) ) ) )
105 88 98 104 3brtr4d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑘 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑘 ) ) ) → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ ( 𝑘 + 1 ) ) ) ≤ ( ! ‘ ( 𝑁 + ( 𝑘 + 1 ) ) ) )
106 5 10 15 20 34 105 nn0indd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) ↑ 𝑀 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑀 ) ) )