Theorem dvdsfac

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

	Ref	Expression
Assertion	dvdsfac	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∥ ( ! ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝐾 → ( ! ‘ 𝑥 ) = ( ! ‘ 𝐾 ) )
2	1	breq2d	⊢ ( 𝑥 = 𝐾 → ( 𝐾 ∥ ( ! ‘ 𝑥 ) ↔ 𝐾 ∥ ( ! ‘ 𝐾 ) ) )
3	2	imbi2d	⊢ ( 𝑥 = 𝐾 → ( ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ 𝑥 ) ) ↔ ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ 𝐾 ) ) ) )
4		fveq2	⊢ ( 𝑥 = 𝑦 → ( ! ‘ 𝑥 ) = ( ! ‘ 𝑦 ) )
5	4	breq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐾 ∥ ( ! ‘ 𝑥 ) ↔ 𝐾 ∥ ( ! ‘ 𝑦 ) ) )
6	5	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ 𝑥 ) ) ↔ ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ 𝑦 ) ) ) )
7		fveq2	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ! ‘ 𝑥 ) = ( ! ‘ ( 𝑦 + 1 ) ) )
8	7	breq2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐾 ∥ ( ! ‘ 𝑥 ) ↔ 𝐾 ∥ ( ! ‘ ( 𝑦 + 1 ) ) ) )
9	8	imbi2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ 𝑥 ) ) ↔ ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ ( 𝑦 + 1 ) ) ) ) )
10		fveq2	⊢ ( 𝑥 = 𝑁 → ( ! ‘ 𝑥 ) = ( ! ‘ 𝑁 ) )
11	10	breq2d	⊢ ( 𝑥 = 𝑁 → ( 𝐾 ∥ ( ! ‘ 𝑥 ) ↔ 𝐾 ∥ ( ! ‘ 𝑁 ) ) )
12	11	imbi2d	⊢ ( 𝑥 = 𝑁 → ( ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ 𝑥 ) ) ↔ ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ 𝑁 ) ) ) )
13		nnm1nn0	⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
14	13	faccld	⊢ ( 𝐾 ∈ ℕ → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℕ )
15	14	nnzd	⊢ ( 𝐾 ∈ ℕ → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℤ )
16		nnz	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
17		dvdsmul2	⊢ ( ( ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∥ ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) )
18	15 16 17	syl2anc	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) )
19		facnn2	⊢ ( 𝐾 ∈ ℕ → ( ! ‘ 𝐾 ) = ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) )
20	18 19	breqtrrd	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ 𝐾 ) )
21	16	adantl	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → 𝐾 ∈ ℤ )
22		elnnuz	⊢ ( 𝐾 ∈ ℕ ↔ 𝐾 ∈ ( ℤ≥ ‘ 1 ) )
23		uztrn	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
24	22 23	sylan2b	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
25		elnnuz	⊢ ( 𝑦 ∈ ℕ ↔ 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
26	24 25	sylibr	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → 𝑦 ∈ ℕ )
27	26	nnnn0d	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → 𝑦 ∈ ℕ0 )
28	27	faccld	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → ( ! ‘ 𝑦 ) ∈ ℕ )
29	28	nnzd	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → ( ! ‘ 𝑦 ) ∈ ℤ )
30	26	nnzd	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → 𝑦 ∈ ℤ )
31	30	peano2zd	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → ( 𝑦 + 1 ) ∈ ℤ )
32		dvdsmultr1	⊢ ( ( 𝐾 ∈ ℤ ∧ ( ! ‘ 𝑦 ) ∈ ℤ ∧ ( 𝑦 + 1 ) ∈ ℤ ) → ( 𝐾 ∥ ( ! ‘ 𝑦 ) → 𝐾 ∥ ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ) )
33	21 29 31 32	syl3anc	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → ( 𝐾 ∥ ( ! ‘ 𝑦 ) → 𝐾 ∥ ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ) )
34		facp1	⊢ ( 𝑦 ∈ ℕ0 → ( ! ‘ ( 𝑦 + 1 ) ) = ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) )
35	27 34	syl	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → ( ! ‘ ( 𝑦 + 1 ) ) = ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) )
36	35	breq2d	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → ( 𝐾 ∥ ( ! ‘ ( 𝑦 + 1 ) ) ↔ 𝐾 ∥ ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ) )
37	33 36	sylibrd	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ℕ ) → ( 𝐾 ∥ ( ! ‘ 𝑦 ) → 𝐾 ∥ ( ! ‘ ( 𝑦 + 1 ) ) ) )
38	37	ex	⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝐾 ∈ ℕ → ( 𝐾 ∥ ( ! ‘ 𝑦 ) → 𝐾 ∥ ( ! ‘ ( 𝑦 + 1 ) ) ) ) )
39	38	a2d	⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ 𝑦 ) ) → ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ ( 𝑦 + 1 ) ) ) ) )
40	3 6 9 12 20 39	uzind4i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝐾 ∈ ℕ → 𝐾 ∥ ( ! ‘ 𝑁 ) ) )
41	40	impcom	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∥ ( ! ‘ 𝑁 ) )