Theorem modprm0 16734

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.)

Assertion

Ref	Expression
modprm0	⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)

Distinct variable groups:   𝑗,𝐼   𝑗,𝑁   𝑃,𝑗

Proof of Theorem modprm0

Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		reumodprminv 16733	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃!𝑟 ∈ (1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1)
2		reurex 3380	. . . 4 ⊢ (∃!𝑟 ∈ (1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1 → ∃𝑟 ∈ (1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1)
3		prmz 16608	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
4	3	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℤ)
5	4	adantl 482	. . . . . . . . 9 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℤ)
6		elfzelz 13497	. . . . . . . . . . 11 ⊢ (𝑟 ∈ (1...(𝑃 − 1)) → 𝑟 ∈ ℤ)
7	6	adantr 481	. . . . . . . . . 10 ⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → 𝑟 ∈ ℤ)
8		elfzoelz 13628	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (1..^𝑃) → 𝐼 ∈ ℤ)
9	8	3ad2ant3 1135	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℤ)
10		zmulcl 12607	. . . . . . . . . 10 ⊢ ((𝑟 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑟 · 𝐼) ∈ ℤ)
11	7, 9, 10	syl2an 596	. . . . . . . . 9 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝐼) ∈ ℤ)
12	5, 11	zsubcld 12667	. . . . . . . 8 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑃 − (𝑟 · 𝐼)) ∈ ℤ)
13		prmnn 16607	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
14	13	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℕ)
15	14	adantl 482	. . . . . . . 8 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℕ)
16		zmodfzo 13855	. . . . . . . 8 ⊢ (((𝑃 − (𝑟 · 𝐼)) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) ∈ (0..^𝑃))
17	12, 15, 16	syl2anc 584	. . . . . . 7 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) ∈ (0..^𝑃))
18	8	zred 12662	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (1..^𝑃) → 𝐼 ∈ ℝ)
19	18	3ad2ant3 1135	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℝ)
20	19	adantl 482	. . . . . . . . 9 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈ ℝ)
21	13	nnred 12223	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
22	21	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℝ)
23	22	adantl 482	. . . . . . . . . 10 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℝ)
24	6	zred 12662	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ (1...(𝑃 − 1)) → 𝑟 ∈ ℝ)
25	24	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → 𝑟 ∈ ℝ)
26		remulcl 11191	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ ℝ ∧ 𝐼 ∈ ℝ) → (𝑟 · 𝐼) ∈ ℝ)
27	25, 19, 26	syl2an 596	. . . . . . . . . 10 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝐼) ∈ ℝ)
28	23, 27	resubcld 11638	. . . . . . . . 9 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑃 − (𝑟 · 𝐼)) ∈ ℝ)
29		elfzoelz 13628	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℤ)
30	29	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑁 ∈ ℤ)
31	30	adantl 482	. . . . . . . . 9 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑁 ∈ ℤ)
32	13	nnrpd 13010	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ+)
33	32	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℝ+)
34	33	adantl 482	. . . . . . . . 9 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℝ+)
35		modaddmulmod 13899	. . . . . . . . 9 ⊢ (((𝐼 ∈ ℝ ∧ (𝑃 − (𝑟 · 𝐼)) ∈ ℝ ∧ 𝑁 ∈ ℤ) ∧ 𝑃 ∈ ℝ+) → ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = ((𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) mod 𝑃))
36	20, 28, 31, 34, 35	syl31anc 1373	. . . . . . . 8 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = ((𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) mod 𝑃))
37	13	nncnd 12224	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
38	37	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℂ)
39	38	adantl 482	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑃 ∈ ℂ)
40	6	zcnd 12663	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ (1...(𝑃 − 1)) → 𝑟 ∈ ℂ)
41	40	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → 𝑟 ∈ ℂ)
42	8	zcnd 12663	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ (1..^𝑃) → 𝐼 ∈ ℂ)
43	42	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℂ)
44		mulcl 11190	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ ℂ ∧ 𝐼 ∈ ℂ) → (𝑟 · 𝐼) ∈ ℂ)
45	41, 43, 44	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝐼) ∈ ℂ)
46	29	zcnd 12663	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℂ)
47	46	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑁 ∈ ℂ)
48	47	adantl 482	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑁 ∈ ℂ)
49	39, 45, 48	subdird 11667	. . . . . . . . . 10 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 − (𝑟 · 𝐼)) · 𝑁) = ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)))
50	49	oveq2d 7421	. . . . . . . . 9 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) = (𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))))
51	50	oveq1d 7420	. . . . . . . 8 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((𝑃 − (𝑟 · 𝐼)) · 𝑁)) mod 𝑃) = ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃))
52		mulcom 11192	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑃 · 𝑁) = (𝑁 · 𝑃))
53	37, 46, 52	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝑃 · 𝑁) = (𝑁 · 𝑃))
54	53	oveq1d 7420	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑃 · 𝑁) mod 𝑃) = ((𝑁 · 𝑃) mod 𝑃))
55		mulmod0 13838	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℝ+) → ((𝑁 · 𝑃) mod 𝑃) = 0)
56	29, 32, 55	syl2anr 597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑁 · 𝑃) mod 𝑃) = 0)
57	54, 56	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑃 · 𝑁) mod 𝑃) = 0)
58	57	3adant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝑃 · 𝑁) mod 𝑃) = 0)
59	58	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 · 𝑁) mod 𝑃) = 0)
60	41	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑟 ∈ ℂ)
61	43	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈ ℂ)
62	60, 61, 48	mul32d 11420	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑟 · 𝐼) · 𝑁) = ((𝑟 · 𝑁) · 𝐼))
63	62	oveq1d 7420	. . . . . . . . . . . . . . 15 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑟 · 𝐼) · 𝑁) mod 𝑃) = (((𝑟 · 𝑁) · 𝐼) mod 𝑃))
64	29	zred 12662	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (1..^𝑃) → 𝑁 ∈ ℝ)
65	64	3ad2ant2 1134	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → 𝑁 ∈ ℝ)
66		remulcl 11191	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑟 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑟 · 𝑁) ∈ ℝ)
67	25, 65, 66	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑟 · 𝑁) ∈ ℝ)
68	9	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝐼 ∈ ℤ)
69		modmulmod 13897	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 · 𝑁) ∈ ℝ ∧ 𝐼 ∈ ℤ ∧ 𝑃 ∈ ℝ+) → ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃) = (((𝑟 · 𝑁) · 𝐼) mod 𝑃))
70	67, 68, 34, 69	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃) = (((𝑟 · 𝑁) · 𝐼) mod 𝑃))
71	63, 70	eqtr4d 2775	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑟 · 𝐼) · 𝑁) mod 𝑃) = ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃))
72	59, 71	oveq12d 7423	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) = (0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)))
73	72	oveq1d 7420	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) mod 𝑃) = ((0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) mod 𝑃))
74		remulcl 11191	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑃 · 𝑁) ∈ ℝ)
75	21, 64, 74	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → (𝑃 · 𝑁) ∈ ℝ)
76	75	3adant3 1132	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → (𝑃 · 𝑁) ∈ ℝ)
77	76	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑃 · 𝑁) ∈ ℝ)
78	65	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → 𝑁 ∈ ℝ)
79	27, 78	remulcld 11240	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑟 · 𝐼) · 𝑁) ∈ ℝ)
80		modsubmodmod 13891	. . . . . . . . . . . . 13 ⊢ (((𝑃 · 𝑁) ∈ ℝ ∧ ((𝑟 · 𝐼) · 𝑁) ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) mod 𝑃) = (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃))
81	77, 79, 34, 80	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑃 · 𝑁) mod 𝑃) − (((𝑟 · 𝐼) · 𝑁) mod 𝑃)) mod 𝑃) = (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃))
82		mulcom 11192	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℂ ∧ 𝑟 ∈ ℂ) → (𝑁 · 𝑟) = (𝑟 · 𝑁))
83	47, 40, 82	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝑁 · 𝑟) = (𝑟 · 𝑁))
84	83	oveq1d 7420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑁 · 𝑟) mod 𝑃) = ((𝑟 · 𝑁) mod 𝑃))
85	84	eqeq1d 2734	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑁 · 𝑟) mod 𝑃) = 1 ↔ ((𝑟 · 𝑁) mod 𝑃) = 1))
86	85	biimpd 228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑁 · 𝑟) mod 𝑃) = 1 → ((𝑟 · 𝑁) mod 𝑃) = 1))
87	86	impancom 452	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝑟 · 𝑁) mod 𝑃) = 1))
88	87	imp 407	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑟 · 𝑁) mod 𝑃) = 1)
89	88	oveq1d 7420	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑟 · 𝑁) mod 𝑃) · 𝐼) = (1 · 𝐼))
90	89	oveq1d 7420	. . . . . . . . . . . . . . 15 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃) = ((1 · 𝐼) mod 𝑃))
91	90	oveq2d 7421	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) = (0 − ((1 · 𝐼) mod 𝑃)))
92	91	oveq1d 7420	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) mod 𝑃) = ((0 − ((1 · 𝐼) mod 𝑃)) mod 𝑃))
93	61	mullidd 11228	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (1 · 𝐼) = 𝐼)
94	93	oveq1d 7420	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((1 · 𝐼) mod 𝑃) = (𝐼 mod 𝑃))
95	32, 18	anim12ci 614	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → (𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+))
96		elfzo2 13631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐼 ∈ (1..^𝑃) ↔ (𝐼 ∈ (ℤ≥‘1) ∧ 𝑃 ∈ ℤ ∧ 𝐼 < 𝑃))
97		eluz2 12824	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐼 ∈ (ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 1 ≤ 𝐼))
98		0red 11213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐼 ∈ ℤ → 0 ∈ ℝ)
99		1red 11211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐼 ∈ ℤ → 1 ∈ ℝ)
100		zre 12558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
101	98, 99, 100	3jca 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐼 ∈ ℤ → (0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐼 ∈ ℝ))
102	101	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐼 ∈ ℤ ∧ 1 ≤ 𝐼) → (0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐼 ∈ ℝ))
103		0le1 11733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ≤ 1
104	103	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐼 ∈ ℤ → 0 ≤ 1)
105	104	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐼 ∈ ℤ ∧ 1 ≤ 𝐼) → (0 ≤ 1 ∧ 1 ≤ 𝐼))
106		letr 11304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐼 ∈ ℝ) → ((0 ≤ 1 ∧ 1 ≤ 𝐼) → 0 ≤ 𝐼))
107	102, 105, 106	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐼 ∈ ℤ ∧ 1 ≤ 𝐼) → 0 ≤ 𝐼)
108	107	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 1 ≤ 𝐼) → 0 ≤ 𝐼)
109	97, 108	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐼 ∈ (ℤ≥‘1) → 0 ≤ 𝐼)
110	109	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐼 ∈ (ℤ≥‘1) ∧ 𝑃 ∈ ℤ ∧ 𝐼 < 𝑃) → 0 ≤ 𝐼)
111		simp3 1138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐼 ∈ (ℤ≥‘1) ∧ 𝑃 ∈ ℤ ∧ 𝐼 < 𝑃) → 𝐼 < 𝑃)
112	110, 111	jca 512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ (ℤ≥‘1) ∧ 𝑃 ∈ ℤ ∧ 𝐼 < 𝑃) → (0 ≤ 𝐼 ∧ 𝐼 < 𝑃))
113	96, 112	sylbi 216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ (1..^𝑃) → (0 ≤ 𝐼 ∧ 𝐼 < 𝑃))
114	113	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → (0 ≤ 𝐼 ∧ 𝐼 < 𝑃))
115	95, 114	jca 512	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → ((𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ 𝐼 ∧ 𝐼 < 𝑃)))
116	115	3adant2 1131	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ 𝐼 ∧ 𝐼 < 𝑃)))
117	116	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ 𝐼 ∧ 𝐼 < 𝑃)))
118		modid 13857	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ 𝐼 ∧ 𝐼 < 𝑃)) → (𝐼 mod 𝑃) = 𝐼)
119	117, 118	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 mod 𝑃) = 𝐼)
120	94, 119	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((1 · 𝐼) mod 𝑃) = 𝐼)
121	120	oveq2d 7421	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 − ((1 · 𝐼) mod 𝑃)) = (0 − 𝐼))
122	121	oveq1d 7420	. . . . . . . . . . . . 13 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − ((1 · 𝐼) mod 𝑃)) mod 𝑃) = ((0 − 𝐼) mod 𝑃))
123	92, 122	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − ((((𝑟 · 𝑁) mod 𝑃) · 𝐼) mod 𝑃)) mod 𝑃) = ((0 − 𝐼) mod 𝑃))
124	73, 81, 123	3eqtr3d 2780	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃) = ((0 − 𝐼) mod 𝑃))
125	124	oveq2d 7421	. . . . . . . . . 10 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) = (𝐼 + ((0 − 𝐼) mod 𝑃)))
126	125	oveq1d 7420	. . . . . . . . 9 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) mod 𝑃) = ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃))
127	77, 79	resubcld 11638	. . . . . . . . . 10 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) ∈ ℝ)
128		modadd2mod 13882	. . . . . . . . . 10 ⊢ ((((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) mod 𝑃) = ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃))
129	127, 20, 34, 128	syl3anc 1371	. . . . . . . . 9 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁)) mod 𝑃)) mod 𝑃) = ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃))
130		0red 11213	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (1..^𝑃) → 0 ∈ ℝ)
131	130, 18	resubcld 11638	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ (1..^𝑃) → (0 − 𝐼) ∈ ℝ)
132	131	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → (0 − 𝐼) ∈ ℝ)
133	18	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → 𝐼 ∈ ℝ)
134	32	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → 𝑃 ∈ ℝ+)
135	132, 133, 134	3jca 1128	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℙ ∧ 𝐼 ∈ (1..^𝑃)) → ((0 − 𝐼) ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+))
136	135	3adant2 1131	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((0 − 𝐼) ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+))
137	136	adantl 482	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((0 − 𝐼) ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+))
138		modadd2mod 13882	. . . . . . . . . . 11 ⊢ (((0 − 𝐼) ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃) = ((𝐼 + (0 − 𝐼)) mod 𝑃))
139	137, 138	syl 17	. . . . . . . . . 10 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃) = ((𝐼 + (0 − 𝐼)) mod 𝑃))
140		0cnd 11203	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ (1..^𝑃) → 0 ∈ ℂ)
141	42, 140	pncan3d 11570	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ (1..^𝑃) → (𝐼 + (0 − 𝐼)) = 0)
142	141	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → (𝐼 + (0 − 𝐼)) = 0)
143	142	adantl 482	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (𝐼 + (0 − 𝐼)) = 0)
144	143	oveq1d 7420	. . . . . . . . . 10 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (0 − 𝐼)) mod 𝑃) = (0 mod 𝑃))
145		0mod 13863	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℝ+ → (0 mod 𝑃) = 0)
146	32, 145	syl 17	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → (0 mod 𝑃) = 0)
147	146	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → (0 mod 𝑃) = 0)
148	147	adantl 482	. . . . . . . . . 10 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → (0 mod 𝑃) = 0)
149	139, 144, 148	3eqtrd 2776	. . . . . . . . 9 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((0 − 𝐼) mod 𝑃)) mod 𝑃) = 0)
150	126, 129, 149	3eqtr3d 2780	. . . . . . . 8 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + ((𝑃 · 𝑁) − ((𝑟 · 𝐼) · 𝑁))) mod 𝑃) = 0)
151	36, 51, 150	3eqtrd 2776	. . . . . . 7 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = 0)
152		oveq1 7412	. . . . . . . . . . 11 ⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → (𝑗 · 𝑁) = (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁))
153	152	oveq2d 7421	. . . . . . . . . 10 ⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → (𝐼 + (𝑗 · 𝑁)) = (𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)))
154	153	oveq1d 7420	. . . . . . . . 9 ⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → ((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃))
155	154	eqeq1d 2734	. . . . . . . 8 ⊢ (𝑗 = ((𝑃 − (𝑟 · 𝐼)) mod 𝑃) → (((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0 ↔ ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = 0))
156	155	rspcev 3612	. . . . . . 7 ⊢ ((((𝑃 − (𝑟 · 𝐼)) mod 𝑃) ∈ (0..^𝑃) ∧ ((𝐼 + (((𝑃 − (𝑟 · 𝐼)) mod 𝑃) · 𝑁)) mod 𝑃) = 0) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)
157	17, 151, 156	syl2anc 584	. . . . . 6 ⊢ (((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃))) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)
158	157	ex 413	. . . . 5 ⊢ ((𝑟 ∈ (1...(𝑃 − 1)) ∧ ((𝑁 · 𝑟) mod 𝑃) = 1) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0))
159	158	rexlimiva 3147	. . . 4 ⊢ (∃𝑟 ∈ (1...(𝑃 − 1))((𝑁 · 𝑟) mod 𝑃) = 1 → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0))
160	1, 2, 159	3syl 18	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0))
161	160	3adant3 1132	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0))
162	161	pm2.43i 52	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∃wrex 3070  ∃!wreu 3374   class class class wbr 5147  ‘cfv 6540  (class class class)co 7405  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11244   ≤ cle 11245   − cmin 11440  ℕcn 12208  ℤcz 12554  ℤ_≥cuz 12818  ℝ⁺crp 12970  ...cfz 13480  ..^cfzo 13623   mod cmo 13830  ℙcprime 16604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-dju 9892  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-xnn0 12541  df-z 12555  df-uz 12819  df-rp 12971  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-dvds 16194  df-gcd 16432  df-prm 16605  df-phi 16695

This theorem is referenced by:  nnnn0modprm0  16735