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	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (0 ..^P)) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0$

Proof

Step	Hyp	Ref	Expression
1		prmnn	$⊢ P \in ℙ \to P \in ℕ$
2	1	adantr	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to P \in ℕ$
3		fzo0sn0fzo1	$⊢ P \in ℕ \to (0 ..^P) = \{0\} \cup (1 ..^P)$
4	2 3	syl	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to (0 ..^P) = \{0\} \cup (1 ..^P)$
5	4	eleq2d	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to (I \in (0 ..^P) \leftrightarrow I \in (\{0\} \cup (1 ..^P)))$
6		elun	$⊢ I \in (\{0\} \cup (1 ..^P)) \leftrightarrow (I \in \{0\} \lor I \in (1 ..^P))$
7		elsni	$⊢ I \in \{0\} \to I = 0$
8		lbfzo0	$⊢ 0 \in (0 ..^P) \leftrightarrow P \in ℕ$
9	1 8	sylibr	$⊢ P \in ℙ \to 0 \in (0 ..^P)$
10		elfzoelz	$⊢ N \in (1 ..^P) \to N \in ℤ$
11		zcn	$⊢ N \in ℤ \to N \in ℂ$
12		mul02	$⊢ N \in ℂ \to 0 \cdot N = 0$
13	12	oveq2d	$⊢ N \in ℂ \to 0 + 0 \cdot N = 0 + 0$
14		00id	$⊢ 0 + 0 = 0$
15	13 14	eqtrdi	$⊢ N \in ℂ \to 0 + 0 \cdot N = 0$
16	10 11 15	3syl	$⊢ N \in (1 ..^P) \to 0 + 0 \cdot N = 0$
17	16	adantl	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to 0 + 0 \cdot N = 0$
18	17	oveq1d	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to (0 + 0 \cdot N) \mod P = 0 \mod P$
19		nnrp	$⊢ P \in ℕ \to P \in ℝ^{+}$
20		0mod	$⊢ P \in ℝ^{+} \to 0 \mod P = 0$
21	1 19 20	3syl	$⊢ P \in ℙ \to 0 \mod P = 0$
22	21	adantr	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to 0 \mod P = 0$
23	18 22	eqtrd	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to (0 + 0 \cdot N) \mod P = 0$
24		oveq1	$⊢ j = 0 \to j \cdot N = 0 \cdot N$
25	24	oveq2d	$⊢ j = 0 \to 0 + j \cdot N = 0 + 0 \cdot N$
26	25	oveq1d	$⊢ j = 0 \to (0 + j \cdot N) \mod P = (0 + 0 \cdot N) \mod P$
27	26	eqeq1d	$⊢ j = 0 \to ((0 + j \cdot N) \mod P = 0 \leftrightarrow (0 + 0 \cdot N) \mod P = 0)$
28	27	rspcev	$⊢ (0 \in (0 ..^P) \land (0 + 0 \cdot N) \mod P = 0) \to \exists j \in (0 ..^P) (0 + j \cdot N) \mod P = 0$
29	9 23 28	syl2an2r	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to \exists j \in (0 ..^P) (0 + j \cdot N) \mod P = 0$
30	29	adantl	$⊢ (I = 0 \land (P \in ℙ \land N \in (1 ..^P))) \to \exists j \in (0 ..^P) (0 + j \cdot N) \mod P = 0$
31		oveq1	$⊢ I = 0 \to I + j \cdot N = 0 + j \cdot N$
32	31	oveq1d	$⊢ I = 0 \to (I + j \cdot N) \mod P = (0 + j \cdot N) \mod P$
33	32	eqeq1d	$⊢ I = 0 \to ((I + j \cdot N) \mod P = 0 \leftrightarrow (0 + j \cdot N) \mod P = 0)$
34	33	adantr	$⊢ (I = 0 \land (P \in ℙ \land N \in (1 ..^P))) \to ((I + j \cdot N) \mod P = 0 \leftrightarrow (0 + j \cdot N) \mod P = 0)$
35	34	rexbidv	$⊢ (I = 0 \land (P \in ℙ \land N \in (1 ..^P))) \to (\exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0 \leftrightarrow \exists j \in (0 ..^P) (0 + j \cdot N) \mod P = 0)$
36	30 35	mpbird	$⊢ (I = 0 \land (P \in ℙ \land N \in (1 ..^P))) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0$
37	36	ex	$⊢ I = 0 \to ((P \in ℙ \land N \in (1 ..^P)) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0)$
38	7 37	syl	$⊢ I \in \{0\} \to ((P \in ℙ \land N \in (1 ..^P)) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0)$
39		simpl	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to P \in ℙ$
40	39	adantl	$⊢ (I \in (1 ..^P) \land (P \in ℙ \land N \in (1 ..^P))) \to P \in ℙ$
41		simprr	$⊢ (I \in (1 ..^P) \land (P \in ℙ \land N \in (1 ..^P))) \to N \in (1 ..^P)$
42		simpl	$⊢ (I \in (1 ..^P) \land (P \in ℙ \land N \in (1 ..^P))) \to I \in (1 ..^P)$
43		modprm0	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0$
44	40 41 42 43	syl3anc	$⊢ (I \in (1 ..^P) \land (P \in ℙ \land N \in (1 ..^P))) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0$
45	44	ex	$⊢ I \in (1 ..^P) \to ((P \in ℙ \land N \in (1 ..^P)) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0)$
46	38 45	jaoi	$⊢ (I \in \{0\} \lor I \in (1 ..^P)) \to ((P \in ℙ \land N \in (1 ..^P)) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0)$
47	6 46	sylbi	$⊢ I \in (\{0\} \cup (1 ..^P)) \to ((P \in ℙ \land N \in (1 ..^P)) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0)$
48	47	com12	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to (I \in (\{0\} \cup (1 ..^P)) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0)$
49	5 48	sylbid	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to (I \in (0 ..^P) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0)$
50	49	3impia	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (0 ..^P)) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0$

Metamath Proof Explorer

Theorem nnnn0modprm0

Proof