Proof of Theorem itsclc0
Step | Hyp | Ref
| Expression |
1 | | rprege0 12136 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (𝑅 ∈ ℝ
∧ 0 ≤ 𝑅)) |
2 | | elrege0 12575 |
. . . . . 6
⊢ (𝑅 ∈ (0[,)+∞) ↔
(𝑅 ∈ ℝ ∧ 0
≤ 𝑅)) |
3 | 1, 2 | sylibr 226 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
(0[,)+∞)) |
4 | 3 | 3ad2ant2 1168 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → 𝑅 ∈ (0[,)+∞)) |
5 | | itsclc0.i |
. . . . . 6
⊢ 𝐼 = {1, 2} |
6 | | itsclc0.e |
. . . . . 6
⊢ 𝐸 = (ℝ^‘𝐼) |
7 | | itsclc0.p |
. . . . . 6
⊢ 𝑃 = (ℝ
↑𝑚 𝐼) |
8 | | itsclc0.s |
. . . . . 6
⊢ 𝑆 = (Sphere‘𝐸) |
9 | | itsclc0.0 |
. . . . . 6
⊢ 0 = (𝐼 × {0}) |
10 | | eqid 2825 |
. . . . . 6
⊢ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} |
11 | 5, 6, 7, 8, 9, 10 | 2sphere0 43312 |
. . . . 5
⊢ (𝑅 ∈ (0[,)+∞) → (
0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)}) |
12 | 11 | eleq2d 2892 |
. . . 4
⊢ (𝑅 ∈ (0[,)+∞) →
(𝑋 ∈ ( 0 𝑆𝑅) ↔ 𝑋 ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)})) |
13 | 4, 12 | syl 17 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → (𝑋 ∈ ( 0 𝑆𝑅) ↔ 𝑋 ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)})) |
14 | | fveq1 6436 |
. . . . . . . 8
⊢ (𝑝 = 𝑋 → (𝑝‘1) = (𝑋‘1)) |
15 | 14 | oveq2d 6926 |
. . . . . . 7
⊢ (𝑝 = 𝑋 → (𝐴 · (𝑝‘1)) = (𝐴 · (𝑋‘1))) |
16 | | fveq1 6436 |
. . . . . . . 8
⊢ (𝑝 = 𝑋 → (𝑝‘2) = (𝑋‘2)) |
17 | 16 | oveq2d 6926 |
. . . . . . 7
⊢ (𝑝 = 𝑋 → (𝐵 · (𝑝‘2)) = (𝐵 · (𝑋‘2))) |
18 | 15, 17 | oveq12d 6928 |
. . . . . 6
⊢ (𝑝 = 𝑋 → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2)))) |
19 | 18 | eqeq1d 2827 |
. . . . 5
⊢ (𝑝 = 𝑋 → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶)) |
20 | | itsclc0.l |
. . . . 5
⊢ 𝐿 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} |
21 | 19, 20 | elrab2 3589 |
. . . 4
⊢ (𝑋 ∈ 𝐿 ↔ (𝑋 ∈ 𝑃 ∧ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶)) |
22 | 21 | a1i 11 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → (𝑋 ∈ 𝐿 ↔ (𝑋 ∈ 𝑃 ∧ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶))) |
23 | 13, 22 | anbi12d 624 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → ((𝑋 ∈ ( 0 𝑆𝑅) ∧ 𝑋 ∈ 𝐿) ↔ (𝑋 ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} ∧ (𝑋 ∈ 𝑃 ∧ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶)))) |
24 | 14 | oveq1d 6925 |
. . . . . . 7
⊢ (𝑝 = 𝑋 → ((𝑝‘1)↑2) = ((𝑋‘1)↑2)) |
25 | 16 | oveq1d 6925 |
. . . . . . 7
⊢ (𝑝 = 𝑋 → ((𝑝‘2)↑2) = ((𝑋‘2)↑2)) |
26 | 24, 25 | oveq12d 6928 |
. . . . . 6
⊢ (𝑝 = 𝑋 → (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (((𝑋‘1)↑2) + ((𝑋‘2)↑2))) |
27 | 26 | eqeq1d 2827 |
. . . . 5
⊢ (𝑝 = 𝑋 → ((((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2) ↔ (((𝑋‘1)↑2) + ((𝑋‘2)↑2)) = (𝑅↑2))) |
28 | 27 | elrab 3585 |
. . . 4
⊢ (𝑋 ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} ↔ (𝑋 ∈ 𝑃 ∧ (((𝑋‘1)↑2) + ((𝑋‘2)↑2)) = (𝑅↑2))) |
29 | | simp1 1170 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) |
30 | | 3simpc 1186 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷)) |
31 | 5, 7 | rrx2pxel 42271 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ) |
32 | 5, 7 | rrx2pyel 42272 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) |
33 | 31, 32 | jca 507 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑃 → ((𝑋‘1) ∈ ℝ ∧ (𝑋‘2) ∈
ℝ)) |
34 | | itsclc0.q |
. . . . . . . . . 10
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) |
35 | | itsclc0.d |
. . . . . . . . . 10
⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) |
36 | 34, 35 | itsclc0lem5 43322 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) ∧ ((𝑋‘1) ∈ ℝ ∧
(𝑋‘2) ∈
ℝ)) → (((((𝑋‘1)↑2) + ((𝑋‘2)↑2)) = (𝑅↑2) ∧ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) |
37 | 29, 30, 33, 36 | syl2an3an 1549 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 0 ≤ 𝐷) ∧ 𝑋 ∈ 𝑃) → (((((𝑋‘1)↑2) + ((𝑋‘2)↑2)) = (𝑅↑2) ∧ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) |
38 | 37 | expcomd 408 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ 𝐴 ≠ 0)
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈ ℝ)
∧ 𝑅 ∈
ℝ+ ∧ 0 ≤ 𝐷) ∧ 𝑋 ∈ 𝑃) → (((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶 → ((((𝑋‘1)↑2) + ((𝑋‘2)↑2)) = (𝑅↑2) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) |
39 | 38 | expimpd 447 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → ((𝑋 ∈ 𝑃 ∧ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶) → ((((𝑋‘1)↑2) + ((𝑋‘2)↑2)) = (𝑅↑2) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) |
40 | 39 | com23 86 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → ((((𝑋‘1)↑2) + ((𝑋‘2)↑2)) = (𝑅↑2) → ((𝑋 ∈ 𝑃 ∧ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) |
41 | 40 | adantld 486 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → ((𝑋 ∈ 𝑃 ∧ (((𝑋‘1)↑2) + ((𝑋‘2)↑2)) = (𝑅↑2)) → ((𝑋 ∈ 𝑃 ∧ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) |
42 | 28, 41 | syl5bi 234 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → (𝑋 ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} → ((𝑋 ∈ 𝑃 ∧ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) |
43 | 42 | impd 400 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → ((𝑋 ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} ∧ (𝑋 ∈ 𝑃 ∧ ((𝐴 · (𝑋‘1)) + (𝐵 · (𝑋‘2))) = 𝐶)) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) |
44 | 23, 43 | sylbid 232 |
1
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → ((𝑋 ∈ ( 0 𝑆𝑅) ∧ 𝑋 ∈ 𝐿) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) |