Proof of Theorem itschlc0yqe
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . . . . . . . . . . . 15
⊢ (𝐶 = (𝐵 · 𝑌) → (𝐵 · 𝐶) = (𝐵 · (𝐵 · 𝑌))) | 
| 2 | 1 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝐶 = (𝐵 · 𝑌) → (2 · (𝐵 · 𝐶)) = (2 · (𝐵 · (𝐵 · 𝑌)))) | 
| 3 | 2 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝐶 = (𝐵 · 𝑌) → ((2 · (𝐵 · 𝐶)) · 𝑌) = ((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌)) | 
| 4 | 3 | negeqd 11503 | . . . . . . . . . . . 12
⊢ (𝐶 = (𝐵 · 𝑌) → -((2 · (𝐵 · 𝐶)) · 𝑌) = -((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌)) | 
| 5 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝐶 = (𝐵 · 𝑌) → (𝐶↑2) = ((𝐵 · 𝑌)↑2)) | 
| 6 | 4, 5 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝐶 = (𝐵 · 𝑌) → (-((2 · (𝐵 · 𝐶)) · 𝑌) + (𝐶↑2)) = (-((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌) + ((𝐵 · 𝑌)↑2))) | 
| 7 | 6 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝐶 = (𝐵 · 𝑌) → (((𝐵 · 𝑌)↑2) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + (𝐶↑2))) = (((𝐵 · 𝑌)↑2) + (-((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌) + ((𝐵 · 𝑌)↑2)))) | 
| 8 | 7 | eqcoms 2744 | . . . . . . . . 9
⊢ ((𝐵 · 𝑌) = 𝐶 → (((𝐵 · 𝑌)↑2) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + (𝐶↑2))) = (((𝐵 · 𝑌)↑2) + (-((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌) + ((𝐵 · 𝑌)↑2)))) | 
| 9 |  | simp12 1204 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ 𝐵 ∈
ℝ) | 
| 10 | 9 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ 𝐵 ∈
ℂ) | 
| 11 |  | simp3r 1202 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ 𝑌 ∈
ℝ) | 
| 12 | 11 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ 𝑌 ∈
ℂ) | 
| 13 | 10, 12 | mulcld 11282 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (𝐵 · 𝑌) ∈
ℂ) | 
| 14 | 13 | sqcld 14185 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((𝐵 · 𝑌)↑2) ∈
ℂ) | 
| 15 |  | 2cnd 12345 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ 2 ∈ ℂ) | 
| 16 | 10, 13 | mulcld 11282 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (𝐵 · (𝐵 · 𝑌)) ∈ ℂ) | 
| 17 | 15, 16 | mulcld 11282 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (2 · (𝐵
· (𝐵 · 𝑌))) ∈
ℂ) | 
| 18 | 17, 12 | mulcld 11282 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((2 · (𝐵
· (𝐵 · 𝑌))) · 𝑌) ∈ ℂ) | 
| 19 | 18 | negcld 11608 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ -((2 · (𝐵
· (𝐵 · 𝑌))) · 𝑌) ∈ ℂ) | 
| 20 |  | add32r 11482 | . . . . . . . . . . 11
⊢ ((((𝐵 · 𝑌)↑2) ∈ ℂ ∧ -((2 ·
(𝐵 · (𝐵 · 𝑌))) · 𝑌) ∈ ℂ ∧ ((𝐵 · 𝑌)↑2) ∈ ℂ) → (((𝐵 · 𝑌)↑2) + (-((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌) + ((𝐵 · 𝑌)↑2))) = ((((𝐵 · 𝑌)↑2) + ((𝐵 · 𝑌)↑2)) + -((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌))) | 
| 21 | 14, 19, 14, 20 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (((𝐵 · 𝑌)↑2) + (-((2 ·
(𝐵 · (𝐵 · 𝑌))) · 𝑌) + ((𝐵 · 𝑌)↑2))) = ((((𝐵 · 𝑌)↑2) + ((𝐵 · 𝑌)↑2)) + -((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌))) | 
| 22 | 14, 14 | addcld 11281 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (((𝐵 · 𝑌)↑2) + ((𝐵 · 𝑌)↑2)) ∈ ℂ) | 
| 23 | 22, 18 | negsubd 11627 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((((𝐵 · 𝑌)↑2) + ((𝐵 · 𝑌)↑2)) + -((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌)) = ((((𝐵 · 𝑌)↑2) + ((𝐵 · 𝑌)↑2)) − ((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌))) | 
| 24 | 15, 16, 12 | mulassd 11285 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((2 · (𝐵
· (𝐵 · 𝑌))) · 𝑌) = (2 · ((𝐵 · (𝐵 · 𝑌)) · 𝑌))) | 
| 25 | 10, 13, 12 | mul32d 11472 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((𝐵 · (𝐵 · 𝑌)) · 𝑌) = ((𝐵 · 𝑌) · (𝐵 · 𝑌))) | 
| 26 | 13 | sqvald 14184 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((𝐵 · 𝑌)↑2) = ((𝐵 · 𝑌) · (𝐵 · 𝑌))) | 
| 27 | 25, 26 | eqtr4d 2779 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((𝐵 · (𝐵 · 𝑌)) · 𝑌) = ((𝐵 · 𝑌)↑2)) | 
| 28 | 27 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (2 · ((𝐵
· (𝐵 · 𝑌)) · 𝑌)) = (2 · ((𝐵 · 𝑌)↑2))) | 
| 29 | 14 | 2timesd 12511 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (2 · ((𝐵
· 𝑌)↑2)) =
(((𝐵 · 𝑌)↑2) + ((𝐵 · 𝑌)↑2))) | 
| 30 | 24, 28, 29 | 3eqtrrd 2781 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (((𝐵 · 𝑌)↑2) + ((𝐵 · 𝑌)↑2)) = ((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌)) | 
| 31 | 22, 30 | subeq0bd 11690 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((((𝐵 · 𝑌)↑2) + ((𝐵 · 𝑌)↑2)) − ((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌)) = 0) | 
| 32 | 23, 31 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((((𝐵 · 𝑌)↑2) + ((𝐵 · 𝑌)↑2)) + -((2 · (𝐵 · (𝐵 · 𝑌))) · 𝑌)) = 0) | 
| 33 | 21, 32 | eqtrd 2776 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (((𝐵 · 𝑌)↑2) + (-((2 ·
(𝐵 · (𝐵 · 𝑌))) · 𝑌) + ((𝐵 · 𝑌)↑2))) = 0) | 
| 34 | 8, 33 | sylan9eqr 2798 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
∧ (𝐵 · 𝑌) = 𝐶) → (((𝐵 · 𝑌)↑2) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + (𝐶↑2))) = 0) | 
| 35 | 34 | ex 412 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((𝐵 · 𝑌) = 𝐶 → (((𝐵 · 𝑌)↑2) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + (𝐶↑2))) = 0)) | 
| 36 |  | simp3l 1201 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ 𝑋 ∈
ℝ) | 
| 37 | 36 | recnd 11290 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ 𝑋 ∈
ℂ) | 
| 38 | 37 | mul02d 11460 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (0 · 𝑋) =
0) | 
| 39 | 38 | oveq1d 7447 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((0 · 𝑋) +
(𝐵 · 𝑌)) = (0 + (𝐵 · 𝑌))) | 
| 40 | 13 | addlidd 11463 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (0 + (𝐵 ·
𝑌)) = (𝐵 · 𝑌)) | 
| 41 | 39, 40 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((0 · 𝑋) +
(𝐵 · 𝑌)) = (𝐵 · 𝑌)) | 
| 42 | 41 | eqeq1d 2738 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (((0 · 𝑋) +
(𝐵 · 𝑌)) = 𝐶 ↔ (𝐵 · 𝑌) = 𝐶)) | 
| 43 | 10 | sqcld 14185 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (𝐵↑2) ∈
ℂ) | 
| 44 | 43 | addlidd 11463 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (0 + (𝐵↑2)) =
(𝐵↑2)) | 
| 45 | 44 | oveq1d 7447 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((0 + (𝐵↑2))
· (𝑌↑2)) =
((𝐵↑2) · (𝑌↑2))) | 
| 46 | 10, 12 | sqmuld 14199 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((𝐵 · 𝑌)↑2) = ((𝐵↑2) · (𝑌↑2))) | 
| 47 | 45, 46 | eqtr4d 2779 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((0 + (𝐵↑2))
· (𝑌↑2)) =
((𝐵 · 𝑌)↑2)) | 
| 48 |  | simp13 1205 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ 𝐶 ∈
ℝ) | 
| 49 | 48 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ 𝐶 ∈
ℂ) | 
| 50 | 10, 49 | mulcld 11282 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (𝐵 · 𝐶) ∈
ℂ) | 
| 51 | 15, 50 | mulcld 11282 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (2 · (𝐵
· 𝐶)) ∈
ℂ) | 
| 52 | 51, 12 | mulneg1d 11717 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (-(2 · (𝐵
· 𝐶)) · 𝑌) = -((2 · (𝐵 · 𝐶)) · 𝑌)) | 
| 53 |  | rpcn 13046 | . . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℂ) | 
| 54 | 53 | sqcld 14185 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℂ) | 
| 55 | 54 | mul02d 11460 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (0 · (𝑅↑2)) = 0) | 
| 56 | 55 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ ((𝐶↑2) −
(0 · (𝑅↑2))) =
((𝐶↑2) −
0)) | 
| 57 | 56 | 3ad2ant2 1134 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((𝐶↑2) −
(0 · (𝑅↑2))) =
((𝐶↑2) −
0)) | 
| 58 | 49 | sqcld 14185 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (𝐶↑2) ∈
ℂ) | 
| 59 | 58 | subid1d 11610 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((𝐶↑2) −
0) = (𝐶↑2)) | 
| 60 | 57, 59 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((𝐶↑2) −
(0 · (𝑅↑2))) =
(𝐶↑2)) | 
| 61 | 52, 60 | oveq12d 7450 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((-(2 · (𝐵
· 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2)))) = (-((2 ·
(𝐵 · 𝐶)) · 𝑌) + (𝐶↑2))) | 
| 62 | 47, 61 | oveq12d 7450 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (((0 + (𝐵↑2))
· (𝑌↑2)) +
((-(2 · (𝐵 ·
𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) = (((𝐵 · 𝑌)↑2) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + (𝐶↑2)))) | 
| 63 | 62 | eqeq1d 2738 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ ((((0 + (𝐵↑2))
· (𝑌↑2)) +
((-(2 · (𝐵 ·
𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) = 0 ↔ (((𝐵 · 𝑌)↑2) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + (𝐶↑2))) = 0)) | 
| 64 | 35, 42, 63 | 3imtr4d 294 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+
∧ (𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ))
→ (((0 · 𝑋) +
(𝐵 · 𝑌)) = 𝐶 → (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) =
0)) | 
| 65 | 64 | 3exp 1119 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑅 ∈ ℝ+
→ ((𝑋 ∈ ℝ
∧ 𝑌 ∈ ℝ)
→ (((0 · 𝑋) +
(𝐵 · 𝑌)) = 𝐶 → (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) =
0)))) | 
| 66 | 65 | 3adant1r 1177 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 = 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑅 ∈ ℝ+ → ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (((0
· 𝑋) + (𝐵 · 𝑌)) = 𝐶 → (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) =
0)))) | 
| 67 | 66 | 3imp 1110 | . . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 = 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((0
· 𝑋) + (𝐵 · 𝑌)) = 𝐶 → (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) =
0)) | 
| 68 | 67 | adantld 490 | . 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 = 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) →
((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((0 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) =
0)) | 
| 69 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝐴 = 0 → (𝐴 · 𝑋) = (0 · 𝑋)) | 
| 70 | 69 | oveq1d 7447 | . . . . . . . 8
⊢ (𝐴 = 0 → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((0 · 𝑋) + (𝐵 · 𝑌))) | 
| 71 | 70 | eqeq1d 2738 | . . . . . . 7
⊢ (𝐴 = 0 → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((0 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) | 
| 72 | 71 | anbi2d 630 | . . . . . 6
⊢ (𝐴 = 0 → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) ↔ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((0 · 𝑋) + (𝐵 · 𝑌)) = 𝐶))) | 
| 73 |  | itscnhlc0yqe.q | . . . . . . . . . 10
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) | 
| 74 |  | sq0i 14233 | . . . . . . . . . . 11
⊢ (𝐴 = 0 → (𝐴↑2) = 0) | 
| 75 | 74 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝐴 = 0 → ((𝐴↑2) + (𝐵↑2)) = (0 + (𝐵↑2))) | 
| 76 | 73, 75 | eqtrid 2788 | . . . . . . . . 9
⊢ (𝐴 = 0 → 𝑄 = (0 + (𝐵↑2))) | 
| 77 | 76 | oveq1d 7447 | . . . . . . . 8
⊢ (𝐴 = 0 → (𝑄 · (𝑌↑2)) = ((0 + (𝐵↑2)) · (𝑌↑2))) | 
| 78 |  | itscnhlc0yqe.t | . . . . . . . . . . 11
⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) | 
| 79 | 78 | oveq1i 7442 | . . . . . . . . . 10
⊢ (𝑇 · 𝑌) = (-(2 · (𝐵 · 𝐶)) · 𝑌) | 
| 80 | 79 | a1i 11 | . . . . . . . . 9
⊢ (𝐴 = 0 → (𝑇 · 𝑌) = (-(2 · (𝐵 · 𝐶)) · 𝑌)) | 
| 81 |  | itscnhlc0yqe.u | . . . . . . . . . 10
⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) | 
| 82 | 74 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝐴 = 0 → ((𝐴↑2) · (𝑅↑2)) = (0 · (𝑅↑2))) | 
| 83 | 82 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝐴 = 0 → ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) = ((𝐶↑2) − (0 · (𝑅↑2)))) | 
| 84 | 81, 83 | eqtrid 2788 | . . . . . . . . 9
⊢ (𝐴 = 0 → 𝑈 = ((𝐶↑2) − (0 · (𝑅↑2)))) | 
| 85 | 80, 84 | oveq12d 7450 | . . . . . . . 8
⊢ (𝐴 = 0 → ((𝑇 · 𝑌) + 𝑈) = ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) | 
| 86 | 77, 85 | oveq12d 7450 | . . . . . . 7
⊢ (𝐴 = 0 → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2)))))) | 
| 87 | 86 | eqeq1d 2738 | . . . . . 6
⊢ (𝐴 = 0 → (((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0 ↔ (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) =
0)) | 
| 88 | 72, 87 | imbi12d 344 | . . . . 5
⊢ (𝐴 = 0 → (((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0) ↔ ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((0 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) =
0))) | 
| 89 | 88 | adantl 481 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 0) → (((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0) ↔ ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((0 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) =
0))) | 
| 90 | 89 | 3ad2ant1 1133 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 = 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0) ↔ ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((0 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) =
0))) | 
| 91 | 90 | 3ad2ant1 1133 | . 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 = 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) →
(((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0) ↔ ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((0 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (((0 + (𝐵↑2)) · (𝑌↑2)) + ((-(2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − (0 · (𝑅↑2))))) =
0))) | 
| 92 | 68, 91 | mpbird 257 | 1
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 = 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) →
((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) |