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 e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> P || ( P _C N ) )

Proof

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