itsclinecirc0b

Description: The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space. (Contributed by AV, 2-May-2023) (Revised by AV, 14-May-2023)

	Ref	Expression
Hypotheses	itsclinecirc0b.i	⊢ 𝐼 = { 1 , 2 }
	itsclinecirc0b.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	itsclinecirc0b.p	⊢ 𝑃 = ( ℝ ↑_m 𝐼 )
	itsclinecirc0b.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
	itsclinecirc0b.0	⊢ 0 = ( 𝐼 × { 0 } )
	itsclinecirc0b.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
	itsclinecirc0b.d	⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
	itsclinecirc0b.l	⊢ 𝐿 = ( Line_M ‘ 𝐸 )
	itsclinecirc0b.a	⊢ 𝐴 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
	itsclinecirc0b.b	⊢ 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
	itsclinecirc0b.c	⊢ 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
Assertion	itsclinecirc0b	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		itsclinecirc0b.i	⊢ 𝐼 = { 1 , 2 }
2		itsclinecirc0b.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		itsclinecirc0b.p	⊢ 𝑃 = ( ℝ ↑_m 𝐼 )
4		itsclinecirc0b.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5		itsclinecirc0b.0	⊢ 0 = ( 𝐼 × { 0 } )
6		itsclinecirc0b.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
7		itsclinecirc0b.d	⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
8		itsclinecirc0b.l	⊢ 𝐿 = ( Line_M ‘ 𝐸 )
9		itsclinecirc0b.a	⊢ 𝐴 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
10		itsclinecirc0b.b	⊢ 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
11		itsclinecirc0b.c	⊢ 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
12		eqid	⊢ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) )
13	1 2 3 8 10 12 11	rrx2linest	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )
14	13	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )
15		eqcom	⊢ ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ↔ ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) )
16	1 3	rrx2pxel	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
17	16	adantl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
18	1 3	rrx2pxel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
19	18	adantr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
20	17 19	resubcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ )
21	10 20	eqeltrid	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐵 ∈ ℝ )
22	21	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐵 ∈ ℝ )
23	22	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ∈ ℝ )
24	1 3	rrx2pyel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℝ )
25	24	adantl	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 2 ) ∈ ℝ )
26	23 25	remulcld	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) ∈ ℝ )
27	26	recnd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) ∈ ℂ )
28	1 3	rrx2pyel	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
29	28	adantl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
30	1 3	rrx2pyel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
31	30	adantr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
32	29 31	resubcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℝ )
33	32	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℝ )
34	33	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℝ )
35	1 3	rrx2pxel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
36	35	adantl	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
37	34 36	remulcld	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ∈ ℝ )
38	37	recnd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ∈ ℂ )
39	31 17	remulcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) ∈ ℝ )
40	19 29	remulcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ∈ ℝ )
41	39 40	resubcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ∈ ℝ )
42	11 41	eqeltrid	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐶 ∈ ℝ )
43	42	recnd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐶 ∈ ℂ )
44	43	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐶 ∈ ℂ )
45	44	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐶 ∈ ℂ )
46	27 38 45	subaddd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) )
47	15 46	bitr4id	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ↔ ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ) )
48	31 29	resubcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ )
49	9 48	eqeltrid	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐴 ∈ ℝ )
50	49	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐴 ∈ ℝ )
51	50	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐴 ∈ ℝ )
52	51 36	remulcld	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) ∈ ℝ )
53	52	recnd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) ∈ ℂ )
54	53 27	addcomd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + ( 𝐴 · ( 𝑝 ‘ 1 ) ) ) )
55	29	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
56	55	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
57	56	recnd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℂ )
58	31	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
59	58	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
60	59	recnd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℂ )
61	57 60	negsubdi2d	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) )
62	9 61	eqtr4id	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐴 = - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) )
63	62	oveq1d	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) )
64	32	recnd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℂ )
65	64	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℂ )
66	65	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℂ )
67	36	recnd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℂ )
68	66 67	mulneg1d	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) )
69	63 68	eqtr2d	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · ( 𝑝 ‘ 1 ) ) )
70	69	oveq2d	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + ( 𝐴 · ( 𝑝 ‘ 1 ) ) ) )
71	27 38	negsubd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) )
72	54 70 71	3eqtr2rd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) )
73	72	eqeq1d	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ) )
74	47 73	bitrd	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ) )
75	74	rabbidva	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → { 𝑝 ∈ 𝑃 ∣ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
76	14 75	eqtrd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
77	76	eleq2d	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ 𝑍 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) )
78	77	anbi2d	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) ) )
79	50	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → 𝐴 ∈ ℝ )
80	22	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ∈ ℝ )
81	42	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐶 ∈ ℝ )
82	81	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → 𝐶 ∈ ℝ )
83	1 3 10 9	rrx2pnedifcoorneorr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐵 ≠ 0 ∨ 𝐴 ≠ 0 ) )
84	83	orcomd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
85	84	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
86		simpr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) )
87		eqid	⊢ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
88	1 2 3 4 5 6 7 87	itsclc0b	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
89	79 80 82 85 86 88	syl311anc	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
90	78 89	bitrd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑍 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑍 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )

Metamath Proof Explorer

Theorem itsclinecirc0b

Proof