Metamath Proof Explorer

Theorem nnnn0modprm0

Description: For a positive integer and a nonnegative integer both less than a given prime number there is always a second nonnegative integer (less than the given prime number) so that the sum of this second nonnegative integer multiplied with the positive integer and the first nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 8-Nov-2018)

Ref Expression
Assertion nnnn0modprm0 
|- ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 0 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( P e. Prime -> P e. NN )
2 1 adantr 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> P e. NN )
3 fzo0sn0fzo1 
 |-  ( P e. NN -> ( 0 ..^ P ) = ( { 0 } u. ( 1 ..^ P ) ) )
4 2 3 syl 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( 0 ..^ P ) = ( { 0 } u. ( 1 ..^ P ) ) )
5 4 eleq2d 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( I e. ( 0 ..^ P ) <-> I e. ( { 0 } u. ( 1 ..^ P ) ) ) )
6 elun 
 |-  ( I e. ( { 0 } u. ( 1 ..^ P ) ) <-> ( I e. { 0 } \/ I e. ( 1 ..^ P ) ) )
7 elsni 
 |-  ( I e. { 0 } -> I = 0 )
8 lbfzo0 
 |-  ( 0 e. ( 0 ..^ P ) <-> P e. NN )
9 1 8 sylibr 
 |-  ( P e. Prime -> 0 e. ( 0 ..^ P ) )
10 elfzoelz 
 |-  ( N e. ( 1 ..^ P ) -> N e. ZZ )
11 zcn 
 |-  ( N e. ZZ -> N e. CC )
12 mul02 
 |-  ( N e. CC -> ( 0 x. N ) = 0 )
13 12 oveq2d 
 |-  ( N e. CC -> ( 0 + ( 0 x. N ) ) = ( 0 + 0 ) )
14 00id 
 |-  ( 0 + 0 ) = 0
15 13 14 eqtrdi 
 |-  ( N e. CC -> ( 0 + ( 0 x. N ) ) = 0 )
16 10 11 15 3syl 
 |-  ( N e. ( 1 ..^ P ) -> ( 0 + ( 0 x. N ) ) = 0 )
17 16 adantl 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( 0 + ( 0 x. N ) ) = 0 )
18 17 oveq1d 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( ( 0 + ( 0 x. N ) ) mod P ) = ( 0 mod P ) )
19 nnrp 
 |-  ( P e. NN -> P e. RR+ )
20 0mod 
 |-  ( P e. RR+ -> ( 0 mod P ) = 0 )
21 1 19 20 3syl 
 |-  ( P e. Prime -> ( 0 mod P ) = 0 )
22 21 adantr 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( 0 mod P ) = 0 )
23 18 22 eqtrd 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( ( 0 + ( 0 x. N ) ) mod P ) = 0 )
24 oveq1 
 |-  ( j = 0 -> ( j x. N ) = ( 0 x. N ) )
25 24 oveq2d 
 |-  ( j = 0 -> ( 0 + ( j x. N ) ) = ( 0 + ( 0 x. N ) ) )
26 25 oveq1d 
 |-  ( j = 0 -> ( ( 0 + ( j x. N ) ) mod P ) = ( ( 0 + ( 0 x. N ) ) mod P ) )
27 26 eqeq1d 
 |-  ( j = 0 -> ( ( ( 0 + ( j x. N ) ) mod P ) = 0 <-> ( ( 0 + ( 0 x. N ) ) mod P ) = 0 ) )
28 27 rspcev 
 |-  ( ( 0 e. ( 0 ..^ P ) /\ ( ( 0 + ( 0 x. N ) ) mod P ) = 0 ) -> E. j e. ( 0 ..^ P ) ( ( 0 + ( j x. N ) ) mod P ) = 0 )
29 9 23 28 syl2an2r 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( 0 + ( j x. N ) ) mod P ) = 0 )
30 29 adantl 
 |-  ( ( I = 0 /\ ( P e. Prime /\ N e. ( 1 ..^ P ) ) ) -> E. j e. ( 0 ..^ P ) ( ( 0 + ( j x. N ) ) mod P ) = 0 )
31 oveq1 
 |-  ( I = 0 -> ( I + ( j x. N ) ) = ( 0 + ( j x. N ) ) )
32 31 oveq1d 
 |-  ( I = 0 -> ( ( I + ( j x. N ) ) mod P ) = ( ( 0 + ( j x. N ) ) mod P ) )
33 32 eqeq1d 
 |-  ( I = 0 -> ( ( ( I + ( j x. N ) ) mod P ) = 0 <-> ( ( 0 + ( j x. N ) ) mod P ) = 0 ) )
34 33 adantr 
 |-  ( ( I = 0 /\ ( P e. Prime /\ N e. ( 1 ..^ P ) ) ) -> ( ( ( I + ( j x. N ) ) mod P ) = 0 <-> ( ( 0 + ( j x. N ) ) mod P ) = 0 ) )
35 34 rexbidv 
 |-  ( ( I = 0 /\ ( P e. Prime /\ N e. ( 1 ..^ P ) ) ) -> ( E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 <-> E. j e. ( 0 ..^ P ) ( ( 0 + ( j x. N ) ) mod P ) = 0 ) )
36 30 35 mpbird 
 |-  ( ( I = 0 /\ ( P e. Prime /\ N e. ( 1 ..^ P ) ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )
37 36 ex 
 |-  ( I = 0 -> ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
38 7 37 syl 
 |-  ( I e. { 0 } -> ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
39 simpl 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> P e. Prime )
40 39 adantl 
 |-  ( ( I e. ( 1 ..^ P ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) ) ) -> P e. Prime )
41 simprr 
 |-  ( ( I e. ( 1 ..^ P ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) ) ) -> N e. ( 1 ..^ P ) )
42 simpl 
 |-  ( ( I e. ( 1 ..^ P ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) ) ) -> I e. ( 1 ..^ P ) )
43 modprm0 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )
44 40 41 42 43 syl3anc 
 |-  ( ( I e. ( 1 ..^ P ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )
45 44 ex 
 |-  ( I e. ( 1 ..^ P ) -> ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
46 38 45 jaoi 
 |-  ( ( I e. { 0 } \/ I e. ( 1 ..^ P ) ) -> ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
47 6 46 sylbi 
 |-  ( I e. ( { 0 } u. ( 1 ..^ P ) ) -> ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
48 47 com12 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( I e. ( { 0 } u. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
49 5 48 sylbid 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( I e. ( 0 ..^ P ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
50 49 3impia 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 0 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )