itsclc0

Description: The intersection points of a line L and a circle around the origin. (Contributed by AV, 25-Feb-2023)

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

Proof

Step	Hyp	Ref	Expression
1		itsclc0.i	⊢ 𝐼 = { 1 , 2 }
2		itsclc0.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		itsclc0.p	⊢ 𝑃 = ( ℝ ↑_m 𝐼 )
4		itsclc0.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5		itsclc0.0	⊢ 0 = ( 𝐼 × { 0 } )
6		itsclc0.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
7		itsclc0.d	⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
8		itsclc0.l	⊢ 𝐿 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
9		rprege0	⊢ ( 𝑅 ∈ ℝ⁺ → ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
10		elrege0	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) ↔ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
11	9 10	sylibr	⊢ ( 𝑅 ∈ ℝ⁺ → 𝑅 ∈ ( 0 [,) +∞ ) )
12	11	adantr	⊢ ( ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ( 0 [,) +∞ ) )
13	12	3ad2ant3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → 𝑅 ∈ ( 0 [,) +∞ ) )
14		eqid	⊢ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
15	1 2 3 4 5 14	2sphere0	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
16	15	eleq2d	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ↔ 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ) )
17	13 16	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ↔ 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ) )
18		fveq1	⊢ ( 𝑝 = 𝑋 → ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) )
19	18	oveq2d	⊢ ( 𝑝 = 𝑋 → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · ( 𝑋 ‘ 1 ) ) )
20		fveq1	⊢ ( 𝑝 = 𝑋 → ( 𝑝 ‘ 2 ) = ( 𝑋 ‘ 2 ) )
21	20	oveq2d	⊢ ( 𝑝 = 𝑋 → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 𝐵 · ( 𝑋 ‘ 2 ) ) )
22	19 21	oveq12d	⊢ ( 𝑝 = 𝑋 → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) )
23	22	eqeq1d	⊢ ( 𝑝 = 𝑋 → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) )
24	23 8	elrab2	⊢ ( 𝑋 ∈ 𝐿 ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) )
25	24	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 ∈ 𝐿 ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) )
26	17 25	anbi12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑋 ∈ 𝐿 ) ↔ ( 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ∧ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) ) )
27	18	oveq1d	⊢ ( 𝑝 = 𝑋 → ( ( 𝑝 ‘ 1 ) ↑ 2 ) = ( ( 𝑋 ‘ 1 ) ↑ 2 ) )
28	20	oveq1d	⊢ ( 𝑝 = 𝑋 → ( ( 𝑝 ‘ 2 ) ↑ 2 ) = ( ( 𝑋 ‘ 2 ) ↑ 2 ) )
29	27 28	oveq12d	⊢ ( 𝑝 = 𝑋 → ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) )
30	29	eqeq1d	⊢ ( 𝑝 = 𝑋 → ( ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
31	30	elrab	⊢ ( 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
32		3simpa	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) )
33	32	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) )
34		simpl3	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) )
35	1 3	rrx2pxel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
36	1 3	rrx2pyel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
37	35 36	jca	⊢ ( 𝑋 ∈ 𝑃 → ( ( 𝑋 ‘ 1 ) ∈ ℝ ∧ ( 𝑋 ‘ 2 ) ∈ ℝ ) )
38	37	adantl	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) ∈ ℝ ∧ ( 𝑋 ‘ 2 ) ∈ ℝ ) )
39	6 7	itsclc0xyqsol	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ∧ ( ( 𝑋 ‘ 1 ) ∈ ℝ ∧ ( 𝑋 ‘ 2 ) ∈ ℝ ) ) → ( ( ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
40	33 34 38 39	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → ( ( ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
41	40	expcomd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 → ( ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
42	41	expimpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) → ( ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
43	42	com23	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) → ( ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
44	43	adantld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) → ( ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
45	31 44	syl5bi	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } → ( ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
46	45	impd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ∧ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
47	26 46	sylbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑋 ∈ 𝐿 ) → ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )

Metamath Proof Explorer

Theorem itsclc0

Proof