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 ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ∧ 𝐼 ∈ ( 1 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 )

Proof

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