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

Proof

Step Hyp Ref Expression
1 prmnn ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
2 1 adantr ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → 𝑃 ∈ ℕ )
3 fzo0sn0fzo1 ( 𝑃 ∈ ℕ → ( 0 ..^ 𝑃 ) = ( { 0 } ∪ ( 1 ..^ 𝑃 ) ) )
4 2 3 syl ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ( 0 ..^ 𝑃 ) = ( { 0 } ∪ ( 1 ..^ 𝑃 ) ) )
5 4 eleq2d ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ( 𝐼 ∈ ( 0 ..^ 𝑃 ) ↔ 𝐼 ∈ ( { 0 } ∪ ( 1 ..^ 𝑃 ) ) ) )
6 elun ( 𝐼 ∈ ( { 0 } ∪ ( 1 ..^ 𝑃 ) ) ↔ ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑃 ) ) )
7 elsni ( 𝐼 ∈ { 0 } → 𝐼 = 0 )
8 lbfzo0 ( 0 ∈ ( 0 ..^ 𝑃 ) ↔ 𝑃 ∈ ℕ )
9 1 8 sylibr ( 𝑃 ∈ ℙ → 0 ∈ ( 0 ..^ 𝑃 ) )
10 elfzoelz ( 𝑁 ∈ ( 1 ..^ 𝑃 ) → 𝑁 ∈ ℤ )
11 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
12 mul02 ( 𝑁 ∈ ℂ → ( 0 · 𝑁 ) = 0 )
13 12 oveq2d ( 𝑁 ∈ ℂ → ( 0 + ( 0 · 𝑁 ) ) = ( 0 + 0 ) )
14 00id ( 0 + 0 ) = 0
15 13 14 eqtrdi ( 𝑁 ∈ ℂ → ( 0 + ( 0 · 𝑁 ) ) = 0 )
16 10 11 15 3syl ( 𝑁 ∈ ( 1 ..^ 𝑃 ) → ( 0 + ( 0 · 𝑁 ) ) = 0 )
17 16 adantl ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ( 0 + ( 0 · 𝑁 ) ) = 0 )
18 17 oveq1d ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ( ( 0 + ( 0 · 𝑁 ) ) mod 𝑃 ) = ( 0 mod 𝑃 ) )
19 nnrp ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ+ )
20 0mod ( 𝑃 ∈ ℝ+ → ( 0 mod 𝑃 ) = 0 )
21 1 19 20 3syl ( 𝑃 ∈ ℙ → ( 0 mod 𝑃 ) = 0 )
22 21 adantr ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ( 0 mod 𝑃 ) = 0 )
23 18 22 eqtrd ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ( ( 0 + ( 0 · 𝑁 ) ) mod 𝑃 ) = 0 )
24 oveq1 ( 𝑗 = 0 → ( 𝑗 · 𝑁 ) = ( 0 · 𝑁 ) )
25 24 oveq2d ( 𝑗 = 0 → ( 0 + ( 𝑗 · 𝑁 ) ) = ( 0 + ( 0 · 𝑁 ) ) )
26 25 oveq1d ( 𝑗 = 0 → ( ( 0 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = ( ( 0 + ( 0 · 𝑁 ) ) mod 𝑃 ) )
27 26 eqeq1d ( 𝑗 = 0 → ( ( ( 0 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ↔ ( ( 0 + ( 0 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
28 27 rspcev ( ( 0 ∈ ( 0 ..^ 𝑃 ) ∧ ( ( 0 + ( 0 · 𝑁 ) ) mod 𝑃 ) = 0 ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 0 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 )
29 9 23 28 syl2an2r ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 0 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 )
30 29 adantl ( ( 𝐼 = 0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 0 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 )
31 oveq1 ( 𝐼 = 0 → ( 𝐼 + ( 𝑗 · 𝑁 ) ) = ( 0 + ( 𝑗 · 𝑁 ) ) )
32 31 oveq1d ( 𝐼 = 0 → ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = ( ( 0 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) )
33 32 eqeq1d ( 𝐼 = 0 → ( ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ↔ ( ( 0 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
34 33 adantr ( ( 𝐼 = 0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) ) → ( ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ↔ ( ( 0 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
35 34 rexbidv ( ( 𝐼 = 0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) ) → ( ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ↔ ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 0 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
36 30 35 mpbird ( ( 𝐼 = 0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 )
37 36 ex ( 𝐼 = 0 → ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
38 7 37 syl ( 𝐼 ∈ { 0 } → ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
39 simpl ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → 𝑃 ∈ ℙ )
40 39 adantl ( ( 𝐼 ∈ ( 1 ..^ 𝑃 ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) ) → 𝑃 ∈ ℙ )
41 simprr ( ( 𝐼 ∈ ( 1 ..^ 𝑃 ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) ) → 𝑁 ∈ ( 1 ..^ 𝑃 ) )
42 simpl ( ( 𝐼 ∈ ( 1 ..^ 𝑃 ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) ) → 𝐼 ∈ ( 1 ..^ 𝑃 ) )
43 modprm0 ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ∧ 𝐼 ∈ ( 1 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 )
44 40 41 42 43 syl3anc ( ( 𝐼 ∈ ( 1 ..^ 𝑃 ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 )
45 44 ex ( 𝐼 ∈ ( 1 ..^ 𝑃 ) → ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
46 38 45 jaoi ( ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑃 ) ) → ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
47 6 46 sylbi ( 𝐼 ∈ ( { 0 } ∪ ( 1 ..^ 𝑃 ) ) → ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
48 47 com12 ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ( 𝐼 ∈ ( { 0 } ∪ ( 1 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
49 5 48 sylbid ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ) → ( 𝐼 ∈ ( 0 ..^ 𝑃 ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )
50 49 3impia ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ..^ 𝑃 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 )