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 ) ↑ 𝑀 ) ) ≤ ( ! ‘ ( 𝑁 + 𝑀 ) ) )