Proof of Theorem 4sqlem14
| Step | Hyp | Ref
| Expression |
| 1 | | 4sq.r |
. 2
⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) |
| 2 | | 4sq.6 |
. . . . . . . . 9
⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} |
| 3 | 2 | ssrab3 4082 |
. . . . . . . 8
⊢ 𝑇 ⊆
ℕ |
| 4 | | 4sq.7 |
. . . . . . . . 9
⊢ 𝑀 = inf(𝑇, ℝ, < ) |
| 5 | | nnuz 12921 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
| 6 | 3, 5 | sseqtri 4032 |
. . . . . . . . . 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 16995 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) |
| 13 | 12 | simpld 494 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ≠ ∅) |
| 14 | | infssuzcl 12974 |
. . . . . . . . . 10
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇) |
| 15 | 6, 13, 14 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇) |
| 16 | 4, 15 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ 𝑇) |
| 17 | 3, 16 | sselid 3981 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 18 | 17 | nnzd 12640 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 19 | | prmz 16712 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 20 | 10, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℤ) |
| 21 | 18, 20 | zmulcld 12728 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℤ) |
| 22 | | 4sq.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℤ) |
| 23 | | 4sq.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
| 24 | 22, 17, 23 | 4sqlem5 16980 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)) |
| 25 | 24 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℤ) |
| 26 | | zsqcl2 14178 |
. . . . . . . . . . 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 16980 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)) |
| 31 | 30 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ℤ) |
| 32 | | zsqcl2 14178 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈
ℕ0) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹↑2) ∈
ℕ0) |
| 34 | 27, 33 | nn0addcld 12591 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈
ℕ0) |
| 35 | 34 | nn0zd 12639 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) |
| 36 | | 4sq.c |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℤ) |
| 37 | | 4sq.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
| 38 | 36, 17, 37 | 4sqlem5 16980 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)) |
| 39 | 38 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ ℤ) |
| 40 | | zsqcl2 14178 |
. . . . . . . . . . 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 16980 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)) |
| 45 | 44 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ ℤ) |
| 46 | | zsqcl2 14178 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ ℤ → (𝐻↑2) ∈
ℕ0) |
| 47 | 45, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻↑2) ∈
ℕ0) |
| 48 | 41, 47 | nn0addcld 12591 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈
ℕ0) |
| 49 | 48 | nn0zd 12639 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℤ) |
| 50 | 35, 49 | zaddcld 12726 |
. . . . . . 7
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
| 51 | 21, 50 | zsubcld 12727 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∈ ℤ) |
| 52 | | dvdsmul1 16315 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑃)) |
| 53 | 18, 20, 52 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∥ (𝑀 · 𝑃)) |
| 54 | | zsqcl 14169 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℤ) |
| 55 | 22, 54 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) |
| 56 | | zsqcl 14169 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈
ℤ) |
| 57 | 28, 56 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵↑2) ∈ ℤ) |
| 58 | 55, 57 | zaddcld 12726 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℤ) |
| 59 | 58, 35 | zsubcld 12727 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) ∈ ℤ) |
| 60 | | zsqcl 14169 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈
ℤ) |
| 61 | 36, 60 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶↑2) ∈ ℤ) |
| 62 | | zsqcl 14169 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈
ℤ) |
| 63 | 42, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷↑2) ∈ ℤ) |
| 64 | 61, 63 | zaddcld 12726 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) |
| 65 | 64, 49 | zsubcld 12727 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
| 66 | 27 | nn0zd 12639 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸↑2) ∈ ℤ) |
| 67 | 55, 66 | zsubcld 12727 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴↑2) − (𝐸↑2)) ∈ ℤ) |
| 68 | 33 | nn0zd 12639 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹↑2) ∈ ℤ) |
| 69 | 57, 68 | zsubcld 12727 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵↑2) − (𝐹↑2)) ∈ ℤ) |
| 70 | 22, 17, 23 | 4sqlem8 16983 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐸↑2))) |
| 71 | 28, 17, 29 | 4sqlem8 16983 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐹↑2))) |
| 72 | 18, 67, 69, 70, 71 | dvds2addd 16329 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2)))) |
| 73 | 22 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 74 | 73 | sqcld 14184 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
| 75 | 28 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 76 | 75 | sqcld 14184 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) |
| 77 | 25 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℂ) |
| 78 | 77 | sqcld 14184 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) |
| 79 | 31 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ℂ) |
| 80 | 79 | sqcld 14184 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹↑2) ∈ ℂ) |
| 81 | 74, 76, 78, 80 | addsub4d 11667 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) = (((𝐴↑2) − (𝐸↑2)) + ((𝐵↑2) − (𝐹↑2)))) |
| 82 | 72, 81 | breqtrrd 5171 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2)))) |
| 83 | 41 | nn0zd 12639 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺↑2) ∈ ℤ) |
| 84 | 61, 83 | zsubcld 12727 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶↑2) − (𝐺↑2)) ∈ ℤ) |
| 85 | 47 | nn0zd 12639 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐻↑2) ∈ ℤ) |
| 86 | 63, 85 | zsubcld 12727 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐷↑2) − (𝐻↑2)) ∈ ℤ) |
| 87 | 36, 17, 37 | 4sqlem8 16983 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐶↑2) − (𝐺↑2))) |
| 88 | 42, 17, 43 | 4sqlem8 16983 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐷↑2) − (𝐻↑2))) |
| 89 | 18, 84, 86, 87, 88 | dvds2addd 16329 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2)))) |
| 90 | 36 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 91 | 90 | sqcld 14184 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶↑2) ∈ ℂ) |
| 92 | 42 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℂ) |
| 93 | 92 | sqcld 14184 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) |
| 94 | 39 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ ℂ) |
| 95 | 94 | sqcld 14184 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺↑2) ∈ ℂ) |
| 96 | 45 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ ℂ) |
| 97 | 96 | sqcld 14184 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻↑2) ∈ ℂ) |
| 98 | 91, 93, 95, 97 | addsub4d 11667 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))) = (((𝐶↑2) − (𝐺↑2)) + ((𝐷↑2) − (𝐻↑2)))) |
| 99 | 89, 98 | breqtrrd 5171 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2)))) |
| 100 | 18, 59, 65, 82, 99 | dvds2addd 16329 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∥ ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
| 101 | | 4sq.p |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2)))) |
| 102 | 101 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) |
| 103 | 74, 76 | addcld 11280 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) ∈ ℂ) |
| 104 | 91, 93 | addcld 11280 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℂ) |
| 105 | 78, 80 | addcld 11280 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ) |
| 106 | 95, 97 | addcld 11280 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℂ) |
| 107 | 103, 104,
105, 106 | addsub4d 11667 |
. . . . . . . 8
⊢ (𝜑 → ((((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
| 108 | 102, 107 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝐴↑2) + (𝐵↑2)) − ((𝐸↑2) + (𝐹↑2))) + (((𝐶↑2) + (𝐷↑2)) − ((𝐺↑2) + (𝐻↑2))))) |
| 109 | 100, 108 | breqtrrd 5171 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) |
| 110 | 18, 21, 51, 53, 109 | dvds2subd 16330 |
. . . . 5
⊢ (𝜑 → 𝑀 ∥ ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))))) |
| 111 | 17 | nncnd 12282 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 112 | | prmnn 16711 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 113 | 10, 112 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 114 | 113 | nncnd 12282 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℂ) |
| 115 | 111, 114 | mulcld 11281 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℂ) |
| 116 | 105, 106 | addcld 11280 |
. . . . . 6
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℂ) |
| 117 | 115, 116 | nncand 11625 |
. . . . 5
⊢ (𝜑 → ((𝑀 · 𝑃) − ((𝑀 · 𝑃) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
| 118 | 110, 117 | breqtrd 5169 |
. . . 4
⊢ (𝜑 → 𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
| 119 | 17 | nnne0d 12316 |
. . . . 5
⊢ (𝜑 → 𝑀 ≠ 0) |
| 120 | 34, 48 | nn0addcld 12591 |
. . . . . 6
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈
ℕ0) |
| 121 | 120 | nn0zd 12639 |
. . . . 5
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) |
| 122 | | dvdsval2 16293 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℤ) → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)) |
| 123 | 18, 119, 121, 122 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝑀 ∥ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ↔ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ)) |
| 124 | 118, 123 | mpbid 232 |
. . 3
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ) |
| 125 | 120 | nn0red 12588 |
. . . 4
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ) |
| 126 | 120 | nn0ge0d 12590 |
. . . 4
⊢ (𝜑 → 0 ≤ (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
| 127 | 17 | nnred 12281 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 128 | 17 | nngt0d 12315 |
. . . 4
⊢ (𝜑 → 0 < 𝑀) |
| 129 | | divge0 12137 |
. . . 4
⊢
((((((𝐸↑2) +
(𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ ∧ 0 ≤
(((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)) |
| 130 | 125, 126,
127, 128, 129 | syl22anc 839 |
. . 3
⊢ (𝜑 → 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)) |
| 131 | | elnn0z 12626 |
. . 3
⊢
(((((𝐸↑2) +
(𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℕ0 ↔
(((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈ ℤ ∧ 0 ≤ ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))) |
| 132 | 124, 130,
131 | sylanbrc 583 |
. 2
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) ∈
ℕ0) |
| 133 | 1, 132 | eqeltrid 2845 |
1
⊢ (𝜑 → 𝑅 ∈
ℕ0) |