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	bitrid	⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑚 ∈ ( 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	56	elfzelzd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑛 ∈ ℤ )
58		zsqcl2	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ↑ 2 ) ∈ ℕ₀ )
59	57 58	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ∈ ℕ₀ )
60	59	nn0red	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ∈ ℝ )
61		modlt	⊢ ( ( ( 𝑛 ↑ 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺ ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) < 𝑃 )
62	60 49 61	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) < 𝑃 )
63		zsqcl	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ↑ 2 ) ∈ ℤ )
64	57 63	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ∈ ℤ )
65	64 45	zmodcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∈ ℕ₀ )
66	65	nn0zd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∈ ℤ )
67		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
68	43 67	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∈ ℤ )
69		zltlem1	⊢ ( ( ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( ( 𝑛 ↑ 2 ) mod 𝑃 ) < 𝑃 ↔ ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( 𝑃 − 1 ) ) )
70	66 68 69	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑛 ↑ 2 ) mod 𝑃 ) < 𝑃 ↔ ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( 𝑃 − 1 ) ) )
71	62 70	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( 𝑃 − 1 ) )
72	71 54	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( ( 𝑃 − 1 ) mod 𝑃 ) )
73		modsubdir	⊢ ( ( ( 𝑃 − 1 ) ∈ ℝ ∧ ( 𝑛 ↑ 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺ ) → ( ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( ( 𝑃 − 1 ) mod 𝑃 ) ↔ ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) mod 𝑃 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) )
74	48 60 49 73	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ≤ ( ( 𝑃 − 1 ) mod 𝑃 ) ↔ ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) mod 𝑃 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) )
75	72 74	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) mod 𝑃 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
76		simp3	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) )
77	55 75 76	3eqtr4rd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) )
78		simp2l	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑚 ∈ ( 0 ... 𝑁 ) )
79	78	elfzelzd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑚 ∈ ℤ )
80		zsqcl	⊢ ( 𝑚 ∈ ℤ → ( 𝑚 ↑ 2 ) ∈ ℤ )
81	79 80	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℤ )
82	47	nn0zd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 − 1 ) ∈ ℤ )
83	82 64	zsubcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ∈ ℤ )
84		moddvds	⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑚 ↑ 2 ) ∈ ℤ ∧ ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ∈ ℤ ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑚 ↑ 2 ) − ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ) ) )
85	45 81 83 84	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑚 ↑ 2 ) − ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ) ) )
86	77 85	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∥ ( ( 𝑚 ↑ 2 ) − ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ) )
87		zsqcl2	⊢ ( 𝑚 ∈ ℤ → ( 𝑚 ↑ 2 ) ∈ ℕ₀ )
88	79 87	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℕ₀ )
89	88	nn0cnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℂ )
90	47	nn0cnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 − 1 ) ∈ ℂ )
91	59	nn0cnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ∈ ℂ )
92	89 90 91	subsub3d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) − ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ) = ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) − ( 𝑃 − 1 ) ) )
93	88 59	nn0addcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ∈ ℕ₀ )
94	93	nn0cnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ∈ ℂ )
95	45	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∈ ℂ )
96		1cnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 1 ∈ ℂ )
97	94 95 96	subsub3d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) − ( 𝑃 − 1 ) ) = ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) − 𝑃 ) )
98	92 97	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) − ( ( 𝑃 − 1 ) − ( 𝑛 ↑ 2 ) ) ) = ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) − 𝑃 ) )
99	86 98	breqtrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∥ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) − 𝑃 ) )
100		nn0p1nn	⊢ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ∈ ℕ₀ → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℕ )
101	93 100	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℕ )
102	101	nnzd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℤ )
103		dvdssubr	⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ↔ 𝑃 ∥ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) − 𝑃 ) ) )
104	68 102 103	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 ∥ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ↔ 𝑃 ∥ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) − 𝑃 ) ) )
105	99 104	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ∥ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) )
106	45	nnne0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 ≠ 0 )
107		dvdsval2	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ↔ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ ) )
108	68 106 102 107	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 ∥ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ↔ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ ) )
109	105 108	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ )
110		nnrp	⊢ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℕ → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℝ⁺ )
111		nnrp	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ⁺ )
112		rpdivcl	⊢ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℝ⁺ ∧ 𝑃 ∈ ℝ⁺ ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℝ⁺ )
113	110 111 112	syl2an	⊢ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℝ⁺ )
114	101 45 113	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℝ⁺ )
115	114	rpgt0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 < ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) )
116		elnnz	⊢ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℕ ↔ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ ∧ 0 < ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ) )
117	109 115 116	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℕ )
118	117	nnge1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 1 ≤ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) )
119	93	nn0red	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ∈ ℝ )
120		2nn	⊢ 2 ∈ ℕ
121	2	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑁 ∈ ℕ )
122		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
123	120 121 122	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · 𝑁 ) ∈ ℕ )
124	123	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · 𝑁 ) ∈ ℝ )
125	124	resqcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 2 · 𝑁 ) ↑ 2 ) ∈ ℝ )
126		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ ( 2 · 𝑁 ) ∈ ℕ ) → ( 2 · ( 2 · 𝑁 ) ) ∈ ℕ )
127	120 123 126	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 2 · 𝑁 ) ) ∈ ℕ )
128	127	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 2 · 𝑁 ) ) ∈ ℝ )
129	125 128	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) ∈ ℝ )
130		1red	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 1 ∈ ℝ )
131	121	nnsqcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑁 ↑ 2 ) ∈ ℕ )
132		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ ( 𝑁 ↑ 2 ) ∈ ℕ ) → ( 2 · ( 𝑁 ↑ 2 ) ) ∈ ℕ )
133	120 131 132	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 𝑁 ↑ 2 ) ) ∈ ℕ )
134	133	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 𝑁 ↑ 2 ) ) ∈ ℝ )
135	88	nn0red	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℝ )
136	131	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑁 ↑ 2 ) ∈ ℝ )
137	79	zred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑚 ∈ ℝ )
138		elfzle1	⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑚 )
139	78 138	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 ≤ 𝑚 )
140	121	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑁 ∈ ℝ )
141		elfzle2	⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → 𝑚 ≤ 𝑁 )
142	78 141	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑚 ≤ 𝑁 )
143		le2sq2	⊢ ( ( ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) ∧ ( 𝑁 ∈ ℝ ∧ 𝑚 ≤ 𝑁 ) ) → ( 𝑚 ↑ 2 ) ≤ ( 𝑁 ↑ 2 ) )
144	137 139 140 142 143	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ≤ ( 𝑁 ↑ 2 ) )
145	57	zred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑛 ∈ ℝ )
146		elfzle1	⊢ ( 𝑛 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑛 )
147	56 146	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 ≤ 𝑛 )
148		elfzle2	⊢ ( 𝑛 ∈ ( 0 ... 𝑁 ) → 𝑛 ≤ 𝑁 )
149	56 148	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑛 ≤ 𝑁 )
150		le2sq2	⊢ ( ( ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) ∧ ( 𝑁 ∈ ℝ ∧ 𝑛 ≤ 𝑁 ) ) → ( 𝑛 ↑ 2 ) ≤ ( 𝑁 ↑ 2 ) )
151	145 147 140 149 150	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ≤ ( 𝑁 ↑ 2 ) )
152	135 60 136 136 144 151	le2addd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ≤ ( ( 𝑁 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )
153	131	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑁 ↑ 2 ) ∈ ℂ )
154	153	2timesd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 𝑁 ↑ 2 ) ) = ( ( 𝑁 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )
155	152 154	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ≤ ( 2 · ( 𝑁 ↑ 2 ) ) )
156		2lt4	⊢ 2 < 4
157		2re	⊢ 2 ∈ ℝ
158	157	a1i	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 2 ∈ ℝ )
159		4re	⊢ 4 ∈ ℝ
160	159	a1i	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 4 ∈ ℝ )
161	131	nngt0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 < ( 𝑁 ↑ 2 ) )
162		ltmul1	⊢ ( ( 2 ∈ ℝ ∧ 4 ∈ ℝ ∧ ( ( 𝑁 ↑ 2 ) ∈ ℝ ∧ 0 < ( 𝑁 ↑ 2 ) ) ) → ( 2 < 4 ↔ ( 2 · ( 𝑁 ↑ 2 ) ) < ( 4 · ( 𝑁 ↑ 2 ) ) ) )
163	158 160 136 161 162	syl112anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 < 4 ↔ ( 2 · ( 𝑁 ↑ 2 ) ) < ( 4 · ( 𝑁 ↑ 2 ) ) ) )
164	156 163	mpbii	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 𝑁 ↑ 2 ) ) < ( 4 · ( 𝑁 ↑ 2 ) ) )
165		2cn	⊢ 2 ∈ ℂ
166	121	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑁 ∈ ℂ )
167		sqmul	⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 2 · 𝑁 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) )
168	165 166 167	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 2 · 𝑁 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) )
169		sq2	⊢ ( 2 ↑ 2 ) = 4
170	169	oveq1i	⊢ ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) = ( 4 · ( 𝑁 ↑ 2 ) )
171	168 170	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 2 · 𝑁 ) ↑ 2 ) = ( 4 · ( 𝑁 ↑ 2 ) ) )
172	164 171	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 𝑁 ↑ 2 ) ) < ( ( 2 · 𝑁 ) ↑ 2 ) )
173	119 134 125 155 172	lelttrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) < ( ( 2 · 𝑁 ) ↑ 2 ) )
174	127	nnrpd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · ( 2 · 𝑁 ) ) ∈ ℝ⁺ )
175	125 174	ltaddrpd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 2 · 𝑁 ) ↑ 2 ) < ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) )
176	119 125 129 173 175	lttrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) < ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) )
177	119 129 130 176	ltadd1dd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) < ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
178	3	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 𝑃 = ( ( 2 · 𝑁 ) + 1 ) )
179	178	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 ↑ 2 ) = ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) )
180	95	sqvald	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 ↑ 2 ) = ( 𝑃 · 𝑃 ) )
181	123	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 2 · 𝑁 ) ∈ ℂ )
182		binom21	⊢ ( ( 2 · 𝑁 ) ∈ ℂ → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
183	181 182	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
184	179 180 183	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 · 𝑃 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
185	177 184	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) < ( 𝑃 · 𝑃 ) )
186	101	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℝ )
187	45	nngt0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → 0 < 𝑃 )
188		ltdivmul	⊢ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) ) → ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) < 𝑃 ↔ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) < ( 𝑃 · 𝑃 ) ) )
189	186 51 51 187 188	syl112anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) < 𝑃 ↔ ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) < ( 𝑃 · 𝑃 ) ) )
190	185 189	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) < 𝑃 )
191		1z	⊢ 1 ∈ ℤ
192		elfzm11	⊢ ( ( 1 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ℤ ∧ 1 ≤ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∧ ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) < 𝑃 ) ) )
193	191 68 192	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 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	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
195		gzreim	⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑚 + ( i · 𝑛 ) ) ∈ ℤ[i] )
196	79 57 195	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 + ( i · 𝑛 ) ) ∈ ℤ[i] )
197		gzcn	⊢ ( ( 𝑚 + ( i · 𝑛 ) ) ∈ ℤ[i] → ( 𝑚 + ( i · 𝑛 ) ) ∈ ℂ )
198	196 197	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 + ( i · 𝑛 ) ) ∈ ℂ )
199	198	absvalsq2d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) ) )
200	137 145	crred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ℜ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) = 𝑚 )
201	200	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ℜ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) = ( 𝑚 ↑ 2 ) )
202	137 145	crimd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ℑ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) = 𝑛 )
203	202	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ℑ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) = ( 𝑛 ↑ 2 ) )
204	201 203	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ℜ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) )
205	199 204	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) )
206	205	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + 1 ) = ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) )
207	101	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) ∈ ℂ )
208	207 95 106	divcan1d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) = ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) )
209	206 208	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + 1 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) )
210		oveq1	⊢ ( 𝑘 = ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) → ( 𝑘 · 𝑃 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) )
211	210	eqeq2d	⊢ ( 𝑘 = ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) → ( ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ↔ ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) ) )
212		fveq2	⊢ ( 𝑢 = ( 𝑚 + ( i · 𝑛 ) ) → ( abs ‘ 𝑢 ) = ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) )
213	212	oveq1d	⊢ ( 𝑢 = ( 𝑚 + ( i · 𝑛 ) ) → ( ( abs ‘ 𝑢 ) ↑ 2 ) = ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) )
214	213	oveq1d	⊢ ( 𝑢 = ( 𝑚 + ( i · 𝑛 ) ) → ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + 1 ) )
215	214	eqeq1d	⊢ ( 𝑢 = ( 𝑚 + ( i · 𝑛 ) ) → ( ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) ↔ ( ( ( abs ‘ ( 𝑚 + ( i · 𝑛 ) ) ) ↑ 2 ) + 1 ) = ( ( ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) + 1 ) / 𝑃 ) · 𝑃 ) ) )
216	211 215	rspc2ev	⊢ ( ( ( ( ( ( 𝑚 ↑ 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	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) )
218	217	3expia	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) )
219	42 218	syl5	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ) → ( ( 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) )
220	219	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) ∃ 𝑛 ∈ ( 0 ... 𝑁 ) ( 𝑗 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∧ 𝑗 = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) )
221	41 220	biimtrid	⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝐴 ∩ ran 𝐹 ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) )
222	221	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑗 𝑗 ∈ ( 𝐴 ∩ ran 𝐹 ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) ) )
223	9 222	mpd	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∃ 𝑢 ∈ ℤ[i] ( ( ( abs ‘ 𝑢 ) ↑ 2 ) + 1 ) = ( 𝑘 · 𝑃 ) )

Metamath Proof Explorer

Theorem 4sqlem12

Proof