4sqlem12

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

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

Proof

Step	Hyp	Ref	Expression
1		4sq.1	⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2		4sq.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		4sq.3	⊢ ( 𝜑 → 𝑃 = ( ( 2 · 𝑁 ) + 1 ) )
4		4sq.4	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		4sqlem11.5	⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) }
6		4sqlem11.6	⊢ 𝐹 = ( 𝑣 ∈ 𝐴 ↦ ( ( 𝑃 − 1 ) − 𝑣 ) )
7	1 2 3 4 5 6	4sqlem11	⊢ ( 𝜑 → ( 𝐴 ∩ ran 𝐹 ) ≠ ∅ )
8		n0	⊢ ( ( 𝐴 ∩ ran 𝐹 ) ≠ ∅ ↔ ∃ 𝑗 𝑗 ∈ ( 𝐴 ∩ ran 𝐹 ) )
9	7 8	sylib	⊢ ( 𝜑 → ∃ 𝑗 𝑗 ∈ ( 𝐴 ∩ ran 𝐹 ) )
10		vex	⊢ 𝑗 ∈ V
11		eqeq1	⊢ ( 𝑢 = 𝑗 → ( 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ↔ 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) )
12	11	rexbidv	⊢ ( 𝑢 = 𝑗 → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ↔ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) )
13	10 12 5	elab2	⊢ ( 𝑗 ∈ 𝐴 ↔ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) )
14		abid	⊢ ( 𝑗 ∈ { 𝑗 ∣ ∃ 𝑣 ∈ 𝐴 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) } ↔ ∃ 𝑣 ∈ 𝐴 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) )
15	5	rexeqi	⊢ ( ∃ 𝑣 ∈ 𝐴 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ↔ ∃ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) } 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) )
16		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 ↑ 2 ) = ( 𝑛 ↑ 2 ) )
17	16	oveq1d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) )
18	17	eqeq2d	⊢ ( 𝑚 = 𝑛 → ( 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ↔ 𝑢 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
19	18	cbvrexvw	⊢ ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) )
20		eqeq1	⊢ ( 𝑢 = 𝑣 → ( 𝑢 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ↔ 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
21	20	rexbidv	⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
22	19 21	syl5bb	⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
23	22	rexab	⊢ ( ∃ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) } 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ↔ ∃ 𝑣 ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) )
24	14 15 23	3bitri	⊢ ( 𝑗 ∈ { 𝑗 ∣ ∃ 𝑣 ∈ 𝐴 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) } ↔ ∃ 𝑣 ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) )
25	6	rnmpt	⊢ ran 𝐹 = { 𝑗 ∣ ∃ 𝑣 ∈ 𝐴 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) }
26	25	eleq2i	⊢ ( 𝑗 ∈ ran 𝐹 ↔ 𝑗 ∈ { 𝑗 ∣ ∃ 𝑣 ∈ 𝐴 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) } )
27		rexcom4	⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ∃ 𝑣 ( 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) ↔ ∃ 𝑣 ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ( 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) )
28		r19.41v	⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ( 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) ↔ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) )
29	28	exbii	⊢ ( ∃ 𝑣 ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ( 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) ↔ ∃ 𝑣 ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) )
30	27 29	bitri	⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ∃ 𝑣 ( 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) ↔ ∃ 𝑣 ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) )
31	24 26 30	3bitr4i	⊢ ( 𝑗 ∈ ran 𝐹 ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ∃ 𝑣 ( 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) )
32		ovex	⊢ ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∈ V
33		oveq2	⊢ ( 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) → ( ( 𝑃 − 1 ) − 𝑣 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
34	33	eqeq2d	⊢ ( 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) → ( 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ↔ 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) )
35	32 34	ceqsexv	⊢ ( ∃ 𝑣 ( 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) ↔ 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
36	35	rexbii	⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ∃ 𝑣 ( 𝑣 = ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − 𝑣 ) ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
37	31 36	bitri	⊢ ( 𝑗 ∈ ran 𝐹 ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
38	13 37	anbi12i	⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑗 ∈ ran 𝐹 ) ↔ ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) )
39		elin	⊢ ( 𝑗 ∈ ( 𝐴 ∩ ran 𝐹 ) ↔ ( 𝑗 ∈ 𝐴 ∧ 𝑗 ∈ ran 𝐹 ) )
40		reeanv	⊢ ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ( 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) ↔ ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) )
41	38 39 40	3bitr4i	⊢ ( 𝑗 ∈ ( 𝐴 ∩ ran 𝐹 ) ↔ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ( 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) )
42		eqtr2	⊢ ( ( 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
43	4	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∈ ℙ )
44		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
45	43 44	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∈ ℕ )
46		nnm1nn0	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ₀ )
47	45 46	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 − 1 ) ∈ ℕ₀ )
48	47	nn0red	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 − 1 ) ∈ ℝ )
49	45	nnrpd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∈ ℝ⁺ )
50	47	nn0ge0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 ≤ ( 𝑃 − 1 ) )
51	45	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∈ ℝ )
52	51	ltm1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 − 1 ) < 𝑃 )
53		modid	⊢ ( ( ( ( 𝑃 − 1 ) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺ ) ∧ ( 0 ≤ ( 𝑃 − 1 ) ∧ ( 𝑃 − 1 ) < 𝑃 ) ) → ( ( 𝑃 − 1 ) mod 𝑃 ) = ( 𝑃 − 1 ) )
54	48 49 50 52 53	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑃 − 1 ) mod 𝑃 ) = ( 𝑃 − 1 ) )
55	54	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑃 − 1 ) mod 𝑃 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
56		simp2r	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑛 ∈ ( 0 ... 𝑁 ) )
57		elfzelz	⊢ ( 𝑛 ∈ ( 0 ... 𝑁 ) → 𝑛 ∈ ℤ )
58	56 57	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑛 ∈ ℤ )
59		zsqcl2	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ↑ 2 ) ∈ ℕ₀ )
60	58 59	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ∈ ℕ₀ )
61	60	nn0red	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ∈ ℝ )
62		modlt	⊢ ( ( ( 𝑛 ↑ 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺ ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) < 𝑃 )
63	61 49 62	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) < 𝑃 )
64		zsqcl	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ↑ 2 ) ∈ ℤ )
65	58 64	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ∈ ℤ )
66	65 45	zmodcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∈ ℕ₀ )
67	66	nn0zd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∈ ℤ )
68		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
69	43 68	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∈ ℤ )
70		zltlem1	⊢ ( ( ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( ( 𝑛 ↑ 2 ) mod 𝑃 ) < 𝑃 ↔ ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( 𝑃 − 1 ) ) )
71	67 69 70	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑛 ↑ 2 ) mod 𝑃 ) < 𝑃 ↔ ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( 𝑃 − 1 ) ) )
72	63 71	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( 𝑃 − 1 ) )
73	72 54	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( ( 𝑃 − 1 ) mod 𝑃 ) )
74		modsubdir	⊢ ( ( ( 𝑃 − 1 ) ∈ ℝ ∧ ( 𝑛 ↑ 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺ ) → ( ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( ( 𝑃 − 1 ) mod 𝑃 ) ↔ ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) mod 𝑃 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) )
75	48 61 49 74	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( ( 𝑃 − 1 ) mod 𝑃 ) ↔ ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) mod 𝑃 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) )
76	73 75	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) mod 𝑃 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
77		simp3	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
78	55 76 77	3eqtr4rd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) )
79		simp2l	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑚 ∈ ( 0 ... 𝑁 ) )
80		elfzelz	⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → 𝑚 ∈ ℤ )
81	79 80	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑚 ∈ ℤ )
82		zsqcl	⊢ ( 𝑚 ∈ ℤ → ( 𝑚 ↑ 2 ) ∈ ℤ )
83	81 82	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℤ )
84	47	nn0zd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 − 1 ) ∈ ℤ )
85	84 65	zsubcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ∈ ℤ )
86		moddvds	⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑚 ↑ 2 ) ∈ ℤ ∧ ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ∈ ℤ ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑚 ↑ 2 ) − ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ) ) )
87	45 83 85 86	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑚 ↑ 2 ) − ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ) ) )
88	78 87	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∥ ( ( 𝑚 ↑ 2 ) − ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ) )
89		zsqcl2	⊢ ( 𝑚 ∈ ℤ → ( 𝑚 ↑ 2 ) ∈ ℕ₀ )
90	81 89	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℕ₀ )
91	90	nn0cnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℂ )
92	47	nn0cnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 − 1 ) ∈ ℂ )
93	60	nn0cnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ∈ ℂ )
94	91 92 93	subsub3d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) − ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ) = ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) − ( 𝑃 − 1 ) ) )
95	90 60	nn0addcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ∈ ℕ₀ )
96	95	nn0cnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ∈ ℂ )
97	45	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∈ ℂ )
98		1cnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 1 ∈ ℂ )
99	96 97 98	subsub3d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) − ( 𝑃 − 1 ) ) = ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) − 𝑃 ) )
100	94 99	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) − ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ) = ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) − 𝑃 ) )
101	88 100	breqtrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∥ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) − 𝑃 ) )
102		nn0p1nn	⊢ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ∈ ℕ₀ → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℕ )
103	95 102	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℕ )
104	103	nnzd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℤ )
105		dvdssubr	⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ↔ 𝑃 ∥ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) − 𝑃 ) ) )
106	69 104 105	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 ∥ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ↔ 𝑃 ∥ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) − 𝑃 ) ) )
107	101 106	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∥ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) )
108	45	nnne0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ≠ 0 )
109		dvdsval2	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ↔ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ ) )
110	69 108 104 109	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 ∥ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ↔ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ ) )
111	107 110	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ )
112		nnrp	⊢ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℕ → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℝ⁺ )
113		nnrp	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ⁺ )
114		rpdivcl	⊢ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℝ⁺ ∧ 𝑃 ∈ ℝ⁺ ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℝ⁺ )
115	112 113 114	syl2an	⊢ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℝ⁺ )
116	103 45 115	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℝ⁺ )
117	116	rpgt0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 < ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) )
118		elnnz	⊢ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℕ ↔ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ ∧ 0 < ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ) )
119	111 117 118	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℕ )
120	119	nnge1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 1 ≤ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) )
121	95	nn0red	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ∈ ℝ )
122		2nn	⊢ 2 ∈ ℕ
123	2	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑁 ∈ ℕ )
124		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
125	122 123 124	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · 𝑁 ) ∈ ℕ )
126	125	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · 𝑁 ) ∈ ℝ )
127	126	resqcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 2 · 𝑁 ) ↑ 2 ) ∈ ℝ )
128		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ ( 2 · 𝑁 ) ∈ ℕ ) → ( 2 · ( 2 · 𝑁 ) ) ∈ ℕ )
129	122 125 128	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 2 · 𝑁 ) ) ∈ ℕ )
130	129	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 2 · 𝑁 ) ) ∈ ℝ )
131	127 130	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) ∈ ℝ )
132		1red	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 1 ∈ ℝ )
133	123	nnsqcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑁 ↑ 2 ) ∈ ℕ )
134		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ ( 𝑁 ↑ 2 ) ∈ ℕ ) → ( 2 · ( 𝑁 ↑ 2 ) ) ∈ ℕ )
135	122 133 134	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 𝑁 ↑ 2 ) ) ∈ ℕ )
136	135	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 𝑁 ↑ 2 ) ) ∈ ℝ )
137	90	nn0red	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℝ )
138	133	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑁 ↑ 2 ) ∈ ℝ )
139	81	zred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑚 ∈ ℝ )
140		elfzle1	⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑚 )
141	79 140	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 ≤ 𝑚 )
142	123	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑁 ∈ ℝ )
143		elfzle2	⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → 𝑚 ≤ 𝑁 )
144	79 143	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑚 ≤ 𝑁 )
145		le2sq2	⊢ ( ( ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) ∧ ( 𝑁 ∈ ℝ ∧ 𝑚 ≤ 𝑁 ) ) → ( 𝑚 ↑ 2 ) ≤ ( 𝑁 ↑ 2 ) )
146	139 141 142 144 145	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ≤ ( 𝑁 ↑ 2 ) )
147	58	zred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑛 ∈ ℝ )
148		elfzle1	⊢ ( 𝑛 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑛 )
149	56 148	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 ≤ 𝑛 )
150		elfzle2	⊢ ( 𝑛 ∈ ( 0 ... 𝑁 ) → 𝑛 ≤ 𝑁 )
151	56 150	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑛 ≤ 𝑁 )
152		le2sq2	⊢ ( ( ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) ∧ ( 𝑁 ∈ ℝ ∧ 𝑛 ≤ 𝑁 ) ) → ( 𝑛 ↑ 2 ) ≤ ( 𝑁 ↑ 2 ) )
153	147 149 142 151 152	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ≤ ( 𝑁 ↑ 2 ) )
154	137 61 138 138 146 153	le2addd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ≤ ( ( 𝑁 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )
155	133	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑁 ↑ 2 ) ∈ ℂ )
156	155	2timesd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 𝑁 ↑ 2 ) ) = ( ( 𝑁 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )
157	154 156	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ≤ ( 2 · ( 𝑁 ↑ 2 ) ) )
158		2lt4	⊢ 2 < 4
159		2re	⊢ 2 ∈ ℝ
160	159	a1i	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 2 ∈ ℝ )
161		4re	⊢ 4 ∈ ℝ
162	161	a1i	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 4 ∈ ℝ )
163	133	nngt0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 < ( 𝑁 ↑ 2 ) )
164		ltmul1	⊢ ( ( 2 ∈ ℝ ∧ 4 ∈ ℝ ∧ ( ( 𝑁 ↑ 2 ) ∈ ℝ ∧ 0 < ( 𝑁 ↑ 2 ) ) ) → ( 2 < 4 ↔ ( 2 · ( 𝑁 ↑ 2 ) ) < ( 4 · ( 𝑁 ↑ 2 ) ) ) )
165	160 162 138 163 164	syl112anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 < 4 ↔ ( 2 · ( 𝑁 ↑ 2 ) ) < ( 4 · ( 𝑁 ↑ 2 ) ) ) )
166	158 165	mpbii	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 𝑁 ↑ 2 ) ) < ( 4 · ( 𝑁 ↑ 2 ) ) )
167		2cn	⊢ 2 ∈ ℂ
168	123	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑁 ∈ ℂ )
169		sqmul	⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 2 · 𝑁 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) )
170	167 168 169	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 2 · 𝑁 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) )
171		sq2	⊢ ( 2 ↑ 2 ) = 4
172	171	oveq1i	⊢ ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) = ( 4 · ( 𝑁 ↑ 2 ) )
173	170 172	syl6eq	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 2 · 𝑁 ) ↑ 2 ) = ( 4 · ( 𝑁 ↑ 2 ) ) )
174	166 173	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 𝑁 ↑ 2 ) ) < ( ( 2 · 𝑁 ) ↑ 2 ) )
175	121 136 127 157 174	lelttrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) < ( ( 2 · 𝑁 ) ↑ 2 ) )
176	129	nnrpd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 2 · 𝑁 ) ) ∈ ℝ⁺ )
177	127 176	ltaddrpd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 2 · 𝑁 ) ↑ 2 ) < ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) )
178	121 127 131 175 177	lttrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) < ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) )
179	121 131 132 178	ltadd1dd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) < ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
180	3	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 = ( ( 2 · 𝑁 ) + 1 ) )
181	180	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 ↑ 2 ) = ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) )
182	97	sqvald	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 ↑ 2 ) = ( 𝑃 · 𝑃 ) )
183	125	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · 𝑁 ) ∈ ℂ )
184		binom21	⊢ ( ( 2 · 𝑁 ) ∈ ℂ → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
185	183 184	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
186	181 182 185	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 · 𝑃 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
187	179 186	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) < ( 𝑃 · 𝑃 ) )
188	103	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℝ )
189	45	nngt0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 < 𝑃 )
190		ltdivmul	⊢ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) ) → ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) < 𝑃 ↔ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) < ( 𝑃 · 𝑃 ) ) )
191	188 51 51 189 190	syl112anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) < 𝑃 ↔ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) < ( 𝑃 · 𝑃 ) ) )
192	187 191	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) < 𝑃 )
193		1z	⊢ 1 ∈ ℤ
194		elfzm11	⊢ ( ( 1 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ ∧ 1 ≤ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∧ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) < 𝑃 ) ) )
195	193 69 194	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ ∧ 1 ≤ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∧ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) < 𝑃 ) ) )
196	111 120 192 195	mpbir3and	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
197		gzreim	⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑚 + ( i · 𝑛 ) ) ∈ ℤ[i] )
198	81 58 197	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 + ( i · 𝑛 ) ) ∈ ℤ[i] )
199		gzcn	⊢ ( ( 𝑚 + ( i · 𝑛 ) ) ∈ ℤ[i] → ( 𝑚 + ( i · 𝑛 ) ) ∈ ℂ )
200	198 199	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 + ( i · 𝑛 ) ) ∈ ℂ )
201	200	absvalsq2d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) ) )
202	139 147	crred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ℜ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) = 𝑚 )
203	202	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ℜ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) = ( 𝑚 ↑ 2 ) )
204	139 147	crimd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ℑ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) = 𝑛 )
205	204	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ℑ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) = ( 𝑛 ↑ 2 ) )
206	203 205	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ℜ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) )
207	201 206	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) )
208	207	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + 1 ) = ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) )
209	103	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℂ )
210	209 97 108	divcan1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) = ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) )
211	208 210	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + 1 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) )
212		oveq1	⊢ ( 𝑘 = ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) → ( 𝑘 · 𝑃 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) )
213	212	eqeq2d	⊢ ( 𝑘 = ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) → ( ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ↔ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) ) )
214		fveq2	⊢ ( 𝑢 = ( 𝑚 + ( i · 𝑛 ) ) → ( abs ‘ 𝑢 ) = ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) )
215	214	oveq1d	⊢ ( 𝑢 = ( 𝑚 + ( i · 𝑛 ) ) → ( ( abs ‘ 𝑢 ) ↑ 2 ) = ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) )
216	215	oveq1d	⊢ ( 𝑢 = ( 𝑚 + ( i · 𝑛 ) ) → ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + 1 ) )
217	216	eqeq1d	⊢ ( 𝑢 = ( 𝑚 + ( i · 𝑛 ) ) → ( ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) ↔ ( ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + 1 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) ) )
218	213 217	rspc2ev	⊢ ( ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ( 𝑚 + ( i · 𝑛 ) ) ∈ ℤ[i] ∧ ( ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + 1 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) )
219	196 198 211 218	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) )
220	219	3expia	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) )
221	42 220	syl5	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ) → ( ( 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) )
222	221	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ( 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) )
223	41 222	syl5bi	⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝐴 ∩ ran 𝐹 ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) )
224	223	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑗 𝑗 ∈ ( 𝐴 ∩ ran 𝐹 ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) )
225	9 224	mpd	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) )

Metamath Proof Explorer

Theorem 4sqlem12

Proof