Proof of Theorem 4sqlem14
Step | Hyp | Ref
| Expression |
1 | | 4sq.r |
. 2
⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) |
2 | | 4sq.6 |
. . . . . . . . 9
⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} |
3 | 2 | ssrab3 3971 |
. . . . . . . 8
⊢ 𝑇 ⊆
ℕ |
4 | | 4sq.7 |
. . . . . . . . 9
⊢ 𝑀 = inf(𝑇, ℝ, < ) |
5 | | nnuz 12363 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
6 | 3, 5 | sseqtri 3913 |
. . . . . . . . . 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 16393 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) |
13 | 12 | simpld 498 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ≠ ∅) |
14 | | infssuzcl 12414 |
. . . . . . . . . 10
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇) |
15 | 6, 13, 14 | sylancr 590 |
. . . . . . . . 9
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇) |
16 | 4, 15 | eqeltrid 2837 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ 𝑇) |
17 | 3, 16 | sseldi 3875 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) |
18 | 17 | nnzd 12167 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
19 | | prmz 16116 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
20 | 10, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℤ) |
21 | 18, 20 | zmulcld 12174 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℤ) |
22 | | 4sq.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℤ) |
23 | | 4sq.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
24 | 22, 17, 23 | 4sqlem5 16378 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)) |
25 | 24 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℤ) |
26 | | zsqcl2 13594 |
. . . . . . . . . . 11
⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈
ℕ0) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸↑2) ∈
ℕ0) |
28 | | 4sq.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℤ) |
29 | | 4sq.f |
. . . . . . . . . . . . 13
⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
30 | 28, 17, 29 | 4sqlem5 16378 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)) |
31 | 30 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ℤ) |
32 | | zsqcl2 13594 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈
ℕ0) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹↑2) ∈
ℕ0) |
34 | 27, 33 | nn0addcld 12040 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈
ℕ0) |
35 | 34 | nn0zd 12166 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) |
36 | | 4sq.c |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℤ) |
37 | | 4sq.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
38 | 36, 17, 37 | 4sqlem5 16378 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)) |
39 | 38 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ ℤ) |
40 | | zsqcl2 13594 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ ℤ → (𝐺↑2) ∈
ℕ0) |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺↑2) ∈
ℕ0) |
42 | | 4sq.d |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ∈ ℤ) |
43 | | 4sq.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
44 | 42, 17, 43 | 4sqlem5 16378 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)) |
45 | 44 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ ℤ) |
46 | | zsqcl2 13594 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ ℤ → (𝐻↑2) ∈
ℕ0) |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻↑2) ∈
ℕ0) |
48 | 41, 47 | nn0addcld 12040 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈
ℕ0) |
49 | 48 | nn0zd 12166 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℤ) |
50 | 35, 49 | zaddcld 12172 |
. . . . . . 7
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
51 | 21, 50 | zsubcld 12173 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∈ ℤ) |
52 | | dvdsmul1 15723 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑃)) |
53 | 18, 20, 52 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∥ (𝑀 · 𝑃)) |
54 | | zsqcl 13586 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℤ) |
55 | 22, 54 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) |
56 | | zsqcl 13586 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈
ℤ) |
57 | 28, 56 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵↑2) ∈ ℤ) |
58 | 55, 57 | zaddcld 12172 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℤ) |
59 | 58, 35 | zsubcld 12173 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∈ ℤ) |
60 | | zsqcl 13586 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈
ℤ) |
61 | 36, 60 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶↑2) ∈ ℤ) |
62 | | zsqcl 13586 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈
ℤ) |
63 | 42, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷↑2) ∈ ℤ) |
64 | 61, 63 | zaddcld 12172 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) |
65 | 64, 49 | zsubcld 12173 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
66 | 27 | nn0zd 12166 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸↑2) ∈ ℤ) |
67 | 55, 66 | zsubcld 12173 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴↑2) − (𝐸↑2)) ∈ ℤ) |
68 | 33 | nn0zd 12166 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹↑2) ∈ ℤ) |
69 | 57, 68 | zsubcld 12173 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵↑2) − (𝐹↑2)) ∈ ℤ) |
70 | 22, 17, 23 | 4sqlem8 16381 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐸↑2))) |
71 | 28, 17, 29 | 4sqlem8 16381 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐹↑2))) |
72 | 18, 67, 69, 70, 71 | dvds2addd 15737 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2)))) |
73 | 22 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
74 | 73 | sqcld 13600 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
75 | 28 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
76 | 75 | sqcld 13600 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) |
77 | 25 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℂ) |
78 | 77 | sqcld 13600 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) |
79 | 31 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ℂ) |
80 | 79 | sqcld 13600 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹↑2) ∈ ℂ) |
81 | 74, 76, 78, 80 | addsub4d 11122 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) = (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2)))) |
82 | 72, 81 | breqtrrd 5058 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2)))) |
83 | 41 | nn0zd 12166 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺↑2) ∈ ℤ) |
84 | 61, 83 | zsubcld 12173 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶↑2) − (𝐺↑2)) ∈ ℤ) |
85 | 47 | nn0zd 12166 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐻↑2) ∈ ℤ) |
86 | 63, 85 | zsubcld 12173 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐷↑2) − (𝐻↑2)) ∈ ℤ) |
87 | 36, 17, 37 | 4sqlem8 16381 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐶↑2) − (𝐺↑2))) |
88 | 42, 17, 43 | 4sqlem8 16381 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐷↑2) − (𝐻↑2))) |
89 | 18, 84, 86, 87, 88 | dvds2addd 15737 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2)))) |
90 | 36 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) |
91 | 90 | sqcld 13600 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶↑2) ∈ ℂ) |
92 | 42 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℂ) |
93 | 92 | sqcld 13600 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) |
94 | 39 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ ℂ) |
95 | 94 | sqcld 13600 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺↑2) ∈ ℂ) |
96 | 45 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ ℂ) |
97 | 96 | sqcld 13600 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻↑2) ∈ ℂ) |
98 | 91, 93, 95, 97 | addsub4d 11122 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) = (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2)))) |
99 | 89, 98 | breqtrrd 5058 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))) |
100 | 18, 59, 65, 82, 99 | dvds2addd 15737 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
101 | | 4sq.p |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2)))) |
102 | 101 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) |
103 | 74, 76 | addcld 10738 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℂ) |
104 | 91, 93 | addcld 10738 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℂ) |
105 | 78, 80 | addcld 10738 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ) |
106 | 95, 97 | addcld 10738 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℂ) |
107 | 103, 104,
105, 106 | addsub4d 11122 |
. . . . . . . 8
⊢ (𝜑 → ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
108 | 102, 107 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
109 | 100, 108 | breqtrrd 5058 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) |
110 | 18, 21, 51, 53, 109 | dvds2subd 15738 |
. . . . 5
⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))) |
111 | 17 | nncnd 11732 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
112 | | prmnn 16115 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
113 | 10, 112 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℕ) |
114 | 113 | nncnd 11732 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℂ) |
115 | 111, 114 | mulcld 10739 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℂ) |
116 | 105, 106 | addcld 10738 |
. . . . . 6
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℂ) |
117 | 115, 116 | nncand 11080 |
. . . . 5
⊢ (𝜑 → ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
118 | 110, 117 | breqtrd 5056 |
. . . 4
⊢ (𝜑 → 𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
119 | 17 | nnne0d 11766 |
. . . . 5
⊢ (𝜑 → 𝑀 ≠ 0) |
120 | 34, 48 | nn0addcld 12040 |
. . . . . 6
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈
ℕ0) |
121 | 120 | nn0zd 12166 |
. . . . 5
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
122 | | dvdsval2 15702 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)) |
123 | 18, 119, 121, 122 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)) |
124 | 118, 123 | mpbid 235 |
. . 3
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ) |
125 | 120 | nn0red 12037 |
. . . 4
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ) |
126 | 120 | nn0ge0d 12039 |
. . . 4
⊢ (𝜑 → 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
127 | 17 | nnred 11731 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℝ) |
128 | 17 | nngt0d 11765 |
. . . 4
⊢ (𝜑 → 0 < 𝑀) |
129 | | divge0 11587 |
. . . 4
⊢
((((((𝐸↑2) +
(𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ ∧ 0 ≤
(((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)) |
130 | 125, 126,
127, 128, 129 | syl22anc 838 |
. . 3
⊢ (𝜑 → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)) |
131 | | elnn0z 12075 |
. . 3
⊢
(((((𝐸↑2) +
(𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ0 ↔
(((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ ∧ 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))) |
132 | 124, 130,
131 | sylanbrc 586 |
. 2
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈
ℕ0) |
133 | 1, 132 | eqeltrid 2837 |
1
⊢ (𝜑 → 𝑅 ∈
ℕ0) |