This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∥ ( ! ‘ 𝑁 ) )