Step | Hyp | Ref
| Expression |
1 | | oveq1 7178 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥↑2) = (𝑧↑2)) |
2 | 1 | oveq1d 7186 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑥↑2) + (𝑌↑2)) = ((𝑧↑2) + (𝑌↑2))) |
3 | 2 | eqeq1d 2740 |
. . . . 5
⊢ (𝑥 = 𝑧 → (((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ↔ ((𝑧↑2) + (𝑌↑2)) = (𝑅↑2))) |
4 | | oveq2 7179 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝐴 · 𝑥) = (𝐴 · 𝑧)) |
5 | 4 | oveq1d 7186 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = ((𝐴 · 𝑧) + (𝐵 · 𝑌))) |
6 | 5 | eqeq1d 2740 |
. . . . 5
⊢ (𝑥 = 𝑧 → (((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶)) |
7 | 3, 6 | anbi12d 634 |
. . . 4
⊢ (𝑥 = 𝑧 → ((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ (((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶))) |
8 | 7 | reu8 3633 |
. . 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 2746 |
. . . . . . . . . . . . 13
⊢ (((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶 → 𝐶 = ((𝐴 · 𝑥) + (𝐵 · 𝑌))) |
12 | 11 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶 → (((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)))) |
13 | 12 | adantl 485 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) → (((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)))) |
14 | | simp11l 1285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → 𝐴 ∈
ℝ) |
15 | 14 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝐴
∈ ℝ) |
16 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝑧
∈ ℝ) |
17 | 15, 16 | remulcld 10750 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐴
· 𝑧) ∈
ℝ) |
18 | 17 | recnd 10748 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐴
· 𝑧) ∈
ℂ) |
19 | 14 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → 𝐴
∈ ℝ) |
20 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → 𝑥
∈ ℝ) |
21 | 19, 20 | remulcld 10750 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → (𝐴
· 𝑥) ∈
ℝ) |
22 | 21 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐴
· 𝑥) ∈
ℝ) |
23 | 22 | recnd 10748 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐴
· 𝑥) ∈
ℂ) |
24 | | simp12 1205 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → 𝐵 ∈
ℝ) |
25 | | simp3 1139 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → 𝑌 ∈
ℝ) |
26 | 24, 25 | remulcld 10750 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → (𝐵 · 𝑌) ∈ ℝ) |
27 | 26 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐵
· 𝑌) ∈
ℝ) |
28 | 27 | recnd 10748 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝐵
· 𝑌) ∈
ℂ) |
29 | 18, 23, 28 | addcan2d 10923 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (((𝐴
· 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)) ↔ (𝐴 · 𝑧) = (𝐴 · 𝑥))) |
30 | 16 | recnd 10748 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝑧
∈ ℂ) |
31 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝑥
∈ ℝ) |
32 | 31 | recnd 10748 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝑥
∈ ℂ) |
33 | 15 | recnd 10748 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝐴
∈ ℂ) |
34 | | simp11r 1286 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → 𝐴 ≠ 0) |
35 | 34 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → 𝐴
≠ 0) |
36 | 30, 32, 33, 35 | mulcand 11352 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → ((𝐴
· 𝑧) = (𝐴 · 𝑥) ↔ 𝑧 = 𝑥)) |
37 | | equcom 2029 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 ↔ 𝑥 = 𝑧) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (𝑧 =
𝑥 ↔ 𝑥 = 𝑧)) |
39 | 29, 36, 38 | 3bitrd 308 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (((𝐴
· 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)) ↔ 𝑥 = 𝑧)) |
40 | 39 | biimpd 232 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) → (((𝐴
· 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)) → 𝑥 = 𝑧)) |
41 | 40 | adantr 484 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) → (((𝐴 · 𝑧) + (𝐵 · 𝑌)) = ((𝐴 · 𝑥) + (𝐵 · 𝑌)) → 𝑥 = 𝑧)) |
42 | 13, 41 | sylbid 243 |
. . . . . . . . . 10
⊢
(((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ 𝑧
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) → (((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶 → 𝑥 = 𝑧)) |
43 | 42 | an32s 652 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ 𝑧 ∈ ℝ) → (((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶 → 𝑥 = 𝑧)) |
44 | 43 | adantld 494 |
. . . . . . . 8
⊢
(((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ 𝑧 ∈ ℝ) → ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧)) |
45 | 44 | ralrimiva 3096 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) ∧ ((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶) → ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧)) |
46 | 45 | ex 416 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → (((𝐴
· 𝑥) + (𝐵 · 𝑌)) = 𝐶 → ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧))) |
47 | 46 | adantld 494 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → ((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) → ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧))) |
48 | 47 | pm4.71d 565 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → ((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧)))) |
49 | 48 | bicomd 226 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 𝑌
∈ ℝ) ∧ 𝑥
∈ ℝ) → (((((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ∧ ∀𝑧 ∈ ℝ ((((𝑧↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑧) + (𝐵 · 𝑌)) = 𝐶) → 𝑥 = 𝑧)) ↔ (((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶))) |
50 | 49 | rexbidva 3206 |
. 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 45648 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) →
(∃𝑥 ∈ ℝ
(((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) |
55 | 9, 50, 54 | 3bitrd 308 |
1
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) →
(∃!𝑥 ∈ ℝ
(((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) |