facdiv

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

		Ref	Expression
	Assertion	facdiv	$⊢ (M \in ℕ_{0} \land N \in ℕ \land N \leq M) \to \frac{M!}{N} \in ℕ$

Proof

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

Metamath Proof Explorer

Theorem facdiv

Proof