Proof of Theorem quart1lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | quart1.c | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 2 |  | quart1.a | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 3 |  | quart1.b | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 4 | 2, 3 | mulcld 11281 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) | 
| 5 | 4 | halfcld 12511 | . . . . . . . . 9
⊢ (𝜑 → ((𝐴 · 𝐵) / 2) ∈ ℂ) | 
| 6 | 1, 5 | subcld 11620 | . . . . . . . 8
⊢ (𝜑 → (𝐶 − ((𝐴 · 𝐵) / 2)) ∈ ℂ) | 
| 7 |  | 3nn0 12544 | . . . . . . . . . 10
⊢ 3 ∈
ℕ0 | 
| 8 |  | expcl 14120 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℂ) | 
| 9 | 2, 7, 8 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → (𝐴↑3) ∈ ℂ) | 
| 10 |  | 8cn 12363 | . . . . . . . . . 10
⊢ 8 ∈
ℂ | 
| 11 | 10 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 8 ∈
ℂ) | 
| 12 |  | 8nn 12361 | . . . . . . . . . . 11
⊢ 8 ∈
ℕ | 
| 13 | 12 | nnne0i 12306 | . . . . . . . . . 10
⊢ 8 ≠
0 | 
| 14 | 13 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 8 ≠ 0) | 
| 15 | 9, 11, 14 | divcld 12043 | . . . . . . . 8
⊢ (𝜑 → ((𝐴↑3) / 8) ∈
ℂ) | 
| 16 |  | 4cn 12351 | . . . . . . . . . 10
⊢ 4 ∈
ℂ | 
| 17 | 16 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 4 ∈
ℂ) | 
| 18 |  | 4ne0 12374 | . . . . . . . . . 10
⊢ 4 ≠
0 | 
| 19 | 18 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 4 ≠ 0) | 
| 20 | 2, 17, 19 | divcld 12043 | . . . . . . . 8
⊢ (𝜑 → (𝐴 / 4) ∈ ℂ) | 
| 21 | 6, 15, 20 | adddird 11286 | . . . . . . 7
⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) · (𝐴 / 4)) = (((𝐶 − ((𝐴 · 𝐵) / 2)) · (𝐴 / 4)) + (((𝐴↑3) / 8) · (𝐴 / 4)))) | 
| 22 |  | quart1.q | . . . . . . . 8
⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) | 
| 23 | 22 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → (𝑄 · (𝐴 / 4)) = (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) · (𝐴 / 4))) | 
| 24 | 1, 2, 17, 19 | divassd 12078 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐶 · 𝐴) / 4) = (𝐶 · (𝐴 / 4))) | 
| 25 | 2 | sqvald 14183 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) | 
| 26 | 25 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴↑2) · 𝐵) = ((𝐴 · 𝐴) · 𝐵)) | 
| 27 | 2, 2, 3 | mul32d 11471 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 · 𝐴) · 𝐵) = ((𝐴 · 𝐵) · 𝐴)) | 
| 28 | 26, 27 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴↑2) · 𝐵) = ((𝐴 · 𝐵) · 𝐴)) | 
| 29 | 28 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴↑2) · 𝐵) / 8) = (((𝐴 · 𝐵) · 𝐴) / 8)) | 
| 30 |  | 2cn 12341 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ | 
| 31 |  | 4t2e8 12434 | . . . . . . . . . . . . . 14
⊢ (4
· 2) = 8 | 
| 32 | 16, 30, 31 | mulcomli 11270 | . . . . . . . . . . . . 13
⊢ (2
· 4) = 8 | 
| 33 | 32 | oveq2i 7442 | . . . . . . . . . . . 12
⊢ (((𝐴 · 𝐵) · 𝐴) / (2 · 4)) = (((𝐴 · 𝐵) · 𝐴) / 8) | 
| 34 | 29, 33 | eqtr4di 2795 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐴↑2) · 𝐵) / 8) = (((𝐴 · 𝐵) · 𝐴) / (2 · 4))) | 
| 35 | 30 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℂ) | 
| 36 |  | 2ne0 12370 | . . . . . . . . . . . . 13
⊢ 2 ≠
0 | 
| 37 | 36 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 2 ≠ 0) | 
| 38 | 4, 35, 2, 17, 37, 19 | divmuldivd 12084 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐴 · 𝐵) / 2) · (𝐴 / 4)) = (((𝐴 · 𝐵) · 𝐴) / (2 · 4))) | 
| 39 | 34, 38 | eqtr4d 2780 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐴↑2) · 𝐵) / 8) = (((𝐴 · 𝐵) / 2) · (𝐴 / 4))) | 
| 40 | 24, 39 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝜑 → (((𝐶 · 𝐴) / 4) − (((𝐴↑2) · 𝐵) / 8)) = ((𝐶 · (𝐴 / 4)) − (((𝐴 · 𝐵) / 2) · (𝐴 / 4)))) | 
| 41 | 1, 5, 20 | subdird 11720 | . . . . . . . . 9
⊢ (𝜑 → ((𝐶 − ((𝐴 · 𝐵) / 2)) · (𝐴 / 4)) = ((𝐶 · (𝐴 / 4)) − (((𝐴 · 𝐵) / 2) · (𝐴 / 4)))) | 
| 42 | 40, 41 | eqtr4d 2780 | . . . . . . . 8
⊢ (𝜑 → (((𝐶 · 𝐴) / 4) − (((𝐴↑2) · 𝐵) / 8)) = ((𝐶 − ((𝐴 · 𝐵) / 2)) · (𝐴 / 4))) | 
| 43 |  | df-4 12331 | . . . . . . . . . . . . . 14
⊢ 4 = (3 +
1) | 
| 44 | 43 | oveq2i 7442 | . . . . . . . . . . . . 13
⊢ (𝐴↑4) = (𝐴↑(3 + 1)) | 
| 45 |  | expp1 14109 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝐴↑(3 + 1)) = ((𝐴↑3) · 𝐴)) | 
| 46 | 2, 7, 45 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴↑(3 + 1)) = ((𝐴↑3) · 𝐴)) | 
| 47 | 44, 46 | eqtrid 2789 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴↑4) = ((𝐴↑3) · 𝐴)) | 
| 48 | 47 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴↑4) / 8) = (((𝐴↑3) · 𝐴) / 8)) | 
| 49 | 9, 2, 11, 14 | div23d 12080 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐴↑3) · 𝐴) / 8) = (((𝐴↑3) / 8) · 𝐴)) | 
| 50 | 48, 49 | eqtrd 2777 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴↑4) / 8) = (((𝐴↑3) / 8) · 𝐴)) | 
| 51 | 50 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝜑 → (((𝐴↑4) / 8) / 4) = ((((𝐴↑3) / 8) · 𝐴) / 4)) | 
| 52 | 15, 2, 17, 19 | divassd 12078 | . . . . . . . . 9
⊢ (𝜑 → ((((𝐴↑3) / 8) · 𝐴) / 4) = (((𝐴↑3) / 8) · (𝐴 / 4))) | 
| 53 | 51, 52 | eqtrd 2777 | . . . . . . . 8
⊢ (𝜑 → (((𝐴↑4) / 8) / 4) = (((𝐴↑3) / 8) · (𝐴 / 4))) | 
| 54 | 42, 53 | oveq12d 7449 | . . . . . . 7
⊢ (𝜑 → ((((𝐶 · 𝐴) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (((𝐴↑4) / 8) / 4)) = (((𝐶 − ((𝐴 · 𝐵) / 2)) · (𝐴 / 4)) + (((𝐴↑3) / 8) · (𝐴 / 4)))) | 
| 55 | 21, 23, 54 | 3eqtr4d 2787 | . . . . . 6
⊢ (𝜑 → (𝑄 · (𝐴 / 4)) = ((((𝐶 · 𝐴) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (((𝐴↑4) / 8) / 4))) | 
| 56 | 1, 2 | mulcld 11281 | . . . . . . . 8
⊢ (𝜑 → (𝐶 · 𝐴) ∈ ℂ) | 
| 57 | 56, 17, 19 | divcld 12043 | . . . . . . 7
⊢ (𝜑 → ((𝐶 · 𝐴) / 4) ∈ ℂ) | 
| 58 | 2 | sqcld 14184 | . . . . . . . . 9
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) | 
| 59 | 58, 3 | mulcld 11281 | . . . . . . . 8
⊢ (𝜑 → ((𝐴↑2) · 𝐵) ∈ ℂ) | 
| 60 | 59, 11, 14 | divcld 12043 | . . . . . . 7
⊢ (𝜑 → (((𝐴↑2) · 𝐵) / 8) ∈ ℂ) | 
| 61 |  | 4nn0 12545 | . . . . . . . . . 10
⊢ 4 ∈
ℕ0 | 
| 62 |  | expcl 14120 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℂ) | 
| 63 | 2, 61, 62 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → (𝐴↑4) ∈ ℂ) | 
| 64 | 63, 11, 14 | divcld 12043 | . . . . . . . 8
⊢ (𝜑 → ((𝐴↑4) / 8) ∈
ℂ) | 
| 65 | 64, 17, 19 | divcld 12043 | . . . . . . 7
⊢ (𝜑 → (((𝐴↑4) / 8) / 4) ∈
ℂ) | 
| 66 | 57, 60, 65 | subadd23d 11642 | . . . . . 6
⊢ (𝜑 → ((((𝐶 · 𝐴) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (((𝐴↑4) / 8) / 4)) = (((𝐶 · 𝐴) / 4) + ((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)))) | 
| 67 | 65, 60 | subcld 11620 | . . . . . . 7
⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) ∈
ℂ) | 
| 68 | 57, 67 | addcomd 11463 | . . . . . 6
⊢ (𝜑 → (((𝐶 · 𝐴) / 4) + ((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8))) = (((((𝐴↑4) / 8) / 4) −
(((𝐴↑2) · 𝐵) / 8)) + ((𝐶 · 𝐴) / 4))) | 
| 69 | 55, 66, 68 | 3eqtrd 2781 | . . . . 5
⊢ (𝜑 → (𝑄 · (𝐴 / 4)) = (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((𝐶 · 𝐴) / 4))) | 
| 70 |  | quart1.r | . . . . . 6
⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))) | 
| 71 |  | quart1.d | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 72 |  | 1nn0 12542 | . . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 | 
| 73 |  | 6nn 12355 | . . . . . . . . . . . 12
⊢ 6 ∈
ℕ | 
| 74 | 72, 73 | decnncl 12753 | . . . . . . . . . . 11
⊢ ;16 ∈ ℕ | 
| 75 | 74 | nncni 12276 | . . . . . . . . . 10
⊢ ;16 ∈ ℂ | 
| 76 | 75 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ;16 ∈ ℂ) | 
| 77 | 74 | nnne0i 12306 | . . . . . . . . . 10
⊢ ;16 ≠ 0 | 
| 78 | 77 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ;16 ≠ 0) | 
| 79 | 59, 76, 78 | divcld 12043 | . . . . . . . 8
⊢ (𝜑 → (((𝐴↑2) · 𝐵) / ;16) ∈ ℂ) | 
| 80 |  | 3cn 12347 | . . . . . . . . . 10
⊢ 3 ∈
ℂ | 
| 81 |  | 2nn0 12543 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 | 
| 82 |  | 5nn0 12546 | . . . . . . . . . . . . 13
⊢ 5 ∈
ℕ0 | 
| 83 | 81, 82 | deccl 12748 | . . . . . . . . . . . 12
⊢ ;25 ∈
ℕ0 | 
| 84 | 83, 73 | decnncl 12753 | . . . . . . . . . . 11
⊢ ;;256 ∈ ℕ | 
| 85 | 84 | nncni 12276 | . . . . . . . . . 10
⊢ ;;256 ∈ ℂ | 
| 86 | 84 | nnne0i 12306 | . . . . . . . . . 10
⊢ ;;256 ≠ 0 | 
| 87 | 80, 85, 86 | divcli 12009 | . . . . . . . . 9
⊢ (3 /
;;256) ∈ ℂ | 
| 88 |  | mulcl 11239 | . . . . . . . . 9
⊢ (((3 /
;;256) ∈ ℂ ∧ (𝐴↑4) ∈ ℂ) → ((3 / ;;256) · (𝐴↑4)) ∈ ℂ) | 
| 89 | 87, 63, 88 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → ((3 / ;;256)
· (𝐴↑4)) ∈
ℂ) | 
| 90 | 79, 89 | subcld 11620 | . . . . . . 7
⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4)))
∈ ℂ) | 
| 91 | 71, 90, 57 | addsubd 11641 | . . . . . 6
⊢ (𝜑 → ((𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))
− ((𝐶 · 𝐴) / 4)) = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))) | 
| 92 | 70, 91 | eqtr4d 2780 | . . . . 5
⊢ (𝜑 → 𝑅 = ((𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))
− ((𝐶 · 𝐴) / 4))) | 
| 93 | 69, 92 | oveq12d 7449 | . . . 4
⊢ (𝜑 → ((𝑄 · (𝐴 / 4)) + 𝑅) = ((((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((𝐶 · 𝐴) / 4)) + ((𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))
− ((𝐶 · 𝐴) / 4)))) | 
| 94 | 71, 90 | addcld 11280 | . . . . 5
⊢ (𝜑 → (𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))
∈ ℂ) | 
| 95 | 67, 57, 94 | ppncand 11660 | . . . 4
⊢ (𝜑 → ((((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((𝐶 · 𝐴) / 4)) + ((𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))
− ((𝐶 · 𝐴) / 4))) = (((((𝐴↑4) / 8) / 4) −
(((𝐴↑2) · 𝐵) / 8)) + (𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4)))))) | 
| 96 | 67, 71, 90 | add12d 11488 | . . . . 5
⊢ (𝜑 → (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))) =
(𝐷 + (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4)))))) | 
| 97 | 60, 89 | addcld 11280 | . . . . . . . 8
⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256)
· (𝐴↑4)))
∈ ℂ) | 
| 98 | 65, 79 | addcld 11280 | . . . . . . . 8
⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16)) ∈ ℂ) | 
| 99 | 97, 98 | negsubdi2d 11636 | . . . . . . 7
⊢ (𝜑 → -(((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256)
· (𝐴↑4)))
− ((((𝐴↑4) / 8)
/ 4) + (((𝐴↑2)
· 𝐵) / ;16))) = (((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16)) − ((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256)
· (𝐴↑4))))) | 
| 100 | 65, 79 | addcomd 11463 | . . . . . . . . . 10
⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16)) = ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑4) / 8) / 4))) | 
| 101 | 100 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → (((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256)
· (𝐴↑4)))
− ((((𝐴↑4) / 8)
/ 4) + (((𝐴↑2)
· 𝐵) / ;16))) = (((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256)
· (𝐴↑4)))
− ((((𝐴↑2)
· 𝐵) / ;16) + (((𝐴↑4) / 8) / 4)))) | 
| 102 | 60, 89, 79, 65 | addsub4d 11667 | . . . . . . . . 9
⊢ (𝜑 → (((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256)
· (𝐴↑4)))
− ((((𝐴↑2)
· 𝐵) / ;16) + (((𝐴↑4) / 8) / 4))) = (((((𝐴↑2) · 𝐵) / 8) − (((𝐴↑2) · 𝐵) / ;16)) + (((3 / ;;256)
· (𝐴↑4))
− (((𝐴↑4) / 8) /
4)))) | 
| 103 | 80 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 3 ∈
ℂ) | 
| 104 | 85 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ;;256
∈ ℂ) | 
| 105 | 86 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ;;256
≠ 0) | 
| 106 | 103, 63, 104, 105 | divassd 12078 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((3 · (𝐴↑4)) / ;;256) =
(3 · ((𝐴↑4) /
;;256))) | 
| 107 | 103, 63, 104, 105 | div23d 12080 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((3 · (𝐴↑4)) / ;;256) =
((3 / ;;256) · (𝐴↑4))) | 
| 108 |  | 1p2e3 12409 | . . . . . . . . . . . . . . . . . 18
⊢ (1 + 2) =
3 | 
| 109 | 108 | oveq1i 7441 | . . . . . . . . . . . . . . . . 17
⊢ ((1 + 2)
· ((𝐴↑4) /
;;256)) = (3 · ((𝐴↑4) / ;;256)) | 
| 110 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℂ) | 
| 111 | 63, 104, 105 | divcld 12043 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐴↑4) / ;;256)
∈ ℂ) | 
| 112 | 110, 35, 111 | adddird 11286 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + 2) · ((𝐴↑4) / ;;256))
= ((1 · ((𝐴↑4)
/ ;;256)) + (2 · ((𝐴↑4) / ;;256)))) | 
| 113 | 109, 112 | eqtr3id 2791 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (3 · ((𝐴↑4) / ;;256))
= ((1 · ((𝐴↑4)
/ ;;256)) + (2 · ((𝐴↑4) / ;;256)))) | 
| 114 | 111 | mullidd 11279 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 · ((𝐴↑4) / ;;256))
= ((𝐴↑4) / ;;256)) | 
| 115 | 114 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1 · ((𝐴↑4) / ;;256))
+ (2 · ((𝐴↑4) /
;;256))) = (((𝐴↑4) / ;;256) +
(2 · ((𝐴↑4) /
;;256)))) | 
| 116 | 113, 115 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (3 · ((𝐴↑4) / ;;256))
= (((𝐴↑4) / ;;256) + (2 · ((𝐴↑4) / ;;256)))) | 
| 117 | 106, 107,
116 | 3eqtr3d 2785 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((3 / ;;256)
· (𝐴↑4)) =
(((𝐴↑4) / ;;256) + (2 · ((𝐴↑4) / ;;256)))) | 
| 118 | 43 | oveq1i 7441 | . . . . . . . . . . . . . . . 16
⊢ (4
· ((((𝐴↑4) / 8)
/ 4) / 4)) = ((3 + 1) · ((((𝐴↑4) / 8) / 4) / 4)) | 
| 119 | 65, 17, 19 | divcld 12043 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) / 4) ∈
ℂ) | 
| 120 | 103, 110,
119 | adddird 11286 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((3 + 1) ·
((((𝐴↑4) / 8) / 4) /
4)) = ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (1 ·
((((𝐴↑4) / 8) / 4) /
4)))) | 
| 121 | 118, 120 | eqtrid 2789 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (4 · ((((𝐴↑4) / 8) / 4) / 4)) = ((3
· ((((𝐴↑4) / 8)
/ 4) / 4)) + (1 · ((((𝐴↑4) / 8) / 4) / 4)))) | 
| 122 | 65, 17, 19 | divcan2d 12045 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (4 · ((((𝐴↑4) / 8) / 4) / 4)) =
(((𝐴↑4) / 8) /
4)) | 
| 123 | 119 | mullidd 11279 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 · ((((𝐴↑4) / 8) / 4) / 4)) =
((((𝐴↑4) / 8) / 4) /
4)) | 
| 124 | 64, 17, 17, 19, 19 | divdiv1d 12074 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) / 4) = (((𝐴↑4) / 8) / (4 ·
4))) | 
| 125 |  | 4t4e16 12832 | . . . . . . . . . . . . . . . . . . 19
⊢ (4
· 4) = ;16 | 
| 126 | 125 | oveq2i 7442 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴↑4) / 8) / (4 · 4))
= (((𝐴↑4) / 8) / ;16) | 
| 127 | 124, 126 | eqtrdi 2793 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) / 4) = (((𝐴↑4) / 8) / ;16)) | 
| 128 | 63, 11, 76, 14, 78 | divdiv1d 12074 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝐴↑4) / 8) / ;16) = ((𝐴↑4) / (8 · ;16))) | 
| 129 | 10, 75 | mulcli 11268 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (8
· ;16) ∈
ℂ | 
| 130 | 129 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (8 · ;16) ∈ ℂ) | 
| 131 | 10, 75, 13, 77 | mulne0i 11906 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (8
· ;16) ≠
0 | 
| 132 | 131 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (8 · ;16) ≠ 0) | 
| 133 | 63, 130, 132 | divcld 12043 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐴↑4) / (8 · ;16)) ∈ ℂ) | 
| 134 | 133, 35, 37 | divcan2d 12045 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 · (((𝐴↑4) / (8 · ;16)) / 2)) = ((𝐴↑4) / (8 · ;16))) | 
| 135 | 63, 130, 35, 132, 37 | divdiv1d 12074 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐴↑4) / (8 · ;16)) / 2) = ((𝐴↑4) / ((8 · ;16) · 2))) | 
| 136 | 10, 75, 30 | mul32i 11457 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((8
· ;16) · 2) = ((8
· 2) · ;16) | 
| 137 |  | 2exp4 17122 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(2↑4) = ;16 | 
| 138 |  | 8t2e16 12848 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (8
· 2) = ;16 | 
| 139 | 137, 138 | eqtr4i 2768 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2↑4) = (8 · 2) | 
| 140 | 139, 137 | oveq12i 7443 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((2↑4) · (2↑4)) = ((8 · 2) · ;16) | 
| 141 |  | 4p4e8 12421 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (4 + 4) =
8 | 
| 142 | 141 | oveq2i 7442 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2↑(4 + 4)) = (2↑8) | 
| 143 |  | expadd 14145 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
∈ ℂ ∧ 4 ∈ ℕ0 ∧ 4 ∈
ℕ0) → (2↑(4 + 4)) = ((2↑4) ·
(2↑4))) | 
| 144 | 30, 61, 61, 143 | mp3an 1463 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2↑(4 + 4)) = ((2↑4) · (2↑4)) | 
| 145 |  | 2exp8 17126 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2↑8) = ;;256 | 
| 146 | 142, 144,
145 | 3eqtr3i 2773 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((2↑4) · (2↑4)) = ;;256 | 
| 147 | 136, 140,
146 | 3eqtr2i 2771 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((8
· ;16) · 2) = ;;256 | 
| 148 | 147 | oveq2i 7442 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴↑4) / ((8 · ;16) · 2)) = ((𝐴↑4) / ;;256) | 
| 149 | 135, 148 | eqtrdi 2793 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((𝐴↑4) / (8 · ;16)) / 2) = ((𝐴↑4) / ;;256)) | 
| 150 | 149 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 · (((𝐴↑4) / (8 · ;16)) / 2)) = (2 · ((𝐴↑4) / ;;256))) | 
| 151 | 128, 134,
150 | 3eqtr2d 2783 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐴↑4) / 8) / ;16) = (2 · ((𝐴↑4) / ;;256))) | 
| 152 | 123, 127,
151 | 3eqtrd 2781 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 · ((((𝐴↑4) / 8) / 4) / 4)) = (2
· ((𝐴↑4) /
;;256))) | 
| 153 | 152 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (1
· ((((𝐴↑4) / 8)
/ 4) / 4))) = ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (2 ·
((𝐴↑4) / ;;256)))) | 
| 154 | 121, 122,
153 | 3eqtr3d 2785 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴↑4) / 8) / 4) = ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (2
· ((𝐴↑4) /
;;256)))) | 
| 155 | 117, 154 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((3 / ;;256)
· (𝐴↑4))
− (((𝐴↑4) / 8) /
4)) = ((((𝐴↑4) / ;;256) + (2 · ((𝐴↑4) / ;;256)))
− ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (2 ·
((𝐴↑4) / ;;256))))) | 
| 156 |  | mulcl 11239 | . . . . . . . . . . . . . . 15
⊢ ((3
∈ ℂ ∧ ((((𝐴↑4) / 8) / 4) / 4) ∈ ℂ)
→ (3 · ((((𝐴↑4) / 8) / 4) / 4)) ∈
ℂ) | 
| 157 | 80, 119, 156 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (3 · ((((𝐴↑4) / 8) / 4) / 4)) ∈
ℂ) | 
| 158 |  | mulcl 11239 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ ((𝐴↑4) / ;;256)
∈ ℂ) → (2 · ((𝐴↑4) / ;;256))
∈ ℂ) | 
| 159 | 30, 111, 158 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · ((𝐴↑4) / ;;256))
∈ ℂ) | 
| 160 | 111, 157,
159 | pnpcan2d 11658 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐴↑4) / ;;256) +
(2 · ((𝐴↑4) /
;;256))) − ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (2 ·
((𝐴↑4) / ;;256)))) = (((𝐴↑4) / ;;256)
− (3 · ((((𝐴↑4) / 8) / 4) / 4)))) | 
| 161 | 155, 160 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝜑 → (((3 / ;;256)
· (𝐴↑4))
− (((𝐴↑4) / 8) /
4)) = (((𝐴↑4) / ;;256) − (3 · ((((𝐴↑4) / 8) / 4) / 4)))) | 
| 162 | 161 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / ;16) + (((3 / ;;256)
· (𝐴↑4))
− (((𝐴↑4) / 8) /
4))) = ((((𝐴↑2)
· 𝐵) / ;16) + (((𝐴↑4) / ;;256)
− (3 · ((((𝐴↑4) / 8) / 4) / 4))))) | 
| 163 | 79, 111, 157 | addsub12d 11643 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑4) / ;;256)
− (3 · ((((𝐴↑4) / 8) / 4) / 4)))) = (((𝐴↑4) / ;;256) +
((((𝐴↑2) ·
𝐵) / ;16) − (3 · ((((𝐴↑4) / 8) / 4) / 4))))) | 
| 164 | 162, 163 | eqtrd 2777 | . . . . . . . . . 10
⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / ;16) + (((3 / ;;256)
· (𝐴↑4))
− (((𝐴↑4) / 8) /
4))) = (((𝐴↑4) / ;;256) + ((((𝐴↑2) · 𝐵) / ;16) − (3 · ((((𝐴↑4) / 8) / 4) / 4))))) | 
| 165 | 59, 11, 35, 14, 37 | divdiv1d 12074 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / 8) / 2) = (((𝐴↑2) · 𝐵) / (8 · 2))) | 
| 166 | 138 | oveq2i 7442 | . . . . . . . . . . . . . . 15
⊢ (((𝐴↑2) · 𝐵) / (8 · 2)) = (((𝐴↑2) · 𝐵) / ;16) | 
| 167 | 165, 166 | eqtrdi 2793 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / 8) / 2) = (((𝐴↑2) · 𝐵) / ;16)) | 
| 168 | 167 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 · ((((𝐴↑2) · 𝐵) / 8) / 2)) = (2 ·
(((𝐴↑2) · 𝐵) / ;16))) | 
| 169 | 60, 35, 37 | divcan2d 12045 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 · ((((𝐴↑2) · 𝐵) / 8) / 2)) = (((𝐴↑2) · 𝐵) / 8)) | 
| 170 | 79 | 2timesd 12509 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (((𝐴↑2) · 𝐵) / ;16)) = ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑2) · 𝐵) / ;16))) | 
| 171 | 168, 169,
170 | 3eqtr3d 2785 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴↑2) · 𝐵) / 8) = ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑2) · 𝐵) / ;16))) | 
| 172 | 79, 79, 171 | mvrladdd 11676 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / 8) − (((𝐴↑2) · 𝐵) / ;16)) = (((𝐴↑2) · 𝐵) / ;16)) | 
| 173 | 172 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝜑 → (((((𝐴↑2) · 𝐵) / 8) − (((𝐴↑2) · 𝐵) / ;16)) + (((3 / ;;256)
· (𝐴↑4))
− (((𝐴↑4) / 8) /
4))) = ((((𝐴↑2)
· 𝐵) / ;16) + (((3 / ;;256)
· (𝐴↑4))
− (((𝐴↑4) / 8) /
4)))) | 
| 174 |  | quart1.p | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) | 
| 175 | 174 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) = ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐴 / 4)↑2))) | 
| 176 | 80, 10, 13 | divcli 12009 | . . . . . . . . . . . . . 14
⊢ (3 / 8)
∈ ℂ | 
| 177 |  | mulcl 11239 | . . . . . . . . . . . . . 14
⊢ (((3 / 8)
∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8)
· (𝐴↑2)) ∈
ℂ) | 
| 178 | 176, 58, 177 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) ∈
ℂ) | 
| 179 | 20 | sqcld 14184 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 / 4)↑2) ∈
ℂ) | 
| 180 | 3, 178, 179 | subdird 11720 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐴 / 4)↑2)) = ((𝐵 · ((𝐴 / 4)↑2)) − (((3 / 8) ·
(𝐴↑2)) ·
((𝐴 /
4)↑2)))) | 
| 181 | 2, 17, 19 | sqdivd 14199 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / (4↑2))) | 
| 182 | 16 | sqvali 14219 | . . . . . . . . . . . . . . . . . 18
⊢
(4↑2) = (4 · 4) | 
| 183 | 182, 125 | eqtri 2765 | . . . . . . . . . . . . . . . . 17
⊢
(4↑2) = ;16 | 
| 184 | 183 | oveq2i 7442 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴↑2) / (4↑2)) = ((𝐴↑2) / ;16) | 
| 185 | 181, 184 | eqtrdi 2793 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / ;16)) | 
| 186 | 185 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 · ((𝐴 / 4)↑2)) = (𝐵 · ((𝐴↑2) / ;16))) | 
| 187 | 3, 58, 76, 78 | divassd 12078 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 · (𝐴↑2)) / ;16) = (𝐵 · ((𝐴↑2) / ;16))) | 
| 188 | 3, 58 | mulcomd 11282 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 · (𝐴↑2)) = ((𝐴↑2) · 𝐵)) | 
| 189 | 188 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 · (𝐴↑2)) / ;16) = (((𝐴↑2) · 𝐵) / ;16)) | 
| 190 | 186, 187,
189 | 3eqtr2d 2783 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 · ((𝐴 / 4)↑2)) = (((𝐴↑2) · 𝐵) / ;16)) | 
| 191 | 176 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (3 / 8) ∈
ℂ) | 
| 192 | 191, 58, 58 | mulassd 11284 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝐴↑2)) = ((3 / 8) ·
((𝐴↑2) · (𝐴↑2)))) | 
| 193 | 103, 63, 11, 14 | div23d 12080 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((3 · (𝐴↑4)) / 8) = ((3 / 8)
· (𝐴↑4))) | 
| 194 |  | 2p2e4 12401 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (2 + 2) =
4 | 
| 195 | 194 | oveq2i 7442 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴↑(2 + 2)) = (𝐴↑4) | 
| 196 | 81 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ∈
ℕ0) | 
| 197 | 2, 196, 196 | expaddd 14188 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐴↑(2 + 2)) = ((𝐴↑2) · (𝐴↑2))) | 
| 198 | 195, 197 | eqtr3id 2791 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2) · (𝐴↑2))) | 
| 199 | 198 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((3 / 8) · (𝐴↑4)) = ((3 / 8) ·
((𝐴↑2) · (𝐴↑2)))) | 
| 200 | 193, 199 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((3 · (𝐴↑4)) / 8) = ((3 / 8)
· ((𝐴↑2)
· (𝐴↑2)))) | 
| 201 | 103, 63, 11, 14 | divassd 12078 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((3 · (𝐴↑4)) / 8) = (3 ·
((𝐴↑4) /
8))) | 
| 202 | 192, 200,
201 | 3eqtr2d 2783 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝐴↑2)) = (3 · ((𝐴↑4) / 8))) | 
| 203 | 202 | oveq1d 7446 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝐴↑2)) / (4↑2)) = ((3
· ((𝐴↑4) / 8))
/ (4↑2))) | 
| 204 | 183, 76 | eqeltrid 2845 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (4↑2) ∈
ℂ) | 
| 205 | 183, 77 | eqnetri 3011 | . . . . . . . . . . . . . . . . 17
⊢
(4↑2) ≠ 0 | 
| 206 | 205 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (4↑2) ≠
0) | 
| 207 | 178, 58, 204, 206 | divassd 12078 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝐴↑2)) / (4↑2)) = (((3 /
8) · (𝐴↑2))
· ((𝐴↑2) /
(4↑2)))) | 
| 208 | 103, 64, 204, 206 | divassd 12078 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((3 · ((𝐴↑4) / 8)) / (4↑2)) =
(3 · (((𝐴↑4) /
8) / (4↑2)))) | 
| 209 | 203, 207,
208 | 3eqtr3d 2785 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · ((𝐴↑2) / (4↑2))) = (3
· (((𝐴↑4) / 8)
/ (4↑2)))) | 
| 210 | 181 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · ((𝐴 / 4)↑2)) = (((3 / 8)
· (𝐴↑2))
· ((𝐴↑2) /
(4↑2)))) | 
| 211 | 183 | oveq2i 7442 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴↑4) / 8) / (4↑2)) =
(((𝐴↑4) / 8) / ;16) | 
| 212 | 127, 211 | eqtr4di 2795 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) / 4) = (((𝐴↑4) / 8) /
(4↑2))) | 
| 213 | 212 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (3 · ((((𝐴↑4) / 8) / 4) / 4)) = (3
· (((𝐴↑4) / 8)
/ (4↑2)))) | 
| 214 | 209, 210,
213 | 3eqtr4d 2787 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · ((𝐴 / 4)↑2)) = (3 ·
((((𝐴↑4) / 8) / 4) /
4))) | 
| 215 | 190, 214 | oveq12d 7449 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 · ((𝐴 / 4)↑2)) − (((3 / 8) ·
(𝐴↑2)) ·
((𝐴 / 4)↑2))) =
((((𝐴↑2) ·
𝐵) / ;16) − (3 · ((((𝐴↑4) / 8) / 4) / 4)))) | 
| 216 | 175, 180,
215 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) = ((((𝐴↑2) · 𝐵) / ;16) − (3 · ((((𝐴↑4) / 8) / 4) / 4)))) | 
| 217 | 216 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 / 4)↑2))) = (((𝐴↑4) / ;;256) +
((((𝐴↑2) ·
𝐵) / ;16) − (3 · ((((𝐴↑4) / 8) / 4) / 4))))) | 
| 218 | 164, 173,
217 | 3eqtr4d 2787 | . . . . . . . . 9
⊢ (𝜑 → (((((𝐴↑2) · 𝐵) / 8) − (((𝐴↑2) · 𝐵) / ;16)) + (((3 / ;;256)
· (𝐴↑4))
− (((𝐴↑4) / 8) /
4))) = (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) | 
| 219 | 101, 102,
218 | 3eqtrd 2781 | . . . . . . . 8
⊢ (𝜑 → (((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256)
· (𝐴↑4)))
− ((((𝐴↑4) / 8)
/ 4) + (((𝐴↑2)
· 𝐵) / ;16))) = (((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 /
4)↑2)))) | 
| 220 | 219 | negeqd 11502 | . . . . . . 7
⊢ (𝜑 → -(((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256)
· (𝐴↑4)))
− ((((𝐴↑4) / 8)
/ 4) + (((𝐴↑2)
· 𝐵) / ;16))) = -(((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 /
4)↑2)))) | 
| 221 | 65, 79, 60, 89 | addsub4d 11667 | . . . . . . 7
⊢ (𝜑 → (((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16)) − ((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256)
· (𝐴↑4)))) =
(((((𝐴↑4) / 8) / 4)
− (((𝐴↑2)
· 𝐵) / 8)) +
((((𝐴↑2) ·
𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))) | 
| 222 | 99, 220, 221 | 3eqtr3rd 2786 | . . . . . 6
⊢ (𝜑 → (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4)))) =
-(((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) | 
| 223 | 222 | oveq2d 7447 | . . . . 5
⊢ (𝜑 → (𝐷 + (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))) =
(𝐷 + -(((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 /
4)↑2))))) | 
| 224 | 3, 178 | subcld 11620 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 − ((3 / 8) · (𝐴↑2))) ∈
ℂ) | 
| 225 | 174, 224 | eqeltrd 2841 | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 226 | 225, 179 | mulcld 11281 | . . . . . . 7
⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) ∈
ℂ) | 
| 227 | 111, 226 | addcld 11280 | . . . . . 6
⊢ (𝜑 → (((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 / 4)↑2))) ∈
ℂ) | 
| 228 | 71, 227 | negsubd 11626 | . . . . 5
⊢ (𝜑 → (𝐷 + -(((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 / 4)↑2)))) = (𝐷 − (((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 /
4)↑2))))) | 
| 229 | 96, 223, 228 | 3eqtrd 2781 | . . . 4
⊢ (𝜑 → (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256)
· (𝐴↑4))))) =
(𝐷 − (((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 /
4)↑2))))) | 
| 230 | 93, 95, 229 | 3eqtrd 2781 | . . 3
⊢ (𝜑 → ((𝑄 · (𝐴 / 4)) + 𝑅) = (𝐷 − (((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 /
4)↑2))))) | 
| 231 | 230 | oveq2d 7447 | . 2
⊢ (𝜑 → ((((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)) = ((((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 / 4)↑2))) + (𝐷 − (((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 /
4)↑2)))))) | 
| 232 | 227, 71 | pncan3d 11623 | . 2
⊢ (𝜑 → ((((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 / 4)↑2))) + (𝐷 − (((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 / 4)↑2))))) = 𝐷) | 
| 233 | 231, 232 | eqtr2d 2778 | 1
⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) +
(𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))) |