Proof of Theorem 2itscplem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2itscplem3.s | . . 3
⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) | 
| 2 | 1 | a1i 11 | . 2
⊢ (𝜑 → 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2))) | 
| 3 |  | 2itscplem3.q | . . . . . 6
⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2)) | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝑄 = ((𝐸↑2) + (𝐷↑2))) | 
| 5 | 4 | oveq2d 7447 | . . . 4
⊢ (𝜑 → ((𝑅↑2) · 𝑄) = ((𝑅↑2) · ((𝐸↑2) + (𝐷↑2)))) | 
| 6 |  | 2itscp.r | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℝ) | 
| 7 | 6 | recnd 11289 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ ℂ) | 
| 8 | 7 | sqcld 14184 | . . . . 5
⊢ (𝜑 → (𝑅↑2) ∈ ℂ) | 
| 9 |  | 2itscp.e | . . . . . . . 8
⊢ 𝐸 = (𝐵 − 𝑌) | 
| 10 |  | 2itscp.b | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 11 | 10 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 12 |  | 2itscp.y | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 13 | 12 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ ℂ) | 
| 14 | 11, 13 | subcld 11620 | . . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝑌) ∈ ℂ) | 
| 15 | 9, 14 | eqeltrid 2845 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 16 | 15 | sqcld 14184 | . . . . . 6
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) | 
| 17 |  | 2itscp.d | . . . . . . . 8
⊢ 𝐷 = (𝑋 − 𝐴) | 
| 18 |  | 2itscp.x | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 19 | 18 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 20 |  | 2itscp.a | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 21 | 20 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 22 | 19, 21 | subcld 11620 | . . . . . . . 8
⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ) | 
| 23 | 17, 22 | eqeltrid 2845 | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 24 | 23 | sqcld 14184 | . . . . . 6
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) | 
| 25 | 16, 24 | addcld 11280 | . . . . 5
⊢ (𝜑 → ((𝐸↑2) + (𝐷↑2)) ∈ ℂ) | 
| 26 | 8, 25 | mulcomd 11282 | . . . 4
⊢ (𝜑 → ((𝑅↑2) · ((𝐸↑2) + (𝐷↑2))) = (((𝐸↑2) + (𝐷↑2)) · (𝑅↑2))) | 
| 27 | 16, 24, 8 | adddird 11286 | . . . 4
⊢ (𝜑 → (((𝐸↑2) + (𝐷↑2)) · (𝑅↑2)) = (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2)))) | 
| 28 | 5, 26, 27 | 3eqtrd 2781 | . . 3
⊢ (𝜑 → ((𝑅↑2) · 𝑄) = (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2)))) | 
| 29 |  | 2itscp.c | . . . 4
⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) | 
| 30 | 20, 10, 18, 12, 17, 9, 29 | 2itscplem2 48700 | . . 3
⊢ (𝜑 → (𝐶↑2) = ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2)))) | 
| 31 | 28, 30 | oveq12d 7449 | . 2
⊢ (𝜑 → (((𝑅↑2) · 𝑄) − (𝐶↑2)) = ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2))))) | 
| 32 | 16, 8 | mulcld 11281 | . . . . . . . 8
⊢ (𝜑 → ((𝐸↑2) · (𝑅↑2)) ∈ ℂ) | 
| 33 | 24, 8 | mulcld 11281 | . . . . . . . 8
⊢ (𝜑 → ((𝐷↑2) · (𝑅↑2)) ∈ ℂ) | 
| 34 | 32, 33 | addcld 11280 | . . . . . . 7
⊢ (𝜑 → (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) ∈ ℂ) | 
| 35 | 11 | sqcld 14184 | . . . . . . . 8
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) | 
| 36 | 24, 35 | mulcld 11281 | . . . . . . 7
⊢ (𝜑 → ((𝐷↑2) · (𝐵↑2)) ∈ ℂ) | 
| 37 |  | 2cnd 12344 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℂ) | 
| 38 | 23, 21 | mulcld 11281 | . . . . . . . . 9
⊢ (𝜑 → (𝐷 · 𝐴) ∈ ℂ) | 
| 39 | 15, 11 | mulcld 11281 | . . . . . . . . 9
⊢ (𝜑 → (𝐸 · 𝐵) ∈ ℂ) | 
| 40 | 38, 39 | mulcld 11281 | . . . . . . . 8
⊢ (𝜑 → ((𝐷 · 𝐴) · (𝐸 · 𝐵)) ∈ ℂ) | 
| 41 | 37, 40 | mulcld 11281 | . . . . . . 7
⊢ (𝜑 → (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))) ∈ ℂ) | 
| 42 | 34, 36, 41 | subsub4d 11651 | . . . . . 6
⊢ (𝜑 → (((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) = ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))))) | 
| 43 | 42 | eqcomd 2743 | . . . . 5
⊢ (𝜑 → ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) = (((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) | 
| 44 | 43 | oveq1d 7446 | . . . 4
⊢ (𝜑 → (((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) − ((𝐸↑2) · (𝐴↑2))) = ((((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) − ((𝐸↑2) · (𝐴↑2)))) | 
| 45 | 34, 36 | subcld 11620 | . . . . 5
⊢ (𝜑 → ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) ∈ ℂ) | 
| 46 | 21 | sqcld 14184 | . . . . . 6
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) | 
| 47 | 16, 46 | mulcld 11281 | . . . . 5
⊢ (𝜑 → ((𝐸↑2) · (𝐴↑2)) ∈ ℂ) | 
| 48 | 45, 41, 47 | sub32d 11652 | . . . 4
⊢ (𝜑 → ((((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) − ((𝐸↑2) · (𝐴↑2))) = ((((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) − ((𝐸↑2) · (𝐴↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) | 
| 49 | 44, 48 | eqtrd 2777 | . . 3
⊢ (𝜑 → (((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) − ((𝐸↑2) · (𝐴↑2))) = ((((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) − ((𝐸↑2) · (𝐴↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) | 
| 50 | 36, 41 | addcld 11280 | . . . 4
⊢ (𝜑 → (((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) ∈ ℂ) | 
| 51 | 34, 50, 47 | subsub4d 11651 | . . 3
⊢ (𝜑 → (((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) − ((𝐸↑2) · (𝐴↑2))) = ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2))))) | 
| 52 | 32, 33, 36 | addsubassd 11640 | . . . . . . 7
⊢ (𝜑 → ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) = (((𝐸↑2) · (𝑅↑2)) + (((𝐷↑2) · (𝑅↑2)) − ((𝐷↑2) · (𝐵↑2))))) | 
| 53 | 24, 8, 35 | subdid 11719 | . . . . . . . . 9
⊢ (𝜑 → ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2))) = (((𝐷↑2) · (𝑅↑2)) − ((𝐷↑2) · (𝐵↑2)))) | 
| 54 | 53 | eqcomd 2743 | . . . . . . . 8
⊢ (𝜑 → (((𝐷↑2) · (𝑅↑2)) − ((𝐷↑2) · (𝐵↑2))) = ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) | 
| 55 | 54 | oveq2d 7447 | . . . . . . 7
⊢ (𝜑 → (((𝐸↑2) · (𝑅↑2)) + (((𝐷↑2) · (𝑅↑2)) − ((𝐷↑2) · (𝐵↑2)))) = (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2))))) | 
| 56 | 52, 55 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) = (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2))))) | 
| 57 | 56 | oveq1d 7446 | . . . . 5
⊢ (𝜑 → (((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) − ((𝐸↑2) · (𝐴↑2))) = ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − ((𝐸↑2) · (𝐴↑2)))) | 
| 58 | 8, 35 | subcld 11620 | . . . . . . 7
⊢ (𝜑 → ((𝑅↑2) − (𝐵↑2)) ∈ ℂ) | 
| 59 | 24, 58 | mulcld 11281 | . . . . . 6
⊢ (𝜑 → ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2))) ∈ ℂ) | 
| 60 | 32, 59, 47 | addsubd 11641 | . . . . 5
⊢ (𝜑 → ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − ((𝐸↑2) · (𝐴↑2))) = ((((𝐸↑2) · (𝑅↑2)) − ((𝐸↑2) · (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2))))) | 
| 61 | 16, 8, 46 | subdid 11719 | . . . . . . 7
⊢ (𝜑 → ((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) = (((𝐸↑2) · (𝑅↑2)) − ((𝐸↑2) · (𝐴↑2)))) | 
| 62 | 61 | eqcomd 2743 | . . . . . 6
⊢ (𝜑 → (((𝐸↑2) · (𝑅↑2)) − ((𝐸↑2) · (𝐴↑2))) = ((𝐸↑2) · ((𝑅↑2) − (𝐴↑2)))) | 
| 63 | 62 | oveq1d 7446 | . . . . 5
⊢ (𝜑 → ((((𝐸↑2) · (𝑅↑2)) − ((𝐸↑2) · (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) = (((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2))))) | 
| 64 | 57, 60, 63 | 3eqtrd 2781 | . . . 4
⊢ (𝜑 → (((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) − ((𝐸↑2) · (𝐴↑2))) = (((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2))))) | 
| 65 | 64 | oveq1d 7446 | . . 3
⊢ (𝜑 → ((((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((𝐷↑2) · (𝐵↑2))) − ((𝐸↑2) · (𝐴↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) | 
| 66 | 49, 51, 65 | 3eqtr3d 2785 | . 2
⊢ (𝜑 → ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2)))) = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) | 
| 67 | 2, 31, 66 | 3eqtrd 2781 | 1
⊢ (𝜑 → 𝑆 = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) |