Metamath Proof Explorer

Theorem modprm0

Description: For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018)

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

Proof

Step Hyp Ref Expression
1 reumodprminv 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> E! r e. ( 1 ... ( P - 1 ) ) ( ( N x. r ) mod P ) = 1 )
2 reurex 
 |-  ( E! r e. ( 1 ... ( P - 1 ) ) ( ( N x. r ) mod P ) = 1 -> E. r e. ( 1 ... ( P - 1 ) ) ( ( N x. r ) mod P ) = 1 )
3 prmz 
 |-  ( P e. Prime -> P e. ZZ )
4 3 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> P e. ZZ )
5 4 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> P e. ZZ )
6 elfzelz 
 |-  ( r e. ( 1 ... ( P - 1 ) ) -> r e. ZZ )
7 6 adantr 
 |-  ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) -> r e. ZZ )
8 elfzoelz 
 |-  ( I e. ( 1 ..^ P ) -> I e. ZZ )
9 8 3ad2ant3 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> I e. ZZ )
10 zmulcl 
 |-  ( ( r e. ZZ /\ I e. ZZ ) -> ( r x. I ) e. ZZ )
11 7 9 10 syl2an 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( r x. I ) e. ZZ )
12 5 11 zsubcld 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( P - ( r x. I ) ) e. ZZ )
13 prmnn 
 |-  ( P e. Prime -> P e. NN )
14 13 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> P e. NN )
15 14 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> P e. NN )
16 zmodfzo 
 |-  ( ( ( P - ( r x. I ) ) e. ZZ /\ P e. NN ) -> ( ( P - ( r x. I ) ) mod P ) e. ( 0 ..^ P ) )
17 12 15 16 syl2anc 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( P - ( r x. I ) ) mod P ) e. ( 0 ..^ P ) )
18 8 zred 
 |-  ( I e. ( 1 ..^ P ) -> I e. RR )
19 18 3ad2ant3 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> I e. RR )
20 19 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> I e. RR )
21 13 nnred 
 |-  ( P e. Prime -> P e. RR )
22 21 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> P e. RR )
23 22 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> P e. RR )
24 6 zred 
 |-  ( r e. ( 1 ... ( P - 1 ) ) -> r e. RR )
25 24 adantr 
 |-  ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) -> r e. RR )
26 remulcl 
 |-  ( ( r e. RR /\ I e. RR ) -> ( r x. I ) e. RR )
27 25 19 26 syl2an 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( r x. I ) e. RR )
28 23 27 resubcld 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( P - ( r x. I ) ) e. RR )
29 elfzoelz 
 |-  ( N e. ( 1 ..^ P ) -> N e. ZZ )
30 29 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> N e. ZZ )
31 30 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> N e. ZZ )
32 13 nnrpd 
 |-  ( P e. Prime -> P e. RR+ )
33 32 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> P e. RR+ )
34 33 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> P e. RR+ )
35 modaddmulmod 
 |-  ( ( ( I e. RR /\ ( P - ( r x. I ) ) e. RR /\ N e. ZZ ) /\ P e. RR+ ) -> ( ( I + ( ( ( P - ( r x. I ) ) mod P ) x. N ) ) mod P ) = ( ( I + ( ( P - ( r x. I ) ) x. N ) ) mod P ) )
36 20 28 31 34 35 syl31anc 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( I + ( ( ( P - ( r x. I ) ) mod P ) x. N ) ) mod P ) = ( ( I + ( ( P - ( r x. I ) ) x. N ) ) mod P ) )
37 13 nncnd 
 |-  ( P e. Prime -> P e. CC )
38 37 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> P e. CC )
39 38 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> P e. CC )
40 6 zcnd 
 |-  ( r e. ( 1 ... ( P - 1 ) ) -> r e. CC )
41 40 adantr 
 |-  ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) -> r e. CC )
42 8 zcnd 
 |-  ( I e. ( 1 ..^ P ) -> I e. CC )
43 42 3ad2ant3 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> I e. CC )
44 mulcl 
 |-  ( ( r e. CC /\ I e. CC ) -> ( r x. I ) e. CC )
45 41 43 44 syl2an 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( r x. I ) e. CC )
46 29 zcnd 
 |-  ( N e. ( 1 ..^ P ) -> N e. CC )
47 46 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> N e. CC )
48 47 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> N e. CC )
49 39 45 48 subdird 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( P - ( r x. I ) ) x. N ) = ( ( P x. N ) - ( ( r x. I ) x. N ) ) )
50 49 oveq2d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( I + ( ( P - ( r x. I ) ) x. N ) ) = ( I + ( ( P x. N ) - ( ( r x. I ) x. N ) ) ) )
51 50 oveq1d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( I + ( ( P - ( r x. I ) ) x. N ) ) mod P ) = ( ( I + ( ( P x. N ) - ( ( r x. I ) x. N ) ) ) mod P ) )
52 mulcom 
 |-  ( ( P e. CC /\ N e. CC ) -> ( P x. N ) = ( N x. P ) )
53 37 46 52 syl2an 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( P x. N ) = ( N x. P ) )
54 53 oveq1d 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( ( P x. N ) mod P ) = ( ( N x. P ) mod P ) )
55 mulmod0 
 |-  ( ( N e. ZZ /\ P e. RR+ ) -> ( ( N x. P ) mod P ) = 0 )
56 29 32 55 syl2anr 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( ( N x. P ) mod P ) = 0 )
57 54 56 eqtrd 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( ( P x. N ) mod P ) = 0 )
58 57 3adant3 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> ( ( P x. N ) mod P ) = 0 )
59 58 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( P x. N ) mod P ) = 0 )
60 41 adantr 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> r e. CC )
61 43 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> I e. CC )
62 60 61 48 mul32d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( r x. I ) x. N ) = ( ( r x. N ) x. I ) )
63 62 oveq1d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( r x. I ) x. N ) mod P ) = ( ( ( r x. N ) x. I ) mod P ) )
64 29 zred 
 |-  ( N e. ( 1 ..^ P ) -> N e. RR )
65 64 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> N e. RR )
66 remulcl 
 |-  ( ( r e. RR /\ N e. RR ) -> ( r x. N ) e. RR )
67 25 65 66 syl2an 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( r x. N ) e. RR )
68 9 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> I e. ZZ )
69 modmulmod 
 |-  ( ( ( r x. N ) e. RR /\ I e. ZZ /\ P e. RR+ ) -> ( ( ( ( r x. N ) mod P ) x. I ) mod P ) = ( ( ( r x. N ) x. I ) mod P ) )
70 67 68 34 69 syl3anc 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( ( r x. N ) mod P ) x. I ) mod P ) = ( ( ( r x. N ) x. I ) mod P ) )
71 63 70 eqtr4d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( r x. I ) x. N ) mod P ) = ( ( ( ( r x. N ) mod P ) x. I ) mod P ) )
72 59 71 oveq12d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( P x. N ) mod P ) - ( ( ( r x. I ) x. N ) mod P ) ) = ( 0 - ( ( ( ( r x. N ) mod P ) x. I ) mod P ) ) )
73 72 oveq1d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( ( P x. N ) mod P ) - ( ( ( r x. I ) x. N ) mod P ) ) mod P ) = ( ( 0 - ( ( ( ( r x. N ) mod P ) x. I ) mod P ) ) mod P ) )
74 remulcl 
 |-  ( ( P e. RR /\ N e. RR ) -> ( P x. N ) e. RR )
75 21 64 74 syl2an 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( P x. N ) e. RR )
76 75 3adant3 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> ( P x. N ) e. RR )
77 76 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( P x. N ) e. RR )
78 65 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> N e. RR )
79 27 78 remulcld 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( r x. I ) x. N ) e. RR )
80 modsubmodmod 
 |-  ( ( ( P x. N ) e. RR /\ ( ( r x. I ) x. N ) e. RR /\ P e. RR+ ) -> ( ( ( ( P x. N ) mod P ) - ( ( ( r x. I ) x. N ) mod P ) ) mod P ) = ( ( ( P x. N ) - ( ( r x. I ) x. N ) ) mod P ) )
81 77 79 34 80 syl3anc 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( ( P x. N ) mod P ) - ( ( ( r x. I ) x. N ) mod P ) ) mod P ) = ( ( ( P x. N ) - ( ( r x. I ) x. N ) ) mod P ) )
82 mulcom 
 |-  ( ( N e. CC /\ r e. CC ) -> ( N x. r ) = ( r x. N ) )
83 47 40 82 syl2anr 
 |-  ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( N x. r ) = ( r x. N ) )
84 83 oveq1d 
 |-  ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( N x. r ) mod P ) = ( ( r x. N ) mod P ) )
85 84 eqeq1d 
 |-  ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( N x. r ) mod P ) = 1 <-> ( ( r x. N ) mod P ) = 1 ) )
86 85 biimpd 
 |-  ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( N x. r ) mod P ) = 1 -> ( ( r x. N ) mod P ) = 1 ) )
87 86 impancom 
 |-  ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) -> ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> ( ( r x. N ) mod P ) = 1 ) )
88 87 imp 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( r x. N ) mod P ) = 1 )
89 88 oveq1d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( r x. N ) mod P ) x. I ) = ( 1 x. I ) )
90 89 oveq1d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( ( r x. N ) mod P ) x. I ) mod P ) = ( ( 1 x. I ) mod P ) )
91 90 oveq2d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( 0 - ( ( ( ( r x. N ) mod P ) x. I ) mod P ) ) = ( 0 - ( ( 1 x. I ) mod P ) ) )
92 91 oveq1d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( 0 - ( ( ( ( r x. N ) mod P ) x. I ) mod P ) ) mod P ) = ( ( 0 - ( ( 1 x. I ) mod P ) ) mod P ) )
93 61 mullidd 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( 1 x. I ) = I )
94 93 oveq1d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( 1 x. I ) mod P ) = ( I mod P ) )
95 32 18 anim12ci 
 |-  ( ( P e. Prime /\ I e. ( 1 ..^ P ) ) -> ( I e. RR /\ P e. RR+ ) )
96 elfzo2 
 |-  ( I e. ( 1 ..^ P ) <-> ( I e. ( ZZ>= ` 1 ) /\ P e. ZZ /\ I < P ) )
97 eluz2 
 |-  ( I e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ I e. ZZ /\ 1 <_ I ) )
98 0red 
 |-  ( I e. ZZ -> 0 e. RR )
99 1red 
 |-  ( I e. ZZ -> 1 e. RR )
100 zre 
 |-  ( I e. ZZ -> I e. RR )
101 98 99 100 3jca 
 |-  ( I e. ZZ -> ( 0 e. RR /\ 1 e. RR /\ I e. RR ) )
102 101 adantr 
 |-  ( ( I e. ZZ /\ 1 <_ I ) -> ( 0 e. RR /\ 1 e. RR /\ I e. RR ) )
103 0le1 
 |-  0 <_ 1
104 103 a1i 
 |-  ( I e. ZZ -> 0 <_ 1 )
105 104 anim1i 
 |-  ( ( I e. ZZ /\ 1 <_ I ) -> ( 0 <_ 1 /\ 1 <_ I ) )
106 letr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ I e. RR ) -> ( ( 0 <_ 1 /\ 1 <_ I ) -> 0 <_ I ) )
107 102 105 106 sylc 
 |-  ( ( I e. ZZ /\ 1 <_ I ) -> 0 <_ I )
108 107 3adant1 
 |-  ( ( 1 e. ZZ /\ I e. ZZ /\ 1 <_ I ) -> 0 <_ I )
109 97 108 sylbi 
 |-  ( I e. ( ZZ>= ` 1 ) -> 0 <_ I )
110 109 3ad2ant1 
 |-  ( ( I e. ( ZZ>= ` 1 ) /\ P e. ZZ /\ I < P ) -> 0 <_ I )
111 simp3 
 |-  ( ( I e. ( ZZ>= ` 1 ) /\ P e. ZZ /\ I < P ) -> I < P )
112 110 111 jca 
 |-  ( ( I e. ( ZZ>= ` 1 ) /\ P e. ZZ /\ I < P ) -> ( 0 <_ I /\ I < P ) )
113 96 112 sylbi 
 |-  ( I e. ( 1 ..^ P ) -> ( 0 <_ I /\ I < P ) )
114 113 adantl 
 |-  ( ( P e. Prime /\ I e. ( 1 ..^ P ) ) -> ( 0 <_ I /\ I < P ) )
115 95 114 jca 
 |-  ( ( P e. Prime /\ I e. ( 1 ..^ P ) ) -> ( ( I e. RR /\ P e. RR+ ) /\ ( 0 <_ I /\ I < P ) ) )
116 115 3adant2 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> ( ( I e. RR /\ P e. RR+ ) /\ ( 0 <_ I /\ I < P ) ) )
117 116 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( I e. RR /\ P e. RR+ ) /\ ( 0 <_ I /\ I < P ) ) )
118 modid 
 |-  ( ( ( I e. RR /\ P e. RR+ ) /\ ( 0 <_ I /\ I < P ) ) -> ( I mod P ) = I )
119 117 118 syl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( I mod P ) = I )
120 94 119 eqtrd 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( 1 x. I ) mod P ) = I )
121 120 oveq2d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( 0 - ( ( 1 x. I ) mod P ) ) = ( 0 - I ) )
122 121 oveq1d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( 0 - ( ( 1 x. I ) mod P ) ) mod P ) = ( ( 0 - I ) mod P ) )
123 92 122 eqtrd 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( 0 - ( ( ( ( r x. N ) mod P ) x. I ) mod P ) ) mod P ) = ( ( 0 - I ) mod P ) )
124 73 81 123 3eqtr3d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( ( P x. N ) - ( ( r x. I ) x. N ) ) mod P ) = ( ( 0 - I ) mod P ) )
125 124 oveq2d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( I + ( ( ( P x. N ) - ( ( r x. I ) x. N ) ) mod P ) ) = ( I + ( ( 0 - I ) mod P ) ) )
126 125 oveq1d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( I + ( ( ( P x. N ) - ( ( r x. I ) x. N ) ) mod P ) ) mod P ) = ( ( I + ( ( 0 - I ) mod P ) ) mod P ) )
127 77 79 resubcld 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( P x. N ) - ( ( r x. I ) x. N ) ) e. RR )
128 modadd2mod 
 |-  ( ( ( ( P x. N ) - ( ( r x. I ) x. N ) ) e. RR /\ I e. RR /\ P e. RR+ ) -> ( ( I + ( ( ( P x. N ) - ( ( r x. I ) x. N ) ) mod P ) ) mod P ) = ( ( I + ( ( P x. N ) - ( ( r x. I ) x. N ) ) ) mod P ) )
129 127 20 34 128 syl3anc 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( I + ( ( ( P x. N ) - ( ( r x. I ) x. N ) ) mod P ) ) mod P ) = ( ( I + ( ( P x. N ) - ( ( r x. I ) x. N ) ) ) mod P ) )
130 0red 
 |-  ( I e. ( 1 ..^ P ) -> 0 e. RR )
131 130 18 resubcld 
 |-  ( I e. ( 1 ..^ P ) -> ( 0 - I ) e. RR )
132 131 adantl 
 |-  ( ( P e. Prime /\ I e. ( 1 ..^ P ) ) -> ( 0 - I ) e. RR )
133 18 adantl 
 |-  ( ( P e. Prime /\ I e. ( 1 ..^ P ) ) -> I e. RR )
134 32 adantr 
 |-  ( ( P e. Prime /\ I e. ( 1 ..^ P ) ) -> P e. RR+ )
135 132 133 134 3jca 
 |-  ( ( P e. Prime /\ I e. ( 1 ..^ P ) ) -> ( ( 0 - I ) e. RR /\ I e. RR /\ P e. RR+ ) )
136 135 3adant2 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> ( ( 0 - I ) e. RR /\ I e. RR /\ P e. RR+ ) )
137 136 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( 0 - I ) e. RR /\ I e. RR /\ P e. RR+ ) )
138 modadd2mod 
 |-  ( ( ( 0 - I ) e. RR /\ I e. RR /\ P e. RR+ ) -> ( ( I + ( ( 0 - I ) mod P ) ) mod P ) = ( ( I + ( 0 - I ) ) mod P ) )
139 137 138 syl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( I + ( ( 0 - I ) mod P ) ) mod P ) = ( ( I + ( 0 - I ) ) mod P ) )
140 0cnd 
 |-  ( I e. ( 1 ..^ P ) -> 0 e. CC )
141 42 140 pncan3d 
 |-  ( I e. ( 1 ..^ P ) -> ( I + ( 0 - I ) ) = 0 )
142 141 3ad2ant3 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> ( I + ( 0 - I ) ) = 0 )
143 142 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( I + ( 0 - I ) ) = 0 )
144 143 oveq1d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( I + ( 0 - I ) ) mod P ) = ( 0 mod P ) )
145 0mod 
 |-  ( P e. RR+ -> ( 0 mod P ) = 0 )
146 32 145 syl 
 |-  ( P e. Prime -> ( 0 mod P ) = 0 )
147 146 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> ( 0 mod P ) = 0 )
148 147 adantl 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( 0 mod P ) = 0 )
149 139 144 148 3eqtrd 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( I + ( ( 0 - I ) mod P ) ) mod P ) = 0 )
150 126 129 149 3eqtr3d 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( I + ( ( P x. N ) - ( ( r x. I ) x. N ) ) ) mod P ) = 0 )
151 36 51 150 3eqtrd 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> ( ( I + ( ( ( P - ( r x. I ) ) mod P ) x. N ) ) mod P ) = 0 )
152 oveq1 
 |-  ( j = ( ( P - ( r x. I ) ) mod P ) -> ( j x. N ) = ( ( ( P - ( r x. I ) ) mod P ) x. N ) )
153 152 oveq2d 
 |-  ( j = ( ( P - ( r x. I ) ) mod P ) -> ( I + ( j x. N ) ) = ( I + ( ( ( P - ( r x. I ) ) mod P ) x. N ) ) )
154 153 oveq1d 
 |-  ( j = ( ( P - ( r x. I ) ) mod P ) -> ( ( I + ( j x. N ) ) mod P ) = ( ( I + ( ( ( P - ( r x. I ) ) mod P ) x. N ) ) mod P ) )
155 154 eqeq1d 
 |-  ( j = ( ( P - ( r x. I ) ) mod P ) -> ( ( ( I + ( j x. N ) ) mod P ) = 0 <-> ( ( I + ( ( ( P - ( r x. I ) ) mod P ) x. N ) ) mod P ) = 0 ) )
156 155 rspcev 
 |-  ( ( ( ( P - ( r x. I ) ) mod P ) e. ( 0 ..^ P ) /\ ( ( I + ( ( ( P - ( r x. I ) ) mod P ) x. N ) ) mod P ) = 0 ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )
157 17 151 156 syl2anc 
 |-  ( ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) /\ ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )
158 157 ex 
 |-  ( ( r e. ( 1 ... ( P - 1 ) ) /\ ( ( N x. r ) mod P ) = 1 ) -> ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
159 158 rexlimiva 
 |-  ( E. r e. ( 1 ... ( P - 1 ) ) ( ( N x. r ) mod P ) = 1 -> ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
160 1 2 159 3syl 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) ) -> ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
161 160 3adant3 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
162 161 pm2.43i 
 |-  ( ( P e. Prime /\ N e. ( 1 ..^ P ) /\ I e. ( 1 ..^ P ) ) -> E. j e. ( 0 ..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )