4sqlem12 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 4sqlem12		GIF version

Theorem 4sqlem12 13038

Description: Lemma for 4sq 13046. 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
4sqlem11.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		4sqlem11.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 13037	. . 3 ⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅)
8		prmnn 12745	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	4, 8	syl 14	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ ℕ)
10	2, 9, 5, 6	4sqleminfi 13033	. . . 4 ⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ∈ Fin)
11		fin0 7117	. . . 4 ⊢ ((𝐴 ∩ ran 𝐹) ∈ Fin → ((𝐴 ∩ ran 𝐹) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹)))
12	10, 11	syl 14	. . 3 ⊢ (𝜑 → ((𝐴 ∩ ran 𝐹) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹)))
13	7, 12	mpbid 147	. 2 ⊢ (𝜑 → ∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹))
14		vex 2806	. . . . . . . 8 ⊢ 𝑗 ∈ V
15		eqeq1 2238	. . . . . . . . 9 ⊢ (𝑢 = 𝑗 → (𝑢 = ((𝑚↑2) mod 𝑃) ↔ 𝑗 = ((𝑚↑2) mod 𝑃)))
16	15	rexbidv 2534	. . . . . . . 8 ⊢ (𝑢 = 𝑗 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃)))
17	14, 16, 5	elab2 2955	. . . . . . 7 ⊢ (𝑗 ∈ 𝐴 ↔ ∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃))
18	17	a1i 9	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ 𝐴 ↔ ∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃)))
19		abid 2219	. . . . . . . . 9 ⊢ (𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)} ↔ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣))
20	5	rexeqi 2736	. . . . . . . . 9 ⊢ (∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣) ↔ ∃𝑣 ∈ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}𝑗 = ((𝑃 − 1) − 𝑣))
21		oveq1 6035	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → (𝑚↑2) = (𝑛↑2))
22	21	oveq1d 6043	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → ((𝑚↑2) mod 𝑃) = ((𝑛↑2) mod 𝑃))
23	22	eqeq2d 2243	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑢 = ((𝑚↑2) mod 𝑃) ↔ 𝑢 = ((𝑛↑2) mod 𝑃)))
24	23	cbvrexvw 2773	. . . . . . . . . . 11 ⊢ (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑢 = ((𝑛↑2) mod 𝑃))
25		eqeq1 2238	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑣 → (𝑢 = ((𝑛↑2) mod 𝑃) ↔ 𝑣 = ((𝑛↑2) mod 𝑃)))
26	25	rexbidv 2534	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → (∃𝑛 ∈ (0...𝑁)𝑢 = ((𝑛↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃)))
27	24, 26	bitrid 192	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃)))
28	27	rexab 2969	. . . . . . . . 9 ⊢ (∃𝑣 ∈ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}𝑗 = ((𝑃 − 1) − 𝑣) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
29	19, 20, 28	3bitri 206	. . . . . . . 8 ⊢ (𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)} ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
30	6	rnmpt 4986	. . . . . . . . 9 ⊢ ran 𝐹 = {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)}
31	30	eleq2i 2298	. . . . . . . 8 ⊢ (𝑗 ∈ ran 𝐹 ↔ 𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)})
32		rexcom4 2827	. . . . . . . . 9 ⊢ (∃𝑛 ∈ (0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣∃𝑛 ∈ (0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
33		r19.41v 2690	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ (0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ (∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
34	33	exbii 1654	. . . . . . . . 9 ⊢ (∃𝑣∃𝑛 ∈ (0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
35	32, 34	bitri 184	. . . . . . . 8 ⊢ (∃𝑛 ∈ (0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
36	29, 31, 35	3bitr4i 212	. . . . . . 7 ⊢ (𝑗 ∈ ran 𝐹 ↔ ∃𝑛 ∈ (0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)))
37		elfzelz 10305	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (0...𝑁) → 𝑛 ∈ ℤ)
38	37	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑁)) → 𝑛 ∈ ℤ)
39		zsqcl 10918	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ → (𝑛↑2) ∈ ℤ)
40	38, 39	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑁)) → (𝑛↑2) ∈ ℤ)
41	9	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑁)) → 𝑃 ∈ ℕ)
42	40, 41	zmodcld 10653	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑁)) → ((𝑛↑2) mod 𝑃) ∈ ℕ₀)
43		oveq2 6036	. . . . . . . . . . 11 ⊢ (𝑣 = ((𝑛↑2) mod 𝑃) → ((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
44	43	eqeq2d 2243	. . . . . . . . . 10 ⊢ (𝑣 = ((𝑛↑2) mod 𝑃) → (𝑗 = ((𝑃 − 1) − 𝑣) ↔ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))))
45	44	ceqsexgv 2936	. . . . . . . . 9 ⊢ (((𝑛↑2) mod 𝑃) ∈ ℕ₀ → (∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))))
46	42, 45	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑁)) → (∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))))
47	46	rexbidva 2530	. . . . . . 7 ⊢ (𝜑 → (∃𝑛 ∈ (0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))))
48	36, 47	bitrid 192	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ran 𝐹 ↔ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))))
49	18, 48	anbi12d 473	. . . . 5 ⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑗 ∈ ran 𝐹) ↔ (∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃) ∧ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))))
50		elin 3392	. . . . 5 ⊢ (𝑗 ∈ (𝐴 ∩ ran 𝐹) ↔ (𝑗 ∈ 𝐴 ∧ 𝑗 ∈ ran 𝐹))
51		reeanv 2704	. . . . 5 ⊢ (∃𝑚 ∈ (0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) ↔ (∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃) ∧ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))))
52	49, 50, 51	3bitr4g 223	. . . 4 ⊢ (𝜑 → (𝑗 ∈ (𝐴 ∩ ran 𝐹) ↔ ∃𝑚 ∈ (0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))))
53		eqtr2 2250	. . . . . 6 ⊢ ((𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
54	9	nnzd 9645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 ∈ ℤ)
55		peano2zm 9561	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
56	54, 55	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑃 − 1) ∈ ℤ)
57		zq 9904	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 − 1) ∈ ℤ → (𝑃 − 1) ∈ ℚ)
58	56, 57	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 − 1) ∈ ℚ)
59	58	3ad2ant1 1045	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℚ)
60		zq 9904	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℤ → 𝑃 ∈ ℚ)
61	54, 60	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℚ)
62	61	3ad2ant1 1045	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℚ)
63	4	3ad2ant1 1045	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℙ)
64	63, 8	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℕ)
65		nnm1nn0 9485	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
66	64, 65	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℕ₀)
67	66	nn0ge0d 9502	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ (𝑃 − 1))
68	64	nnred 9198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℝ)
69	68	ltm1d 9154	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) < 𝑃)
70		modqid 10657	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑃 − 1) ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤ (𝑃 − 1) ∧ (𝑃 − 1) < 𝑃)) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1))
71	59, 62, 67, 69, 70	syl22anc 1275	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1))
72	71	oveq1d 6043	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃)) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
73		simp2r 1051	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ (0...𝑁))
74	73	elfzelzd 10306	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ ℤ)
75	74, 39	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℤ)
76		zq 9904	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛↑2) ∈ ℤ → (𝑛↑2) ∈ ℚ)
77	75, 76	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℚ)
78	64	nngt0d 9229	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < 𝑃)
79		modqlt 10641	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛↑2) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → ((𝑛↑2) mod 𝑃) < 𝑃)
80	77, 62, 78, 79	syl3anc 1274	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) < 𝑃)
81	75, 64	zmodcld 10653	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ∈ ℕ₀)
82	81	nn0zd 9644	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ∈ ℤ)
83		prmz 12746	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
84	63, 83	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℤ)
85		zltlem1 9581	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛↑2) mod 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ) → (((𝑛↑2) mod 𝑃) < 𝑃 ↔ ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1)))
86	82, 84, 85	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑛↑2) mod 𝑃) < 𝑃 ↔ ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1)))
87	80, 86	mpbid 147	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1))
88	87, 71	breqtrrd 4121	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃))
89		modqsubdir 10701	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑃 − 1) ∈ ℚ ∧ (𝑛↑2) ∈ ℚ) ∧ (𝑃 ∈ ℚ ∧ 0 < 𝑃)) → (((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃) ↔ (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃))))
90	59, 77, 62, 78, 89	syl22anc 1275	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃) ↔ (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃))))
91	88, 90	mpbid 147	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃)))
92		simp3 1026	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))
93	72, 91, 92	3eqtr4rd 2275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃))
94		simp2l 1050	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ (0...𝑁))
95	94	elfzelzd 10306	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ ℤ)
96		zsqcl 10918	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℤ → (𝑚↑2) ∈ ℤ)
97	95, 96	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℤ)
98	66	nn0zd 9644	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℤ)
99	98, 75	zsubcld 9651	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑃 − 1) − (𝑛↑2)) ∈ ℤ)
100		moddvds 12423	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℕ ∧ (𝑚↑2) ∈ ℤ ∧ ((𝑃 − 1) − (𝑛↑2)) ∈ ℤ) → (((𝑚↑2) mod 𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2)))))
101	64, 97, 99, 100	syl3anc 1274	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) mod 𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2)))))
102	93, 101	mpbid 147	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))))
103		zsqcl2 10925	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℤ → (𝑚↑2) ∈ ℕ₀)
104	95, 103	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℕ₀)
105	104	nn0cnd 9501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℂ)
106	66	nn0cnd 9501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℂ)
107		zsqcl2 10925	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℤ → (𝑛↑2) ∈ ℕ₀)
108	74, 107	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℕ₀)
109	108	nn0cnd 9501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℂ)
110	105, 106, 109	subsub3d 8562	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))) = (((𝑚↑2) + (𝑛↑2)) − (𝑃 − 1)))
111	104, 108	nn0addcld 9503	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈ ℕ₀)
112	111	nn0cnd 9501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈ ℂ)
113	64	nncnd 9199	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℂ)
114		1cnd 8238	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ∈ ℂ)
115	112, 113, 114	subsub3d 8562	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) − (𝑃 − 1)) = ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃))
116	110, 115	eqtrd 2264	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))) = ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃))
117	102, 116	breqtrd 4119	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃))
118		nn0p1nn 9483	. . . . . . . . . . . . . 14 ⊢ (((𝑚↑2) + (𝑛↑2)) ∈ ℕ₀ → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℕ)
119	111, 118	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℕ)
120	119	nnzd 9645	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℤ)
121		dvdssubr 12463	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℤ ∧ (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℤ) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃)))
122	84, 120, 121	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃)))
123	117, 122	mpbird 167	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1))
124	64	nnne0d 9230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ≠ 0)
125		dvdsval2 12414	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℤ) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ))
126	84, 124, 120, 125	syl3anc 1274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ))
127	123, 126	mpbid 147	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ)
128		nnrp 9942	. . . . . . . . . . . . . 14 ⊢ ((((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℕ → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℝ⁺)
129		nnrp 9942	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℝ⁺)
130		rpdivcl 9958	. . . . . . . . . . . . . 14 ⊢ (((((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℝ⁺ ∧ 𝑃 ∈ ℝ⁺) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℝ⁺)
131	128, 129, 130	syl2an 289	. . . . . . . . . . . . 13 ⊢ (((((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℕ ∧ 𝑃 ∈ ℕ) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℝ⁺)
132	119, 64, 131	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℝ⁺)
133	132	rpgt0d 9978	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃))
134		elnnz 9533	. . . . . . . . . . 11 ⊢ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℕ ↔ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 0 < ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃)))
135	127, 133, 134	sylanbrc 417	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℕ)
136	135	nnge1d 9228	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃))
137	111	nn0red 9500	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈ ℝ)
138		2nn 9347	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
139	2	3ad2ant1 1045	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℕ)
140		nnmulcl 9206	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
141	138, 139, 140	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℕ)
142	141	nnred 9198	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℝ)
143	142	resqcld 11007	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) ∈ ℝ)
144		nnmulcl 9206	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ ∧ (2 · 𝑁) ∈ ℕ) → (2 · (2 · 𝑁)) ∈ ℕ)
145	138, 141, 144	sylancr 414	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈ ℕ)
146	145	nnred 9198	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈ ℝ)
147	143, 146	readdcld 8251	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) ∈ ℝ)
148		1red 8237	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ∈ ℝ)
149	139	nnsqcld 11002	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℕ)
150		nnmulcl 9206	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ (𝑁↑2) ∈ ℕ) → (2 · (𝑁↑2)) ∈ ℕ)
151	138, 149, 150	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) ∈ ℕ)
152	151	nnred 9198	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) ∈ ℝ)
153	104	nn0red 9500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℝ)
154	108	nn0red 9500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℝ)
155	149	nnred 9198	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℝ)
156	95	zred 9646	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ ℝ)
157		elfzle1 10307	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (0...𝑁) → 0 ≤ 𝑚)
158	94, 157	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ 𝑚)
159	139	nnred 9198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℝ)
160		elfzle2 10308	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ≤ 𝑁)
161	94, 160	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ≤ 𝑁)
162		le2sq2 10923	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (𝑁 ∈ ℝ ∧ 𝑚 ≤ 𝑁)) → (𝑚↑2) ≤ (𝑁↑2))
163	156, 158, 159, 161, 162	syl22anc 1275	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ≤ (𝑁↑2))
164	74	zred 9646	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ ℝ)
165		elfzle1 10307	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (0...𝑁) → 0 ≤ 𝑛)
166	73, 165	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ 𝑛)
167		elfzle2 10308	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (0...𝑁) → 𝑛 ≤ 𝑁)
168	73, 167	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ≤ 𝑁)
169		le2sq2 10923	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 𝑛 ≤ 𝑁)) → (𝑛↑2) ≤ (𝑁↑2))
170	164, 166, 159, 168, 169	syl22anc 1275	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ≤ (𝑁↑2))
171	153, 154, 155, 155, 163, 170	le2addd 8785	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ≤ ((𝑁↑2) + (𝑁↑2)))
172	149	nncnd 9199	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℂ)
173	172	2timesd 9429	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) = ((𝑁↑2) + (𝑁↑2)))
174	171, 173	breqtrrd 4121	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ≤ (2 · (𝑁↑2)))
175		2lt4 9359	. . . . . . . . . . . . . . . 16 ⊢ 2 < 4
176		2re 9255	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
177	176	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 2 ∈ ℝ)
178		4re 9262	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ ℝ
179	178	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 4 ∈ ℝ)
180	149	nngt0d 9229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < (𝑁↑2))
181		ltmul1 8814	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℝ ∧ 4 ∈ ℝ ∧ ((𝑁↑2) ∈ ℝ ∧ 0 < (𝑁↑2))) → (2 < 4 ↔ (2 · (𝑁↑2)) < (4 · (𝑁↑2))))
182	177, 179, 155, 180, 181	syl112anc 1278	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 < 4 ↔ (2 · (𝑁↑2)) < (4 · (𝑁↑2))))
183	175, 182	mpbii 148	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) < (4 · (𝑁↑2)))
184		2cn 9256	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℂ
185	139	nncnd 9199	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℂ)
186		sqmul 10909	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((2 · 𝑁)↑2) = ((2↑2) · (𝑁↑2)))
187	184, 185, 186	sylancr 414	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) = ((2↑2) · (𝑁↑2)))
188		sq2 10943	. . . . . . . . . . . . . . . . 17 ⊢ (2↑2) = 4
189	188	oveq1i 6038	. . . . . . . . . . . . . . . 16 ⊢ ((2↑2) · (𝑁↑2)) = (4 · (𝑁↑2))
190	187, 189	eqtrdi 2280	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) = (4 · (𝑁↑2)))
191	183, 190	breqtrrd 4121	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) < ((2 · 𝑁)↑2))
192	137, 152, 143, 174, 191	lelttrd 8346	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) < ((2 · 𝑁)↑2))
193	145	nnrpd 9973	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈ ℝ⁺)
194	143, 193	ltaddrpd 10009	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) < (((2 · 𝑁)↑2) + (2 · (2 · 𝑁))))
195	137, 143, 147, 192, 194	lttrd 8347	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) < (((2 · 𝑁)↑2) + (2 · (2 · 𝑁))))
196	137, 147, 148, 195	ltadd1dd 8778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) < ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1))
197	3	3ad2ant1 1045	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 = ((2 · 𝑁) + 1))
198	197	oveq1d 6043	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃↑2) = (((2 · 𝑁) + 1)↑2))
199	113	sqvald 10978	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃↑2) = (𝑃 · 𝑃))
200	141	nncnd 9199	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℂ)
201		binom21 10960	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℂ → (((2 · 𝑁) + 1)↑2) = ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1))
202	200, 201	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((2 · 𝑁) + 1)↑2) = ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1))
203	198, 199, 202	3eqtr3d 2272	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 · 𝑃) = ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1))
204	196, 203	breqtrrd 4121	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃))
205	119	nnred 9198	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℝ)
206		ltdivmul 9098	. . . . . . . . . . 11 ⊢ (((((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃 ↔ (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃)))
207	205, 68, 68, 78, 206	syl112anc 1278	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃 ↔ (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃)))
208	204, 207	mpbird 167	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃)
209		1z 9549	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
210		elfzm11 10371	. . . . . . . . . 10 ⊢ ((1 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ↔ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∧ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃)))
211	209, 84, 210	sylancr 414	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ↔ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∧ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃)))
212	127, 136, 208, 211	mpbir3and 1207	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)))
213		gzreim 13015	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑚 + (i · 𝑛)) ∈ ℤ[i])
214	95, 74, 213	syl2anc 411	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚 + (i · 𝑛)) ∈ ℤ[i])
215		gzcn 13008	. . . . . . . . . . . . 13 ⊢ ((𝑚 + (i · 𝑛)) ∈ ℤ[i] → (𝑚 + (i · 𝑛)) ∈ ℂ)
216	214, 215	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚 + (i · 𝑛)) ∈ ℂ)
217	216	absvalsq2d 11806	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((abs‘(𝑚 + (i · 𝑛)))↑2) = (((ℜ‘(𝑚 + (i · 𝑛)))↑2) + ((ℑ‘(𝑚 + (i · 𝑛)))↑2)))
218	156, 164	crred 11599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (ℜ‘(𝑚 + (i · 𝑛))) = 𝑚)
219	218	oveq1d 6043	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((ℜ‘(𝑚 + (i · 𝑛)))↑2) = (𝑚↑2))
220	156, 164	crimd 11600	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (ℑ‘(𝑚 + (i · 𝑛))) = 𝑛)
221	220	oveq1d 6043	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((ℑ‘(𝑚 + (i · 𝑛)))↑2) = (𝑛↑2))
222	219, 221	oveq12d 6046	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((ℜ‘(𝑚 + (i · 𝑛)))↑2) + ((ℑ‘(𝑚 + (i · 𝑛)))↑2)) = ((𝑚↑2) + (𝑛↑2)))
223	217, 222	eqtrd 2264	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((abs‘(𝑚 + (i · 𝑛)))↑2) = ((𝑚↑2) + (𝑛↑2)))
224	223	oveq1d 6043	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((𝑚↑2) + (𝑛↑2)) + 1))
225	119	nncnd 9199	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℂ)
226	64	nnap0d 9231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 # 0)
227	225, 113, 226	divcanap1d 9013	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃) = (((𝑚↑2) + (𝑛↑2)) + 1))
228	224, 227	eqtr4d 2267	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃))
229		oveq1 6035	. . . . . . . . . 10 ⊢ (𝑘 = ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) → (𝑘 · 𝑃) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃))
230	229	eqeq2d 2243	. . . . . . . . 9 ⊢ (𝑘 = ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) → ((((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃) ↔ (((abs‘𝑢)↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)))
231		fveq2 5648	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑚 + (i · 𝑛)) → (abs‘𝑢) = (abs‘(𝑚 + (i · 𝑛))))
232	231	oveq1d 6043	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑚 + (i · 𝑛)) → ((abs‘𝑢)↑2) = ((abs‘(𝑚 + (i · 𝑛)))↑2))
233	232	oveq1d 6043	. . . . . . . . . 10 ⊢ (𝑢 = (𝑚 + (i · 𝑛)) → (((abs‘𝑢)↑2) + 1) = (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1))
234	233	eqeq1d 2240	. . . . . . . . 9 ⊢ (𝑢 = (𝑚 + (i · 𝑛)) → ((((abs‘𝑢)↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃) ↔ (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)))
235	230, 234	rspc2ev 2926	. . . . . . . 8 ⊢ ((((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ∧ (𝑚 + (i · 𝑛)) ∈ ℤ[i] ∧ (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))
236	212, 214, 228, 235	syl3anc 1274	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))
237	236	3expia 1232	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)))
238	53, 237	syl5 32	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁))) → ((𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)))
239	238	rexlimdvva 2659	. . . 4 ⊢ (𝜑 → (∃𝑚 ∈ (0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)))
240	52, 239	sylbid 150	. . 3 ⊢ (𝜑 → (𝑗 ∈ (𝐴 ∩ ran 𝐹) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)))
241	240	exlimdv 1867	. 2 ⊢ (𝜑 → (∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)))
242	13, 241	mpd 13	1 ⊢ (𝜑 → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 1005 = wceq 1398 ∃wex 1541 ∈ wcel 2202 {cab 2217 ≠ wne 2403 ∃wrex 2512 ∩ cin 3200 ∅c0 3496 class class class wbr 4093 ↦ cmpt 4155 ran crn 4732 ‘cfv 5333 (class class class)co 6028 Fincfn 6952 ℂcc 8073 ℝcr 8074 0cc0 8075 1c1 8076 ici 8077 + caddc 8078 · cmul 8080 < clt 8256 ≤ cle 8257 − cmin 8392 / cdiv 8894 ℕcn 9185 2c2 9236 4c4 9238 ℕ₀cn0 9444 ℤcz 9523 ℚcq 9897 ℝ⁺crp 9932 ...cfz 10288 mod cmo 10630 ↑cexp 10846 ℜcre 11463 ℑcim 11464 abscabs 11620 ∥ cdvds 12411 ℙcprime 12742 ℤ[i]cgz 13005

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692 ax-cnex 8166 ax-resscn 8167 ax-1cn 8168 ax-1re 8169 ax-icn 8170 ax-addcl 8171 ax-addrcl 8172 ax-mulcl 8173 ax-mulrcl 8174 ax-addcom 8175 ax-mulcom 8176 ax-addass 8177 ax-mulass 8178 ax-distr 8179 ax-i2m1 8180 ax-0lt1 8181 ax-1rid 8182 ax-0id 8183 ax-rnegex 8184 ax-precex 8185 ax-cnre 8186 ax-pre-ltirr 8187 ax-pre-ltwlin 8188 ax-pre-lttrn 8189 ax-pre-apti 8190 ax-pre-ltadd 8191 ax-pre-mulgt0 8192 ax-pre-mulext 8193 ax-arch 8194 ax-caucvg 8195

This theorem depends on definitions: df-bi 117 df-stab 839 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-nel 2499 df-ral 2516 df-rex 2517 df-reu 2518 df-rmo 2519 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-if 3608 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-po 4399 df-iso 4400 df-iord 4469 df-on 4471 df-ilim 4472 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-riota 5981 df-ov 6031 df-oprab 6032 df-mpo 6033 df-1st 6312 df-2nd 6313 df-recs 6514 df-irdg 6579 df-frec 6600 df-1o 6625 df-2o 6626 df-oadd 6629 df-er 6745 df-en 6953 df-dom 6954 df-fin 6955 df-sup 7226 df-pnf 8258 df-mnf 8259 df-xr 8260 df-ltxr 8261 df-le 8262 df-sub 8394 df-neg 8395 df-reap 8797 df-ap 8804 df-div 8895 df-inn 9186 df-2 9244 df-3 9245 df-4 9246 df-n0 9445 df-z 9524 df-uz 9800 df-q 9898 df-rp 9933 df-fz 10289 df-fzo 10423 df-fl 10576 df-mod 10631 df-seqfrec 10756 df-exp 10847 df-ihash 11084 df-cj 11465 df-re 11466 df-im 11467 df-rsqrt 11621 df-abs 11622 df-dvds 12412 df-gcd 12588 df-prm 12743 df-gz 13006

This theorem is referenced by: 4sqlem13m 13039

W3C validator