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 P N 1 P 1 P ( P N)

Proof

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