Metamath Proof Explorer

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 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) → ( ( ! ‘ 𝑀 ) / 𝑁 ) ∈ ℕ )