| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2sqlem4.3 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 2 |  | 2sqlem4.4 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 3 |  | gzreim 16978 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i]) | 
| 4 | 1, 2, 3 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i]) | 
| 5 |  | 2sqlem4.5 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℤ) | 
| 6 |  | 2sqlem4.6 | . . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℤ) | 
| 7 |  | gzreim 16978 | . . . . . . . 8
⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i]) | 
| 8 | 5, 6, 7 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i]) | 
| 9 |  | gzmulcl 16977 | . . . . . . 7
⊢ (((𝐴 + (i · 𝐵)) ∈ ℤ[i] ∧ (𝐶 + (i · 𝐷)) ∈ ℤ[i]) → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i]) | 
| 10 | 4, 8, 9 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i]) | 
| 11 |  | gzcn 16971 | . . . . . 6
⊢ (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ) | 
| 12 | 10, 11 | syl 17 | . . . . 5
⊢ (𝜑 → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ) | 
| 13 |  | 2sqlem5.2 | . . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 14 |  | prmnn 16712 | . . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 15 | 13, 14 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 16 | 15 | nncnd 12283 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 17 | 15 | nnne0d 12317 | . . . . 5
⊢ (𝜑 → 𝑃 ≠ 0) | 
| 18 | 12, 16, 17 | divcld 12044 | . . . 4
⊢ (𝜑 → (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℂ) | 
| 19 | 15 | nnred 12282 | . . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℝ) | 
| 20 | 19, 12, 17 | redivd 15269 | . . . . 5
⊢ (𝜑 → (ℜ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃)) | 
| 21 |  | prmz 16713 | . . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) | 
| 22 | 13, 21 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 23 |  | zsqcl 14170 | . . . . . . . . . . . 12
⊢ (𝑃 ∈ ℤ → (𝑃↑2) ∈
ℤ) | 
| 24 | 22, 23 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑃↑2) ∈ ℤ) | 
| 25 |  | 2sqlem5.1 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 26 | 25 | nnzd 12642 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 27 | 26, 24 | zmulcld 12730 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁 · (𝑃↑2)) ∈ ℤ) | 
| 28 |  | dvdsmul2 16317 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑃 · 𝑃)) | 
| 29 | 22, 22, 28 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∥ (𝑃 · 𝑃)) | 
| 30 | 16 | sqvald 14184 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃↑2) = (𝑃 · 𝑃)) | 
| 31 | 29, 30 | breqtrrd 5170 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∥ (𝑃↑2)) | 
| 32 |  | dvdsmul2 16317 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ (𝑃↑2) ∈ ℤ) →
(𝑃↑2) ∥ (𝑁 · (𝑃↑2))) | 
| 33 | 26, 24, 32 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑃↑2) ∥ (𝑁 · (𝑃↑2))) | 
| 34 | 22, 24, 27, 31, 33 | dvdstrd 16333 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∥ (𝑁 · (𝑃↑2))) | 
| 35 |  | gzcn 16971 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ) | 
| 36 | 4, 35 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ) | 
| 37 | 36 | abscld 15476 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘(𝐴 + (i · 𝐵))) ∈ ℝ) | 
| 38 | 37 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘(𝐴 + (i · 𝐵))) ∈ ℂ) | 
| 39 |  | gzcn 16971 | . . . . . . . . . . . . . . . 16
⊢ ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ) | 
| 40 | 8, 39 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ) | 
| 41 | 40 | abscld 15476 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘(𝐶 + (i · 𝐷))) ∈ ℝ) | 
| 42 | 41 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘(𝐶 + (i · 𝐷))) ∈ ℂ) | 
| 43 | 38, 42 | sqmuld 14199 | . . . . . . . . . . . 12
⊢ (𝜑 → (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2) = (((abs‘(𝐴 + (i · 𝐵)))↑2) · ((abs‘(𝐶 + (i · 𝐷)))↑2))) | 
| 44 | 1 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 45 | 2 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 46 | 44, 45 | crred 15271 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴) | 
| 47 | 46 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2)) | 
| 48 | 44, 45 | crimd 15272 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵) | 
| 49 | 48 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2)) | 
| 50 | 47, 49 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2))) | 
| 51 | 36 | absvalsq2d 15483 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2))) | 
| 52 |  | 2sqlem4.7 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2))) | 
| 53 | 50, 51, 52 | 3eqtr4d 2786 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (𝑁 · 𝑃)) | 
| 54 | 5 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 55 | 6 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 56 | 54, 55 | crred 15271 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶) | 
| 57 | 56 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2)) | 
| 58 | 54, 55 | crimd 15272 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷) | 
| 59 | 58 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2)) | 
| 60 | 57, 59 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2))) | 
| 61 | 40 | absvalsq2d 15483 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2))) | 
| 62 |  | 2sqlem4.8 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2))) | 
| 63 | 60, 61, 62 | 3eqtr4d 2786 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = 𝑃) | 
| 64 | 53, 63 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) · ((abs‘(𝐶 + (i · 𝐷)))↑2)) = ((𝑁 · 𝑃) · 𝑃)) | 
| 65 | 25 | nncnd 12283 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 66 | 65, 16, 16 | mulassd 11285 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 · 𝑃) · 𝑃) = (𝑁 · (𝑃 · 𝑃))) | 
| 67 | 43, 64, 66 | 3eqtrd 2780 | . . . . . . . . . . 11
⊢ (𝜑 → (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2) = (𝑁 · (𝑃 · 𝑃))) | 
| 68 | 36, 40 | absmuld 15494 | . . . . . . . . . . . 12
⊢ (𝜑 → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = ((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))) | 
| 69 | 68 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2)) | 
| 70 | 30 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁 · (𝑃↑2)) = (𝑁 · (𝑃 · 𝑃))) | 
| 71 | 67, 69, 70 | 3eqtr4d 2786 | . . . . . . . . . 10
⊢ (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (𝑁 · (𝑃↑2))) | 
| 72 | 34, 71 | breqtrrd 5170 | . . . . . . . . 9
⊢ (𝜑 → 𝑃 ∥ ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)) | 
| 73 | 12 | absvalsq2d 15483 | . . . . . . . . . 10
⊢ (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))) | 
| 74 |  | elgz 16970 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] ↔ (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ ∧
(ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) ∈ ℤ ∧
(ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) ∈
ℤ)) | 
| 75 | 74 | simp2bi 1146 | . . . . . . . . . . . . . 14
⊢ (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] →
(ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) ∈
ℤ) | 
| 76 | 10, 75 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ) | 
| 77 |  | zsqcl 14170 | . . . . . . . . . . . . 13
⊢
((ℜ‘((𝐴 +
(i · 𝐵)) ·
(𝐶 + (i · 𝐷)))) ∈ ℤ →
((ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷))))↑2) ∈
ℤ) | 
| 78 | 76, 77 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈
ℤ) | 
| 79 | 78 | zcnd 12725 | . . . . . . . . . . 11
⊢ (𝜑 → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈
ℂ) | 
| 80 | 74 | simp3bi 1147 | . . . . . . . . . . . . . 14
⊢ (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] →
(ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) ∈
ℤ) | 
| 81 | 10, 80 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ) | 
| 82 |  | zsqcl 14170 | . . . . . . . . . . . . 13
⊢
((ℑ‘((𝐴
+ (i · 𝐵)) ·
(𝐶 + (i · 𝐷)))) ∈ ℤ →
((ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷))))↑2) ∈
ℤ) | 
| 83 | 81, 82 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈
ℤ) | 
| 84 | 83 | zcnd 12725 | . . . . . . . . . . 11
⊢ (𝜑 → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈
ℂ) | 
| 85 | 79, 84 | addcomd 11464 | . . . . . . . . . 10
⊢ (𝜑 → (((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)) = (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))) | 
| 86 | 73, 85 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))) | 
| 87 | 72, 86 | breqtrd 5168 | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∥ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))) | 
| 88 |  | 2sqlem4.9 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) | 
| 89 | 5 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 90 | 2 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 91 | 89, 90 | mulcld 11282 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 · 𝐵) ∈ ℂ) | 
| 92 | 1 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 93 | 6 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 94 | 92, 93 | mulcld 11282 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℂ) | 
| 95 | 91, 94 | addcomd 11464 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 · 𝐵) + (𝐴 · 𝐷)) = ((𝐴 · 𝐷) + (𝐶 · 𝐵))) | 
| 96 | 89, 90 | mulcomd 11283 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶)) | 
| 97 | 96 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶))) | 
| 98 | 95, 97 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 · 𝐵) + (𝐴 · 𝐷)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶))) | 
| 99 | 88, 98 | breqtrd 5168 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∥ ((𝐴 · 𝐷) + (𝐵 · 𝐶))) | 
| 100 | 36, 40 | immuld 15259 | . . . . . . . . . . . 12
⊢ (𝜑 → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = (((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) + ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷)))))) | 
| 101 | 46, 58 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) = (𝐴 · 𝐷)) | 
| 102 | 48, 56 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷)))) = (𝐵 · 𝐶)) | 
| 103 | 101, 102 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) + ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷))))) = ((𝐴 · 𝐷) + (𝐵 · 𝐶))) | 
| 104 | 100, 103 | eqtrd 2776 | . . . . . . . . . . 11
⊢ (𝜑 → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = ((𝐴 · 𝐷) + (𝐵 · 𝐶))) | 
| 105 | 99, 104 | breqtrrd 5170 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))) | 
| 106 |  | 2nn 12340 | . . . . . . . . . . . 12
⊢ 2 ∈
ℕ | 
| 107 | 106 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℕ) | 
| 108 |  | prmdvdsexp 16753 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧
(ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) ∈ ℤ ∧ 2
∈ ℕ) → (𝑃
∥ ((ℑ‘((𝐴
+ (i · 𝐵)) ·
(𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))))) | 
| 109 | 13, 81, 107, 108 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → (𝑃 ∥ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))))) | 
| 110 | 105, 109 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → 𝑃 ∥ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)) | 
| 111 |  | dvdsadd2b 16344 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧
((ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷))))↑2) ∈ ℤ
∧ (((ℑ‘((𝐴
+ (i · 𝐵)) ·
(𝐶 + (i · 𝐷))))↑2) ∈ ℤ
∧ 𝑃 ∥
((ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷))))↑2))) → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)))) | 
| 112 | 22, 78, 83, 110, 111 | syl112anc 1375 | . . . . . . . 8
⊢ (𝜑 → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)))) | 
| 113 | 87, 112 | mpbird 257 | . . . . . . 7
⊢ (𝜑 → 𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)) | 
| 114 |  | prmdvdsexp 16753 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧
(ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) ∈ ℤ ∧ 2
∈ ℕ) → (𝑃
∥ ((ℜ‘((𝐴
+ (i · 𝐵)) ·
(𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))))) | 
| 115 | 13, 76, 107, 114 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))))) | 
| 116 | 113, 115 | mpbid 232 | . . . . . 6
⊢ (𝜑 → 𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))) | 
| 117 |  | dvdsval2 16294 | . . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧
(ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) ∈ ℤ) →
(𝑃 ∥
(ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) ↔
((ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ)) | 
| 118 | 22, 17, 76, 117 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ↔ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ)) | 
| 119 | 116, 118 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ) | 
| 120 | 20, 119 | eqeltrd 2840 | . . . 4
⊢ (𝜑 → (ℜ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ) | 
| 121 | 19, 12, 17 | imdivd 15270 | . . . . 5
⊢ (𝜑 → (ℑ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃)) | 
| 122 |  | dvdsval2 16294 | . . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧
(ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) ∈ ℤ) →
(𝑃 ∥
(ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) ↔
((ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ)) | 
| 123 | 22, 17, 81, 122 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ↔ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ)) | 
| 124 | 105, 123 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ) | 
| 125 | 121, 124 | eqeltrd 2840 | . . . 4
⊢ (𝜑 → (ℑ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ) | 
| 126 |  | elgz 16970 | . . . 4
⊢ ((((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℤ[i] ↔ ((((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℂ ∧
(ℜ‘(((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ ∧
(ℑ‘(((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ)) | 
| 127 | 18, 120, 125, 126 | syl3anbrc 1343 | . . 3
⊢ (𝜑 → (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℤ[i]) | 
| 128 | 12, 16, 17 | absdivd 15495 | . . . . . 6
⊢ (𝜑 → (abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / (abs‘𝑃))) | 
| 129 | 15 | nnnn0d 12589 | . . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈
ℕ0) | 
| 130 | 129 | nn0ge0d 12592 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ 𝑃) | 
| 131 | 19, 130 | absidd 15462 | . . . . . . 7
⊢ (𝜑 → (abs‘𝑃) = 𝑃) | 
| 132 | 131 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / (abs‘𝑃)) = ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃)) | 
| 133 | 128, 132 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → (abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃)) | 
| 134 | 133 | oveq1d 7447 | . . . 4
⊢ (𝜑 → ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2) = (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃)↑2)) | 
| 135 | 12 | abscld 15476 | . . . . . 6
⊢ (𝜑 → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℝ) | 
| 136 | 135 | recnd 11290 | . . . . 5
⊢ (𝜑 → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℂ) | 
| 137 | 136, 16, 17 | sqdivd 14200 | . . . 4
⊢ (𝜑 → (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃)↑2) = (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) / (𝑃↑2))) | 
| 138 | 71 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) / (𝑃↑2)) = ((𝑁 · (𝑃↑2)) / (𝑃↑2))) | 
| 139 | 15 | nnsqcld 14284 | . . . . . . 7
⊢ (𝜑 → (𝑃↑2) ∈ ℕ) | 
| 140 | 139 | nncnd 12283 | . . . . . 6
⊢ (𝜑 → (𝑃↑2) ∈ ℂ) | 
| 141 | 139 | nnne0d 12317 | . . . . . 6
⊢ (𝜑 → (𝑃↑2) ≠ 0) | 
| 142 | 65, 140, 141 | divcan4d 12050 | . . . . 5
⊢ (𝜑 → ((𝑁 · (𝑃↑2)) / (𝑃↑2)) = 𝑁) | 
| 143 | 138, 142 | eqtrd 2776 | . . . 4
⊢ (𝜑 → (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) / (𝑃↑2)) = 𝑁) | 
| 144 | 134, 137,
143 | 3eqtrrd 2781 | . . 3
⊢ (𝜑 → 𝑁 = ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2)) | 
| 145 |  | fveq2 6905 | . . . . 5
⊢ (𝑥 = (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) → (abs‘𝑥) = (abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))) | 
| 146 | 145 | oveq1d 7447 | . . . 4
⊢ (𝑥 = (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) → ((abs‘𝑥)↑2) = ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2)) | 
| 147 | 146 | rspceeqv 3644 | . . 3
⊢
(((((𝐴 + (i ·
𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℤ[i] ∧ 𝑁 = ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2)) → ∃𝑥 ∈ ℤ[i] 𝑁 = ((abs‘𝑥)↑2)) | 
| 148 | 127, 144,
147 | syl2anc 584 | . 2
⊢ (𝜑 → ∃𝑥 ∈ ℤ[i] 𝑁 = ((abs‘𝑥)↑2)) | 
| 149 |  | 2sq.1 | . . 3
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) | 
| 150 | 149 | 2sqlem1 27462 | . 2
⊢ (𝑁 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ[i] 𝑁 = ((abs‘𝑥)↑2)) | 
| 151 | 148, 150 | sylibr 234 | 1
⊢ (𝜑 → 𝑁 ∈ 𝑆) |