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 syl5bir ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( ( ¬ 𝑃 ∥ ( ! ‘ ( 𝑃𝑁 ) ) ∧ ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) → ¬ 𝑃 ∥ ( ( ! ‘ ( 𝑃𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
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 𝑁 ) )