Metamath Proof Explorer

Theorem modprmn0modprm0

Description: For an integer not being 0 modulo a given prime number and a nonnegative integer less than the 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 integer and the first nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 10-Nov-2018)

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

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> P e. Prime )
2 prmnn 
 |-  ( P e. Prime -> P e. NN )
3 zmodfzo 
 |-  ( ( N e. ZZ /\ P e. NN ) -> ( N mod P ) e. ( 0 ..^ P ) )
4 2 3 sylan2 
 |-  ( ( N e. ZZ /\ P e. Prime ) -> ( N mod P ) e. ( 0 ..^ P ) )
5 4 ancoms 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( N mod P ) e. ( 0 ..^ P ) )
6 5 3adant3 
 |-  ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) -> ( N mod P ) e. ( 0 ..^ P ) )
7 fzo1fzo0n0 
 |-  ( ( N mod P ) e. ( 1 ..^ P ) <-> ( ( N mod P ) e. ( 0 ..^ P ) /\ ( N mod P ) =/= 0 ) )
8 7 simplbi2com 
 |-  ( ( N mod P ) =/= 0 -> ( ( N mod P ) e. ( 0 ..^ P ) -> ( N mod P ) e. ( 1 ..^ P ) ) )
9 8 3ad2ant3 
 |-  ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) -> ( ( N mod P ) e. ( 0 ..^ P ) -> ( N mod P ) e. ( 1 ..^ P ) ) )
10 6 9 mpd 
 |-  ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) -> ( N mod P ) e. ( 1 ..^ P ) )
11 10 adantr 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> ( N mod P ) e. ( 1 ..^ P ) )
12 simpr 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> I e. ( 0 ..^ P ) )
13 nnnn0modprm0 
 |-  ( ( P e. Prime /\ ( N mod P ) e. ( 1 ..^ P ) /\ I e. ( 0 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. ( N mod P ) ) ) mod P ) = 0 )
14 1 11 12 13 syl3anc 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. ( N mod P ) ) ) mod P ) = 0 )
15 elfzoelz 
 |-  ( j e. ( 0 ..^ P ) -> j e. ZZ )
16 15 zcnd 
 |-  ( j e. ( 0 ..^ P ) -> j e. CC )
17 2 anim1ci 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( N e. ZZ /\ P e. NN ) )
18 zmodcl 
 |-  ( ( N e. ZZ /\ P e. NN ) -> ( N mod P ) e. NN0 )
19 nn0cn 
 |-  ( ( N mod P ) e. NN0 -> ( N mod P ) e. CC )
20 17 18 19 3syl 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( N mod P ) e. CC )
21 20 3adant3 
 |-  ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) -> ( N mod P ) e. CC )
22 21 adantr 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> ( N mod P ) e. CC )
23 mulcom 
 |-  ( ( j e. CC /\ ( N mod P ) e. CC ) -> ( j x. ( N mod P ) ) = ( ( N mod P ) x. j ) )
24 16 22 23 syl2anr 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> ( j x. ( N mod P ) ) = ( ( N mod P ) x. j ) )
25 24 oveq2d 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> ( I + ( j x. ( N mod P ) ) ) = ( I + ( ( N mod P ) x. j ) ) )
26 25 oveq1d 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> ( ( I + ( j x. ( N mod P ) ) ) mod P ) = ( ( I + ( ( N mod P ) x. j ) ) mod P ) )
27 elfzoelz 
 |-  ( I e. ( 0 ..^ P ) -> I e. ZZ )
28 27 zred 
 |-  ( I e. ( 0 ..^ P ) -> I e. RR )
29 28 adantl 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> I e. RR )
30 29 adantr 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> I e. RR )
31 zre 
 |-  ( N e. ZZ -> N e. RR )
32 31 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) -> N e. RR )
33 32 adantr 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> N e. RR )
34 33 adantr 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> N e. RR )
35 15 adantl 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> j e. ZZ )
36 2 nnrpd 
 |-  ( P e. Prime -> P e. RR+ )
37 36 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) -> P e. RR+ )
38 37 adantr 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> P e. RR+ )
39 38 adantr 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> P e. RR+ )
40 modaddmulmod 
 |-  ( ( ( I e. RR /\ N e. RR /\ j e. ZZ ) /\ P e. RR+ ) -> ( ( I + ( ( N mod P ) x. j ) ) mod P ) = ( ( I + ( N x. j ) ) mod P ) )
41 30 34 35 39 40 syl31anc 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> ( ( I + ( ( N mod P ) x. j ) ) mod P ) = ( ( I + ( N x. j ) ) mod P ) )
42 zcn 
 |-  ( N e. ZZ -> N e. CC )
43 42 adantr 
 |-  ( ( N e. ZZ /\ j e. ( 0 ..^ P ) ) -> N e. CC )
44 16 adantl 
 |-  ( ( N e. ZZ /\ j e. ( 0 ..^ P ) ) -> j e. CC )
45 43 44 mulcomd 
 |-  ( ( N e. ZZ /\ j e. ( 0 ..^ P ) ) -> ( N x. j ) = ( j x. N ) )
46 45 ex 
 |-  ( N e. ZZ -> ( j e. ( 0 ..^ P ) -> ( N x. j ) = ( j x. N ) ) )
47 46 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) -> ( j e. ( 0 ..^ P ) -> ( N x. j ) = ( j x. N ) ) )
48 47 adantr 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> ( j e. ( 0 ..^ P ) -> ( N x. j ) = ( j x. N ) ) )
49 48 imp 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> ( N x. j ) = ( j x. N ) )
50 49 oveq2d 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> ( I + ( N x. j ) ) = ( I + ( j x. N ) ) )
51 50 oveq1d 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> ( ( I + ( N x. j ) ) mod P ) = ( ( I + ( j x. N ) ) mod P ) )
52 26 41 51 3eqtrrd 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> ( ( I + ( j x. N ) ) mod P ) = ( ( I + ( j x. ( N mod P ) ) ) mod P ) )
53 52 eqeq1d 
 |-  ( ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) /\ j e. ( 0 ..^ P ) ) -> ( ( ( I + ( j x. N ) ) mod P ) = 0 <-> ( ( I + ( j x. ( N mod P ) ) ) mod P ) = 0 ) )
54 53 rexbidva 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> ( E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 <-> E. j e. ( 0 ..^ P ) ( ( I + ( j x. ( N mod P ) ) ) mod P ) = 0 ) )
55 14 54 mpbird 
 |-  ( ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) /\ I e. ( 0 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )
56 55 ex 
 |-  ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) -> ( I e. ( 0 ..^ P ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )