| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 4sq.1 | . . . 4
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} | 
| 2 |  | 4sq.2 | . . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 3 |  | 4sq.3 | . . . 4
⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) | 
| 4 |  | 4sq.4 | . . . 4
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 5 |  | 4sqlem11.5 | . . . 4
⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} | 
| 6 |  | 4sqlem11.6 | . . . 4
⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣)) | 
| 7 | 1, 2, 3, 4, 5, 6 | 4sqlem11 16994 | . . 3
⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅) | 
| 8 |  | n0 4352 | . . 3
⊢ ((𝐴 ∩ ran 𝐹) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹)) | 
| 9 | 7, 8 | sylib 218 | . 2
⊢ (𝜑 → ∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹)) | 
| 10 |  | vex 3483 | . . . . . . 7
⊢ 𝑗 ∈ V | 
| 11 |  | eqeq1 2740 | . . . . . . . 8
⊢ (𝑢 = 𝑗 → (𝑢 = ((𝑚↑2) mod 𝑃) ↔ 𝑗 = ((𝑚↑2) mod 𝑃))) | 
| 12 | 11 | rexbidv 3178 | . . . . . . 7
⊢ (𝑢 = 𝑗 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃))) | 
| 13 | 10, 12, 5 | elab2 3681 | . . . . . 6
⊢ (𝑗 ∈ 𝐴 ↔ ∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃)) | 
| 14 |  | abid 2717 | . . . . . . . . 9
⊢ (𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)} ↔ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)) | 
| 15 | 5 | rexeqi 3324 | . . . . . . . . 9
⊢
(∃𝑣 ∈
𝐴 𝑗 = ((𝑃 − 1) − 𝑣) ↔ ∃𝑣 ∈ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}𝑗 = ((𝑃 − 1) − 𝑣)) | 
| 16 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑚↑2) = (𝑛↑2)) | 
| 17 | 16 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → ((𝑚↑2) mod 𝑃) = ((𝑛↑2) mod 𝑃)) | 
| 18 | 17 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑢 = ((𝑚↑2) mod 𝑃) ↔ 𝑢 = ((𝑛↑2) mod 𝑃))) | 
| 19 | 18 | cbvrexvw 3237 | . . . . . . . . . . 11
⊢
(∃𝑚 ∈
(0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑢 = ((𝑛↑2) mod 𝑃)) | 
| 20 |  | eqeq1 2740 | . . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → (𝑢 = ((𝑛↑2) mod 𝑃) ↔ 𝑣 = ((𝑛↑2) mod 𝑃))) | 
| 21 | 20 | rexbidv 3178 | . . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → (∃𝑛 ∈ (0...𝑁)𝑢 = ((𝑛↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃))) | 
| 22 | 19, 21 | bitrid 283 | . . . . . . . . . 10
⊢ (𝑢 = 𝑣 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃))) | 
| 23 | 22 | rexab 3699 | . . . . . . . . 9
⊢
(∃𝑣 ∈
{𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}𝑗 = ((𝑃 − 1) − 𝑣) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) | 
| 24 | 14, 15, 23 | 3bitri 297 | . . . . . . . 8
⊢ (𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)} ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) | 
| 25 | 6 | rnmpt 5967 | . . . . . . . . 9
⊢ ran 𝐹 = {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)} | 
| 26 | 25 | eleq2i 2832 | . . . . . . . 8
⊢ (𝑗 ∈ ran 𝐹 ↔ 𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)}) | 
| 27 |  | rexcom4 3287 | . . . . . . . . 9
⊢
(∃𝑛 ∈
(0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣∃𝑛 ∈ (0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) | 
| 28 |  | r19.41v 3188 | . . . . . . . . . 10
⊢
(∃𝑛 ∈
(0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ (∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) | 
| 29 | 28 | exbii 1847 | . . . . . . . . 9
⊢
(∃𝑣∃𝑛 ∈ (0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) | 
| 30 | 27, 29 | bitri 275 | . . . . . . . 8
⊢
(∃𝑛 ∈
(0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) | 
| 31 | 24, 26, 30 | 3bitr4i 303 | . . . . . . 7
⊢ (𝑗 ∈ ran 𝐹 ↔ ∃𝑛 ∈ (0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) | 
| 32 |  | ovex 7465 | . . . . . . . . 9
⊢ ((𝑛↑2) mod 𝑃) ∈ V | 
| 33 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑣 = ((𝑛↑2) mod 𝑃) → ((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) | 
| 34 | 33 | eqeq2d 2747 | . . . . . . . . 9
⊢ (𝑣 = ((𝑛↑2) mod 𝑃) → (𝑗 = ((𝑃 − 1) − 𝑣) ↔ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))) | 
| 35 | 32, 34 | ceqsexv 3531 | . . . . . . . 8
⊢
(∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) | 
| 36 | 35 | rexbii 3093 | . . . . . . 7
⊢
(∃𝑛 ∈
(0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) | 
| 37 | 31, 36 | bitri 275 | . . . . . 6
⊢ (𝑗 ∈ ran 𝐹 ↔ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) | 
| 38 | 13, 37 | anbi12i 628 | . . . . 5
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑗 ∈ ran 𝐹) ↔ (∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃) ∧ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))) | 
| 39 |  | elin 3966 | . . . . 5
⊢ (𝑗 ∈ (𝐴 ∩ ran 𝐹) ↔ (𝑗 ∈ 𝐴 ∧ 𝑗 ∈ ran 𝐹)) | 
| 40 |  | reeanv 3228 | . . . . 5
⊢
(∃𝑚 ∈
(0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) ↔ (∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃) ∧ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))) | 
| 41 | 38, 39, 40 | 3bitr4i 303 | . . . 4
⊢ (𝑗 ∈ (𝐴 ∩ ran 𝐹) ↔ ∃𝑚 ∈ (0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))) | 
| 42 |  | eqtr2 2760 | . . . . . 6
⊢ ((𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) | 
| 43 | 4 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℙ) | 
| 44 |  | prmnn 16712 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 45 | 43, 44 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℕ) | 
| 46 |  | nnm1nn0 12569 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) | 
| 47 | 45, 46 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈
ℕ0) | 
| 48 | 47 | nn0red 12590 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℝ) | 
| 49 | 45 | nnrpd 13076 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈
ℝ+) | 
| 50 | 47 | nn0ge0d 12592 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ (𝑃 − 1)) | 
| 51 | 45 | nnred 12282 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℝ) | 
| 52 | 51 | ltm1d 12201 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) < 𝑃) | 
| 53 |  | modid 13937 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑃 − 1) ∈ ℝ ∧
𝑃 ∈
ℝ+) ∧ (0 ≤ (𝑃 − 1) ∧ (𝑃 − 1) < 𝑃)) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1)) | 
| 54 | 48, 49, 50, 52, 53 | syl22anc 838 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1)) | 
| 55 | 54 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃)) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) | 
| 56 |  | simp2r 1200 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ (0...𝑁)) | 
| 57 | 56 | elfzelzd 13566 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ ℤ) | 
| 58 |  | zsqcl2 14179 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℤ → (𝑛↑2) ∈
ℕ0) | 
| 59 | 57, 58 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈
ℕ0) | 
| 60 | 59 | nn0red 12590 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℝ) | 
| 61 |  | modlt 13921 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑛↑2) ∈ ℝ ∧
𝑃 ∈
ℝ+) → ((𝑛↑2) mod 𝑃) < 𝑃) | 
| 62 | 60, 49, 61 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) < 𝑃) | 
| 63 |  | zsqcl 14170 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℤ → (𝑛↑2) ∈
ℤ) | 
| 64 | 57, 63 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℤ) | 
| 65 | 64, 45 | zmodcld 13933 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ∈
ℕ0) | 
| 66 | 65 | nn0zd 12641 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ∈ ℤ) | 
| 67 |  | prmz 16713 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) | 
| 68 | 43, 67 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℤ) | 
| 69 |  | zltlem1 12672 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛↑2) mod 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ) → (((𝑛↑2) mod 𝑃) < 𝑃 ↔ ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1))) | 
| 70 | 66, 68, 69 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑛↑2) mod 𝑃) < 𝑃 ↔ ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1))) | 
| 71 | 62, 70 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1)) | 
| 72 | 71, 54 | breqtrrd 5170 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃)) | 
| 73 |  | modsubdir 13982 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 − 1) ∈ ℝ ∧
(𝑛↑2) ∈ ℝ
∧ 𝑃 ∈
ℝ+) → (((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃) ↔ (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃)))) | 
| 74 | 48, 60, 49, 73 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃) ↔ (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃)))) | 
| 75 | 72, 74 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃))) | 
| 76 |  | simp3 1138 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) | 
| 77 | 55, 75, 76 | 3eqtr4rd 2787 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃)) | 
| 78 |  | simp2l 1199 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ (0...𝑁)) | 
| 79 | 78 | elfzelzd 13566 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ ℤ) | 
| 80 |  | zsqcl 14170 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℤ → (𝑚↑2) ∈
ℤ) | 
| 81 | 79, 80 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℤ) | 
| 82 | 47 | nn0zd 12641 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℤ) | 
| 83 | 82, 64 | zsubcld 12729 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑃 − 1) − (𝑛↑2)) ∈ ℤ) | 
| 84 |  | moddvds 16302 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℕ ∧ (𝑚↑2) ∈ ℤ ∧
((𝑃 − 1) −
(𝑛↑2)) ∈ ℤ)
→ (((𝑚↑2) mod
𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))))) | 
| 85 | 45, 81, 83, 84 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) mod 𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))))) | 
| 86 | 77, 85 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2)))) | 
| 87 |  | zsqcl2 14179 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℤ → (𝑚↑2) ∈
ℕ0) | 
| 88 | 79, 87 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈
ℕ0) | 
| 89 | 88 | nn0cnd 12591 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℂ) | 
| 90 | 47 | nn0cnd 12591 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℂ) | 
| 91 | 59 | nn0cnd 12591 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℂ) | 
| 92 | 89, 90, 91 | subsub3d 11651 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))) = (((𝑚↑2) + (𝑛↑2)) − (𝑃 − 1))) | 
| 93 | 88, 59 | nn0addcld 12593 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈
ℕ0) | 
| 94 | 93 | nn0cnd 12591 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈ ℂ) | 
| 95 | 45 | nncnd 12283 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℂ) | 
| 96 |  | 1cnd 11257 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ∈
ℂ) | 
| 97 | 94, 95, 96 | subsub3d 11651 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) − (𝑃 − 1)) = ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃)) | 
| 98 | 92, 97 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))) = ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃)) | 
| 99 | 86, 98 | breqtrd 5168 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃)) | 
| 100 |  | nn0p1nn 12567 | . . . . . . . . . . . . . 14
⊢ (((𝑚↑2) + (𝑛↑2)) ∈ ℕ0 →
(((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℕ) | 
| 101 | 93, 100 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℕ) | 
| 102 | 101 | nnzd 12642 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℤ) | 
| 103 |  | dvdssubr 16343 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℤ ∧ (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℤ) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃))) | 
| 104 | 68, 102, 103 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃))) | 
| 105 | 99, 104 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1)) | 
| 106 | 45 | nnne0d 12317 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ≠ 0) | 
| 107 |  | dvdsval2 16294 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℤ) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ)) | 
| 108 | 68, 106, 102, 107 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ)) | 
| 109 | 105, 108 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ) | 
| 110 |  | nnrp 13047 | . . . . . . . . . . . . . 14
⊢ ((((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℕ → (((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℝ+) | 
| 111 |  | nnrp 13047 | . . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ+) | 
| 112 |  | rpdivcl 13061 | . . . . . . . . . . . . . 14
⊢
(((((𝑚↑2) +
(𝑛↑2)) + 1) ∈
ℝ+ ∧ 𝑃
∈ ℝ+) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈
ℝ+) | 
| 113 | 110, 111,
112 | syl2an 596 | . . . . . . . . . . . . 13
⊢
(((((𝑚↑2) +
(𝑛↑2)) + 1) ∈
ℕ ∧ 𝑃 ∈
ℕ) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈
ℝ+) | 
| 114 | 101, 45, 113 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈
ℝ+) | 
| 115 | 114 | rpgt0d 13081 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃)) | 
| 116 |  | elnnz 12625 | . . . . . . . . . . 11
⊢
(((((𝑚↑2) +
(𝑛↑2)) + 1) / 𝑃) ∈ ℕ ↔
(((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 0 <
((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃))) | 
| 117 | 109, 115,
116 | sylanbrc 583 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℕ) | 
| 118 | 117 | nnge1d 12315 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃)) | 
| 119 | 93 | nn0red 12590 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈ ℝ) | 
| 120 |  | 2nn 12340 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ | 
| 121 | 2 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℕ) | 
| 122 |  | nnmulcl 12291 | . . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) | 
| 123 | 120, 121,
122 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℕ) | 
| 124 | 123 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℝ) | 
| 125 | 124 | resqcld 14166 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) ∈ ℝ) | 
| 126 |  | nnmulcl 12291 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ (2 · 𝑁) ∈ ℕ) → (2 · (2
· 𝑁)) ∈
ℕ) | 
| 127 | 120, 123,
126 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈
ℕ) | 
| 128 | 127 | nnred 12282 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈
ℝ) | 
| 129 | 125, 128 | readdcld 11291 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) ∈
ℝ) | 
| 130 |  | 1red 11263 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ∈
ℝ) | 
| 131 | 121 | nnsqcld 14284 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℕ) | 
| 132 |  | nnmulcl 12291 | . . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ (𝑁↑2) ∈ ℕ) → (2 ·
(𝑁↑2)) ∈
ℕ) | 
| 133 | 120, 131,
132 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) ∈ ℕ) | 
| 134 | 133 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) ∈ ℝ) | 
| 135 | 88 | nn0red 12590 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℝ) | 
| 136 | 131 | nnred 12282 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℝ) | 
| 137 | 79 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ ℝ) | 
| 138 |  | elfzle1 13568 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ (0...𝑁) → 0 ≤ 𝑚) | 
| 139 | 78, 138 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ 𝑚) | 
| 140 | 121 | nnred 12282 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℝ) | 
| 141 |  | elfzle2 13569 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ≤ 𝑁) | 
| 142 | 78, 141 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ≤ 𝑁) | 
| 143 |  | le2sq2 14176 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) ∧ (𝑁 ∈ ℝ ∧ 𝑚 ≤ 𝑁)) → (𝑚↑2) ≤ (𝑁↑2)) | 
| 144 | 137, 139,
140, 142, 143 | syl22anc 838 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ≤ (𝑁↑2)) | 
| 145 | 57 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ ℝ) | 
| 146 |  | elfzle1 13568 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (0...𝑁) → 0 ≤ 𝑛) | 
| 147 | 56, 146 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ 𝑛) | 
| 148 |  | elfzle2 13569 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (0...𝑁) → 𝑛 ≤ 𝑁) | 
| 149 | 56, 148 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ≤ 𝑁) | 
| 150 |  | le2sq2 14176 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) ∧ (𝑁 ∈ ℝ ∧ 𝑛 ≤ 𝑁)) → (𝑛↑2) ≤ (𝑁↑2)) | 
| 151 | 145, 147,
140, 149, 150 | syl22anc 838 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ≤ (𝑁↑2)) | 
| 152 | 135, 60, 136, 136, 144, 151 | le2addd 11883 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ≤ ((𝑁↑2) + (𝑁↑2))) | 
| 153 | 131 | nncnd 12283 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℂ) | 
| 154 | 153 | 2timesd 12511 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) = ((𝑁↑2) + (𝑁↑2))) | 
| 155 | 152, 154 | breqtrrd 5170 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ≤ (2 · (𝑁↑2))) | 
| 156 |  | 2lt4 12442 | . . . . . . . . . . . . . . . 16
⊢ 2 <
4 | 
| 157 |  | 2re 12341 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ | 
| 158 | 157 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 2 ∈
ℝ) | 
| 159 |  | 4re 12351 | . . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℝ | 
| 160 | 159 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 4 ∈
ℝ) | 
| 161 | 131 | nngt0d 12316 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < (𝑁↑2)) | 
| 162 |  | ltmul1 12118 | . . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℝ ∧ 4 ∈ ℝ ∧ ((𝑁↑2) ∈ ℝ ∧ 0 < (𝑁↑2))) → (2 < 4
↔ (2 · (𝑁↑2)) < (4 · (𝑁↑2)))) | 
| 163 | 158, 160,
136, 161, 162 | syl112anc 1375 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 < 4 ↔ (2 ·
(𝑁↑2)) < (4
· (𝑁↑2)))) | 
| 164 | 156, 163 | mpbii 233 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) < (4 · (𝑁↑2))) | 
| 165 |  | 2cn 12342 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ | 
| 166 | 121 | nncnd 12283 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℂ) | 
| 167 |  | sqmul 14160 | . . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ 𝑁
∈ ℂ) → ((2 · 𝑁)↑2) = ((2↑2) · (𝑁↑2))) | 
| 168 | 165, 166,
167 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) = ((2↑2) · (𝑁↑2))) | 
| 169 |  | sq2 14237 | . . . . . . . . . . . . . . . . 17
⊢
(2↑2) = 4 | 
| 170 | 169 | oveq1i 7442 | . . . . . . . . . . . . . . . 16
⊢
((2↑2) · (𝑁↑2)) = (4 · (𝑁↑2)) | 
| 171 | 168, 170 | eqtrdi 2792 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) = (4 · (𝑁↑2))) | 
| 172 | 164, 171 | breqtrrd 5170 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) < ((2 · 𝑁)↑2)) | 
| 173 | 119, 134,
125, 155, 172 | lelttrd 11420 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) < ((2 · 𝑁)↑2)) | 
| 174 | 127 | nnrpd 13076 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈
ℝ+) | 
| 175 | 125, 174 | ltaddrpd 13111 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) < (((2 · 𝑁)↑2) + (2 · (2
· 𝑁)))) | 
| 176 | 119, 125,
129, 173, 175 | lttrd 11423 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) < (((2 · 𝑁)↑2) + (2 · (2
· 𝑁)))) | 
| 177 | 119, 129,
130, 176 | ltadd1dd 11875 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) < ((((2 · 𝑁)↑2) + (2 · (2
· 𝑁))) +
1)) | 
| 178 | 3 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 = ((2 · 𝑁) + 1)) | 
| 179 | 178 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃↑2) = (((2 · 𝑁) + 1)↑2)) | 
| 180 | 95 | sqvald 14184 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃↑2) = (𝑃 · 𝑃)) | 
| 181 | 123 | nncnd 12283 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℂ) | 
| 182 |  | binom21 14259 | . . . . . . . . . . . . 13
⊢ ((2
· 𝑁) ∈ ℂ
→ (((2 · 𝑁) +
1)↑2) = ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1)) | 
| 183 | 181, 182 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((2 · 𝑁) + 1)↑2) = ((((2 · 𝑁)↑2) + (2 · (2
· 𝑁))) +
1)) | 
| 184 | 179, 180,
183 | 3eqtr3d 2784 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 · 𝑃) = ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1)) | 
| 185 | 177, 184 | breqtrrd 5170 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃)) | 
| 186 | 101 | nnred 12282 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℝ) | 
| 187 | 45 | nngt0d 12316 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < 𝑃) | 
| 188 |  | ltdivmul 12144 | . . . . . . . . . . 11
⊢
(((((𝑚↑2) +
(𝑛↑2)) + 1) ∈
ℝ ∧ 𝑃 ∈
ℝ ∧ (𝑃 ∈
ℝ ∧ 0 < 𝑃))
→ (((((𝑚↑2) +
(𝑛↑2)) + 1) / 𝑃) < 𝑃 ↔ (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃))) | 
| 189 | 186, 51, 51, 187, 188 | syl112anc 1375 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃 ↔ (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃))) | 
| 190 | 185, 189 | mpbird 257 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃) | 
| 191 |  | 1z 12649 | . . . . . . . . . 10
⊢ 1 ∈
ℤ | 
| 192 |  | elfzm11 13636 | . . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ 𝑃
∈ ℤ) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ↔ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∧ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃))) | 
| 193 | 191, 68, 192 | sylancr 587 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ↔ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∧ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃))) | 
| 194 | 109, 118,
190, 193 | mpbir3and 1342 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1))) | 
| 195 |  | gzreim 16978 | . . . . . . . . 9
⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑚 + (i · 𝑛)) ∈
ℤ[i]) | 
| 196 | 79, 57, 195 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚 + (i · 𝑛)) ∈ ℤ[i]) | 
| 197 |  | gzcn 16971 | . . . . . . . . . . . . 13
⊢ ((𝑚 + (i · 𝑛)) ∈ ℤ[i] →
(𝑚 + (i · 𝑛)) ∈
ℂ) | 
| 198 | 196, 197 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚 + (i · 𝑛)) ∈ ℂ) | 
| 199 | 198 | absvalsq2d 15483 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((abs‘(𝑚 + (i · 𝑛)))↑2) = (((ℜ‘(𝑚 + (i · 𝑛)))↑2) +
((ℑ‘(𝑚 + (i
· 𝑛)))↑2))) | 
| 200 | 137, 145 | crred 15271 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (ℜ‘(𝑚 + (i · 𝑛))) = 𝑚) | 
| 201 | 200 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((ℜ‘(𝑚 + (i · 𝑛)))↑2) = (𝑚↑2)) | 
| 202 | 137, 145 | crimd 15272 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (ℑ‘(𝑚 + (i · 𝑛))) = 𝑛) | 
| 203 | 202 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((ℑ‘(𝑚 + (i · 𝑛)))↑2) = (𝑛↑2)) | 
| 204 | 201, 203 | oveq12d 7450 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((ℜ‘(𝑚 + (i · 𝑛)))↑2) +
((ℑ‘(𝑚 + (i
· 𝑛)))↑2)) =
((𝑚↑2) + (𝑛↑2))) | 
| 205 | 199, 204 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((abs‘(𝑚 + (i · 𝑛)))↑2) = ((𝑚↑2) + (𝑛↑2))) | 
| 206 | 205 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((𝑚↑2) + (𝑛↑2)) + 1)) | 
| 207 | 101 | nncnd 12283 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℂ) | 
| 208 | 207, 95, 106 | divcan1d 12045 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃) = (((𝑚↑2) + (𝑛↑2)) + 1)) | 
| 209 | 206, 208 | eqtr4d 2779 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)) | 
| 210 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑘 = ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) → (𝑘 · 𝑃) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)) | 
| 211 | 210 | eqeq2d 2747 | . . . . . . . . 9
⊢ (𝑘 = ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) → ((((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃) ↔ (((abs‘𝑢)↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃))) | 
| 212 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑢 = (𝑚 + (i · 𝑛)) → (abs‘𝑢) = (abs‘(𝑚 + (i · 𝑛)))) | 
| 213 | 212 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑢 = (𝑚 + (i · 𝑛)) → ((abs‘𝑢)↑2) = ((abs‘(𝑚 + (i · 𝑛)))↑2)) | 
| 214 | 213 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑢 = (𝑚 + (i · 𝑛)) → (((abs‘𝑢)↑2) + 1) = (((abs‘(𝑚 + (i · 𝑛)))↑2) +
1)) | 
| 215 | 214 | eqeq1d 2738 | . . . . . . . . 9
⊢ (𝑢 = (𝑚 + (i · 𝑛)) → ((((abs‘𝑢)↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃) ↔ (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃))) | 
| 216 | 211, 215 | rspc2ev 3634 | . . . . . . . 8
⊢
((((((𝑚↑2) +
(𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ∧ (𝑚 + (i · 𝑛)) ∈ ℤ[i] ∧
(((abs‘(𝑚 + (i
· 𝑛)))↑2) + 1)
= (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) | 
| 217 | 194, 196,
209, 216 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) | 
| 218 | 217 | 3expia 1121 | . . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))) | 
| 219 | 42, 218 | syl5 34 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁))) → ((𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))) | 
| 220 | 219 | rexlimdvva 3212 | . . . 4
⊢ (𝜑 → (∃𝑚 ∈ (0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))) | 
| 221 | 41, 220 | biimtrid 242 | . . 3
⊢ (𝜑 → (𝑗 ∈ (𝐴 ∩ ran 𝐹) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))) | 
| 222 | 221 | exlimdv 1932 | . 2
⊢ (𝜑 → (∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))) | 
| 223 | 9, 222 | mpd 15 | 1
⊢ (𝜑 → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) |