itscnhlinecirc02p - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > itscnhlinecirc02p		Structured version Visualization version GIF version

Theorem itscnhlinecirc02p 50100

Description: Intersection of a nonhorizontal line with a circle: A nonhorizontal line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 28-Jan-2023.)

**Hypotheses**
Ref	Expression
itscnhlinecirc02p.i	⊢ 𝐼 = (0..^2)
itscnhlinecirc02p.e	⊢ 𝐸 = (ℝ^‘𝐼)
itscnhlinecirc02p.p	⊢ 𝑃 = (ℝ ↑_m 𝐼)
itscnhlinecirc02p.s	⊢ 𝑆 = (Sphere‘𝐸)
itscnhlinecirc02p.0	⊢ 0 = (𝐼 × {0})
itscnhlinecirc02p.l	⊢ 𝐿 = (Line_M‘𝐸)
itscnhlinecirc02p.d	⊢ 𝐷 = (dist‘𝐸)

**Assertion**
Ref	Expression
itscnhlinecirc02p	⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑠 ∈ 𝒫 ℝ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ∃!𝑥 ∈ ℝ (⟨“𝑥𝑦”⟩ ∈ ( 0 𝑆𝑅) ∧ ⟨“𝑥𝑦”⟩ ∈ (𝑋𝐿𝑌))))

Distinct variable groups: 𝐷,𝑠,𝑥,𝑦 𝑃,𝑠,𝑦 𝑅,𝑠,𝑦 𝑋,𝑠,𝑦 𝑌,𝑠,𝑦 0 ,𝑠,𝑦 𝑥,𝑃 𝑥,𝑅 𝑥,𝑋 𝑥, 0 𝑥,𝑌 Allowed substitution hints: 𝑆(𝑥, 𝑦, 𝑠) 𝐸(𝑥, 𝑦, 𝑠) 𝐼(𝑥, 𝑦, 𝑠) 𝐿(𝑥, 𝑦, 𝑠)

Proof of Theorem itscnhlinecirc02p Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		itscnhlinecirc02p.i	. . . 4 ⊢ 𝐼 = (0..^2)
2		itscnhlinecirc02p.e	. . . 4 ⊢ 𝐸 = (ℝ^‘𝐼)
3		itscnhlinecirc02p.p	. . . 4 ⊢ 𝑃 = (ℝ ↑_m 𝐼)
4		itscnhlinecirc02p.s	. . . 4 ⊢ 𝑆 = (Sphere‘𝐸)
5		itscnhlinecirc02p.0	. . . 4 ⊢ 0 = (𝐼 × {0})
6		itscnhlinecirc02p.l	. . . 4 ⊢ 𝐿 = (Line_M‘𝐸)
7		itscnhlinecirc02p.d	. . . 4 ⊢ 𝐷 = (dist‘𝐸)
8	1, 2, 3, 4, 5, 6, 7	itscnhlinecirc02plem3 50099	. . 3 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → 0 < (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))↑2) − (4 · (((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2)))))))
9	1, 3	rrx2pyel 50027	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ)
10	9	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (𝑋‘1) ∈ ℝ)
11	10	adantr 486	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑋‘1) ∈ ℝ)
12	1, 3	rrx2pyel 50027	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ)
13	12	3ad2ant2 1152	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (𝑌‘1) ∈ ℝ)
14	13	adantr 486	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑌‘1) ∈ ℝ)
15	11, 14	resubcld 11768	. . . . . 6 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((𝑋‘1) − (𝑌‘1)) ∈ ℝ)
16	15	resqcld 14292	. . . . 5 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑋‘1) − (𝑌‘1))↑2) ∈ ℝ)
17	1, 3	rrx2pxel 50026	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘0) ∈ ℝ)
18	17	3ad2ant2 1152	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (𝑌‘0) ∈ ℝ)
19	18	adantr 486	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑌‘0) ∈ ℝ)
20	1, 3	rrx2pxel 50026	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑃 → (𝑋‘0) ∈ ℝ)
21	20	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (𝑋‘0) ∈ ℝ)
22	21	adantr 486	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑋‘0) ∈ ℝ)
23	19, 22	resubcld 11768	. . . . . 6 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((𝑌‘0) − (𝑋‘0)) ∈ ℝ)
24	23	resqcld 14292	. . . . 5 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑌‘0) − (𝑋‘0))↑2) ∈ ℝ)
25	16, 24	readdcld 11362	. . . 4 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) ∈ ℝ)
26	10, 13	resubcld 11768	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → ((𝑋‘1) − (𝑌‘1)) ∈ ℝ)
27	26	resqcld 14292	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (((𝑋‘1) − (𝑌‘1))↑2) ∈ ℝ)
28	18, 21	resubcld 11768	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → ((𝑌‘0) − (𝑋‘0)) ∈ ℝ)
29	28	resqcld 14292	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (((𝑌‘0) − (𝑋‘0))↑2) ∈ ℝ)
30	10	recnd 11361	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (𝑋‘1) ∈ ℂ)
31	13	recnd 11361	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (𝑌‘1) ∈ ℂ)
32		simp3 1156	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (𝑋‘1) ≠ (𝑌‘1))
33	30, 31, 32	subne0d 11703	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → ((𝑋‘1) − (𝑌‘1)) ≠ 0)
34	26, 33	sqgt0d 14418	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → 0 < (((𝑋‘1) − (𝑌‘1))↑2))
35	28	sqge0d 14304	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → 0 ≤ (((𝑌‘0) − (𝑋‘0))↑2))
36	27, 29, 34, 35	addgtge0d 11914	. . . . . 6 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → 0 < ((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)))
37	36	gt0ne0d 11904	. . . . 5 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → ((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) ≠ 0)
38	37	adantr 486	. . . 4 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) ≠ 0)
39		2re 12441	. . . . . . 7 ⊢ 2 ∈ ℝ
40	39	a1i 11	. . . . . 6 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → 2 ∈ ℝ)
41	11, 19	remulcld 11363	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((𝑋‘1) · (𝑌‘0)) ∈ ℝ)
42	22, 14	remulcld 11363	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((𝑋‘0) · (𝑌‘1)) ∈ ℝ)
43	41, 42	resubcld 11768	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) ∈ ℝ)
44	23, 43	remulcld 11363	. . . . . 6 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))) ∈ ℝ)
45	40, 44	remulcld 11363	. . . . 5 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) ∈ ℝ)
46	45	renegcld 11767	. . . 4 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) ∈ ℝ)
47	43	resqcld 14292	. . . . 5 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) ∈ ℝ)
48		rpre 13153	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
49	48	ad2antrl 741	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → 𝑅 ∈ ℝ)
50	49	resqcld 14292	. . . . . 6 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑅↑2) ∈ ℝ)
51	16, 50	remulcld 11363	. . . . 5 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2)) ∈ ℝ)
52	47, 51	resubcld 11768	. . . 4 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))) ∈ ℝ)
53		eqidd 2764	. . . 4 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))↑2) − (4 · (((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2)))))) = (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))↑2) − (4 · (((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2)))))))
54	25, 38, 46, 52, 53	requad2 48924	. . 3 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (∃!𝑠 ∈ 𝒫 ℝ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ((((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (𝑦↑2)) + (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) · 𝑦) + (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))))) = 0) ↔ 0 < (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))↑2) − (4 · (((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))))))))
55	8, 54	mpbird 260	. 2 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑠 ∈ 𝒫 ℝ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ((((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (𝑦↑2)) + (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) · 𝑦) + (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))))) = 0))
56		0xr 11380	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ^*
57	56	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → 0 ∈ ℝ^*)
58		pnfxr 11387	. . . . . . . . . . . . . . . 16 ⊢ +∞ ∈ ℝ^*
59	58	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → +∞ ∈ ℝ^*)
60		rpxr 13154	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ^*)
61		rpge0 13158	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → 0 ≤ 𝑅)
62	48	ltpnfd 13274	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 < +∞)
63	57, 59, 60, 61, 62	elicod 13550	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ (0[,)+∞))
64		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ {𝑝 ∈ 𝑃 ∣ (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2)} = {𝑝 ∈ 𝑃 ∣ (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2)}
65	1, 2, 3, 4, 5, 64	2sphere0 50065	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ (0[,)+∞) → ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2)})
66	63, 65	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ ℝ⁺ → ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2)})
67	66	ad2antrl 741	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2)})
68	67	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) → ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2)})
69	68	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2)})
70	69	eleq2d 2850	. . . . . . . . 9 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (⟨“𝑥𝑦”⟩ ∈ ( 0 𝑆𝑅) ↔ ⟨“𝑥𝑦”⟩ ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2)}))
71		fveq1 6904	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨“𝑥𝑦”⟩ → (𝑝‘0) = (⟨“𝑥𝑦”⟩‘0))
72	71	oveq1d 7455	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨“𝑥𝑦”⟩ → ((𝑝‘0)↑2) = ((⟨“𝑥𝑦”⟩‘0)↑2))
73		fveq1 6904	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨“𝑥𝑦”⟩ → (𝑝‘1) = (⟨“𝑥𝑦”⟩‘1))
74	73	oveq1d 7455	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨“𝑥𝑦”⟩ → ((𝑝‘1)↑2) = ((⟨“𝑥𝑦”⟩‘1)↑2))
75	72, 74	oveq12d 7458	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨“𝑥𝑦”⟩ → (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (((⟨“𝑥𝑦”⟩‘0)↑2) + ((⟨“𝑥𝑦”⟩‘1)↑2)))
76	75	eqeq1d 2765	. . . . . . . . . . 11 ⊢ (𝑝 = ⟨“𝑥𝑦”⟩ → ((((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2) ↔ (((⟨“𝑥𝑦”⟩‘0)↑2) + ((⟨“𝑥𝑦”⟩‘1)↑2)) = (𝑅↑2)))
77	76	elrab 3648	. . . . . . . . . 10 ⊢ (⟨“𝑥𝑦”⟩ ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2)} ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ (((⟨“𝑥𝑦”⟩‘0)↑2) + ((⟨“𝑥𝑦”⟩‘1)↑2)) = (𝑅↑2)))
78	77	a1i 11	. . . . . . . . 9 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (⟨“𝑥𝑦”⟩ ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘0)↑2) + ((𝑝‘1)↑2)) = (𝑅↑2)} ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ (((⟨“𝑥𝑦”⟩‘0)↑2) + ((⟨“𝑥𝑦”⟩‘1)↑2)) = (𝑅↑2))))
79		simpr 490	. . . . . . . . . 10 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
80		elpwi 4567	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝒫 ℝ → 𝑠 ⊆ ℝ)
81	80	ad4antlr 746	. . . . . . . . . . 11 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → 𝑠 ⊆ ℝ)
82		simplr 781	. . . . . . . . . . 11 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ 𝑠)
83	81, 82	sseldd 3914	. . . . . . . . . 10 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ℝ)
84		s2fv0 15063	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (⟨“𝑥𝑦”⟩‘0) = 𝑥)
85	84	oveq1d 7455	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((⟨“𝑥𝑦”⟩‘0)↑2) = (𝑥↑2))
86		s2fv1 15064	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (⟨“𝑥𝑦”⟩‘1) = 𝑦)
87	86	oveq1d 7455	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → ((⟨“𝑥𝑦”⟩‘1)↑2) = (𝑦↑2))
88	85, 87	oveqan12d 7459	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((⟨“𝑥𝑦”⟩‘0)↑2) + ((⟨“𝑥𝑦”⟩‘1)↑2)) = ((𝑥↑2) + (𝑦↑2)))
89	88	eqeq1d 2765	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((((⟨“𝑥𝑦”⟩‘0)↑2) + ((⟨“𝑥𝑦”⟩‘1)↑2)) = (𝑅↑2) ↔ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)))
90	89	anbi2d 642	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ (((⟨“𝑥𝑦”⟩‘0)↑2) + ((⟨“𝑥𝑦”⟩‘1)↑2)) = (𝑅↑2)) ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2))))
91	79, 83, 90	syl2anc 596	. . . . . . . . 9 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ (((⟨“𝑥𝑦”⟩‘0)↑2) + ((⟨“𝑥𝑦”⟩‘1)↑2)) = (𝑅↑2)) ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2))))
92	70, 78, 91	3bitrd 308	. . . . . . . 8 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (⟨“𝑥𝑦”⟩ ∈ ( 0 𝑆𝑅) ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2))))
93		simp1 1154	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → 𝑋 ∈ 𝑃)
94		simp2 1155	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → 𝑌 ∈ 𝑃)
95		fveq1 6904	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 = 𝑌 → (𝑋‘1) = (𝑌‘1))
96	95	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋 = 𝑌 → (𝑋‘1) = (𝑌‘1)))
97	96	necon3d 2980	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘1) ≠ (𝑌‘1) → 𝑋 ≠ 𝑌))
98	97	3impia 1135	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → 𝑋 ≠ 𝑌)
99	93, 94, 98	3jca 1146	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
100	99	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
101	100	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
102		eqid 2763	. . . . . . . . . . . 12 ⊢ ((𝑋‘1) − (𝑌‘1)) = ((𝑋‘1) − (𝑌‘1))
103		eqid 2763	. . . . . . . . . . . 12 ⊢ ((𝑌‘0) − (𝑋‘0)) = ((𝑌‘0) − (𝑋‘0))
104		eqid 2763	. . . . . . . . . . . 12 ⊢ (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))
105	1, 2, 3, 6, 102, 103, 104	rrx2linest2 50059	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ((((𝑋‘1) − (𝑌‘1)) · (𝑝‘0)) + (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))})
106	101, 105	syl 18	. . . . . . . . . 10 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ((((𝑋‘1) − (𝑌‘1)) · (𝑝‘0)) + (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))})
107	106	eleq2d 2850	. . . . . . . . 9 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (⟨“𝑥𝑦”⟩ ∈ (𝑋𝐿𝑌) ↔ ⟨“𝑥𝑦”⟩ ∈ {𝑝 ∈ 𝑃 ∣ ((((𝑋‘1) − (𝑌‘1)) · (𝑝‘0)) + (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))}))
108	71	oveq2d 7456	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨“𝑥𝑦”⟩ → (((𝑋‘1) − (𝑌‘1)) · (𝑝‘0)) = (((𝑋‘1) − (𝑌‘1)) · (⟨“𝑥𝑦”⟩‘0)))
109	73	oveq2d 7456	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨“𝑥𝑦”⟩ → (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1)) = (((𝑌‘0) − (𝑋‘0)) · (⟨“𝑥𝑦”⟩‘1)))
110	108, 109	oveq12d 7458	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨“𝑥𝑦”⟩ → ((((𝑋‘1) − (𝑌‘1)) · (𝑝‘0)) + (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1))) = ((((𝑋‘1) − (𝑌‘1)) · (⟨“𝑥𝑦”⟩‘0)) + (((𝑌‘0) − (𝑋‘0)) · (⟨“𝑥𝑦”⟩‘1))))
111	110	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨“𝑥𝑦”⟩ → (((((𝑋‘1) − (𝑌‘1)) · (𝑝‘0)) + (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) ↔ ((((𝑋‘1) − (𝑌‘1)) · (⟨“𝑥𝑦”⟩‘0)) + (((𝑌‘0) − (𝑋‘0)) · (⟨“𝑥𝑦”⟩‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))
112	111	elrab 3648	. . . . . . . . . . 11 ⊢ (⟨“𝑥𝑦”⟩ ∈ {𝑝 ∈ 𝑃 ∣ ((((𝑋‘1) − (𝑌‘1)) · (𝑝‘0)) + (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))} ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · (⟨“𝑥𝑦”⟩‘0)) + (((𝑌‘0) − (𝑋‘0)) · (⟨“𝑥𝑦”⟩‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))
113	84	oveq2d 7456	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑋‘1) − (𝑌‘1)) · (⟨“𝑥𝑦”⟩‘0)) = (((𝑋‘1) − (𝑌‘1)) · 𝑥))
114	86	oveq2d 7456	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (((𝑌‘0) − (𝑋‘0)) · (⟨“𝑥𝑦”⟩‘1)) = (((𝑌‘0) − (𝑋‘0)) · 𝑦))
115	113, 114	oveqan12d 7459	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((((𝑋‘1) − (𝑌‘1)) · (⟨“𝑥𝑦”⟩‘0)) + (((𝑌‘0) − (𝑋‘0)) · (⟨“𝑥𝑦”⟩‘1))) = ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)))
116	115	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((((𝑋‘1) − (𝑌‘1)) · (⟨“𝑥𝑦”⟩‘0)) + (((𝑌‘0) − (𝑋‘0)) · (⟨“𝑥𝑦”⟩‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) ↔ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))
117	116	anbi2d 642	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · (⟨“𝑥𝑦”⟩‘0)) + (((𝑌‘0) − (𝑋‘0)) · (⟨“𝑥𝑦”⟩‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))) ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
118	112, 117	bitrid 286	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (⟨“𝑥𝑦”⟩ ∈ {𝑝 ∈ 𝑃 ∣ ((((𝑋‘1) − (𝑌‘1)) · (𝑝‘0)) + (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))} ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
119	79, 83, 118	syl2anc 596	. . . . . . . . 9 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (⟨“𝑥𝑦”⟩ ∈ {𝑝 ∈ 𝑃 ∣ ((((𝑋‘1) − (𝑌‘1)) · (𝑝‘0)) + (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))} ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
120	107, 119	bitrd 282	. . . . . . . 8 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (⟨“𝑥𝑦”⟩ ∈ (𝑋𝐿𝑌) ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
121	92, 120	anbi12d 644	. . . . . . 7 ⊢ (((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → ((⟨“𝑥𝑦”⟩ ∈ ( 0 𝑆𝑅) ∧ ⟨“𝑥𝑦”⟩ ∈ (𝑋𝐿𝑌)) ↔ ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))))
122	121	reubidva 3383	. . . . . 6 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → (∃!𝑥 ∈ ℝ (⟨“𝑥𝑦”⟩ ∈ ( 0 𝑆𝑅) ∧ ⟨“𝑥𝑦”⟩ ∈ (𝑋𝐿𝑌)) ↔ ∃!𝑥 ∈ ℝ ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))))
123		elelpwi 4570	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝒫 ℝ) → 𝑦 ∈ ℝ)
124	1, 3	prelrrx2 50028	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ⟨“𝑥𝑦”⟩ ∈ 𝑃)
125	124	ancoms 464	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ⟨“𝑥𝑦”⟩ ∈ 𝑃)
126	125	biantrurd 542	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2))))
127	126	bicomd 226	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ↔ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)))
128	125	biantrurd 542	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) ↔ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
129	128	bicomd 226	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))) ↔ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))
130	127, 129	anbi12d 644	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) ↔ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
131	130	reubidva 3383	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ → (∃!𝑥 ∈ ℝ ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
132	123, 131	syl 18	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝒫 ℝ) → (∃!𝑥 ∈ ℝ ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
133	132	expcom 419	. . . . . . . 8 ⊢ (𝑠 ∈ 𝒫 ℝ → (𝑦 ∈ 𝑠 → (∃!𝑥 ∈ ℝ ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))))
134	133	ad2antlr 740	. . . . . . 7 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) → (𝑦 ∈ 𝑠 → (∃!𝑥 ∈ ℝ ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))))
135	134	imp 412	. . . . . 6 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → (∃!𝑥 ∈ ℝ ((⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (⟨“𝑥𝑦”⟩ ∈ 𝑃 ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
136	26, 33	jca 521	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (((𝑋‘1) − (𝑌‘1)) ∈ ℝ ∧ ((𝑋‘1) − (𝑌‘1)) ≠ 0))
137	136	adantr 486	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑋‘1) − (𝑌‘1)) ∈ ℝ ∧ ((𝑋‘1) − (𝑌‘1)) ≠ 0))
138	137	ad3antrrr 743	. . . . . . 7 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → (((𝑋‘1) − (𝑌‘1)) ∈ ℝ ∧ ((𝑋‘1) − (𝑌‘1)) ≠ 0))
139	19	ad3antrrr 743	. . . . . . . 8 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → (𝑌‘0) ∈ ℝ)
140	22	ad3antrrr 743	. . . . . . . 8 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → (𝑋‘0) ∈ ℝ)
141	139, 140	resubcld 11768	. . . . . . 7 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → ((𝑌‘0) − (𝑋‘0)) ∈ ℝ)
142	11	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → (𝑋‘1) ∈ ℝ)
143	142, 139	remulcld 11363	. . . . . . . 8 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → ((𝑋‘1) · (𝑌‘0)) ∈ ℝ)
144	14	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → (𝑌‘1) ∈ ℝ)
145	140, 144	remulcld 11363	. . . . . . . 8 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → ((𝑋‘0) · (𝑌‘1)) ∈ ℝ)
146	143, 145	resubcld 11768	. . . . . . 7 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) ∈ ℝ)
147		simplrl 789	. . . . . . . 8 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) → 𝑅 ∈ ℝ⁺)
148	147	ad2antrr 739	. . . . . . 7 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → 𝑅 ∈ ℝ⁺)
149	123	expcom 419	. . . . . . . . 9 ⊢ (𝑠 ∈ 𝒫 ℝ → (𝑦 ∈ 𝑠 → 𝑦 ∈ ℝ))
150	149	ad2antlr 740	. . . . . . . 8 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) → (𝑦 ∈ 𝑠 → 𝑦 ∈ ℝ))
151	150	imp 412	. . . . . . 7 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ ℝ)
152		eqid 2763	. . . . . . . 8 ⊢ ((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) = ((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2))
153		eqid 2763	. . . . . . . 8 ⊢ -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) = -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))))
154		eqid 2763	. . . . . . . 8 ⊢ (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))) = (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2)))
155	152, 153, 154	itsclquadeu 50092	. . . . . . 7 ⊢ ((((((𝑋‘1) − (𝑌‘1)) ∈ ℝ ∧ ((𝑋‘1) − (𝑌‘1)) ≠ 0) ∧ ((𝑌‘0) − (𝑋‘0)) ∈ ℝ ∧ (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ) → (∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))) ↔ ((((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (𝑦↑2)) + (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) · 𝑦) + (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))))) = 0))
156	138, 141, 146, 148, 151, 155	syl311anc 1412	. . . . . 6 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → (∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘1) − (𝑌‘1)) · 𝑥) + (((𝑌‘0) − (𝑋‘0)) · 𝑦)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))) ↔ ((((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (𝑦↑2)) + (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) · 𝑦) + (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))))) = 0))
157	122, 135, 156	3bitrd 308	. . . . 5 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) ∧ 𝑦 ∈ 𝑠) → (∃!𝑥 ∈ ℝ (⟨“𝑥𝑦”⟩ ∈ ( 0 𝑆𝑅) ∧ ⟨“𝑥𝑦”⟩ ∈ (𝑋𝐿𝑌)) ↔ ((((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (𝑦↑2)) + (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) · 𝑦) + (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))))) = 0))
158	157	ralbidva 3187	. . . 4 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧ (♯‘𝑠) = 2) → (∀𝑦 ∈ 𝑠 ∃!𝑥 ∈ ℝ (⟨“𝑥𝑦”⟩ ∈ ( 0 𝑆𝑅) ∧ ⟨“𝑥𝑦”⟩ ∈ (𝑋𝐿𝑌)) ↔ ∀𝑦 ∈ 𝑠 ((((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (𝑦↑2)) + (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) · 𝑦) + (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))))) = 0))
159	158	pm5.32da 590	. . 3 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) → (((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ∃!𝑥 ∈ ℝ (⟨“𝑥𝑦”⟩ ∈ ( 0 𝑆𝑅) ∧ ⟨“𝑥𝑦”⟩ ∈ (𝑋𝐿𝑌))) ↔ ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ((((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (𝑦↑2)) + (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) · 𝑦) + (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))))) = 0)))
160	159	reubidva 3383	. 2 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → (∃!𝑠 ∈ 𝒫 ℝ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ∃!𝑥 ∈ ℝ (⟨“𝑥𝑦”⟩ ∈ ( 0 𝑆𝑅) ∧ ⟨“𝑥𝑦”⟩ ∈ (𝑋𝐿𝑌))) ↔ ∃!𝑠 ∈ 𝒫 ℝ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ((((((𝑋‘1) − (𝑌‘1))↑2) + (((𝑌‘0) − (𝑋‘0))↑2)) · (𝑦↑2)) + (( -(2 · (((𝑌‘0) − (𝑋‘0)) · (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))) · 𝑦) + (((((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))↑2) − ((((𝑋‘1) − (𝑌‘1))↑2) · (𝑅↑2))))) = 0)))
161	55, 160	mpbird 260	1 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) ∧ (𝑅 ∈ ℝ⁺ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑠 ∈ 𝒫 ℝ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ∃!𝑥 ∈ ℝ (⟨“𝑥𝑦”⟩ ∈ ( 0 𝑆𝑅) ∧ ⟨“𝑥𝑦”⟩ ∈ (𝑋𝐿𝑌))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃!wreu 3367 {crab 3416 ⊆ wss 3900 𝒫 cpw 4560 {csn 4588 class class class wbr 5106 × cxp 5653 ‘cfv 6555 (class class class)co 7440 ↑_m cmap 8872 ℝcr 11223 0cc0 11224 1c1 11225 + caddc 11227 · cmul 11229 +∞cpnf 11364 ℝ^*cxr 11366 < clt 11367 − cmin 11565 -cneg 11566 2c2 12421 4c4 12423 ℝ⁺crp 13144 [,)cico 13502 ..^cfzo 13812 ↑cexp 14228 ♯chash 14498 ⟨“cs2 15017 distcds 17463 ℝ^crrx 25731 Line_Mcline 50043 Spherecsph 50044

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-inf2 9666 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302 ax-addf 11303 ax-mulf 11304

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-isom 6564 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-of 7714 df-om 7899 df-1st 8022 df-2nd 8023 df-supp 8202 df-tpos 8268 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-2o 8502 df-oadd 8505 df-er 8742 df-map 8874 df-ixp 8951 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-fsupp 9379 df-sup 9458 df-oi 9528 df-dju 10006 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-7 12434 df-8 12435 df-9 12436 df-n0 12631 df-z 12718 df-dec 12839 df-uz 12990 df-rp 13145 df-xneg 13265 df-xadd 13266 df-xmul 13267 df-ico 13506 df-icc 13507 df-fz 13664 df-fzo 13813 df-seq 14169 df-exp 14229 df-hash 14499 df-word 14683 df-concat 14740 df-s1 14767 df-s2 15024 df-cj 15292 df-re 15293 df-im 15294 df-sqrt 15428 df-abs 15429 df-clim 15681 df-sum 15880 df-struct 17351 df-sets 17368 df-slot 17386 df-ndx 17398 df-base 17414 df-ress 17435 df-plusg 17467 df-mulr 17468 df-starv 17469 df-sca 17470 df-vsca 17471 df-ip 17472 df-tset 17473 df-ple 17474 df-ds 17476 df-unif 17477 df-hom 17478 df-cco 17479 df-0g 17638 df-gsum 17639 df-prds 17644 df-pws 17646 df-mgm 18842 df-sgrp 18934 df-mnd 18950 df-mhm 19004 df-grp 19173 df-minusg 19174 df-sbg 19175 df-subg 19359 df-ghm 19454 df-cntz 19558 df-cmn 20023 df-abl 20024 df-mgp 20388 df-rng 20402 df-ur 20435 df-ring 20488 df-cring 20489 df-oppr 20594 df-dvdsr 20614 df-unit 20615 df-invr 20645 df-dvr 20658 df-rhm 20729 df-subrng 20825 df-subrg 20849 df-drng 21009 df-field 21010 df-staf 21123 df-srng 21124 df-lmod 21164 df-lss 21234 df-sra 21475 df-rgmod 21476 df-xmet 21698 df-met 21699 df-cnfld 21706 df-refld 21938 df-dsmm 22065 df-frlm 22080 df-nm 24928 df-tng 24930 df-tcph 25517 df-rrx 25733 df-ehl 25734 df-line 50045 df-sph 50046

This theorem is used by: (None)

W3C validator