dvdsfac

Description: A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012)

		Ref	Expression
	Assertion	dvdsfac	$⊢ (K \in ℕ \land N \in ℤ_{\geq K}) \to K ∥ N!$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = K \to x! = K!$
2	1	breq2d	$⊢ x = K \to (K ∥ x! \leftrightarrow K ∥ K!)$
3	2	imbi2d	$⊢ x = K \to ((K \in ℕ \to K ∥ x!) \leftrightarrow (K \in ℕ \to K ∥ K!))$
4		fveq2	$⊢ x = y \to x! = y!$
5	4	breq2d	$⊢ x = y \to (K ∥ x! \leftrightarrow K ∥ y!)$
6	5	imbi2d	$⊢ x = y \to ((K \in ℕ \to K ∥ x!) \leftrightarrow (K \in ℕ \to K ∥ y!))$
7		fveq2	$⊢ x = y + 1 \to x! = (y + 1)!$
8	7	breq2d	$⊢ x = y + 1 \to (K ∥ x! \leftrightarrow K ∥ (y + 1)!)$
9	8	imbi2d	$⊢ x = y + 1 \to ((K \in ℕ \to K ∥ x!) \leftrightarrow (K \in ℕ \to K ∥ (y + 1)!))$
10		fveq2	$⊢ x = N \to x! = N!$
11	10	breq2d	$⊢ x = N \to (K ∥ x! \leftrightarrow K ∥ N!)$
12	11	imbi2d	$⊢ x = N \to ((K \in ℕ \to K ∥ x!) \leftrightarrow (K \in ℕ \to K ∥ N!))$
13		nnm1nn0	$⊢ K \in ℕ \to K - 1 \in ℕ_{0}$
14	13	faccld	$⊢ K \in ℕ \to (K - 1)! \in ℕ$
15	14	nnzd	$⊢ K \in ℕ \to (K - 1)! \in ℤ$
16		nnz	$⊢ K \in ℕ \to K \in ℤ$
17		dvdsmul2	$⊢ ((K - 1)! \in ℤ \land K \in ℤ) \to K ∥ (K - 1)! K$
18	15 16 17	syl2anc	$⊢ K \in ℕ \to K ∥ (K - 1)! K$
19		facnn2	$⊢ K \in ℕ \to K! = (K - 1)! K$
20	18 19	breqtrrd	$⊢ K \in ℕ \to K ∥ K!$
21	16	adantl	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to K \in ℤ$
22		elnnuz	$⊢ K \in ℕ \leftrightarrow K \in ℤ_{\geq 1}$
23		uztrn	$⊢ (y \in ℤ_{\geq K} \land K \in ℤ_{\geq 1}) \to y \in ℤ_{\geq 1}$
24	22 23	sylan2b	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to y \in ℤ_{\geq 1}$
25		elnnuz	$⊢ y \in ℕ \leftrightarrow y \in ℤ_{\geq 1}$
26	24 25	sylibr	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to y \in ℕ$
27	26	nnnn0d	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to y \in ℕ_{0}$
28	27	faccld	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to y! \in ℕ$
29	28	nnzd	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to y! \in ℤ$
30	26	nnzd	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to y \in ℤ$
31	30	peano2zd	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to y + 1 \in ℤ$
32		dvdsmultr1	$⊢ (K \in ℤ \land y! \in ℤ \land y + 1 \in ℤ) \to (K ∥ y! \to K ∥ y! (y + 1))$
33	21 29 31 32	syl3anc	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to (K ∥ y! \to K ∥ y! (y + 1))$
34		facp1	$⊢ y \in ℕ_{0} \to (y + 1)! = y! (y + 1)$
35	27 34	syl	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to (y + 1)! = y! (y + 1)$
36	35	breq2d	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to (K ∥ (y + 1)! \leftrightarrow K ∥ y! (y + 1))$
37	33 36	sylibrd	$⊢ (y \in ℤ_{\geq K} \land K \in ℕ) \to (K ∥ y! \to K ∥ (y + 1)!)$
38	37	ex	$⊢ y \in ℤ_{\geq K} \to (K \in ℕ \to (K ∥ y! \to K ∥ (y + 1)!))$
39	38	a2d	$⊢ y \in ℤ_{\geq K} \to ((K \in ℕ \to K ∥ y!) \to (K \in ℕ \to K ∥ (y + 1)!))$
40	3 6 9 12 20 39	uzind4i	$⊢ N \in ℤ_{\geq K} \to (K \in ℕ \to K ∥ N!)$
41	40	impcom	$⊢ (K \in ℕ \land N \in ℤ_{\geq K}) \to K ∥ N!$

Metamath Proof Explorer

Theorem dvdsfac

Proof