Proof of Theorem 4sqlem14
Step | Hyp | Ref
| Expression |
1 | | 4sq.r |
. 2
⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) |
2 | | 4sq.6 |
. . . . . . . . . 10
⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} |
3 | | ssrab2 3914 |
. . . . . . . . . 10
⊢ {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} ⊆ ℕ |
4 | 2, 3 | eqsstri 3860 |
. . . . . . . . 9
⊢ 𝑇 ⊆
ℕ |
5 | | 4sq.7 |
. . . . . . . . . 10
⊢ 𝑀 = inf(𝑇, ℝ, < ) |
6 | | nnuz 12012 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
7 | 4, 6 | sseqtri 3862 |
. . . . . . . . . . 11
⊢ 𝑇 ⊆
(ℤ≥‘1) |
8 | | 4sq.1 |
. . . . . . . . . . . . 13
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} |
9 | | 4sq.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) |
10 | | 4sq.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) |
11 | | 4sq.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℙ) |
12 | | 4sq.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆) |
13 | 8, 9, 10, 11, 12, 2, 5 | 4sqlem13 16039 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) |
14 | 13 | simpld 490 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ≠ ∅) |
15 | | infssuzcl 12062 |
. . . . . . . . . . 11
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇) |
16 | 7, 14, 15 | sylancr 581 |
. . . . . . . . . 10
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇) |
17 | 5, 16 | syl5eqel 2910 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ 𝑇) |
18 | 4, 17 | sseldi 3825 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
19 | 18 | nnzd 11816 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
20 | | prmz 15768 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
21 | 11, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℤ) |
22 | | dvdsmul1 15387 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑃)) |
23 | 19, 21, 22 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∥ (𝑀 · 𝑃)) |
24 | | 4sq.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℤ) |
25 | | 4sq.e |
. . . . . . . . . . 11
⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
26 | 24, 18, 25 | 4sqlem8 16027 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐸↑2))) |
27 | | 4sq.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℤ) |
28 | | 4sq.f |
. . . . . . . . . . 11
⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
29 | 27, 18, 28 | 4sqlem8 16027 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐹↑2))) |
30 | | zsqcl 13235 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℤ) |
31 | 24, 30 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) |
32 | 24, 18, 25 | 4sqlem5 16024 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)) |
33 | 32 | simpld 490 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ ℤ) |
34 | | zsqcl2 13242 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈
ℕ0) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸↑2) ∈
ℕ0) |
36 | 35 | nn0zd 11815 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸↑2) ∈ ℤ) |
37 | 31, 36 | zsubcld 11822 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴↑2) − (𝐸↑2)) ∈ ℤ) |
38 | | zsqcl 13235 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈
ℤ) |
39 | 27, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵↑2) ∈ ℤ) |
40 | 27, 18, 28 | 4sqlem5 16024 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)) |
41 | 40 | simpld 490 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ ℤ) |
42 | | zsqcl2 13242 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈
ℕ0) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹↑2) ∈
ℕ0) |
44 | 43 | nn0zd 11815 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹↑2) ∈ ℤ) |
45 | 39, 44 | zsubcld 11822 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵↑2) − (𝐹↑2)) ∈ ℤ) |
46 | | dvds2add 15399 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ ((𝐴↑2) − (𝐸↑2)) ∈ ℤ ∧
((𝐵↑2) − (𝐹↑2)) ∈ ℤ) →
((𝑀 ∥ ((𝐴↑2) − (𝐸↑2)) ∧ 𝑀 ∥ ((𝐵↑2) − (𝐹↑2))) → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))) |
47 | 19, 37, 45, 46 | syl3anc 1494 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 ∥ ((𝐴↑2) − (𝐸↑2)) ∧ 𝑀 ∥ ((𝐵↑2) − (𝐹↑2))) → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2))))) |
48 | 26, 29, 47 | mp2and 690 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2)))) |
49 | 24 | zcnd 11818 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
50 | 49 | sqcld 13307 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
51 | 27 | zcnd 11818 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
52 | 51 | sqcld 13307 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) |
53 | 33 | zcnd 11818 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℂ) |
54 | 53 | sqcld 13307 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) |
55 | 41 | zcnd 11818 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ℂ) |
56 | 55 | sqcld 13307 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹↑2) ∈ ℂ) |
57 | 50, 52, 54, 56 | addsub4d 10767 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) = (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2)))) |
58 | 48, 57 | breqtrrd 4903 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2)))) |
59 | | 4sq.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℤ) |
60 | | 4sq.g |
. . . . . . . . . . 11
⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
61 | 59, 18, 60 | 4sqlem8 16027 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐶↑2) − (𝐺↑2))) |
62 | | 4sq.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℤ) |
63 | | 4sq.h |
. . . . . . . . . . 11
⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
64 | 62, 18, 63 | 4sqlem8 16027 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐷↑2) − (𝐻↑2))) |
65 | | zsqcl 13235 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈
ℤ) |
66 | 59, 65 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶↑2) ∈ ℤ) |
67 | 59, 18, 60 | 4sqlem5 16024 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)) |
68 | 67 | simpld 490 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ ℤ) |
69 | | zsqcl2 13242 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ ℤ → (𝐺↑2) ∈
ℕ0) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺↑2) ∈
ℕ0) |
71 | 70 | nn0zd 11815 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺↑2) ∈ ℤ) |
72 | 66, 71 | zsubcld 11822 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶↑2) − (𝐺↑2)) ∈ ℤ) |
73 | | zsqcl 13235 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈
ℤ) |
74 | 62, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷↑2) ∈ ℤ) |
75 | 62, 18, 63 | 4sqlem5 16024 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)) |
76 | 75 | simpld 490 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 ∈ ℤ) |
77 | | zsqcl2 13242 |
. . . . . . . . . . . . . 14
⊢ (𝐻 ∈ ℤ → (𝐻↑2) ∈
ℕ0) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐻↑2) ∈
ℕ0) |
79 | 78 | nn0zd 11815 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐻↑2) ∈ ℤ) |
80 | 74, 79 | zsubcld 11822 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐷↑2) − (𝐻↑2)) ∈ ℤ) |
81 | | dvds2add 15399 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ ((𝐶↑2) − (𝐺↑2)) ∈ ℤ ∧
((𝐷↑2) − (𝐻↑2)) ∈ ℤ) →
((𝑀 ∥ ((𝐶↑2) − (𝐺↑2)) ∧ 𝑀 ∥ ((𝐷↑2) − (𝐻↑2))) → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))) |
82 | 19, 72, 80, 81 | syl3anc 1494 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 ∥ ((𝐶↑2) − (𝐺↑2)) ∧ 𝑀 ∥ ((𝐷↑2) − (𝐻↑2))) → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2))))) |
83 | 61, 64, 82 | mp2and 690 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2)))) |
84 | 59 | zcnd 11818 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) |
85 | 84 | sqcld 13307 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶↑2) ∈ ℂ) |
86 | 62 | zcnd 11818 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℂ) |
87 | 86 | sqcld 13307 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) |
88 | 68 | zcnd 11818 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ ℂ) |
89 | 88 | sqcld 13307 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺↑2) ∈ ℂ) |
90 | 76 | zcnd 11818 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ ℂ) |
91 | 90 | sqcld 13307 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻↑2) ∈ ℂ) |
92 | 85, 87, 89, 91 | addsub4d 10767 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) = (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2)))) |
93 | 83, 92 | breqtrrd 4903 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))) |
94 | 31, 39 | zaddcld 11821 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℤ) |
95 | 35, 43 | nn0addcld 11689 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈
ℕ0) |
96 | 95 | nn0zd 11815 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) |
97 | 94, 96 | zsubcld 11822 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∈ ℤ) |
98 | 66, 74 | zaddcld 11821 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) |
99 | 70, 78 | nn0addcld 11689 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈
ℕ0) |
100 | 99 | nn0zd 11815 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℤ) |
101 | 98, 100 | zsubcld 11822 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
102 | | dvds2add 15399 |
. . . . . . . . 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)))))) |
103 | 19, 97, 101, 102 | syl3anc 1494 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∧ 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))) → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))))) |
104 | 58, 93, 103 | mp2and 690 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
105 | | 4sq.p |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2)))) |
106 | 105 | oveq1d 6925 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) |
107 | 50, 52 | addcld 10383 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℂ) |
108 | 85, 87 | addcld 10383 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℂ) |
109 | 54, 56 | addcld 10383 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ) |
110 | 89, 91 | addcld 10383 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℂ) |
111 | 107, 108,
109, 110 | addsub4d 10767 |
. . . . . . . 8
⊢ (𝜑 → ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
112 | 106, 111 | eqtrd 2861 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
113 | 104, 112 | breqtrrd 4903 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) |
114 | 19, 21 | zmulcld 11823 |
. . . . . . 7
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℤ) |
115 | 96, 100 | zaddcld 11821 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
116 | 114, 115 | zsubcld 11822 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∈ ℤ) |
117 | | dvds2sub 15400 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 · 𝑃) ∈ ℤ ∧ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∈ ℤ) → ((𝑀 ∥ (𝑀 · 𝑃) ∧ 𝑀 ∥ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) → 𝑀 ∥ ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))))) |
118 | 19, 114, 116, 117 | syl3anc 1494 |
. . . . . 6
⊢ (𝜑 → ((𝑀 ∥ (𝑀 · 𝑃) ∧ 𝑀 ∥ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) → 𝑀 ∥ ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))))) |
119 | 23, 113, 118 | mp2and 690 |
. . . . 5
⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))) |
120 | 18 | nncnd 11375 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
121 | | prmnn 15767 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
122 | 11, 121 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℕ) |
123 | 122 | nncnd 11375 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℂ) |
124 | 120, 123 | mulcld 10384 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℂ) |
125 | 109, 110 | addcld 10383 |
. . . . . 6
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℂ) |
126 | 124, 125 | nncand 10725 |
. . . . 5
⊢ (𝜑 → ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
127 | 119, 126 | breqtrd 4901 |
. . . 4
⊢ (𝜑 → 𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
128 | 18 | nnne0d 11408 |
. . . . 5
⊢ (𝜑 → 𝑀 ≠ 0) |
129 | 95, 99 | nn0addcld 11689 |
. . . . . 6
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈
ℕ0) |
130 | 129 | nn0zd 11815 |
. . . . 5
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
131 | | dvdsval2 15367 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)) |
132 | 19, 128, 130, 131 | syl3anc 1494 |
. . . 4
⊢ (𝜑 → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)) |
133 | 127, 132 | mpbid 224 |
. . 3
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ) |
134 | 129 | nn0red 11686 |
. . . 4
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ) |
135 | 129 | nn0ge0d 11688 |
. . . 4
⊢ (𝜑 → 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
136 | 18 | nnred 11374 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℝ) |
137 | 18 | nngt0d 11407 |
. . . 4
⊢ (𝜑 → 0 < 𝑀) |
138 | | divge0 11229 |
. . . 4
⊢
((((((𝐸↑2) +
(𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ ∧ 0 ≤
(((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)) |
139 | 134, 135,
136, 137, 138 | syl22anc 872 |
. . 3
⊢ (𝜑 → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)) |
140 | | elnn0z 11724 |
. . 3
⊢
(((((𝐸↑2) +
(𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ0 ↔
(((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ ∧ 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))) |
141 | 133, 139,
140 | sylanbrc 578 |
. 2
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈
ℕ0) |
142 | 1, 141 | syl5eqel 2910 |
1
⊢ (𝜑 → 𝑅 ∈
ℕ0) |