Theorem facdiv

Description: A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005)

	Ref	Expression
Assertion	facdiv	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) → ( ( ! ‘ 𝑀 ) / 𝑁 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑗 = 0 → ( 𝑁 ≤ 𝑗 ↔ 𝑁 ≤ 0 ) )
2		fveq2	⊢ ( 𝑗 = 0 → ( ! ‘ 𝑗 ) = ( ! ‘ 0 ) )
3	2	oveq1d	⊢ ( 𝑗 = 0 → ( ( ! ‘ 𝑗 ) / 𝑁 ) = ( ( ! ‘ 0 ) / 𝑁 ) )
4	3	eleq1d	⊢ ( 𝑗 = 0 → ( ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ↔ ( ( ! ‘ 0 ) / 𝑁 ) ∈ ℕ ) )
5	1 4	imbi12d	⊢ ( 𝑗 = 0 → ( ( 𝑁 ≤ 𝑗 → ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ) ↔ ( 𝑁 ≤ 0 → ( ( ! ‘ 0 ) / 𝑁 ) ∈ ℕ ) ) )
6	5	imbi2d	⊢ ( 𝑗 = 0 → ( ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 𝑗 → ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ) ) ↔ ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 0 → ( ( ! ‘ 0 ) / 𝑁 ) ∈ ℕ ) ) ) )
7		breq2	⊢ ( 𝑗 = 𝑘 → ( 𝑁 ≤ 𝑗 ↔ 𝑁 ≤ 𝑘 ) )
8		fveq2	⊢ ( 𝑗 = 𝑘 → ( ! ‘ 𝑗 ) = ( ! ‘ 𝑘 ) )
9	8	oveq1d	⊢ ( 𝑗 = 𝑘 → ( ( ! ‘ 𝑗 ) / 𝑁 ) = ( ( ! ‘ 𝑘 ) / 𝑁 ) )
10	9	eleq1d	⊢ ( 𝑗 = 𝑘 → ( ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ↔ ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) )
11	7 10	imbi12d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 ≤ 𝑗 → ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ) ↔ ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) ) )
12	11	imbi2d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 𝑗 → ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ) ) ↔ ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) ) ) )
13		breq2	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑁 ≤ 𝑗 ↔ 𝑁 ≤ ( 𝑘 + 1 ) ) )
14		fveq2	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ! ‘ 𝑗 ) = ( ! ‘ ( 𝑘 + 1 ) ) )
15	14	oveq1d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ! ‘ 𝑗 ) / 𝑁 ) = ( ( ! ‘ ( 𝑘 + 1 ) ) / 𝑁 ) )
16	15	eleq1d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ↔ ( ( ! ‘ ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) )
17	13 16	imbi12d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑁 ≤ 𝑗 → ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ) ↔ ( 𝑁 ≤ ( 𝑘 + 1 ) → ( ( ! ‘ ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) )
18	17	imbi2d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 𝑗 → ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ) ) ↔ ( 𝑁 ∈ ℕ → ( 𝑁 ≤ ( 𝑘 + 1 ) → ( ( ! ‘ ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) ) )
19		breq2	⊢ ( 𝑗 = 𝑀 → ( 𝑁 ≤ 𝑗 ↔ 𝑁 ≤ 𝑀 ) )
20		fveq2	⊢ ( 𝑗 = 𝑀 → ( ! ‘ 𝑗 ) = ( ! ‘ 𝑀 ) )
21	20	oveq1d	⊢ ( 𝑗 = 𝑀 → ( ( ! ‘ 𝑗 ) / 𝑁 ) = ( ( ! ‘ 𝑀 ) / 𝑁 ) )
22	21	eleq1d	⊢ ( 𝑗 = 𝑀 → ( ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ↔ ( ( ! ‘ 𝑀 ) / 𝑁 ) ∈ ℕ ) )
23	19 22	imbi12d	⊢ ( 𝑗 = 𝑀 → ( ( 𝑁 ≤ 𝑗 → ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ) ↔ ( 𝑁 ≤ 𝑀 → ( ( ! ‘ 𝑀 ) / 𝑁 ) ∈ ℕ ) ) )
24	23	imbi2d	⊢ ( 𝑗 = 𝑀 → ( ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 𝑗 → ( ( ! ‘ 𝑗 ) / 𝑁 ) ∈ ℕ ) ) ↔ ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 𝑀 → ( ( ! ‘ 𝑀 ) / 𝑁 ) ∈ ℕ ) ) ) )
25		nnnle0	⊢ ( 𝑁 ∈ ℕ → ¬ 𝑁 ≤ 0 )
26	25	pm2.21d	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 0 → ( ( ! ‘ 0 ) / 𝑁 ) ∈ ℕ ) )
27		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
28		peano2nn0	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
29	28	nn0red	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℝ )
30		leloe	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( 𝑁 ≤ ( 𝑘 + 1 ) ↔ ( 𝑁 < ( 𝑘 + 1 ) ∨ 𝑁 = ( 𝑘 + 1 ) ) ) )
31	27 29 30	syl2an	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ≤ ( 𝑘 + 1 ) ↔ ( 𝑁 < ( 𝑘 + 1 ) ∨ 𝑁 = ( 𝑘 + 1 ) ) ) )
32		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
33		nn0leltp1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ≤ 𝑘 ↔ 𝑁 < ( 𝑘 + 1 ) ) )
34	32 33	sylan	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ≤ 𝑘 ↔ 𝑁 < ( 𝑘 + 1 ) ) )
35		nn0p1nn	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ )
36		nnmulcl	⊢ ( ( ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( ( ( ! ‘ 𝑘 ) / 𝑁 ) · ( 𝑘 + 1 ) ) ∈ ℕ )
37	35 36	sylan2	⊢ ( ( ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ! ‘ 𝑘 ) / 𝑁 ) · ( 𝑘 + 1 ) ) ∈ ℕ )
38	37	expcom	⊢ ( 𝑘 ∈ ℕ0 → ( ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ → ( ( ( ! ‘ 𝑘 ) / 𝑁 ) · ( 𝑘 + 1 ) ) ∈ ℕ ) )
39	38	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ → ( ( ( ! ‘ 𝑘 ) / 𝑁 ) · ( 𝑘 + 1 ) ) ∈ ℕ ) )
40		faccl	⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
41	40	nncnd	⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℂ )
42	28	nn0cnd	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℂ )
43		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
44		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
45	43 44	jca	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
46	45	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
47		div23	⊢ ( ( ( ! ‘ 𝑘 ) ∈ ℂ ∧ ( 𝑘 + 1 ) ∈ ℂ ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) = ( ( ( ! ‘ 𝑘 ) / 𝑁 ) · ( 𝑘 + 1 ) ) )
48	41 42 46 47	syl2an23an	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) = ( ( ( ! ‘ 𝑘 ) / 𝑁 ) · ( 𝑘 + 1 ) ) )
49	48	eleq1d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ↔ ( ( ( ! ‘ 𝑘 ) / 𝑁 ) · ( 𝑘 + 1 ) ) ∈ ℕ ) )
50	39 49	sylibrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) )
51	50	imim2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) → ( 𝑁 ≤ 𝑘 → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) )
52	51	com23	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ≤ 𝑘 → ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) )
53	34 52	sylbird	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 < ( 𝑘 + 1 ) → ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) )
54	41	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℂ )
55	43	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
56	44	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ≠ 0 )
57	54 55 56	divcan4d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ! ‘ 𝑘 ) · 𝑁 ) / 𝑁 ) = ( ! ‘ 𝑘 ) )
58	40	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℕ )
59	57 58	eqeltrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ! ‘ 𝑘 ) · 𝑁 ) / 𝑁 ) ∈ ℕ )
60		oveq2	⊢ ( 𝑁 = ( 𝑘 + 1 ) → ( ( ! ‘ 𝑘 ) · 𝑁 ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
61	60	oveq1d	⊢ ( 𝑁 = ( 𝑘 + 1 ) → ( ( ( ! ‘ 𝑘 ) · 𝑁 ) / 𝑁 ) = ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) )
62	61	eleq1d	⊢ ( 𝑁 = ( 𝑘 + 1 ) → ( ( ( ( ! ‘ 𝑘 ) · 𝑁 ) / 𝑁 ) ∈ ℕ ↔ ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) )
63	59 62	syl5ibcom	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 = ( 𝑘 + 1 ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) )
64	63	a1dd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 = ( 𝑘 + 1 ) → ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) )
65	53 64	jaod	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 < ( 𝑘 + 1 ) ∨ 𝑁 = ( 𝑘 + 1 ) ) → ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) )
66	31 65	sylbid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ≤ ( 𝑘 + 1 ) → ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) )
67	66	ex	⊢ ( 𝑁 ∈ ℕ → ( 𝑘 ∈ ℕ0 → ( 𝑁 ≤ ( 𝑘 + 1 ) → ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) ) )
68	67	com34	⊢ ( 𝑁 ∈ ℕ → ( 𝑘 ∈ ℕ0 → ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) → ( 𝑁 ≤ ( 𝑘 + 1 ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) ) )
69	68	com12	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑁 ∈ ℕ → ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) → ( 𝑁 ≤ ( 𝑘 + 1 ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) ) )
70	69	imp4d	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) ∧ 𝑁 ≤ ( 𝑘 + 1 ) ) ) → ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) )
71		facp1	⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
72	71	oveq1d	⊢ ( 𝑘 ∈ ℕ0 → ( ( ! ‘ ( 𝑘 + 1 ) ) / 𝑁 ) = ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) )
73	72	eleq1d	⊢ ( 𝑘 ∈ ℕ0 → ( ( ( ! ‘ ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ↔ ( ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) )
74	70 73	sylibrd	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) ∧ 𝑁 ≤ ( 𝑘 + 1 ) ) ) → ( ( ! ‘ ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) )
75	74	exp4d	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑁 ∈ ℕ → ( ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) → ( 𝑁 ≤ ( 𝑘 + 1 ) → ( ( ! ‘ ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) ) )
76	75	a2d	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 𝑘 → ( ( ! ‘ 𝑘 ) / 𝑁 ) ∈ ℕ ) ) → ( 𝑁 ∈ ℕ → ( 𝑁 ≤ ( 𝑘 + 1 ) → ( ( ! ‘ ( 𝑘 + 1 ) ) / 𝑁 ) ∈ ℕ ) ) ) )
77	6 12 18 24 26 76	nn0ind	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 𝑀 → ( ( ! ‘ 𝑀 ) / 𝑁 ) ∈ ℕ ) ) )
78	77	3imp	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) → ( ( ! ‘ 𝑀 ) / 𝑁 ) ∈ ℕ )