4sqlem12 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 4sqlem12		Structured version Visualization version GIF version

Theorem 4sqlem12 17040

Description: Lemma for 4sq 17048. For any odd prime 𝑃, there is a 𝑘 < 𝑃 such that 𝑘𝑃 − 1 is a sum of two squares. (Contributed by Mario Carneiro, 15-Jul-2014.)

**Hypotheses**
Ref	Expression
4sq.1	⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
4sq.2	⊢ (𝜑 → 𝑁 ∈ ℕ)
4sq.3	⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))
4sq.4	⊢ (𝜑 → 𝑃 ∈ ℙ)
4sqlem11.5	⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
4sqlem11.6	⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))

**Assertion**
Ref	Expression
4sqlem12	⊢ (𝜑 → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))

Distinct variable groups: 𝑤,𝑛,𝑥,𝑦,𝑧 𝑘,𝑛,𝑣,𝐴 𝑛,𝐹 𝑢,𝑘,𝑛,𝑚,𝑁,𝑣 𝑃,𝑘,𝑚,𝑛,𝑢,𝑣 𝜑,𝑘,𝑚,𝑛,𝑢,𝑣 𝑆,𝑘,𝑚,𝑛,𝑢,𝑣 Allowed substitution hints: 𝜑(𝑥, 𝑦, 𝑧, 𝑤) 𝐴(𝑥, 𝑦, 𝑧, 𝑤, 𝑢, 𝑚) 𝑃(𝑥, 𝑦, 𝑧, 𝑤) 𝑆(𝑥, 𝑦, 𝑧, 𝑤) 𝐹(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑢, 𝑘, 𝑚) 𝑁(𝑥, 𝑦, 𝑧, 𝑤)

Proof of Theorem 4sqlem12 Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		4sq.1	. . . 4 ⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
2		4sq.2	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3		4sq.3	. . . 4 ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))
4		4sq.4	. . . 4 ⊢ (𝜑 → 𝑃 ∈ ℙ)
5		4sqlem11.5	. . . 4 ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
6		4sqlem11.6	. . . 4 ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))
7	1, 2, 3, 4, 5, 6	4sqlem11 17039	. . 3 ⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅)
8		n0 4307	. . 3 ⊢ ((𝐴 ∩ ran 𝐹) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹))
9	7, 8	sylib 221	. 2 ⊢ (𝜑 → ∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹))
10		vex 3461	. . . . . . 7 ⊢ 𝑗 ∈ V
11		eqeq1 2769	. . . . . . . 8 ⊢ (𝑢 = 𝑗 → (𝑢 = ((𝑚↑2) mod 𝑃) ↔ 𝑗 = ((𝑚↑2) mod 𝑃)))
12	11	rexbidv 3191	. . . . . . 7 ⊢ (𝑢 = 𝑗 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃)))
13	10, 12, 5	elab2 3643	. . . . . 6 ⊢ (𝑗 ∈ 𝐴 ↔ ∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃))
14		abid 2747	. . . . . . . . 9 ⊢ (𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)} ↔ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣))
15	5	rexeqi 3324	. . . . . . . . 9 ⊢ (∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣) ↔ ∃𝑣 ∈ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}𝑗 = ((𝑃 − 1) − 𝑣))
16		oveq1 7426	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → (𝑚↑2) = (𝑛↑2))
17	16	oveq1d 7434	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → ((𝑚↑2) mod 𝑃) = ((𝑛↑2) mod 𝑃))
18	17	eqeq2d 2776	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑢 = ((𝑚↑2) mod 𝑃) ↔ 𝑢 = ((𝑛↑2) mod 𝑃)))
19	18	cbvrexvw 3246	. . . . . . . . . . 11 ⊢ (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑢 = ((𝑛↑2) mod 𝑃))
20		eqeq1 2769	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑣 → (𝑢 = ((𝑛↑2) mod 𝑃) ↔ 𝑣 = ((𝑛↑2) mod 𝑃)))
21	20	rexbidv 3191	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → (∃𝑛 ∈ (0...𝑁)𝑢 = ((𝑛↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃)))
22	19, 21	bitrid 286	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃)))
23	22	rexab 3660	. . . . . . . . 9 ⊢ (∃𝑣 ∈ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}𝑗 = ((𝑃 − 1) − 𝑣) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
24	14, 15, 23	3bitri 300	. . . . . . . 8 ⊢ (𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)} ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
25	6	rnmpt 5949	. . . . . . . . 9 ⊢ ran 𝐹 = {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)}
26	25	eleq2i 2857	. . . . . . . 8 ⊢ (𝑗 ∈ ran 𝐹 ↔ 𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)})
27		rexcom4 3294	. . . . . . . . 9 ⊢ (∃𝑛 ∈ (0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣∃𝑛 ∈ (0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
28		r19.41v 3197	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ (0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ (∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
29	28	exbii 1881	. . . . . . . . 9 ⊢ (∃𝑣∃𝑛 ∈ (0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
30	27, 29	bitri 278	. . . . . . . 8 ⊢ (∃𝑛 ∈ (0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
31	24, 26, 30	3bitr4i 306	. . . . . . 7 ⊢ (𝑗 ∈ ran 𝐹 ↔ ∃𝑛 ∈ (0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
32		ovex 7452	. . . . . . . . 9 ⊢ ((𝑛↑2) mod 𝑃) ∈ V
33		oveq2 7427	. . . . . . . . . 10 ⊢ (𝑣 = ((𝑛↑2) mod 𝑃) → ((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
34	33	eqeq2d 2776	. . . . . . . . 9 ⊢ (𝑣 = ((𝑛↑2) mod 𝑃) → (𝑗 = ((𝑃 − 1) − 𝑣) ↔ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))))
35	32, 34	ceqsexv 3505	. . . . . . . 8 ⊢ (∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
36	35	rexbii 3114	. . . . . . 7 ⊢ (∃𝑛 ∈ (0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
37	31, 36	bitri 278	. . . . . 6 ⊢ (𝑗 ∈ ran 𝐹 ↔ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
38	13, 37	anbi12i 640	. . . . 5 ⊢ ((𝑗 ∈ 𝐴 ∧ 𝑗 ∈ ran 𝐹) ↔ (∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃) ∧ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))))
39		elin 3922	. . . . 5 ⊢ (𝑗 ∈ (𝐴 ∩ ran 𝐹) ↔ (𝑗 ∈ 𝐴 ∧ 𝑗 ∈ ran 𝐹))
40		reeanv 3239	. . . . 5 ⊢ (∃𝑚 ∈ (0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) ↔ (∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃) ∧ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))))
41	38, 39, 40	3bitr4i 306	. . . 4 ⊢ (𝑗 ∈ (𝐴 ∩ ran 𝐹) ↔ ∃𝑚 ∈ (0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))))
42		eqtr2 2786	. . . . . 6 ⊢ ((𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
43	4	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℙ)
44		prmnn 16756	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
45	43, 44	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℕ)
46		nnm1nn0 12562	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
47	45, 46	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℕ₀)
48	47	nn0red 12583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℝ)
49	45	nnrpd 13076	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℝ⁺)
50	47	nn0ge0d 12585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ (𝑃 − 1))
51	45	nnred 12265	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℝ)
52	51	ltm1d 12164	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) < 𝑃)
53		modid 13949	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑃 − 1) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ (𝑃 − 1) ∧ (𝑃 − 1) < 𝑃)) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1))
54	48, 49, 50, 52, 53	syl22anc 852	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1))
55	54	oveq1d 7434	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃)) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
56		simp2r 1219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ (0...𝑁))
57	56	elfzelzd 13571	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ ℤ)
58		zsqcl2 14194	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℤ → (𝑛↑2) ∈ ℕ₀)
59	57, 58	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℕ₀)
60	59	nn0red 12583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℝ)
61		modlt 13933	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛↑2) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → ((𝑛↑2) mod 𝑃) < 𝑃)
62	60, 49, 61	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) < 𝑃)
63		zsqcl 14185	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℤ → (𝑛↑2) ∈ ℤ)
64	57, 63	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℤ)
65	64, 45	zmodcld 13945	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ∈ ℕ₀)
66	65	nn0zd 12633	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ∈ ℤ)
67		prmz 16757	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
68	43, 67	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℤ)
69		zltlem1 12664	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛↑2) mod 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ) → (((𝑛↑2) mod 𝑃) < 𝑃 ↔ ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1)))
70	66, 68, 69	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑛↑2) mod 𝑃) < 𝑃 ↔ ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1)))
71	62, 70	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1))
72	71, 54	breqtrrd 5141	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃))
73		modsubdir 13996	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 − 1) ∈ ℝ ∧ (𝑛↑2) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → (((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃) ↔ (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃))))
74	48, 60, 49, 73	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃) ↔ (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃))))
75	72, 74	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃)))
76		simp3 1156	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
77	55, 75, 76	3eqtr4rd 2811	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃))
78		simp2l 1218	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ (0...𝑁))
79	78	elfzelzd 13571	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ ℤ)
80		zsqcl 14185	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℤ → (𝑚↑2) ∈ ℤ)
81	79, 80	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℤ)
82	47	nn0zd 12633	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℤ)
83	82, 64	zsubcld 12723	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑃 − 1) − (𝑛↑2)) ∈ ℤ)
84		moddvds 16345	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℕ ∧ (𝑚↑2) ∈ ℤ ∧ ((𝑃 − 1) − (𝑛↑2)) ∈ ℤ) → (((𝑚↑2) mod 𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2)))))
85	45, 81, 83, 84	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) mod 𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2)))))
86	77, 85	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))))
87		zsqcl2 14194	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℤ → (𝑚↑2) ∈ ℕ₀)
88	79, 87	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℕ₀)
89	88	nn0cnd 12584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℂ)
90	47	nn0cnd 12584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℂ)
91	59	nn0cnd 12584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℂ)
92	89, 90, 91	subsub3d 11616	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))) = (((𝑚↑2) + (𝑛↑2)) − (𝑃 − 1)))
93	88, 59	nn0addcld 12586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈ ℕ₀)
94	93	nn0cnd 12584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈ ℂ)
95	45	nncnd 12266	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℂ)
96		1cnd 11219	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ∈ ℂ)
97	94, 95, 96	subsub3d 11616	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) − (𝑃 − 1)) = ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃))
98	92, 97	eqtrd 2800	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))) = ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃))
99	86, 98	breqtrd 5139	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃))
100		nn0p1nn 12560	. . . . . . . . . . . . . 14 ⊢ (((𝑚↑2) + (𝑛↑2)) ∈ ℕ₀ → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℕ)
101	93, 100	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℕ)
102	101	nnzd 12634	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℤ)
103		dvdssubr 16387	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℤ ∧ (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℤ) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃)))
104	68, 102, 103	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃)))
105	99, 104	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1))
106	45	nnne0d 12303	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ≠ 0)
107		dvdsval2 16337	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℤ) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ))
108	68, 106, 102, 107	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ))
109	105, 108	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ)
110		nnrp 13046	. . . . . . . . . . . . . 14 ⊢ ((((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℕ → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℝ⁺)
111		nnrp 13046	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℝ⁺)
112		rpdivcl 13061	. . . . . . . . . . . . . 14 ⊢ (((((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℝ⁺ ∧ 𝑃 ∈ ℝ⁺) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℝ⁺)
113	110, 111, 112	syl2an 608	. . . . . . . . . . . . 13 ⊢ (((((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℕ ∧ 𝑃 ∈ ℕ) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℝ⁺)
114	101, 45, 113	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℝ⁺)
115	114	rpgt0d 13081	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃))
116		elnnz 12618	. . . . . . . . . . 11 ⊢ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℕ ↔ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 0 < ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃)))
117	109, 115, 116	sylanbrc 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℕ)
118	117	nnge1d 12301	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃))
119	93	nn0red 12583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈ ℝ)
120		2nn 12331	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
121	2	3ad2ant1 1151	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℕ)
122		nnmulcl 12274	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
123	120, 121, 122	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℕ)
124	123	nnred 12265	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℝ)
125	124	resqcld 14181	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) ∈ ℝ)
126		nnmulcl 12274	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ ∧ (2 · 𝑁) ∈ ℕ) → (2 · (2 · 𝑁)) ∈ ℕ)
127	120, 123, 126	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈ ℕ)
128	127	nnred 12265	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈ ℝ)
129	125, 128	readdcld 11255	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) ∈ ℝ)
130		1red 11226	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ∈ ℝ)
131	121	nnsqcld 14300	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℕ)
132		nnmulcl 12274	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ (𝑁↑2) ∈ ℕ) → (2 · (𝑁↑2)) ∈ ℕ)
133	120, 131, 132	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) ∈ ℕ)
134	133	nnred 12265	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) ∈ ℝ)
135	88	nn0red 12583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℝ)
136	131	nnred 12265	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℝ)
137	79	zred 12718	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ ℝ)
138		elfzle1 13573	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (0...𝑁) → 0 ≤ 𝑚)
139	78, 138	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ 𝑚)
140	121	nnred 12265	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℝ)
141		elfzle2 13574	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ≤ 𝑁)
142	78, 141	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ≤ 𝑁)
143		le2sq2 14191	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (𝑁 ∈ ℝ ∧ 𝑚 ≤ 𝑁)) → (𝑚↑2) ≤ (𝑁↑2))
144	137, 139, 140, 142, 143	syl22anc 852	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ≤ (𝑁↑2))
145	57	zred 12718	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ ℝ)
146		elfzle1 13573	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (0...𝑁) → 0 ≤ 𝑛)
147	56, 146	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ 𝑛)
148		elfzle2 13574	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (0...𝑁) → 𝑛 ≤ 𝑁)
149	56, 148	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ≤ 𝑁)
150		le2sq2 14191	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 𝑛 ≤ 𝑁)) → (𝑛↑2) ≤ (𝑁↑2))
151	145, 147, 140, 149, 150	syl22anc 852	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ≤ (𝑁↑2))
152	135, 60, 136, 136, 144, 151	le2addd 11850	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ≤ ((𝑁↑2) + (𝑁↑2)))
153	131	nncnd 12266	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℂ)
154	153	2timesd 12504	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) = ((𝑁↑2) + (𝑁↑2)))
155	152, 154	breqtrrd 5141	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ≤ (2 · (𝑁↑2)))
156		2lt4 12435	. . . . . . . . . . . . . . . 16 ⊢ 2 < 4
157		2re 12332	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
158	157	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 2 ∈ ℝ)
159		4re 12342	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ ℝ
160	159	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 4 ∈ ℝ)
161	131	nngt0d 12302	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < (𝑁↑2))
162		ltmul1 12082	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℝ ∧ 4 ∈ ℝ ∧ ((𝑁↑2) ∈ ℝ ∧ 0 < (𝑁↑2))) → (2 < 4 ↔ (2 · (𝑁↑2)) < (4 · (𝑁↑2))))
163	158, 160, 136, 161, 162	syl112anc 1401	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 < 4 ↔ (2 · (𝑁↑2)) < (4 · (𝑁↑2))))
164	156, 163	mpbii 236	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) < (4 · (𝑁↑2)))
165		2cn 12333	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℂ
166	121	nncnd 12266	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℂ)
167		sqmul 14175	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((2 · 𝑁)↑2) = ((2↑2) · (𝑁↑2)))
168	165, 166, 167	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) = ((2↑2) · (𝑁↑2)))
169		sq2 14253	. . . . . . . . . . . . . . . . 17 ⊢ (2↑2) = 4
170	169	oveq1i 7429	. . . . . . . . . . . . . . . 16 ⊢ ((2↑2) · (𝑁↑2)) = (4 · (𝑁↑2))
171	168, 170	eqtrdi 2816	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) = (4 · (𝑁↑2)))
172	164, 171	breqtrrd 5141	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) < ((2 · 𝑁)↑2))
173	119, 134, 125, 155, 172	lelttrd 11385	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) < ((2 · 𝑁)↑2))
174	127	nnrpd 13076	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈ ℝ⁺)
175	125, 174	ltaddrpd 13111	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) < (((2 · 𝑁)↑2) + (2 · (2 · 𝑁))))
176	119, 125, 129, 173, 175	lttrd 11388	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) < (((2 · 𝑁)↑2) + (2 · (2 · 𝑁))))
177	119, 129, 130, 176	ltadd1dd 11842	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) < ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1))
178	3	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 = ((2 · 𝑁) + 1))
179	178	oveq1d 7434	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃↑2) = (((2 · 𝑁) + 1)↑2))
180	95	sqvald 14199	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃↑2) = (𝑃 · 𝑃))
181	123	nncnd 12266	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℂ)
182		binom21 14275	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℂ → (((2 · 𝑁) + 1)↑2) = ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1))
183	181, 182	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((2 · 𝑁) + 1)↑2) = ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1))
184	179, 180, 183	3eqtr3d 2808	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 · 𝑃) = ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1))
185	177, 184	breqtrrd 5141	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃))
186	101	nnred 12265	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℝ)
187	45	nngt0d 12302	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < 𝑃)
188		ltdivmul 12107	. . . . . . . . . . 11 ⊢ (((((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃 ↔ (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃)))
189	186, 51, 51, 187, 188	syl112anc 1401	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃 ↔ (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃)))
190	185, 189	mpbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃)
191		1z 12641	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
192		elfzm11 13642	. . . . . . . . . 10 ⊢ ((1 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ↔ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∧ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃)))
193	191, 68, 192	sylancr 599	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ↔ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∧ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃)))
194	109, 118, 190, 193	mpbir3and 1361	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)))
195		gzreim 17023	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑚 + (i · 𝑛)) ∈ ℤ[i])
196	79, 57, 195	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚 + (i · 𝑛)) ∈ ℤ[i])
197		gzcn 17016	. . . . . . . . . . . . 13 ⊢ ((𝑚 + (i · 𝑛)) ∈ ℤ[i] → (𝑚 + (i · 𝑛)) ∈ ℂ)
198	196, 197	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚 + (i · 𝑛)) ∈ ℂ)
199	198	absvalsq2d 15523	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((abs‘(𝑚 + (i · 𝑛)))↑2) = (((ℜ‘(𝑚 + (i · 𝑛)))↑2) + ((ℑ‘(𝑚 + (i · 𝑛)))↑2)))
200	137, 145	crred 15308	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (ℜ‘(𝑚 + (i · 𝑛))) = 𝑚)
201	200	oveq1d 7434	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((ℜ‘(𝑚 + (i · 𝑛)))↑2) = (𝑚↑2))
202	137, 145	crimd 15309	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (ℑ‘(𝑚 + (i · 𝑛))) = 𝑛)
203	202	oveq1d 7434	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((ℑ‘(𝑚 + (i · 𝑛)))↑2) = (𝑛↑2))
204	201, 203	oveq12d 7437	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((ℜ‘(𝑚 + (i · 𝑛)))↑2) + ((ℑ‘(𝑚 + (i · 𝑛)))↑2)) = ((𝑚↑2) + (𝑛↑2)))
205	199, 204	eqtrd 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((abs‘(𝑚 + (i · 𝑛)))↑2) = ((𝑚↑2) + (𝑛↑2)))
206	205	oveq1d 7434	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((𝑚↑2) + (𝑛↑2)) + 1))
207	101	nncnd 12266	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℂ)
208	207, 95, 106	divcan1d 12009	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃) = (((𝑚↑2) + (𝑛↑2)) + 1))
209	206, 208	eqtr4d 2803	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃))
210		oveq1 7426	. . . . . . . . . 10 ⊢ (𝑘 = ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) → (𝑘 · 𝑃) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃))
211	210	eqeq2d 2776	. . . . . . . . 9 ⊢ (𝑘 = ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) → ((((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃) ↔ (((abs‘𝑢)↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)))
212		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑚 + (i · 𝑛)) → (abs‘𝑢) = (abs‘(𝑚 + (i · 𝑛))))
213	212	oveq1d 7434	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑚 + (i · 𝑛)) → ((abs‘𝑢)↑2) = ((abs‘(𝑚 + (i · 𝑛)))↑2))
214	213	oveq1d 7434	. . . . . . . . . 10 ⊢ (𝑢 = (𝑚 + (i · 𝑛)) → (((abs‘𝑢)↑2) + 1) = (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1))
215	214	eqeq1d 2767	. . . . . . . . 9 ⊢ (𝑢 = (𝑚 + (i · 𝑛)) → ((((abs‘𝑢)↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃) ↔ (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)))
216	211, 215	rspc2ev 3596	. . . . . . . 8 ⊢ ((((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ∧ (𝑚 + (i · 𝑛)) ∈ ℤ[i] ∧ (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))
217	194, 196, 209, 216	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))
218	217	3expia 1139	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)))
219	42, 218	syl5 35	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁))) → ((𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)))
220	219	rexlimdvva 3224	. . . 4 ⊢ (𝜑 → (∃𝑚 ∈ (0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)))
221	41, 220	biimtrid 245	. . 3 ⊢ (𝜑 → (𝑗 ∈ (𝐴 ∩ ran 𝐹) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)))
222	221	exlimdv 1966	. 2 ⊢ (𝜑 → (∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)))
223	9, 222	mpd 16	1 ⊢ (𝜑 → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2146 {cab 2743 ≠ wne 2960 ∃wrex 3091 ∩ cin 3905 ∅c0 4286 class class class wbr 5111 ↦ cmpt 5194 ran crn 5664 ‘cfv 6540 (class class class)co 7419 ℂcc 11115 ℝcr 11116 0cc0 11117 1c1 11118 ici 11119 + caddc 11120 · cmul 11122 < clt 11260 ≤ cle 11261 − cmin 11458 / cdiv 11888 ℕcn 12250 2c2 12312 4c4 12314 ℕ₀cn0 12521 ℤcz 12608 ℝ⁺crp 13034 ...cfz 13553 mod cmo 13922 ↑cexp 14117 ℜcre 15174 ℑcim 15175 abscabs 15311 ∥ cdvds 16334 ℙcprime 16753 ℤ[i]cgz 17013

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194 ax-pre-sup 11195

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-sup 9409 df-inf 9410 df-dju 9903 df-card 9941 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-div 11889 df-nn 12251 df-2 12320 df-3 12321 df-4 12322 df-n0 12522 df-xnn0 12595 df-z 12609 df-uz 12881 df-rp 13035 df-fz 13554 df-fl 13845 df-mod 13923 df-seq 14058 df-exp 14118 df-hash 14387 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-dvds 16335 df-gcd 16577 df-prm 16754 df-gz 17014

This theorem is used by: 4sqlem13 17041

W3C validator