| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥↑2) = (𝑧↑2)) |
| 2 | 1 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑥↑2) + (𝑌↑2)) = ((𝑧↑2) + (𝑌↑2))) |
| 3 | 2 | eqeq1d 2739 |
. . . . 5
⊢ (𝑥 = 𝑧 → (((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ↔ ((𝑧↑2) + (𝑌↑2)) = (𝑅↑2))) |
| 4 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝐴 · 𝑥) = (𝐴 · 𝑧)) |
| 5 | 4 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = ((𝐴 · 𝑧) + (𝐵 · 𝑌))) |
| 6 | 5 | eqeq1d 2739 |
. . . . 5
⊢ (𝑥 = 𝑧 → (((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶)) |
| 7 | 3, 6 | anbi12d 632 |
. . . 4
⊢ (𝑥 = 𝑧 → ((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ (((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶))) |
| 8 | 7 | reu8 3739 |
. . 3
⊢
(∃!𝑥 ∈
ℝ (((𝑥↑2) +
(𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ∃𝑥 ∈ ℝ ((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧))) |
| 9 | 8 | a1i 11 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) →
(∃!𝑥 ∈ ℝ
(((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ∃𝑥 ∈ ℝ ((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧)))) |
| 10 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝐶 = ((𝐴 · 𝑥) + (𝐵 · 𝑌)) → 𝐶 = ((𝐴 · 𝑥) + (𝐵 · 𝑌))) |
| 11 | 10 | eqcoms 2745 |
. . . . . . . . . . . . 13
⊢ (((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶 → 𝐶 = ((𝐴 · 𝑥) + (𝐵 · 𝑌))) |
| 12 | 11 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶 → (((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)))) |
| 13 | 12 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) → (((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)))) |
| 14 | | simp11l 1285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → 𝐴 ∈
ℝ) |
| 15 | 14 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝐴
∈ ℝ) |
| 16 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝑧
∈ ℝ) |
| 17 | 15, 16 | remulcld 11291 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐴
· 𝑧) ∈
ℝ) |
| 18 | 17 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐴
· 𝑧) ∈
ℂ) |
| 19 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → 𝐴
∈ ℝ) |
| 20 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → 𝑥
∈ ℝ) |
| 21 | 19, 20 | remulcld 11291 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → (𝐴
· 𝑥) ∈
ℝ) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐴
· 𝑥) ∈
ℝ) |
| 23 | 22 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐴
· 𝑥) ∈
ℂ) |
| 24 | | simp12 1205 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → 𝐵 ∈
ℝ) |
| 25 | | simp3 1139 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → 𝑌 ∈
ℝ) |
| 26 | 24, 25 | remulcld 11291 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → (𝐵 · 𝑌) ∈ ℝ) |
| 27 | 26 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐵
· 𝑌) ∈
ℝ) |
| 28 | 27 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐵
· 𝑌) ∈
ℂ) |
| 29 | 18, 23, 28 | addcan2d 11465 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (((𝐴
· 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)) ↔ (𝐴 · 𝑧) = (𝐴 · 𝑥))) |
| 30 | 16 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝑧
∈ ℂ) |
| 31 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝑥
∈ ℝ) |
| 32 | 31 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝑥
∈ ℂ) |
| 33 | 15 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝐴
∈ ℂ) |
| 34 | | simp11r 1286 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → 𝐴 ≠ 0) |
| 35 | 34 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝐴
≠ 0) |
| 36 | 30, 32, 33, 35 | mulcand 11896 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → ((𝐴
· 𝑧) = (𝐴 · 𝑥) ↔ 𝑧 = 𝑥)) |
| 37 | | equcom 2017 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 ↔ 𝑥 = 𝑧) |
| 38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝑧 =
𝑥 ↔ 𝑥 = 𝑧)) |
| 39 | 29, 36, 38 | 3bitrd 305 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (((𝐴
· 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)) ↔ 𝑥 = 𝑧)) |
| 40 | 39 | biimpd 229 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (((𝐴
· 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)) → 𝑥 = 𝑧)) |
| 41 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) → (((𝐴 · 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)) → 𝑥 = 𝑧)) |
| 42 | 13, 41 | sylbid 240 |
. . . . . . . . . 10
⊢
(((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) → (((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶 → 𝑥 = 𝑧)) |
| 43 | 42 | an32s 652 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ 𝑧 ∈ ℝ) → (((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶 → 𝑥 = 𝑧)) |
| 44 | 43 | adantld 490 |
. . . . . . . 8
⊢
(((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ 𝑧 ∈ ℝ) → ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧)) |
| 45 | 44 | ralrimiva 3146 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) → ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧)) |
| 46 | 45 | ex 412 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → (((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶 → ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧))) |
| 47 | 46 | adantld 490 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → ((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) → ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧))) |
| 48 | 47 | pm4.71d 561 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → ((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧)))) |
| 49 | 48 | bicomd 223 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → (((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧)) ↔ (((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶))) |
| 50 | 49 | rexbidva 3177 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) →
(∃𝑥 ∈ ℝ
((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧)) ↔ ∃𝑥 ∈ ℝ (((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶))) |
| 51 | | itsclquadb.q |
. . 3
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) |
| 52 | | itsclquadb.t |
. . 3
⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) |
| 53 | | itsclquadb.u |
. . 3
⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) |
| 54 | 51, 52, 53 | itsclquadb 48697 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) →
(∃𝑥 ∈ ℝ
(((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) |
| 55 | 9, 50, 54 | 3bitrd 305 |
1
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) →
(∃!𝑥 ∈ ℝ
(((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) |