Metamath Proof Explorer

Theorem prmdvdsbc

Description: Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023)

Ref Expression
Assertion prmdvdsbc ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( 𝑃 C 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) = ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) )
2 simpl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℙ )
3 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
4 3 nnzd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
5 1nn0 ⊢ 1 ∈ ℕ0
6 eluzmn ⊢ ( ( 𝑃 ∈ ℤ ∧ 1 ∈ ℕ0 ) → 𝑃 ∈ ( ℤ≥ ‘ ( 𝑃 − 1 ) ) )
7 4 5 6 sylancl ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ ( 𝑃 − 1 ) ) )
8 fzss2 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ ( 𝑃 − 1 ) ) → ( 1 ... ( 𝑃 − 1 ) ) ⊆ ( 1 ... 𝑃 ) )
9 7 8 syl ⊢ ( 𝑃 ∈ ℙ → ( 1 ... ( 𝑃 − 1 ) ) ⊆ ( 1 ... 𝑃 ) )
10 fz1ssfz0 ⊢ ( 1 ... 𝑃 ) ⊆ ( 0 ... 𝑃 )
11 9 10 sstrdi ⊢ ( 𝑃 ∈ ℙ → ( 1 ... ( 𝑃 − 1 ) ) ⊆ ( 0 ... 𝑃 ) )
12 11 sselda ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ( 0 ... 𝑃 ) )
13 bcval2 ⊢ ( 𝑁 ∈ ( 0 ... 𝑃 ) → ( 𝑃 C 𝑁 ) = ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
14 12 13 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑃 C 𝑁 ) = ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
15 3 nnnn0d ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ0 )
16 15 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℕ0 )
17 elfzelz ⊢ ( 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑁 ∈ ℤ )
18 17 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ℤ )
19 bccl ⊢ ( ( 𝑃 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( 𝑃 C 𝑁 ) ∈ ℕ0 )
20 16 18 19 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑃 C 𝑁 ) ∈ ℕ0 )
21 20 nn0zd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑃 C 𝑁 ) ∈ ℤ )
22 14 21 eqeltrrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) ∈ ℤ )
23 elfznn ⊢ ( 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑁 ∈ ℕ )
24 23 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ℕ )
25 24 nnnn0d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ℕ0 )
26 1zzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 1 ∈ ℤ )
27 4 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℤ )
28 simpr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) )
29 elfzm11 ⊢ ( ( 1 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ∧ 𝑁 < 𝑃 ) ) )
30 29 biimpa ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ∧ 𝑁 < 𝑃 ) )
31 30 simp3d ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 < 𝑃 )
32 26 27 28 31 syl21anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 < 𝑃 )
33 ltsubnn0 ⊢ ( ( 𝑃 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < 𝑃 → ( 𝑃 − 𝑁 ) ∈ ℕ0 ) )
34 33 imp ⊢ ( ( ( 𝑃 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 < 𝑃 ) → ( 𝑃 − 𝑁 ) ∈ ℕ0 )
35 16 25 32 34 syl21anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑃 − 𝑁 ) ∈ ℕ0 )
36 35 faccld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℕ )
37 36 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ )
38 25 faccld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ 𝑁 ) ∈ ℕ )
39 38 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ 𝑁 ) ∈ ℤ )
40 37 39 zmulcld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ∈ ℤ )
41 37 zcnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℂ )
42 39 zcnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ 𝑁 ) ∈ ℂ )
43 facne0 ⊢ ( ( 𝑃 − 𝑁 ) ∈ ℕ0 → ( ! ‘ ( 𝑃 − 𝑁 ) ) ≠ 0 )
44 35 43 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ ( 𝑃 − 𝑁 ) ) ≠ 0 )
45 facne0 ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ≠ 0 )
46 25 45 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ 𝑁 ) ≠ 0 )
47 41 42 44 46 mulne0d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ≠ 0 )
48 uzid ⊢ ( 𝑃 ∈ ℤ → 𝑃 ∈ ( ℤ≥ ‘ 𝑃 ) )
49 4 48 syl ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 𝑃 ) )
50 dvdsfac ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 𝑃 ) ) → 𝑃 ∥ ( ! ‘ 𝑃 ) )
51 3 49 50 syl2anc ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∥ ( ! ‘ 𝑃 ) )
52 51 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( ! ‘ 𝑃 ) )
53 16 nn0red ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℝ )
54 24 nnrpd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ℝ+ )
55 53 54 ltsubrpd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑃 − 𝑁 ) < 𝑃 )
56 prmndvdsfaclt ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 − 𝑁 ) ∈ ℕ0 ) → ( ( 𝑃 − 𝑁 ) < 𝑃 → ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ) )
57 56 imp ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 − 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑃 − 𝑁 ) < 𝑃 ) → ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) )
58 2 35 55 57 syl21anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) )
59 prmndvdsfaclt ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < 𝑃 → ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) )
60 59 imp ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 < 𝑃 ) → ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) )
61 2 25 32 60 syl21anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) )
62 ioran ⊢ ( ¬ ( 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∨ 𝑃 ∥ ( ! ‘ 𝑁 ) ) ↔ ( ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∧ ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) )
63 euclemma ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ↔ ( 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∨ 𝑃 ∥ ( ! ‘ 𝑁 ) ) ) )
64 63 biimpd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) → ( 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∨ 𝑃 ∥ ( ! ‘ 𝑁 ) ) ) )
65 64 con3d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( ¬ ( 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∨ 𝑃 ∥ ( ! ‘ 𝑁 ) ) → ¬ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
66 62 65 biimtrrid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( ( ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∧ ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) → ¬ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
67 66 imp ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) ∧ ( ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∧ ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) ) → ¬ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) )
68 2 37 39 58 61 67 syl32anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) )
69 1 2 22 40 47 52 68 dvdszzq ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
70 69 14 breqtrrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( 𝑃 C 𝑁 ) )