Proof of Theorem itschlc0xyqsol
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | itscnhlc0yqe.q | . . 3
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) | 
| 2 |  | itsclc0yqsol.d | . . 3
⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) | 
| 3 | 1, 2 | itschlc0xyqsol1 48692 | . 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (𝐶 / 𝐵) ∧ (𝑋 = -((√‘𝐷) / 𝐵) ∨ 𝑋 = ((√‘𝐷) / 𝐵))))) | 
| 4 |  | orcom 870 | . . . 4
⊢ ((𝑋 = -((√‘𝐷) / 𝐵) ∨ 𝑋 = ((√‘𝐷) / 𝐵)) ↔ (𝑋 = ((√‘𝐷) / 𝐵) ∨ 𝑋 = -((√‘𝐷) / 𝐵))) | 
| 5 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = 0 → (𝐴 · 𝐶) = (0 · 𝐶)) | 
| 6 | 5 | ad2antrl 728 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐶) = (0 · 𝐶)) | 
| 7 | 6 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐴 · 𝐶) = (0 · 𝐶)) | 
| 8 |  | simpll3 1214 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐶 ∈
ℝ) | 
| 9 | 8 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐶 ∈
ℂ) | 
| 10 | 9 | mul02d 11460 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (0 ·
𝐶) = 0) | 
| 11 | 7, 10 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐴 · 𝐶) = 0) | 
| 12 | 11 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = (0 + (𝐵 · (√‘𝐷)))) | 
| 13 |  | simpll2 1213 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐵 ∈
ℝ) | 
| 14 | 13 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐵 ∈
ℂ) | 
| 15 |  | rpre 13044 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) | 
| 16 | 15 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) →
𝑅 ∈
ℝ) | 
| 17 | 16 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) →
𝑅 ∈
ℂ) | 
| 18 | 17 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝑅 ∈
ℂ) | 
| 19 | 18 | sqcld 14185 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑅↑2) ∈
ℂ) | 
| 20 | 1 | resum2sqcl 48632 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈
ℝ) | 
| 21 | 20 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈
ℂ) | 
| 22 | 21 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈
ℂ) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) → 𝑄 ∈ ℂ) | 
| 24 | 23 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝑄 ∈
ℂ) | 
| 25 | 19, 24 | mulcld 11282 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝑅↑2) · 𝑄) ∈
ℂ) | 
| 26 | 9 | sqcld 14185 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐶↑2) ∈
ℂ) | 
| 27 | 25, 26 | subcld 11621 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (((𝑅↑2) · 𝑄) − (𝐶↑2)) ∈ ℂ) | 
| 28 | 2, 27 | eqeltrid 2844 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐷 ∈
ℂ) | 
| 29 | 28 | sqrtcld 15477 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) →
(√‘𝐷) ∈
ℂ) | 
| 30 | 14, 29 | mulcld 11282 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐵 · (√‘𝐷)) ∈
ℂ) | 
| 31 | 30 | addlidd 11463 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (0 + (𝐵 · (√‘𝐷))) = (𝐵 · (√‘𝐷))) | 
| 32 | 12, 31 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = (𝐵 · (√‘𝐷))) | 
| 33 | 32 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = ((𝐵 · (√‘𝐷)) / 𝑄)) | 
| 34 |  | sq0i 14233 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 = 0 → (𝐴↑2) = 0) | 
| 35 | 34 | ad2antrl 728 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) = 0) | 
| 36 | 35 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) + (𝐵↑2)) = (0 + (𝐵↑2))) | 
| 37 |  | simp2 1137 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈
ℝ) | 
| 38 | 37 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈
ℂ) | 
| 39 | 38 | sqcld 14185 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) ∈
ℂ) | 
| 40 | 39 | addlidd 11463 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (0 +
(𝐵↑2)) = (𝐵↑2)) | 
| 41 | 38 | sqvald 14184 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) = (𝐵 · 𝐵)) | 
| 42 | 40, 41 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (0 +
(𝐵↑2)) = (𝐵 · 𝐵)) | 
| 43 | 42 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) → (0 + (𝐵↑2)) = (𝐵 · 𝐵)) | 
| 44 | 36, 43 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) + (𝐵↑2)) = (𝐵 · 𝐵)) | 
| 45 | 1, 44 | eqtrid 2788 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) → 𝑄 = (𝐵 · 𝐵)) | 
| 46 | 45 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝑄 = (𝐵 · 𝐵)) | 
| 47 | 46 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐵 · (√‘𝐷)) / 𝑄) = ((𝐵 · (√‘𝐷)) / (𝐵 · 𝐵))) | 
| 48 |  | simplrr 777 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐵 ≠ 0) | 
| 49 | 29, 14, 14, 48, 48 | divcan5d 12070 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐵 · (√‘𝐷)) / (𝐵 · 𝐵)) = ((√‘𝐷) / 𝐵)) | 
| 50 | 47, 49 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐵 · (√‘𝐷)) / 𝑄) = ((√‘𝐷) / 𝐵)) | 
| 51 | 33, 50 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = ((√‘𝐷) / 𝐵)) | 
| 52 | 51 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = ((√‘𝐷) / 𝐵)) | 
| 53 | 52 | adantr 480 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = ((√‘𝐷) / 𝐵)) | 
| 54 | 53 | eqcomd 2742 | . . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → ((√‘𝐷) / 𝐵) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) | 
| 55 | 54 | eqeq2d 2747 | . . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → (𝑋 = ((√‘𝐷) / 𝐵) ↔ 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))) | 
| 56 | 55 | biimpd 229 | . . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → (𝑋 = ((√‘𝐷) / 𝐵) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))) | 
| 57 |  | oveq1 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 = 0 → (𝐴 · (√‘𝐷)) = (0 · (√‘𝐷))) | 
| 58 | 57 | ad2antrl 728 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) → (𝐴 · (√‘𝐷)) = (0 · (√‘𝐷))) | 
| 59 | 58 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐴 · (√‘𝐷)) = (0 ·
(√‘𝐷))) | 
| 60 | 29 | mul02d 11460 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (0 ·
(√‘𝐷)) =
0) | 
| 61 | 59, 60 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐴 · (√‘𝐷)) = 0) | 
| 62 | 61 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) − 0)) | 
| 63 | 14, 9 | mulcld 11282 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐵 · 𝐶) ∈ ℂ) | 
| 64 | 63 | subid1d 11610 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐵 · 𝐶) − 0) = (𝐵 · 𝐶)) | 
| 65 | 62, 64 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = (𝐵 · 𝐶)) | 
| 66 | 65, 46 | oveq12d 7450 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = ((𝐵 · 𝐶) / (𝐵 · 𝐵))) | 
| 67 | 66 | 3adant3 1132 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = ((𝐵 · 𝐶) / (𝐵 · 𝐵))) | 
| 68 | 9 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ) | 
| 69 | 14 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℂ) | 
| 70 |  | simp1rr 1239 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ≠ 0) | 
| 71 | 68, 69, 69, 70, 70 | divcan5d 12070 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) / (𝐵 · 𝐵)) = (𝐶 / 𝐵)) | 
| 72 | 67, 71 | eqtr2d 2777 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 / 𝐵) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) | 
| 73 | 72 | eqeq2d 2747 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌 = (𝐶 / 𝐵) ↔ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) | 
| 74 | 73 | biimpa 476 | . . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) | 
| 75 | 56, 74 | jctird 526 | . . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → (𝑋 = ((√‘𝐷) / 𝐵) → (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))) | 
| 76 | 14, 29 | mulneg2d 11718 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐵 · -(√‘𝐷)) = -(𝐵 · (√‘𝐷))) | 
| 77 | 76 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → -(𝐵 · (√‘𝐷)) = (𝐵 · -(√‘𝐷))) | 
| 78 | 77, 46 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (-(𝐵 · (√‘𝐷)) / 𝑄) = ((𝐵 · -(√‘𝐷)) / (𝐵 · 𝐵))) | 
| 79 | 29 | negcld 11608 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) →
-(√‘𝐷) ∈
ℂ) | 
| 80 | 79, 14, 14, 48, 48 | divcan5d 12070 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐵 · -(√‘𝐷)) / (𝐵 · 𝐵)) = (-(√‘𝐷) / 𝐵)) | 
| 81 | 78, 80 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (-(𝐵 · (√‘𝐷)) / 𝑄) = (-(√‘𝐷) / 𝐵)) | 
| 82 | 11 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) = (0 − (𝐵 · (√‘𝐷)))) | 
| 83 |  | df-neg 11496 | . . . . . . . . . . . . . 14
⊢ -(𝐵 · (√‘𝐷)) = (0 − (𝐵 · (√‘𝐷))) | 
| 84 | 82, 83 | eqtr4di 2794 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) = -(𝐵 · (√‘𝐷))) | 
| 85 | 84 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) = (-(𝐵 · (√‘𝐷)) / 𝑄)) | 
| 86 | 29, 14, 48 | divnegd 12057 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) →
-((√‘𝐷) / 𝐵) = (-(√‘𝐷) / 𝐵)) | 
| 87 | 81, 85, 86 | 3eqtr4d 2786 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) = -((√‘𝐷) / 𝐵)) | 
| 88 | 87 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) = -((√‘𝐷) / 𝐵)) | 
| 89 | 88 | adantr 480 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) = -((√‘𝐷) / 𝐵)) | 
| 90 | 89 | eqcomd 2742 | . . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → -((√‘𝐷) / 𝐵) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) | 
| 91 | 90 | eqeq2d 2747 | . . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → (𝑋 = -((√‘𝐷) / 𝐵) ↔ 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))) | 
| 92 | 91 | biimpd 229 | . . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → (𝑋 = -((√‘𝐷) / 𝐵) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))) | 
| 93 | 58 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴 · (√‘𝐷)) = (0 · (√‘𝐷))) | 
| 94 | 17 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑅 ∈ ℂ) | 
| 95 | 94 | sqcld 14185 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑅↑2) ∈ ℂ) | 
| 96 | 23 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 ∈ ℂ) | 
| 97 | 95, 96 | mulcld 11282 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑅↑2) · 𝑄) ∈ ℂ) | 
| 98 |  | simp1l3 1268 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℝ) | 
| 99 | 98 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ) | 
| 100 | 99 | sqcld 14185 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶↑2) ∈ ℂ) | 
| 101 | 97, 100 | subcld 11621 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑅↑2) · 𝑄) − (𝐶↑2)) ∈ ℂ) | 
| 102 | 2, 101 | eqeltrid 2844 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐷 ∈ ℂ) | 
| 103 | 102 | sqrtcld 15477 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) →
(√‘𝐷) ∈
ℂ) | 
| 104 | 103 | mul02d 11460 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (0 ·
(√‘𝐷)) =
0) | 
| 105 | 93, 104 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴 · (√‘𝐷)) = 0) | 
| 106 | 105 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + 0)) | 
| 107 |  | simp1l2 1267 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℝ) | 
| 108 | 107 | recnd 11290 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℂ) | 
| 109 | 108, 99 | mulcld 11282 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℂ) | 
| 110 | 109 | addridd 11462 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) + 0) = (𝐵 · 𝐶)) | 
| 111 | 106, 110 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) = (𝐵 · 𝐶)) | 
| 112 | 45 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 = (𝐵 · 𝐵)) | 
| 113 | 111, 112 | oveq12d 7450 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) = ((𝐵 · 𝐶) / (𝐵 · 𝐵))) | 
| 114 | 99, 108, 108, 70, 70 | divcan5d 12070 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) / (𝐵 · 𝐵)) = (𝐶 / 𝐵)) | 
| 115 | 113, 114 | eqtr2d 2777 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 / 𝐵) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) | 
| 116 | 115 | eqeq2d 2747 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌 = (𝐶 / 𝐵) ↔ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) | 
| 117 | 116 | biimpa 476 | . . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) | 
| 118 | 92, 117 | jctird 526 | . . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → (𝑋 = -((√‘𝐷) / 𝐵) → (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))) | 
| 119 | 75, 118 | orim12d 966 | . . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → ((𝑋 = ((√‘𝐷) / 𝐵) ∨ 𝑋 = -((√‘𝐷) / 𝐵)) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) | 
| 120 | 4, 119 | biimtrid 242 | . . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝐴 = 0 ∧
𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) ∧
(𝑋 ∈ ℝ ∧
𝑌 ∈ ℝ)) ∧
𝑌 = (𝐶 / 𝐵)) → ((𝑋 = -((√‘𝐷) / 𝐵) ∨ 𝑋 = ((√‘𝐷) / 𝐵)) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) | 
| 121 | 120 | expimpd 453 | . 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑌 = (𝐶 / 𝐵) ∧ (𝑋 = -((√‘𝐷) / 𝐵) ∨ 𝑋 = ((√‘𝐷) / 𝐵))) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) | 
| 122 | 3, 121 | syld 47 | 1
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) |