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

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → 𝑃 ∈ ℙ )
2 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
3 zmodfzo ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( 𝑁 mod 𝑃 ) ∈ ( 0 ..^ 𝑃 ) )
4 2 3 sylan2 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( 𝑁 mod 𝑃 ) ∈ ( 0 ..^ 𝑃 ) )
5 4 ancoms ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 mod 𝑃 ) ∈ ( 0 ..^ 𝑃 ) )
6 5 3adant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) → ( 𝑁 mod 𝑃 ) ∈ ( 0 ..^ 𝑃 ) )
7 fzo1fzo0n0 ⊢ ( ( 𝑁 mod 𝑃 ) ∈ ( 1 ..^ 𝑃 ) ↔ ( ( 𝑁 mod 𝑃 ) ∈ ( 0 ..^ 𝑃 ) ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) )
8 7 simplbi2com ⊢ ( ( 𝑁 mod 𝑃 ) ≠ 0 → ( ( 𝑁 mod 𝑃 ) ∈ ( 0 ..^ 𝑃 ) → ( 𝑁 mod 𝑃 ) ∈ ( 1 ..^ 𝑃 ) ) )
9 8 3ad2ant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) → ( ( 𝑁 mod 𝑃 ) ∈ ( 0 ..^ 𝑃 ) → ( 𝑁 mod 𝑃 ) ∈ ( 1 ..^ 𝑃 ) ) )
10 6 9 mpd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) → ( 𝑁 mod 𝑃 ) ∈ ( 1 ..^ 𝑃 ) )
11 10 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → ( 𝑁 mod 𝑃 ) ∈ ( 1 ..^ 𝑃 ) )
12 simpr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → 𝐼 ∈ ( 0 ..^ 𝑃 ) )
13 nnnn0modprm0 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 mod 𝑃 ) ∈ ( 1 ..^ 𝑃 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · ( 𝑁 mod 𝑃 ) ) ) mod 𝑃 ) = 0 )
14 1 11 12 13 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · ( 𝑁 mod 𝑃 ) ) ) mod 𝑃 ) = 0 )
15 elfzoelz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑃 ) → 𝑗 ∈ ℤ )
16 15 zcnd ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑃 ) → 𝑗 ∈ ℂ )
17 2 anim1ci ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℕ ) )
18 zmodcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( 𝑁 mod 𝑃 ) ∈ ℕ0 )
19 nn0cn ⊢ ( ( 𝑁 mod 𝑃 ) ∈ ℕ0 → ( 𝑁 mod 𝑃 ) ∈ ℂ )
20 17 18 19 3syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 mod 𝑃 ) ∈ ℂ )
21 20 3adant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) → ( 𝑁 mod 𝑃 ) ∈ ℂ )
22 21 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → ( 𝑁 mod 𝑃 ) ∈ ℂ )
23 mulcom ⊢ ( ( 𝑗 ∈ ℂ ∧ ( 𝑁 mod 𝑃 ) ∈ ℂ ) → ( 𝑗 · ( 𝑁 mod 𝑃 ) ) = ( ( 𝑁 mod 𝑃 ) · 𝑗 ) )
24 16 22 23 syl2anr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → ( 𝑗 · ( 𝑁 mod 𝑃 ) ) = ( ( 𝑁 mod 𝑃 ) · 𝑗 ) )
25 24 oveq2d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → ( 𝐼 + ( 𝑗 · ( 𝑁 mod 𝑃 ) ) ) = ( 𝐼 + ( ( 𝑁 mod 𝑃 ) · 𝑗 ) ) )
26 25 oveq1d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → ( ( 𝐼 + ( 𝑗 · ( 𝑁 mod 𝑃 ) ) ) mod 𝑃 ) = ( ( 𝐼 + ( ( 𝑁 mod 𝑃 ) · 𝑗 ) ) mod 𝑃 ) )
27 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑃 ) → 𝐼 ∈ ℤ )
28 27 zred ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑃 ) → 𝐼 ∈ ℝ )
29 28 adantl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → 𝐼 ∈ ℝ )
30 29 adantr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → 𝐼 ∈ ℝ )
31 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
32 31 3ad2ant2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) → 𝑁 ∈ ℝ )
33 32 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → 𝑁 ∈ ℝ )
34 33 adantr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → 𝑁 ∈ ℝ )
35 15 adantl ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → 𝑗 ∈ ℤ )
36 2 nnrpd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ+ )
37 36 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) → 𝑃 ∈ ℝ+ )
38 37 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → 𝑃 ∈ ℝ+ )
39 38 adantr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → 𝑃 ∈ ℝ+ )
40 modaddmulmod ⊢ ( ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑗 ∈ ℤ ) ∧ 𝑃 ∈ ℝ+ ) → ( ( 𝐼 + ( ( 𝑁 mod 𝑃 ) · 𝑗 ) ) mod 𝑃 ) = ( ( 𝐼 + ( 𝑁 · 𝑗 ) ) mod 𝑃 ) )
41 30 34 35 39 40 syl31anc ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → ( ( 𝐼 + ( ( 𝑁 mod 𝑃 ) · 𝑗 ) ) mod 𝑃 ) = ( ( 𝐼 + ( 𝑁 · 𝑗 ) ) mod 𝑃 ) )
42 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
43 42 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → 𝑁 ∈ ℂ )
44 16 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → 𝑗 ∈ ℂ )
45 43 44 mulcomd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → ( 𝑁 · 𝑗 ) = ( 𝑗 · 𝑁 ) )
46 45 ex ⊢ ( 𝑁 ∈ ℤ → ( 𝑗 ∈ ( 0 ..^ 𝑃 ) → ( 𝑁 · 𝑗 ) = ( 𝑗 · 𝑁 ) ) )
47 46 3ad2ant2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) → ( 𝑗 ∈ ( 0 ..^ 𝑃 ) → ( 𝑁 · 𝑗 ) = ( 𝑗 · 𝑁 ) ) )
48 47 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → ( 𝑗 ∈ ( 0 ..^ 𝑃 ) → ( 𝑁 · 𝑗 ) = ( 𝑗 · 𝑁 ) ) )
49 48 imp ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → ( 𝑁 · 𝑗 ) = ( 𝑗 · 𝑁 ) )
50 49 oveq2d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → ( 𝐼 + ( 𝑁 · 𝑗 ) ) = ( 𝐼 + ( 𝑗 · 𝑁 ) ) )
51 50 oveq1d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → ( ( 𝐼 + ( 𝑁 · 𝑗 ) ) mod 𝑃 ) = ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) )
52 26 41 51 3eqtrrd ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = ( ( 𝐼 + ( 𝑗 · ( 𝑁 mod 𝑃 ) ) ) mod 𝑃 ) )
53 52 eqeq1d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) ∧ 𝑗 ∈ ( 0 ..^ 𝑃 ) ) → ( ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ↔ ( ( 𝐼 + ( 𝑗 · ( 𝑁 mod 𝑃 ) ) ) mod 𝑃 ) = 0 ) )
54 53 rexbidva ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → ( ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ↔ ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · ( 𝑁 mod 𝑃 ) ) ) mod 𝑃 ) = 0 ) )
55 14 54 mpbird ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑃 ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 )
56 55 ex ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝑃 ) ≠ 0 ) → ( 𝐼 ∈ ( 0 ..^ 𝑃 ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑃 ) ( ( 𝐼 + ( 𝑗 · 𝑁 ) ) mod 𝑃 ) = 0 ) )