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 16125 |
. . 3
⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅) |
8 | | n0 4234 |
. . 3
⊢ ((𝐴 ∩ ran 𝐹) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹)) |
9 | 7, 8 | sylib 219 |
. 2
⊢ (𝜑 → ∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹)) |
10 | | vex 3440 |
. . . . . . 7
⊢ 𝑗 ∈ V |
11 | | eqeq1 2799 |
. . . . . . . 8
⊢ (𝑢 = 𝑗 → (𝑢 = ((𝑚↑2) mod 𝑃) ↔ 𝑗 = ((𝑚↑2) mod 𝑃))) |
12 | 11 | rexbidv 3260 |
. . . . . . 7
⊢ (𝑢 = 𝑗 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃))) |
13 | 10, 12, 5 | elab2 3609 |
. . . . . 6
⊢ (𝑗 ∈ 𝐴 ↔ ∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃)) |
14 | | abid 2779 |
. . . . . . . . 9
⊢ (𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)} ↔ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)) |
15 | 5 | rexeqi 3374 |
. . . . . . . . 9
⊢
(∃𝑣 ∈
𝐴 𝑗 = ((𝑃 − 1) − 𝑣) ↔ ∃𝑣 ∈ {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}𝑗 = ((𝑃 − 1) − 𝑣)) |
16 | | oveq1 7028 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑚↑2) = (𝑛↑2)) |
17 | 16 | oveq1d 7036 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → ((𝑚↑2) mod 𝑃) = ((𝑛↑2) mod 𝑃)) |
18 | 17 | eqeq2d 2805 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑢 = ((𝑚↑2) mod 𝑃) ↔ 𝑢 = ((𝑛↑2) mod 𝑃))) |
19 | 18 | cbvrexv 3404 |
. . . . . . . . . . 11
⊢
(∃𝑚 ∈
(0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑢 = ((𝑛↑2) mod 𝑃)) |
20 | | eqeq1 2799 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → (𝑢 = ((𝑛↑2) mod 𝑃) ↔ 𝑣 = ((𝑛↑2) mod 𝑃))) |
21 | 20 | rexbidv 3260 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → (∃𝑛 ∈ (0...𝑁)𝑢 = ((𝑛↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃))) |
22 | 19, 21 | syl5bb 284 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑣 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) ↔ ∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃))) |
23 | 22 | rexab 3625 |
. . . . . . . . 9
⊢
(∃𝑣 ∈
{𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}𝑗 = ((𝑃 − 1) − 𝑣) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) |
24 | 14, 15, 23 | 3bitri 298 |
. . . . . . . 8
⊢ (𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)} ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) |
25 | 6 | rnmpt 5714 |
. . . . . . . . 9
⊢ ran 𝐹 = {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)} |
26 | 25 | eleq2i 2874 |
. . . . . . . 8
⊢ (𝑗 ∈ ran 𝐹 ↔ 𝑗 ∈ {𝑗 ∣ ∃𝑣 ∈ 𝐴 𝑗 = ((𝑃 − 1) − 𝑣)}) |
27 | | rexcom4 3213 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
(0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣∃𝑛 ∈ (0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) |
28 | | r19.41v 3308 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
(0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ (∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) |
29 | 28 | exbii 1829 |
. . . . . . . . 9
⊢
(∃𝑣∃𝑛 ∈ (0...𝑁)(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) |
30 | 27, 29 | bitri 276 |
. . . . . . . 8
⊢
(∃𝑛 ∈
(0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑣(∃𝑛 ∈ (0...𝑁)𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) |
31 | 24, 26, 30 | 3bitr4i 304 |
. . . . . . 7
⊢ (𝑗 ∈ ran 𝐹 ↔ ∃𝑛 ∈ (0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣))) |
32 | | ovex 7053 |
. . . . . . . . 9
⊢ ((𝑛↑2) mod 𝑃) ∈ V |
33 | | oveq2 7029 |
. . . . . . . . . 10
⊢ (𝑣 = ((𝑛↑2) mod 𝑃) → ((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) |
34 | 33 | eqeq2d 2805 |
. . . . . . . . 9
⊢ (𝑣 = ((𝑛↑2) mod 𝑃) → (𝑗 = ((𝑃 − 1) − 𝑣) ↔ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))) |
35 | 32, 34 | ceqsexv 3484 |
. . . . . . . 8
⊢
(∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) |
36 | 35 | rexbii 3211 |
. . . . . . 7
⊢
(∃𝑛 ∈
(0...𝑁)∃𝑣(𝑣 = ((𝑛↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − 𝑣)) ↔ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) |
37 | 31, 36 | bitri 276 |
. . . . . 6
⊢ (𝑗 ∈ ran 𝐹 ↔ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) |
38 | 13, 37 | anbi12i 626 |
. . . . 5
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑗 ∈ ran 𝐹) ↔ (∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃) ∧ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))) |
39 | | elin 4094 |
. . . . 5
⊢ (𝑗 ∈ (𝐴 ∩ ran 𝐹) ↔ (𝑗 ∈ 𝐴 ∧ 𝑗 ∈ ran 𝐹)) |
40 | | reeanv 3328 |
. . . . 5
⊢
(∃𝑚 ∈
(0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) ↔ (∃𝑚 ∈ (0...𝑁)𝑗 = ((𝑚↑2) mod 𝑃) ∧ ∃𝑛 ∈ (0...𝑁)𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))) |
41 | 38, 39, 40 | 3bitr4i 304 |
. . . 4
⊢ (𝑗 ∈ (𝐴 ∩ ran 𝐹) ↔ ∃𝑚 ∈ (0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)))) |
42 | | eqtr2 2817 |
. . . . . 6
⊢ ((𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) |
43 | 4 | 3ad2ant1 1126 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℙ) |
44 | | prmnn 15852 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℕ) |
46 | | nnm1nn0 11791 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈
ℕ0) |
48 | 47 | nn0red 11809 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℝ) |
49 | 45 | nnrpd 12284 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈
ℝ+) |
50 | 47 | nn0ge0d 11811 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ (𝑃 − 1)) |
51 | 45 | nnred 11506 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℝ) |
52 | 51 | ltm1d 11425 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) < 𝑃) |
53 | | modid 13119 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑃 − 1) ∈ ℝ ∧
𝑃 ∈
ℝ+) ∧ (0 ≤ (𝑃 − 1) ∧ (𝑃 − 1) < 𝑃)) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1)) |
54 | 48, 49, 50, 52, 53 | syl22anc 835 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑃 − 1) mod 𝑃) = (𝑃 − 1)) |
55 | 54 | oveq1d 7036 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃)) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) |
56 | | simp2r 1193 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ (0...𝑁)) |
57 | | elfzelz 12763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (0...𝑁) → 𝑛 ∈ ℤ) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ ℤ) |
59 | | zsqcl2 13357 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℤ → (𝑛↑2) ∈
ℕ0) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈
ℕ0) |
61 | 60 | nn0red 11809 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℝ) |
62 | | modlt 13103 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛↑2) ∈ ℝ ∧
𝑃 ∈
ℝ+) → ((𝑛↑2) mod 𝑃) < 𝑃) |
63 | 61, 49, 62 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) < 𝑃) |
64 | | zsqcl 13349 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℤ → (𝑛↑2) ∈
ℤ) |
65 | 58, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℤ) |
66 | 65, 45 | zmodcld 13115 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ∈
ℕ0) |
67 | 66 | nn0zd 11939 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ∈ ℤ) |
68 | | prmz 15853 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
69 | 43, 68 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℤ) |
70 | | zltlem1 11889 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛↑2) mod 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ) → (((𝑛↑2) mod 𝑃) < 𝑃 ↔ ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1))) |
71 | 67, 69, 70 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑛↑2) mod 𝑃) < 𝑃 ↔ ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1))) |
72 | 63, 71 | mpbid 233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ≤ (𝑃 − 1)) |
73 | 72, 54 | breqtrrd 4994 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃)) |
74 | | modsubdir 13163 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 − 1) ∈ ℝ ∧
(𝑛↑2) ∈ ℝ
∧ 𝑃 ∈
ℝ+) → (((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃) ↔ (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃)))) |
75 | 48, 61, 49, 74 | syl3anc 1364 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑛↑2) mod 𝑃) ≤ ((𝑃 − 1) mod 𝑃) ↔ (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃)))) |
76 | 73, 75 | mpbid 233 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) = (((𝑃 − 1) mod 𝑃) − ((𝑛↑2) mod 𝑃))) |
77 | | simp3 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) |
78 | 55, 76, 77 | 3eqtr4rd 2842 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) mod 𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃)) |
79 | | simp2l 1192 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ (0...𝑁)) |
80 | | elfzelz 12763 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ ℤ) |
82 | | zsqcl 13349 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℤ → (𝑚↑2) ∈
ℤ) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℤ) |
84 | 47 | nn0zd 11939 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℤ) |
85 | 84, 65 | zsubcld 11946 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑃 − 1) − (𝑛↑2)) ∈ ℤ) |
86 | | moddvds 15456 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℕ ∧ (𝑚↑2) ∈ ℤ ∧
((𝑃 − 1) −
(𝑛↑2)) ∈ ℤ)
→ (((𝑚↑2) mod
𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))))) |
87 | 45, 83, 85, 86 | syl3anc 1364 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) mod 𝑃) = (((𝑃 − 1) − (𝑛↑2)) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))))) |
88 | 78, 87 | mpbid 233 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2)))) |
89 | | zsqcl2 13357 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℤ → (𝑚↑2) ∈
ℕ0) |
90 | 81, 89 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈
ℕ0) |
91 | 90 | nn0cnd 11810 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℂ) |
92 | 47 | nn0cnd 11810 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 − 1) ∈ ℂ) |
93 | 60 | nn0cnd 11810 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ∈ ℂ) |
94 | 91, 92, 93 | subsub3d 10880 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))) = (((𝑚↑2) + (𝑛↑2)) − (𝑃 − 1))) |
95 | 90, 60 | nn0addcld 11812 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈
ℕ0) |
96 | 95 | nn0cnd 11810 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈ ℂ) |
97 | 45 | nncnd 11507 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∈ ℂ) |
98 | | 1cnd 10487 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ∈
ℂ) |
99 | 96, 97, 98 | subsub3d 10880 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) − (𝑃 − 1)) = ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃)) |
100 | 94, 99 | eqtrd 2831 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) − ((𝑃 − 1) − (𝑛↑2))) = ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃)) |
101 | 88, 100 | breqtrd 4992 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃)) |
102 | | nn0p1nn 11789 |
. . . . . . . . . . . . . 14
⊢ (((𝑚↑2) + (𝑛↑2)) ∈ ℕ0 →
(((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℕ) |
103 | 95, 102 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℕ) |
104 | 103 | nnzd 11940 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℤ) |
105 | | dvdssubr 15493 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℤ ∧ (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℤ) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃))) |
106 | 69, 104, 105 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ 𝑃 ∥ ((((𝑚↑2) + (𝑛↑2)) + 1) − 𝑃))) |
107 | 101, 106 | mpbird 258 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1)) |
108 | 45 | nnne0d 11540 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 ≠ 0) |
109 | | dvdsval2 15448 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ (((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℤ) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ)) |
110 | 69, 108, 104, 109 | syl3anc 1364 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 ∥ (((𝑚↑2) + (𝑛↑2)) + 1) ↔ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ)) |
111 | 107, 110 | mpbid 233 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ) |
112 | | nnrp 12255 |
. . . . . . . . . . . . . 14
⊢ ((((𝑚↑2) + (𝑛↑2)) + 1) ∈ ℕ → (((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℝ+) |
113 | | nnrp 12255 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ+) |
114 | | rpdivcl 12269 |
. . . . . . . . . . . . . 14
⊢
(((((𝑚↑2) +
(𝑛↑2)) + 1) ∈
ℝ+ ∧ 𝑃
∈ ℝ+) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈
ℝ+) |
115 | 112, 113,
114 | syl2an 595 |
. . . . . . . . . . . . 13
⊢
(((((𝑚↑2) +
(𝑛↑2)) + 1) ∈
ℕ ∧ 𝑃 ∈
ℕ) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈
ℝ+) |
116 | 103, 45, 115 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈
ℝ+) |
117 | 116 | rpgt0d 12289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃)) |
118 | | elnnz 11844 |
. . . . . . . . . . 11
⊢
(((((𝑚↑2) +
(𝑛↑2)) + 1) / 𝑃) ∈ ℕ ↔
(((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 0 <
((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃))) |
119 | 111, 117,
118 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℕ) |
120 | 119 | nnge1d 11538 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃)) |
121 | 95 | nn0red 11809 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ∈ ℝ) |
122 | | 2nn 11563 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
123 | 2 | 3ad2ant1 1126 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℕ) |
124 | | nnmulcl 11514 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
125 | 122, 123,
124 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℕ) |
126 | 125 | nnred 11506 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℝ) |
127 | 126 | resqcld 13466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) ∈ ℝ) |
128 | | nnmulcl 11514 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ (2 · 𝑁) ∈ ℕ) → (2 · (2
· 𝑁)) ∈
ℕ) |
129 | 122, 125,
128 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈
ℕ) |
130 | 129 | nnred 11506 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈
ℝ) |
131 | 127, 130 | readdcld 10521 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) ∈
ℝ) |
132 | | 1red 10493 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 1 ∈
ℝ) |
133 | 123 | nnsqcld 13460 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℕ) |
134 | | nnmulcl 11514 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ (𝑁↑2) ∈ ℕ) → (2 ·
(𝑁↑2)) ∈
ℕ) |
135 | 122, 133,
134 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) ∈ ℕ) |
136 | 135 | nnred 11506 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) ∈ ℝ) |
137 | 90 | nn0red 11809 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ∈ ℝ) |
138 | 133 | nnred 11506 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℝ) |
139 | 81 | zred 11941 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ∈ ℝ) |
140 | | elfzle1 12765 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ (0...𝑁) → 0 ≤ 𝑚) |
141 | 79, 140 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ 𝑚) |
142 | 123 | nnred 11506 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℝ) |
143 | | elfzle2 12766 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ≤ 𝑁) |
144 | 79, 143 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑚 ≤ 𝑁) |
145 | | le2sq2 13355 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) ∧ (𝑁 ∈ ℝ ∧ 𝑚 ≤ 𝑁)) → (𝑚↑2) ≤ (𝑁↑2)) |
146 | 139, 141,
142, 144, 145 | syl22anc 835 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚↑2) ≤ (𝑁↑2)) |
147 | 58 | zred 11941 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ∈ ℝ) |
148 | | elfzle1 12765 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (0...𝑁) → 0 ≤ 𝑛) |
149 | 56, 148 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 ≤ 𝑛) |
150 | | elfzle2 12766 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (0...𝑁) → 𝑛 ≤ 𝑁) |
151 | 56, 150 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑛 ≤ 𝑁) |
152 | | le2sq2 13355 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) ∧ (𝑁 ∈ ℝ ∧ 𝑛 ≤ 𝑁)) → (𝑛↑2) ≤ (𝑁↑2)) |
153 | 147, 149,
142, 151, 152 | syl22anc 835 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑛↑2) ≤ (𝑁↑2)) |
154 | 137, 61, 138, 138, 146, 153 | le2addd 11112 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ≤ ((𝑁↑2) + (𝑁↑2))) |
155 | 133 | nncnd 11507 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑁↑2) ∈ ℂ) |
156 | 155 | 2timesd 11733 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) = ((𝑁↑2) + (𝑁↑2))) |
157 | 154, 156 | breqtrrd 4994 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) ≤ (2 · (𝑁↑2))) |
158 | | 2lt4 11665 |
. . . . . . . . . . . . . . . 16
⊢ 2 <
4 |
159 | | 2re 11564 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 2 ∈
ℝ) |
161 | | 4re 11574 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℝ |
162 | 161 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 4 ∈
ℝ) |
163 | 133 | nngt0d 11539 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < (𝑁↑2)) |
164 | | ltmul1 11343 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℝ ∧ 4 ∈ ℝ ∧ ((𝑁↑2) ∈ ℝ ∧ 0 < (𝑁↑2))) → (2 < 4
↔ (2 · (𝑁↑2)) < (4 · (𝑁↑2)))) |
165 | 160, 162,
138, 163, 164 | syl112anc 1367 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 < 4 ↔ (2 ·
(𝑁↑2)) < (4
· (𝑁↑2)))) |
166 | 158, 165 | mpbii 234 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) < (4 · (𝑁↑2))) |
167 | | 2cn 11565 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
168 | 123 | nncnd 11507 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑁 ∈ ℂ) |
169 | | sqmul 13340 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ 𝑁
∈ ℂ) → ((2 · 𝑁)↑2) = ((2↑2) · (𝑁↑2))) |
170 | 167, 168,
169 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) = ((2↑2) · (𝑁↑2))) |
171 | | sq2 13415 |
. . . . . . . . . . . . . . . . 17
⊢
(2↑2) = 4 |
172 | 171 | oveq1i 7031 |
. . . . . . . . . . . . . . . 16
⊢
((2↑2) · (𝑁↑2)) = (4 · (𝑁↑2)) |
173 | 170, 172 | syl6eq 2847 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) = (4 · (𝑁↑2))) |
174 | 166, 173 | breqtrrd 4994 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (𝑁↑2)) < ((2 · 𝑁)↑2)) |
175 | 121, 136,
127, 157, 174 | lelttrd 10650 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) < ((2 · 𝑁)↑2)) |
176 | 129 | nnrpd 12284 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · (2 · 𝑁)) ∈
ℝ+) |
177 | 127, 176 | ltaddrpd 12319 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((2 · 𝑁)↑2) < (((2 · 𝑁)↑2) + (2 · (2
· 𝑁)))) |
178 | 121, 127,
131, 175, 177 | lttrd 10653 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((𝑚↑2) + (𝑛↑2)) < (((2 · 𝑁)↑2) + (2 · (2
· 𝑁)))) |
179 | 121, 131,
132, 178 | ltadd1dd 11104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) < ((((2 · 𝑁)↑2) + (2 · (2
· 𝑁))) +
1)) |
180 | 3 | 3ad2ant1 1126 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 𝑃 = ((2 · 𝑁) + 1)) |
181 | 180 | oveq1d 7036 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃↑2) = (((2 · 𝑁) + 1)↑2)) |
182 | 97 | sqvald 13362 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃↑2) = (𝑃 · 𝑃)) |
183 | 125 | nncnd 11507 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (2 · 𝑁) ∈ ℂ) |
184 | | binom21 13435 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑁) ∈ ℂ
→ (((2 · 𝑁) +
1)↑2) = ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1)) |
185 | 183, 184 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((2 · 𝑁) + 1)↑2) = ((((2 · 𝑁)↑2) + (2 · (2
· 𝑁))) +
1)) |
186 | 181, 182,
185 | 3eqtr3d 2839 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑃 · 𝑃) = ((((2 · 𝑁)↑2) + (2 · (2 · 𝑁))) + 1)) |
187 | 179, 186 | breqtrrd 4994 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃)) |
188 | 103 | nnred 11506 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℝ) |
189 | 45 | nngt0d 11539 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → 0 < 𝑃) |
190 | | ltdivmul 11368 |
. . . . . . . . . . 11
⊢
(((((𝑚↑2) +
(𝑛↑2)) + 1) ∈
ℝ ∧ 𝑃 ∈
ℝ ∧ (𝑃 ∈
ℝ ∧ 0 < 𝑃))
→ (((((𝑚↑2) +
(𝑛↑2)) + 1) / 𝑃) < 𝑃 ↔ (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃))) |
191 | 188, 51, 51, 189, 190 | syl112anc 1367 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃 ↔ (((𝑚↑2) + (𝑛↑2)) + 1) < (𝑃 · 𝑃))) |
192 | 187, 191 | mpbird 258 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃) |
193 | | 1z 11866 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
194 | | elfzm11 12833 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ 𝑃
∈ ℤ) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ↔ (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ ℤ ∧ 1 ≤ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∧ ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) < 𝑃))) |
195 | 193, 69, 194 | 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) / 𝑃) < 𝑃))) |
196 | 111, 120,
192, 195 | mpbir3and 1335 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1))) |
197 | | gzreim 16109 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑚 + (i · 𝑛)) ∈
ℤ[i]) |
198 | 81, 58, 197 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚 + (i · 𝑛)) ∈ ℤ[i]) |
199 | | gzcn 16102 |
. . . . . . . . . . . . 13
⊢ ((𝑚 + (i · 𝑛)) ∈ ℤ[i] →
(𝑚 + (i · 𝑛)) ∈
ℂ) |
200 | 198, 199 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (𝑚 + (i · 𝑛)) ∈ ℂ) |
201 | 200 | absvalsq2d 14642 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((abs‘(𝑚 + (i · 𝑛)))↑2) = (((ℜ‘(𝑚 + (i · 𝑛)))↑2) +
((ℑ‘(𝑚 + (i
· 𝑛)))↑2))) |
202 | 139, 147 | crred 14429 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (ℜ‘(𝑚 + (i · 𝑛))) = 𝑚) |
203 | 202 | oveq1d 7036 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((ℜ‘(𝑚 + (i · 𝑛)))↑2) = (𝑚↑2)) |
204 | 139, 147 | crimd 14430 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (ℑ‘(𝑚 + (i · 𝑛))) = 𝑛) |
205 | 204 | oveq1d 7036 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((ℑ‘(𝑚 + (i · 𝑛)))↑2) = (𝑛↑2)) |
206 | 203, 205 | oveq12d 7039 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((ℜ‘(𝑚 + (i · 𝑛)))↑2) +
((ℑ‘(𝑚 + (i
· 𝑛)))↑2)) =
((𝑚↑2) + (𝑛↑2))) |
207 | 201, 206 | eqtrd 2831 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ((abs‘(𝑚 + (i · 𝑛)))↑2) = ((𝑚↑2) + (𝑛↑2))) |
208 | 207 | oveq1d 7036 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((𝑚↑2) + (𝑛↑2)) + 1)) |
209 | 103 | nncnd 11507 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((𝑚↑2) + (𝑛↑2)) + 1) ∈
ℂ) |
210 | 209, 97, 108 | divcan1d 11270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃) = (((𝑚↑2) + (𝑛↑2)) + 1)) |
211 | 208, 210 | eqtr4d 2834 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)) |
212 | | oveq1 7028 |
. . . . . . . . . 10
⊢ (𝑘 = ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) → (𝑘 · 𝑃) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)) |
213 | 212 | eqeq2d 2805 |
. . . . . . . . 9
⊢ (𝑘 = ((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) → ((((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃) ↔ (((abs‘𝑢)↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃))) |
214 | | fveq2 6543 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝑚 + (i · 𝑛)) → (abs‘𝑢) = (abs‘(𝑚 + (i · 𝑛)))) |
215 | 214 | oveq1d 7036 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝑚 + (i · 𝑛)) → ((abs‘𝑢)↑2) = ((abs‘(𝑚 + (i · 𝑛)))↑2)) |
216 | 215 | oveq1d 7036 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑚 + (i · 𝑛)) → (((abs‘𝑢)↑2) + 1) = (((abs‘(𝑚 + (i · 𝑛)))↑2) +
1)) |
217 | 216 | eqeq1d 2797 |
. . . . . . . . 9
⊢ (𝑢 = (𝑚 + (i · 𝑛)) → ((((abs‘𝑢)↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃) ↔ (((abs‘(𝑚 + (i · 𝑛)))↑2) + 1) = (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃))) |
218 | 213, 217 | rspc2ev 3574 |
. . . . . . . 8
⊢
((((((𝑚↑2) +
(𝑛↑2)) + 1) / 𝑃) ∈ (1...(𝑃 − 1)) ∧ (𝑚 + (i · 𝑛)) ∈ ℤ[i] ∧
(((abs‘(𝑚 + (i
· 𝑛)))↑2) + 1)
= (((((𝑚↑2) + (𝑛↑2)) + 1) / 𝑃) · 𝑃)) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) |
219 | 196, 198,
211, 218 | syl3anc 1364 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁)) ∧ ((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) |
220 | 219 | 3expia 1114 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃)) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))) |
221 | 42, 220 | syl5 34 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑛 ∈ (0...𝑁))) → ((𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))) |
222 | 221 | rexlimdvva 3257 |
. . . 4
⊢ (𝜑 → (∃𝑚 ∈ (0...𝑁)∃𝑛 ∈ (0...𝑁)(𝑗 = ((𝑚↑2) mod 𝑃) ∧ 𝑗 = ((𝑃 − 1) − ((𝑛↑2) mod 𝑃))) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))) |
223 | 41, 222 | syl5bi 243 |
. . 3
⊢ (𝜑 → (𝑗 ∈ (𝐴 ∩ ran 𝐹) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))) |
224 | 223 | exlimdv 1911 |
. 2
⊢ (𝜑 → (∃𝑗 𝑗 ∈ (𝐴 ∩ ran 𝐹) → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))) |
225 | 9, 224 | mpd 15 |
1
⊢ (𝜑 → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) |