Proof of Theorem 4sqlem14
Step | Hyp | Ref
| Expression |
1 | | 4sq.r |
. 2
⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) |
2 | | 4sq.6 |
. . . . . . . . 9
⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} |
3 | 2 | ssrab3 4057 |
. . . . . . . 8
⊢ 𝑇 ⊆
ℕ |
4 | | 4sq.7 |
. . . . . . . . 9
⊢ 𝑀 = inf(𝑇, ℝ, < ) |
5 | | nnuz 12282 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
6 | 3, 5 | sseqtri 4003 |
. . . . . . . . . 10
⊢ 𝑇 ⊆
(ℤ≥‘1) |
7 | | 4sq.1 |
. . . . . . . . . . . 12
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} |
8 | | 4sq.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
9 | | 4sq.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) |
10 | | 4sq.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℙ) |
11 | | 4sq.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆) |
12 | 7, 8, 9, 10, 11, 2, 4 | 4sqlem13 16293 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) |
13 | 12 | simpld 497 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ≠ ∅) |
14 | | infssuzcl 12333 |
. . . . . . . . . 10
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇) |
15 | 6, 13, 14 | sylancr 589 |
. . . . . . . . 9
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇) |
16 | 4, 15 | eqeltrid 2917 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ 𝑇) |
17 | 3, 16 | sseldi 3965 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) |
18 | 17 | nnzd 12087 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
19 | | prmz 16019 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
20 | 10, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℤ) |
21 | | dvdsmul1 15631 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑃)) |
22 | 18, 20, 21 | syl2anc 586 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∥ (𝑀 · 𝑃)) |
23 | | 4sq.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℤ) |
24 | | 4sq.e |
. . . . . . . . . . 11
⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
25 | 23, 17, 24 | 4sqlem8 16281 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐸↑2))) |
26 | | 4sq.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℤ) |
27 | | 4sq.f |
. . . . . . . . . . 11
⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
28 | 26, 17, 27 | 4sqlem8 16281 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐹↑2))) |
29 | | zsqcl 13495 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℤ) |
30 | 23, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) |
31 | 23, 17, 24 | 4sqlem5 16278 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)) |
32 | 31 | simpld 497 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ ℤ) |
33 | | zsqcl2 13503 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈
ℕ0) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸↑2) ∈
ℕ0) |
35 | 34 | nn0zd 12086 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸↑2) ∈ ℤ) |
36 | 30, 35 | zsubcld 12093 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴↑2) − (𝐸↑2)) ∈ ℤ) |
37 | | zsqcl 13495 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈
ℤ) |
38 | 26, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵↑2) ∈ ℤ) |
39 | 26, 17, 27 | 4sqlem5 16278 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)) |
40 | 39 | simpld 497 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ ℤ) |
41 | | zsqcl2 13503 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈
ℕ0) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹↑2) ∈
ℕ0) |
43 | 42 | nn0zd 12086 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹↑2) ∈ ℤ) |
44 | 38, 43 | zsubcld 12093 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵↑2) − (𝐹↑2)) ∈ ℤ) |
45 | | dvds2add 15643 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ ((𝐴↑2) − (𝐸↑2)) ∈ ℤ ∧
((𝐵↑2) − (𝐹↑2)) ∈ ℤ) →
((𝑀 ∥ ((𝐴↑2) − (𝐸↑2)) ∧ 𝑀 ∥ ((𝐵↑2) − (𝐹↑2))) → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))) |
46 | 18, 36, 44, 45 | syl3anc 1367 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 ∥ ((𝐴↑2) − (𝐸↑2)) ∧ 𝑀 ∥ ((𝐵↑2) − (𝐹↑2))) → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))) |
47 | 25, 28, 46 | mp2and 697 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2)))) |
48 | 23 | zcnd 12089 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
49 | 48 | sqcld 13509 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
50 | 26 | zcnd 12089 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
51 | 50 | sqcld 13509 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) |
52 | 32 | zcnd 12089 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℂ) |
53 | 52 | sqcld 13509 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) |
54 | 40 | zcnd 12089 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ℂ) |
55 | 54 | sqcld 13509 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹↑2) ∈ ℂ) |
56 | 49, 51, 53, 55 | addsub4d 11044 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) = (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2)))) |
57 | 47, 56 | breqtrrd 5094 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2)))) |
58 | | 4sq.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℤ) |
59 | | 4sq.g |
. . . . . . . . . . 11
⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
60 | 58, 17, 59 | 4sqlem8 16281 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐶↑2) − (𝐺↑2))) |
61 | | 4sq.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℤ) |
62 | | 4sq.h |
. . . . . . . . . . 11
⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
63 | 61, 17, 62 | 4sqlem8 16281 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐷↑2) − (𝐻↑2))) |
64 | | zsqcl 13495 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈
ℤ) |
65 | 58, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶↑2) ∈ ℤ) |
66 | 58, 17, 59 | 4sqlem5 16278 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)) |
67 | 66 | simpld 497 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ ℤ) |
68 | | zsqcl2 13503 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ ℤ → (𝐺↑2) ∈
ℕ0) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺↑2) ∈
ℕ0) |
70 | 69 | nn0zd 12086 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺↑2) ∈ ℤ) |
71 | 65, 70 | zsubcld 12093 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶↑2) − (𝐺↑2)) ∈ ℤ) |
72 | | zsqcl 13495 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈
ℤ) |
73 | 61, 72 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷↑2) ∈ ℤ) |
74 | 61, 17, 62 | 4sqlem5 16278 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)) |
75 | 74 | simpld 497 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 ∈ ℤ) |
76 | | zsqcl2 13503 |
. . . . . . . . . . . . . 14
⊢ (𝐻 ∈ ℤ → (𝐻↑2) ∈
ℕ0) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐻↑2) ∈
ℕ0) |
78 | 77 | nn0zd 12086 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐻↑2) ∈ ℤ) |
79 | 73, 78 | zsubcld 12093 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐷↑2) − (𝐻↑2)) ∈ ℤ) |
80 | | dvds2add 15643 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ ((𝐶↑2) − (𝐺↑2)) ∈ ℤ ∧
((𝐷↑2) − (𝐻↑2)) ∈ ℤ) →
((𝑀 ∥ ((𝐶↑2) − (𝐺↑2)) ∧ 𝑀 ∥ ((𝐷↑2) − (𝐻↑2))) → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))) |
81 | 18, 71, 79, 80 | syl3anc 1367 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 ∥ ((𝐶↑2) − (𝐺↑2)) ∧ 𝑀 ∥ ((𝐷↑2) − (𝐻↑2))) → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))) |
82 | 60, 63, 81 | mp2and 697 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2)))) |
83 | 58 | zcnd 12089 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) |
84 | 83 | sqcld 13509 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶↑2) ∈ ℂ) |
85 | 61 | zcnd 12089 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℂ) |
86 | 85 | sqcld 13509 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) |
87 | 67 | zcnd 12089 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ ℂ) |
88 | 87 | sqcld 13509 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺↑2) ∈ ℂ) |
89 | 75 | zcnd 12089 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ ℂ) |
90 | 89 | sqcld 13509 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻↑2) ∈ ℂ) |
91 | 84, 86, 88, 90 | addsub4d 11044 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) = (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2)))) |
92 | 82, 91 | breqtrrd 5094 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))) |
93 | 30, 38 | zaddcld 12092 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℤ) |
94 | 34, 42 | nn0addcld 11960 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈
ℕ0) |
95 | 94 | nn0zd 12086 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) |
96 | 93, 95 | zsubcld 12093 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∈ ℤ) |
97 | 65, 73 | zaddcld 12092 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) |
98 | 69, 77 | nn0addcld 11960 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈
ℕ0) |
99 | 98 | nn0zd 12086 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℤ) |
100 | 97, 99 | zsubcld 12093 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
101 | | dvds2add 15643 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∈ ℤ ∧ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) → ((𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∧ 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))) → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))) |
102 | 18, 96, 100, 101 | syl3anc 1367 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∧ 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))) → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))) |
103 | 57, 92, 102 | mp2and 697 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
104 | | 4sq.p |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2)))) |
105 | 104 | oveq1d 7171 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) |
106 | 49, 51 | addcld 10660 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℂ) |
107 | 84, 86 | addcld 10660 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℂ) |
108 | 53, 55 | addcld 10660 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ) |
109 | 88, 90 | addcld 10660 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℂ) |
110 | 106, 107,
108, 109 | addsub4d 11044 |
. . . . . . . 8
⊢ (𝜑 → ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
111 | 105, 110 | eqtrd 2856 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
112 | 103, 111 | breqtrrd 5094 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) |
113 | 18, 20 | zmulcld 12094 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℤ) |
114 | 95, 99 | zaddcld 12092 |
. . . . . . 7
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
115 | 113, 114 | zsubcld 12093 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∈ ℤ) |
116 | 18, 22, 112, 113, 115 | dvds2subd 15645 |
. . . . 5
⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))) |
117 | 17 | nncnd 11654 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
118 | | prmnn 16018 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
119 | 10, 118 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℕ) |
120 | 119 | nncnd 11654 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℂ) |
121 | 117, 120 | mulcld 10661 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℂ) |
122 | 108, 109 | addcld 10660 |
. . . . . 6
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℂ) |
123 | 121, 122 | nncand 11002 |
. . . . 5
⊢ (𝜑 → ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
124 | 116, 123 | breqtrd 5092 |
. . . 4
⊢ (𝜑 → 𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
125 | 17 | nnne0d 11688 |
. . . . 5
⊢ (𝜑 → 𝑀 ≠ 0) |
126 | 94, 98 | nn0addcld 11960 |
. . . . . 6
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈
ℕ0) |
127 | 126 | nn0zd 12086 |
. . . . 5
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
128 | | dvdsval2 15610 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)) |
129 | 18, 125, 127, 128 | syl3anc 1367 |
. . . 4
⊢ (𝜑 → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)) |
130 | 124, 129 | mpbid 234 |
. . 3
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ) |
131 | 126 | nn0red 11957 |
. . . 4
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ) |
132 | 126 | nn0ge0d 11959 |
. . . 4
⊢ (𝜑 → 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
133 | 17 | nnred 11653 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℝ) |
134 | 17 | nngt0d 11687 |
. . . 4
⊢ (𝜑 → 0 < 𝑀) |
135 | | divge0 11509 |
. . . 4
⊢
((((((𝐸↑2) +
(𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ ∧ 0 ≤
(((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)) |
136 | 131, 132,
133, 134, 135 | syl22anc 836 |
. . 3
⊢ (𝜑 → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)) |
137 | | elnn0z 11995 |
. . 3
⊢
(((((𝐸↑2) +
(𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ0 ↔
(((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ ∧ 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))) |
138 | 130, 136,
137 | sylanbrc 585 |
. 2
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈
ℕ0) |
139 | 1, 138 | eqeltrid 2917 |
1
⊢ (𝜑 → 𝑅 ∈
ℕ0) |