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

Proof

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

Metamath Proof Explorer

Theorem modprmn0modprm0

Proof