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 )