This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )