modprm0

Description: For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018)

		Ref	Expression
	Assertion	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$

Proof

Step	Hyp	Ref	Expression
1		reumodprminv	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to \exists! r \in (1 \dots P - 1) N r \mod P = 1$
2		reurex	$⊢ \exists! r \in (1 \dots P - 1) N r \mod P = 1 \to \exists r \in (1 \dots P - 1) N r \mod P = 1$
3		prmz	$⊢ P \in ℙ \to P \in ℤ$
4	3	3ad2ant1	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to P \in ℤ$
5	4	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to P \in ℤ$
6		elfzelz	$⊢ r \in (1 \dots P - 1) \to r \in ℤ$
7	6	adantr	$⊢ (r \in (1 \dots P - 1) \land N r \mod P = 1) \to r \in ℤ$
8		elfzoelz	$⊢ I \in (1 ..^P) \to I \in ℤ$
9	8	3ad2ant3	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to I \in ℤ$
10		zmulcl	$⊢ (r \in ℤ \land I \in ℤ) \to r \cdot I \in ℤ$
11	7 9 10	syl2an	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to r \cdot I \in ℤ$
12	5 11	zsubcld	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to P - r \cdot I \in ℤ$
13		prmnn	$⊢ P \in ℙ \to P \in ℕ$
14	13	3ad2ant1	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to P \in ℕ$
15	14	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to P \in ℕ$
16		zmodfzo	$⊢ (P - r \cdot I \in ℤ \land P \in ℕ) \to (P - r \cdot I) \mod P \in (0 ..^P)$
17	12 15 16	syl2anc	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (P - r \cdot I) \mod P \in (0 ..^P)$
18	8	zred	$⊢ I \in (1 ..^P) \to I \in ℝ$
19	18	3ad2ant3	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to I \in ℝ$
20	19	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to I \in ℝ$
21	13	nnred	$⊢ P \in ℙ \to P \in ℝ$
22	21	3ad2ant1	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to P \in ℝ$
23	22	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to P \in ℝ$
24	6	zred	$⊢ r \in (1 \dots P - 1) \to r \in ℝ$
25	24	adantr	$⊢ (r \in (1 \dots P - 1) \land N r \mod P = 1) \to r \in ℝ$
26		remulcl	$⊢ (r \in ℝ \land I \in ℝ) \to r \cdot I \in ℝ$
27	25 19 26	syl2an	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to r \cdot I \in ℝ$
28	23 27	resubcld	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to P - r \cdot I \in ℝ$
29		elfzoelz	$⊢ N \in (1 ..^P) \to N \in ℤ$
30	29	3ad2ant2	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to N \in ℤ$
31	30	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to N \in ℤ$
32	13	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
33	32	3ad2ant1	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to P \in ℝ^{+}$
34	33	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to P \in ℝ^{+}$
35		modaddmulmod	$⊢ ((I \in ℝ \land P - r \cdot I \in ℝ \land N \in ℤ) \land P \in ℝ^{+}) \to (I + ((P - r \cdot I) \mod P) \cdot N) \mod P = (I + (P - r \cdot I) \cdot N) \mod P$
36	20 28 31 34 35	syl31anc	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (I + ((P - r \cdot I) \mod P) \cdot N) \mod P = (I + (P - r \cdot I) \cdot N) \mod P$
37	13	nncnd	$⊢ P \in ℙ \to P \in ℂ$
38	37	3ad2ant1	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to P \in ℂ$
39	38	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to P \in ℂ$
40	6	zcnd	$⊢ r \in (1 \dots P - 1) \to r \in ℂ$
41	40	adantr	$⊢ (r \in (1 \dots P - 1) \land N r \mod P = 1) \to r \in ℂ$
42	8	zcnd	$⊢ I \in (1 ..^P) \to I \in ℂ$
43	42	3ad2ant3	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to I \in ℂ$
44		mulcl	$⊢ (r \in ℂ \land I \in ℂ) \to r \cdot I \in ℂ$
45	41 43 44	syl2an	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to r \cdot I \in ℂ$
46	29	zcnd	$⊢ N \in (1 ..^P) \to N \in ℂ$
47	46	3ad2ant2	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to N \in ℂ$
48	47	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to N \in ℂ$
49	39 45 48	subdird	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (P - r \cdot I) \cdot N = P \cdot N - r \cdot I \cdot N$
50	49	oveq2d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to I + (P - r \cdot I) \cdot N = I + P \cdot N - r \cdot I \cdot N$
51	50	oveq1d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (I + (P - r \cdot I) \cdot N) \mod P = (I + P \cdot N - r \cdot I \cdot N) \mod P$
52		mulcom	$⊢ (P \in ℂ \land N \in ℂ) \to P \cdot N = N P$
53	37 46 52	syl2an	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to P \cdot N = N P$
54	53	oveq1d	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to P \cdot N \mod P = N P \mod P$
55		mulmod0	$⊢ (N \in ℤ \land P \in ℝ^{+}) \to N P \mod P = 0$
56	29 32 55	syl2anr	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to N P \mod P = 0$
57	54 56	eqtrd	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to P \cdot N \mod P = 0$
58	57	3adant3	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to P \cdot N \mod P = 0$
59	58	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to P \cdot N \mod P = 0$
60	41	adantr	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to r \in ℂ$
61	43	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to I \in ℂ$
62	60 61 48	mul32d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to r \cdot I \cdot N = r \cdot N \cdot I$
63	62	oveq1d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to r \cdot I \cdot N \mod P = r \cdot N \cdot I \mod P$
64	29	zred	$⊢ N \in (1 ..^P) \to N \in ℝ$
65	64	3ad2ant2	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to N \in ℝ$
66		remulcl	$⊢ (r \in ℝ \land N \in ℝ) \to r \cdot N \in ℝ$
67	25 65 66	syl2an	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to r \cdot N \in ℝ$
68	9	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to I \in ℤ$
69		modmulmod	$⊢ (r \cdot N \in ℝ \land I \in ℤ \land P \in ℝ^{+}) \to (r \cdot N \mod P) \cdot I \mod P = r \cdot N \cdot I \mod P$
70	67 68 34 69	syl3anc	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (r \cdot N \mod P) \cdot I \mod P = r \cdot N \cdot I \mod P$
71	63 70	eqtr4d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to r \cdot I \cdot N \mod P = (r \cdot N \mod P) \cdot I \mod P$
72	59 71	oveq12d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (P \cdot N \mod P) - (r \cdot I \cdot N \mod P) = 0 - ((r \cdot N \mod P) \cdot I \mod P)$
73	72	oveq1d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to ((P \cdot N \mod P) - (r \cdot I \cdot N \mod P)) \mod P = (0 - ((r \cdot N \mod P) \cdot I \mod P)) \mod P$
74		remulcl	$⊢ (P \in ℝ \land N \in ℝ) \to P \cdot N \in ℝ$
75	21 64 74	syl2an	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to P \cdot N \in ℝ$
76	75	3adant3	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to P \cdot N \in ℝ$
77	76	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to P \cdot N \in ℝ$
78	65	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to N \in ℝ$
79	27 78	remulcld	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to r \cdot I \cdot N \in ℝ$
80		modsubmodmod	$⊢ (P \cdot N \in ℝ \land r \cdot I \cdot N \in ℝ \land P \in ℝ^{+}) \to ((P \cdot N \mod P) - (r \cdot I \cdot N \mod P)) \mod P = (P \cdot N - r \cdot I \cdot N) \mod P$
81	77 79 34 80	syl3anc	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to ((P \cdot N \mod P) - (r \cdot I \cdot N \mod P)) \mod P = (P \cdot N - r \cdot I \cdot N) \mod P$
82		mulcom	$⊢ (N \in ℂ \land r \in ℂ) \to N r = r \cdot N$
83	47 40 82	syl2anr	$⊢ (r \in (1 \dots P - 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to N r = r \cdot N$
84	83	oveq1d	$⊢ (r \in (1 \dots P - 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to N r \mod P = r \cdot N \mod P$
85	84	eqeq1d	$⊢ (r \in (1 \dots P - 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (N r \mod P = 1 \leftrightarrow r \cdot N \mod P = 1)$
86	85	biimpd	$⊢ (r \in (1 \dots P - 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (N r \mod P = 1 \to r \cdot N \mod P = 1)$
87	86	impancom	$⊢ (r \in (1 \dots P - 1) \land N r \mod P = 1) \to ((P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to r \cdot N \mod P = 1)$
88	87	imp	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to r \cdot N \mod P = 1$
89	88	oveq1d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (r \cdot N \mod P) \cdot I = 1 \cdot I$
90	89	oveq1d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (r \cdot N \mod P) \cdot I \mod P = 1 \cdot I \mod P$
91	90	oveq2d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to 0 - ((r \cdot N \mod P) \cdot I \mod P) = 0 - (1 \cdot I \mod P)$
92	91	oveq1d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (0 - ((r \cdot N \mod P) \cdot I \mod P)) \mod P = (0 - (1 \cdot I \mod P)) \mod P$
93	61	mulid2d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to 1 \cdot I = I$
94	93	oveq1d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to 1 \cdot I \mod P = I \mod P$
95	32 18	anim12ci	$⊢ (P \in ℙ \land I \in (1 ..^P)) \to (I \in ℝ \land P \in ℝ^{+})$
96		elfzo2	$⊢ I \in (1 ..^P) \leftrightarrow (I \in ℤ_{\geq 1} \land P \in ℤ \land I < P)$
97		eluz2	$⊢ I \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land I \in ℤ \land 1 \leq I)$
98		0red	$⊢ I \in ℤ \to 0 \in ℝ$
99		1red	$⊢ I \in ℤ \to 1 \in ℝ$
100		zre	$⊢ I \in ℤ \to I \in ℝ$
101	98 99 100	3jca	$⊢ I \in ℤ \to (0 \in ℝ \land 1 \in ℝ \land I \in ℝ)$
102	101	adantr	$⊢ (I \in ℤ \land 1 \leq I) \to (0 \in ℝ \land 1 \in ℝ \land I \in ℝ)$
103		0le1	$⊢ 0 \leq 1$
104	103	a1i	$⊢ I \in ℤ \to 0 \leq 1$
105	104	anim1i	$⊢ (I \in ℤ \land 1 \leq I) \to (0 \leq 1 \land 1 \leq I)$
106		letr	$⊢ (0 \in ℝ \land 1 \in ℝ \land I \in ℝ) \to ((0 \leq 1 \land 1 \leq I) \to 0 \leq I)$
107	102 105 106	sylc	$⊢ (I \in ℤ \land 1 \leq I) \to 0 \leq I$
108	107	3adant1	$⊢ (1 \in ℤ \land I \in ℤ \land 1 \leq I) \to 0 \leq I$
109	97 108	sylbi	$⊢ I \in ℤ_{\geq 1} \to 0 \leq I$
110	109	3ad2ant1	$⊢ (I \in ℤ_{\geq 1} \land P \in ℤ \land I < P) \to 0 \leq I$
111		simp3	$⊢ (I \in ℤ_{\geq 1} \land P \in ℤ \land I < P) \to I < P$
112	110 111	jca	$⊢ (I \in ℤ_{\geq 1} \land P \in ℤ \land I < P) \to (0 \leq I \land I < P)$
113	96 112	sylbi	$⊢ I \in (1 ..^P) \to (0 \leq I \land I < P)$
114	113	adantl	$⊢ (P \in ℙ \land I \in (1 ..^P)) \to (0 \leq I \land I < P)$
115	95 114	jca	$⊢ (P \in ℙ \land I \in (1 ..^P)) \to ((I \in ℝ \land P \in ℝ^{+}) \land (0 \leq I \land I < P))$
116	115	3adant2	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to ((I \in ℝ \land P \in ℝ^{+}) \land (0 \leq I \land I < P))$
117	116	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to ((I \in ℝ \land P \in ℝ^{+}) \land (0 \leq I \land I < P))$
118		modid	$⊢ ((I \in ℝ \land P \in ℝ^{+}) \land (0 \leq I \land I < P)) \to I \mod P = I$
119	117 118	syl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to I \mod P = I$
120	94 119	eqtrd	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to 1 \cdot I \mod P = I$
121	120	oveq2d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to 0 - (1 \cdot I \mod P) = 0 - I$
122	121	oveq1d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (0 - (1 \cdot I \mod P)) \mod P = (0 - I) \mod P$
123	92 122	eqtrd	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (0 - ((r \cdot N \mod P) \cdot I \mod P)) \mod P = (0 - I) \mod P$
124	73 81 123	3eqtr3d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (P \cdot N - r \cdot I \cdot N) \mod P = (0 - I) \mod P$
125	124	oveq2d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to I + ((P \cdot N - r \cdot I \cdot N) \mod P) = I + ((0 - I) \mod P)$
126	125	oveq1d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (I + ((P \cdot N - r \cdot I \cdot N) \mod P)) \mod P = (I + ((0 - I) \mod P)) \mod P$
127	77 79	resubcld	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to P \cdot N - r \cdot I \cdot N \in ℝ$
128		modadd2mod	$⊢ (P \cdot N - r \cdot I \cdot N \in ℝ \land I \in ℝ \land P \in ℝ^{+}) \to (I + ((P \cdot N - r \cdot I \cdot N) \mod P)) \mod P = (I + P \cdot N - r \cdot I \cdot N) \mod P$
129	127 20 34 128	syl3anc	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (I + ((P \cdot N - r \cdot I \cdot N) \mod P)) \mod P = (I + P \cdot N - r \cdot I \cdot N) \mod P$
130		0red	$⊢ I \in (1 ..^P) \to 0 \in ℝ$
131	130 18	resubcld	$⊢ I \in (1 ..^P) \to 0 - I \in ℝ$
132	131	adantl	$⊢ (P \in ℙ \land I \in (1 ..^P)) \to 0 - I \in ℝ$
133	18	adantl	$⊢ (P \in ℙ \land I \in (1 ..^P)) \to I \in ℝ$
134	32	adantr	$⊢ (P \in ℙ \land I \in (1 ..^P)) \to P \in ℝ^{+}$
135	132 133 134	3jca	$⊢ (P \in ℙ \land I \in (1 ..^P)) \to (0 - I \in ℝ \land I \in ℝ \land P \in ℝ^{+})$
136	135	3adant2	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to (0 - I \in ℝ \land I \in ℝ \land P \in ℝ^{+})$
137	136	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (0 - I \in ℝ \land I \in ℝ \land P \in ℝ^{+})$
138		modadd2mod	$⊢ (0 - I \in ℝ \land I \in ℝ \land P \in ℝ^{+}) \to (I + ((0 - I) \mod P)) \mod P = (I + 0 - I) \mod P$
139	137 138	syl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (I + ((0 - I) \mod P)) \mod P = (I + 0 - I) \mod P$
140		0cnd	$⊢ I \in (1 ..^P) \to 0 \in ℂ$
141	42 140	pncan3d	$⊢ I \in (1 ..^P) \to I + 0 - I = 0$
142	141	3ad2ant3	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to I + 0 - I = 0$
143	142	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to I + 0 - I = 0$
144	143	oveq1d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (I + 0 - I) \mod P = 0 \mod P$
145		0mod	$⊢ P \in ℝ^{+} \to 0 \mod P = 0$
146	32 145	syl	$⊢ P \in ℙ \to 0 \mod P = 0$
147	146	3ad2ant1	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to 0 \mod P = 0$
148	147	adantl	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to 0 \mod P = 0$
149	139 144 148	3eqtrd	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (I + ((0 - I) \mod P)) \mod P = 0$
150	126 129 149	3eqtr3d	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (I + P \cdot N - r \cdot I \cdot N) \mod P = 0$
151	36 51 150	3eqtrd	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P))) \to (I + ((P - r \cdot I) \mod P) \cdot N) \mod P = 0$
152		oveq1	$⊢ j = (P - r \cdot I) \mod P \to j \cdot N = ((P - r \cdot I) \mod P) \cdot N$
153	152	oveq2d	$⊢ j = (P - r \cdot I) \mod P \to I + j \cdot N = I + ((P - r \cdot I) \mod P) \cdot N$
154	153	oveq1d	$⊢ j = (P - r \cdot I) \mod P \to (I + j \cdot N) \mod P = (I + ((P - r \cdot I) \mod P) \cdot N) \mod P$
155	154	eqeq1d	$⊢ j = (P - r \cdot I) \mod P \to ((I + j \cdot N) \mod P = 0 \leftrightarrow (I + ((P - r \cdot I) \mod P) \cdot N) \mod P = 0)$
156	155	rspcev	$⊢ ((P - r \cdot I) \mod P \in (0 ..^P) \land (I + ((P - r \cdot I) \mod P) \cdot N) \mod P = 0) \to \exists j \in (0 ..^P) (I + j \cdot N) \mod P = 0$
157	17 151 156	syl2anc	$⊢ ((r \in (1 \dots P - 1) \land N r \mod P = 1) \land (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$
158	157	ex	$⊢ (r \in (1 \dots P - 1) \land N r \mod P = 1) \to ((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)$
159	158	rexlimiva	$⊢ \exists r \in (1 \dots P - 1) N r \mod P = 1 \to ((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)$
160	1 2 159	3syl	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to ((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)$
161	160	3adant3	$⊢ (P \in ℙ \land N \in (1 ..^P) \land I \in (1 ..^P)) \to ((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)$
162	161	pm2.43i	$⊢ (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$

Metamath Proof Explorer

Theorem modprm0

Proof