Proof of Theorem 4sqlem15
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 4sq.m | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘2)) | 
| 2 |  | eluz2nn 12924 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈
(ℤ≥‘2) → 𝑀 ∈ ℕ) | 
| 3 | 1, 2 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 4 | 3 | nnred 12281 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 5 | 4 | resqcld 14165 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀↑2) ∈ ℝ) | 
| 6 | 5 | rehalfcld 12513 | . . . . . . . . 9
⊢ (𝜑 → ((𝑀↑2) / 2) ∈
ℝ) | 
| 7 | 6 | rehalfcld 12513 | . . . . . . . 8
⊢ (𝜑 → (((𝑀↑2) / 2) / 2) ∈
ℝ) | 
| 8 | 7 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → (((𝑀↑2) / 2) / 2) ∈
ℂ) | 
| 9 |  | 4sq.a | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 10 |  | 4sq.e | . . . . . . . . . . . 12
⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) | 
| 11 | 9, 3, 10 | 4sqlem5 16980 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)) | 
| 12 | 11 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℤ) | 
| 13 |  | zsqcl 14169 | . . . . . . . . . 10
⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈
ℤ) | 
| 14 | 12, 13 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐸↑2) ∈ ℤ) | 
| 15 | 14 | zred 12722 | . . . . . . . 8
⊢ (𝜑 → (𝐸↑2) ∈ ℝ) | 
| 16 | 15 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) | 
| 17 |  | 4sq.b | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 18 |  | 4sq.f | . . . . . . . . . . . 12
⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) | 
| 19 | 17, 3, 18 | 4sqlem5 16980 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)) | 
| 20 | 19 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℤ) | 
| 21 |  | zsqcl 14169 | . . . . . . . . . 10
⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈
ℤ) | 
| 22 | 20, 21 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐹↑2) ∈ ℤ) | 
| 23 | 22 | zred 12722 | . . . . . . . 8
⊢ (𝜑 → (𝐹↑2) ∈ ℝ) | 
| 24 | 23 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → (𝐹↑2) ∈ ℂ) | 
| 25 | 8, 8, 16, 24 | addsub4d 11667 | . . . . . 6
⊢ (𝜑 → (((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) − ((𝐸↑2) + (𝐹↑2))) = (((((𝑀↑2) / 2) / 2) − (𝐸↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐹↑2)))) | 
| 26 | 6 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → ((𝑀↑2) / 2) ∈
ℂ) | 
| 27 | 26 | 2halvesd 12512 | . . . . . . 7
⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2)) | 
| 28 | 27 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → (((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) − ((𝐸↑2) + (𝐹↑2))) = (((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2)))) | 
| 29 | 25, 28 | eqtr3d 2779 | . . . . 5
⊢ (𝜑 → (((((𝑀↑2) / 2) / 2) − (𝐸↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐹↑2))) = (((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2)))) | 
| 30 | 29 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((((𝑀↑2) / 2) / 2) − (𝐸↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐹↑2))) = (((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2)))) | 
| 31 | 5 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀↑2) ∈ ℂ) | 
| 32 | 31 | 2halvesd 12512 | . . . . . . . . 9
⊢ (𝜑 → (((𝑀↑2) / 2) + ((𝑀↑2) / 2)) = (𝑀↑2)) | 
| 33 | 32 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((𝑀↑2) / 2) + ((𝑀↑2) / 2)) = (𝑀↑2)) | 
| 34 | 4 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 35 | 34 | sqvald 14183 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀)) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (𝑀↑2) = (𝑀 · 𝑀)) | 
| 37 |  | 4sq.r | . . . . . . . . . . 11
⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) | 
| 38 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → 𝑅 = 𝑀) | 
| 39 | 37, 38 | eqtr3id 2791 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) = 𝑀) | 
| 40 | 39 | oveq1d 7446 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) · 𝑀) = (𝑀 · 𝑀)) | 
| 41 | 15, 23 | readdcld 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ) | 
| 42 |  | 4sq.c | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐶 ∈ ℤ) | 
| 43 |  | 4sq.g | . . . . . . . . . . . . . . . . . 18
⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) | 
| 44 | 42, 3, 43 | 4sqlem5 16980 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)) | 
| 45 | 44 | simpld 494 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺 ∈ ℤ) | 
| 46 |  | zsqcl 14169 | . . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ ℤ → (𝐺↑2) ∈
ℤ) | 
| 47 | 45, 46 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺↑2) ∈ ℤ) | 
| 48 | 47 | zred 12722 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺↑2) ∈ ℝ) | 
| 49 |  | 4sq.d | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷 ∈ ℤ) | 
| 50 |  | 4sq.h | . . . . . . . . . . . . . . . . . 18
⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) | 
| 51 | 49, 3, 50 | 4sqlem5 16980 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)) | 
| 52 | 51 | simpld 494 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐻 ∈ ℤ) | 
| 53 |  | zsqcl 14169 | . . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ ℤ → (𝐻↑2) ∈
ℤ) | 
| 54 | 52, 53 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐻↑2) ∈ ℤ) | 
| 55 | 54 | zred 12722 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐻↑2) ∈ ℝ) | 
| 56 | 48, 55 | readdcld 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℝ) | 
| 57 | 41, 56 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℝ) | 
| 58 | 57 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) ∈ ℂ) | 
| 59 | 3 | nnne0d 12316 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≠ 0) | 
| 60 | 58, 34, 59 | divcan1d 12044 | . . . . . . . . . 10
⊢ (𝜑 → (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) · 𝑀) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) | 
| 61 | 60 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) · 𝑀) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) | 
| 62 | 36, 40, 61 | 3eqtr2rd 2784 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) = (𝑀↑2)) | 
| 63 | 33, 62 | oveq12d 7449 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → ((((𝑀↑2) / 2) + ((𝑀↑2) / 2)) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((𝑀↑2) − (𝑀↑2))) | 
| 64 | 41 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ) | 
| 65 | 56 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ∈ ℂ) | 
| 66 | 26, 26, 64, 65 | addsub4d 11667 | . . . . . . . 8
⊢ (𝜑 → ((((𝑀↑2) / 2) + ((𝑀↑2) / 2)) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) + (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2))))) | 
| 67 | 66 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → ((((𝑀↑2) / 2) + ((𝑀↑2) / 2)) − (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) = ((((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) + (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2))))) | 
| 68 | 31 | subidd 11608 | . . . . . . . 8
⊢ (𝜑 → ((𝑀↑2) − (𝑀↑2)) = 0) | 
| 69 | 68 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → ((𝑀↑2) − (𝑀↑2)) = 0) | 
| 70 | 63, 67, 69 | 3eqtr3d 2785 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → ((((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) + (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2)))) = 0) | 
| 71 | 6, 41 | resubcld 11691 | . . . . . . . 8
⊢ (𝜑 → (((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) ∈ ℝ) | 
| 72 | 9, 3, 10 | 4sqlem7 16982 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸↑2) ≤ (((𝑀↑2) / 2) / 2)) | 
| 73 | 17, 3, 18 | 4sqlem7 16982 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹↑2) ≤ (((𝑀↑2) / 2) / 2)) | 
| 74 | 15, 23, 7, 7, 72, 73 | le2addd 11882 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2))) | 
| 75 | 74, 27 | breqtrd 5169 | . . . . . . . . 9
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2)) | 
| 76 | 6, 41 | subge0d 11853 | . . . . . . . . 9
⊢ (𝜑 → (0 ≤ (((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) ↔ ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2))) | 
| 77 | 75, 76 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ (((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2)))) | 
| 78 | 6, 56 | resubcld 11691 | . . . . . . . 8
⊢ (𝜑 → (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2))) ∈ ℝ) | 
| 79 | 42, 3, 43 | 4sqlem7 16982 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺↑2) ≤ (((𝑀↑2) / 2) / 2)) | 
| 80 | 49, 3, 50 | 4sqlem7 16982 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐻↑2) ≤ (((𝑀↑2) / 2) / 2)) | 
| 81 | 48, 55, 7, 7, 79, 80 | le2addd 11882 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2))) | 
| 82 | 81, 27 | breqtrd 5169 | . . . . . . . . 9
⊢ (𝜑 → ((𝐺↑2) + (𝐻↑2)) ≤ ((𝑀↑2) / 2)) | 
| 83 | 6, 56 | subge0d 11853 | . . . . . . . . 9
⊢ (𝜑 → (0 ≤ (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2))) ↔ ((𝐺↑2) + (𝐻↑2)) ≤ ((𝑀↑2) / 2))) | 
| 84 | 82, 83 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2)))) | 
| 85 |  | add20 11775 | . . . . . . . 8
⊢
((((((𝑀↑2) / 2)
− ((𝐸↑2) +
(𝐹↑2))) ∈ ℝ
∧ 0 ≤ (((𝑀↑2) /
2) − ((𝐸↑2) +
(𝐹↑2)))) ∧
((((𝑀↑2) / 2) −
((𝐺↑2) + (𝐻↑2))) ∈ ℝ ∧
0 ≤ (((𝑀↑2) / 2)
− ((𝐺↑2) +
(𝐻↑2))))) →
(((((𝑀↑2) / 2) −
((𝐸↑2) + (𝐹↑2))) + (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2)))) = 0 ↔ ((((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) = 0 ∧ (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2))) = 0))) | 
| 86 | 71, 77, 78, 84, 85 | syl22anc 839 | . . . . . . 7
⊢ (𝜑 → (((((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) + (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2)))) = 0 ↔ ((((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) = 0 ∧ (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2))) = 0))) | 
| 87 | 86 | biimpa 476 | . . . . . 6
⊢ ((𝜑 ∧ ((((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) + (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2)))) = 0) → ((((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) = 0 ∧ (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2))) = 0)) | 
| 88 | 70, 87 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → ((((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) = 0 ∧ (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2))) = 0)) | 
| 89 | 88 | simpld 494 | . . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((𝑀↑2) / 2) − ((𝐸↑2) + (𝐹↑2))) = 0) | 
| 90 | 30, 89 | eqtrd 2777 | . . 3
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((((𝑀↑2) / 2) / 2) − (𝐸↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐹↑2))) =
0) | 
| 91 | 7, 15 | resubcld 11691 | . . . . 5
⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) − (𝐸↑2)) ∈
ℝ) | 
| 92 | 7, 15 | subge0d 11853 | . . . . . 6
⊢ (𝜑 → (0 ≤ ((((𝑀↑2) / 2) / 2) −
(𝐸↑2)) ↔ (𝐸↑2) ≤ (((𝑀↑2) / 2) /
2))) | 
| 93 | 72, 92 | mpbird 257 | . . . . 5
⊢ (𝜑 → 0 ≤ ((((𝑀↑2) / 2) / 2) −
(𝐸↑2))) | 
| 94 | 7, 23 | resubcld 11691 | . . . . 5
⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) − (𝐹↑2)) ∈
ℝ) | 
| 95 | 7, 23 | subge0d 11853 | . . . . . 6
⊢ (𝜑 → (0 ≤ ((((𝑀↑2) / 2) / 2) −
(𝐹↑2)) ↔ (𝐹↑2) ≤ (((𝑀↑2) / 2) /
2))) | 
| 96 | 73, 95 | mpbird 257 | . . . . 5
⊢ (𝜑 → 0 ≤ ((((𝑀↑2) / 2) / 2) −
(𝐹↑2))) | 
| 97 |  | add20 11775 | . . . . 5
⊢
(((((((𝑀↑2) /
2) / 2) − (𝐸↑2))
∈ ℝ ∧ 0 ≤ ((((𝑀↑2) / 2) / 2) − (𝐸↑2))) ∧ (((((𝑀↑2) / 2) / 2) −
(𝐹↑2)) ∈ ℝ
∧ 0 ≤ ((((𝑀↑2)
/ 2) / 2) − (𝐹↑2)))) → ((((((𝑀↑2) / 2) / 2) − (𝐸↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐹↑2))) = 0 ↔
(((((𝑀↑2) / 2) / 2)
− (𝐸↑2)) = 0
∧ ((((𝑀↑2) / 2) /
2) − (𝐹↑2)) =
0))) | 
| 98 | 91, 93, 94, 96, 97 | syl22anc 839 | . . . 4
⊢ (𝜑 → ((((((𝑀↑2) / 2) / 2) − (𝐸↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐹↑2))) = 0 ↔
(((((𝑀↑2) / 2) / 2)
− (𝐸↑2)) = 0
∧ ((((𝑀↑2) / 2) /
2) − (𝐹↑2)) =
0))) | 
| 99 | 98 | biimpa 476 | . . 3
⊢ ((𝜑 ∧ (((((𝑀↑2) / 2) / 2) − (𝐸↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐹↑2))) = 0) →
(((((𝑀↑2) / 2) / 2)
− (𝐸↑2)) = 0
∧ ((((𝑀↑2) / 2) /
2) − (𝐹↑2)) =
0)) | 
| 100 | 90, 99 | syldan 591 | . 2
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((((𝑀↑2) / 2) / 2) − (𝐸↑2)) = 0 ∧ ((((𝑀↑2) / 2) / 2) −
(𝐹↑2)) =
0)) | 
| 101 | 48 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → (𝐺↑2) ∈ ℂ) | 
| 102 | 55 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → (𝐻↑2) ∈ ℂ) | 
| 103 | 8, 8, 101, 102 | addsub4d 11667 | . . . . . 6
⊢ (𝜑 → (((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) − ((𝐺↑2) + (𝐻↑2))) = (((((𝑀↑2) / 2) / 2) − (𝐺↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐻↑2)))) | 
| 104 | 27 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → (((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) − ((𝐺↑2) + (𝐻↑2))) = (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2)))) | 
| 105 | 103, 104 | eqtr3d 2779 | . . . . 5
⊢ (𝜑 → (((((𝑀↑2) / 2) / 2) − (𝐺↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐻↑2))) = (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2)))) | 
| 106 | 105 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((((𝑀↑2) / 2) / 2) − (𝐺↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐻↑2))) = (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2)))) | 
| 107 | 88 | simprd 495 | . . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((𝑀↑2) / 2) − ((𝐺↑2) + (𝐻↑2))) = 0) | 
| 108 | 106, 107 | eqtrd 2777 | . . 3
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((((𝑀↑2) / 2) / 2) − (𝐺↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐻↑2))) =
0) | 
| 109 | 7, 48 | resubcld 11691 | . . . . 5
⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) − (𝐺↑2)) ∈
ℝ) | 
| 110 | 7, 48 | subge0d 11853 | . . . . . 6
⊢ (𝜑 → (0 ≤ ((((𝑀↑2) / 2) / 2) −
(𝐺↑2)) ↔ (𝐺↑2) ≤ (((𝑀↑2) / 2) /
2))) | 
| 111 | 79, 110 | mpbird 257 | . . . . 5
⊢ (𝜑 → 0 ≤ ((((𝑀↑2) / 2) / 2) −
(𝐺↑2))) | 
| 112 | 7, 55 | resubcld 11691 | . . . . 5
⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) − (𝐻↑2)) ∈
ℝ) | 
| 113 | 7, 55 | subge0d 11853 | . . . . . 6
⊢ (𝜑 → (0 ≤ ((((𝑀↑2) / 2) / 2) −
(𝐻↑2)) ↔ (𝐻↑2) ≤ (((𝑀↑2) / 2) /
2))) | 
| 114 | 80, 113 | mpbird 257 | . . . . 5
⊢ (𝜑 → 0 ≤ ((((𝑀↑2) / 2) / 2) −
(𝐻↑2))) | 
| 115 |  | add20 11775 | . . . . 5
⊢
(((((((𝑀↑2) /
2) / 2) − (𝐺↑2))
∈ ℝ ∧ 0 ≤ ((((𝑀↑2) / 2) / 2) − (𝐺↑2))) ∧ (((((𝑀↑2) / 2) / 2) −
(𝐻↑2)) ∈ ℝ
∧ 0 ≤ ((((𝑀↑2)
/ 2) / 2) − (𝐻↑2)))) → ((((((𝑀↑2) / 2) / 2) − (𝐺↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐻↑2))) = 0 ↔
(((((𝑀↑2) / 2) / 2)
− (𝐺↑2)) = 0
∧ ((((𝑀↑2) / 2) /
2) − (𝐻↑2)) =
0))) | 
| 116 | 109, 111,
112, 114, 115 | syl22anc 839 | . . . 4
⊢ (𝜑 → ((((((𝑀↑2) / 2) / 2) − (𝐺↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐻↑2))) = 0 ↔
(((((𝑀↑2) / 2) / 2)
− (𝐺↑2)) = 0
∧ ((((𝑀↑2) / 2) /
2) − (𝐻↑2)) =
0))) | 
| 117 | 116 | biimpa 476 | . . 3
⊢ ((𝜑 ∧ (((((𝑀↑2) / 2) / 2) − (𝐺↑2)) + ((((𝑀↑2) / 2) / 2) −
(𝐻↑2))) = 0) →
(((((𝑀↑2) / 2) / 2)
− (𝐺↑2)) = 0
∧ ((((𝑀↑2) / 2) /
2) − (𝐻↑2)) =
0)) | 
| 118 | 108, 117 | syldan 591 | . 2
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → (((((𝑀↑2) / 2) / 2) − (𝐺↑2)) = 0 ∧ ((((𝑀↑2) / 2) / 2) −
(𝐻↑2)) =
0)) | 
| 119 | 100, 118 | jca 511 | 1
⊢ ((𝜑 ∧ 𝑅 = 𝑀) → ((((((𝑀↑2) / 2) / 2) − (𝐸↑2)) = 0 ∧ ((((𝑀↑2) / 2) / 2) −
(𝐹↑2)) = 0) ∧
(((((𝑀↑2) / 2) / 2)
− (𝐺↑2)) = 0
∧ ((((𝑀↑2) / 2) /
2) − (𝐻↑2)) =
0))) |