This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ) ∈ ℕ0 )
47 45 46 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑃 − 1 ) ∈ ℕ0 )
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 ) ∈ ℕ0 )
59 57 58 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑛 ↑ 2 ) ∈ ℕ0 )
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 𝑃 ) ∈ ℕ0 )
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 ) ∈ ℕ0 )
88 79 87 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑃 − 1 ) − ( ( 𝑛 ↑ 2 ) mod 𝑃 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℕ0 )
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 ) ) ∈ ℕ0 )
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 ) ) ∈ ℕ0 → ( ( ( 𝑚 ↑ 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 ) = ( 𝑘 · 𝑃 ) )