inlinecirc02plem - Mathbox for Alexander van der Vekens

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

Theorem inlinecirc02plem 50103

Description: Lemma for inlinecirc02p 50104. (Contributed by AV, 7-May-2023.) (Revised by AV, 15-May-2023.)

**Hypotheses**
Ref	Expression
inlinecirc02p.i	⊢ 𝐼 = (0..^2)
inlinecirc02p.e	⊢ 𝐸 = (ℝ^‘𝐼)
inlinecirc02p.p	⊢ 𝑃 = (ℝ ↑_m 𝐼)
inlinecirc02p.s	⊢ 𝑆 = (Sphere‘𝐸)
inlinecirc02p.0	⊢ 0 = ⟨“00”⟩
inlinecirc02p.l	⊢ 𝐿 = (Line_M‘𝐸)
inlinecirc02plem.q	⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))
inlinecirc02plem.d	⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
inlinecirc02plem.a	⊢ 𝐴 = ((𝑋‘1) − (𝑌‘1))
inlinecirc02plem.b	⊢ 𝐵 = ((𝑌‘0) − (𝑋‘0))
inlinecirc02plem.c	⊢ 𝐶 = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))

**Assertion**
Ref	Expression
inlinecirc02plem	⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏))

Distinct variable groups: 𝐿,𝑎,𝑏 𝑃,𝑎,𝑏 𝑅,𝑎,𝑏 𝑆,𝑎,𝑏 𝑋,𝑎,𝑏 𝑌,𝑎,𝑏 0 ,𝑎,𝑏 𝐴,𝑎,𝑏 𝐵,𝑎,𝑏 𝐶,𝑎,𝑏 𝐷,𝑎,𝑏 𝑄,𝑎,𝑏 Allowed substitution hints: 𝐸(𝑎, 𝑏) 𝐼(𝑎, 𝑏)

**Proof of Theorem inlinecirc02plem**
Step	Hyp	Ref	Expression
1		simprr 785	. . . 4 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 0 < 𝐷)
2	1	gt0ne0d 11907	. . 3 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝐷 ≠ 0)
3		inlinecirc02plem.a	. . . . . . . . . . 11 ⊢ 𝐴 = ((𝑋‘1) − (𝑌‘1))
4		inlinecirc02p.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (0..^2)
5		inlinecirc02p.p	. . . . . . . . . . . . . 14 ⊢ 𝑃 = (ℝ ↑_m 𝐼)
6	4, 5	rrx2pyel 50029	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ)
7	6	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋‘1) ∈ ℝ)
8	4, 5	rrx2pyel 50029	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ)
9	8	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑌‘1) ∈ ℝ)
10	7, 9	resubcld 11771	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘1) − (𝑌‘1)) ∈ ℝ)
11	3, 10	eqeltrid 2868	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐴 ∈ ℝ)
12	11	3adant3 1150	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐴 ∈ ℝ)
13	12	adantr 486	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝐴 ∈ ℝ)
14		inlinecirc02plem.b	. . . . . . . . . . 11 ⊢ 𝐵 = ((𝑌‘0) − (𝑋‘0))
15	4, 5	rrx2pxel 50028	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘0) ∈ ℝ)
16	15	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑌‘0) ∈ ℝ)
17	4, 5	rrx2pxel 50028	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑃 → (𝑋‘0) ∈ ℝ)
18	17	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋‘0) ∈ ℝ)
19	16, 18	resubcld 11771	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑌‘0) − (𝑋‘0)) ∈ ℝ)
20	14, 19	eqeltrid 2868	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐵 ∈ ℝ)
21	20	3adant3 1150	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐵 ∈ ℝ)
22	21	adantr 486	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝐵 ∈ ℝ)
23		inlinecirc02plem.c	. . . . . . . . . . 11 ⊢ 𝐶 = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))
24	7, 16	remulcld 11366	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘1) · (𝑌‘0)) ∈ ℝ)
25	18, 9	remulcld 11366	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘0) · (𝑌‘1)) ∈ ℝ)
26	24, 25	resubcld 11771	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) ∈ ℝ)
27	23, 26	eqeltrid 2868	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐶 ∈ ℝ)
28	27	3adant3 1150	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐶 ∈ ℝ)
29	28	adantr 486	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝐶 ∈ ℝ)
30	11, 20, 27	3jca 1146	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ))
31	30	3adant3 1150	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ))
32		rpre 13156	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
33	32	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷) → 𝑅 ∈ ℝ)
34		inlinecirc02plem.q	. . . . . . . . . . . 12 ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))
35		inlinecirc02plem.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
36	34, 35	itsclc0lem3 50075	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → 𝐷 ∈ ℝ)
37	31, 33, 36	syl2an 608	. . . . . . . . . 10 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝐷 ∈ ℝ)
38	37, 1	elrpd 13188	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝐷 ∈ ℝ⁺)
39	38	rprege0d 13198	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))
40	34	resum2sqcl 50023	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
41	11, 20, 40	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝑄 ∈ ℝ)
42	41	3adant3 1150	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝑄 ∈ ℝ)
43	4, 5, 14, 3	rrx2pnedifcoorneorr 50035	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐵 ≠ 0 ∨ 𝐴 ≠ 0))
44	43	orcomd 885	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0))
45	34	resum2sqorgt0 50026	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < 𝑄)
46	12, 21, 44, 45	syl3anc 1399	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 0 < 𝑄)
47	46	gt0ne0d 11907	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝑄 ≠ 0)
48	42, 47	jca 521	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0))
49	48	adantr 486	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0))
50		itsclc0lem1 50073	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ)
51	13, 22, 29, 39, 49, 50	syl311anc 1412	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ)
52		itsclc0lem2 50074	. . . . . . . 8 ⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)
53	22, 13, 29, 39, 49, 52	syl311anc 1412	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)
54	51, 53	jca 521	. . . . . 6 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ))
55	54	adantr 486	. . . . 5 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ))
56	4, 5	prelrrx2 50030	. . . . 5 ⊢ (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) → ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ∈ 𝑃)
57	55, 56	syl 18	. . . 4 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ∈ 𝑃)
58		itsclc0lem2 50074	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ)
59	13, 22, 29, 39, 49, 58	syl311anc 1412	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ)
60		itsclc0lem1 50073	. . . . . . . 8 ⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)
61	22, 13, 29, 39, 49, 60	syl311anc 1412	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)
62	59, 61	jca 521	. . . . . 6 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ))
63	62	adantr 486	. . . . 5 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ))
64	4, 5	prelrrx2 50030	. . . . 5 ⊢ (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) → ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ∈ 𝑃)
65	63, 64	syl 18	. . . 4 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ∈ 𝑃)
66		simpl 488	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
67		simprl 783	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝑅 ∈ ℝ⁺)
68		0red 11338	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 0 ∈ ℝ)
69	68, 37, 1	ltled 11485	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 0 ≤ 𝐷)
70	66, 67, 69	jca32 525	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)))
71	70	adantr 486	. . . . . 6 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)))
72		inlinecirc02p.e	. . . . . . 7 ⊢ 𝐸 = (ℝ^‘𝐼)
73		inlinecirc02p.s	. . . . . . 7 ⊢ 𝑆 = (Sphere‘𝐸)
74		inlinecirc02p.0	. . . . . . 7 ⊢ 0 = ⟨“00”⟩
75		inlinecirc02p.l	. . . . . . 7 ⊢ 𝐿 = (Line_M‘𝐸)
76	4, 72, 5, 73, 74, 34, 35, 75, 3, 14, 23	itsclinecirc0in 50092	. . . . . 6 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩})
77	71, 76	syl 18	. . . . 5 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩})
78	51	ad2antrr 739	. . . . . . . 8 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ)
79	53	ad2antrr 739	. . . . . . . 8 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)
80	59	ad2antrr 739	. . . . . . . . 9 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ)
81	61	ad2antrr 739	. . . . . . . . 9 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)
82	80, 81	jca 521	. . . . . . . 8 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ))
83		simpr 490	. . . . . . . 8 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩)
84		s2eq2seq 15117	. . . . . . . . 9 ⊢ ((((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) ∧ ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)) → (⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ↔ ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
85	84	biimpa 482	. . . . . . . 8 ⊢ (((((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) ∧ ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
86	78, 79, 82, 83, 85	syl1111anc 854	. . . . . . 7 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
87	13	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝐴 ∈ ℂ)
88	87	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → 𝐴 ∈ ℂ)
89	29	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝐶 ∈ ℂ)
90	89	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → 𝐶 ∈ ℂ)
91	88, 90	mulcld 11356	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (𝐴 · 𝐶) ∈ ℂ)
92	22	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝐵 ∈ ℂ)
93	92	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
94	37	recnd 11364	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝐷 ∈ ℂ)
95	94	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → 𝐷 ∈ ℂ)
96	95	sqrtcld 15636	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (√‘𝐷) ∈ ℂ)
97	93, 96	mulcld 11356	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (𝐵 · (√‘𝐷)) ∈ ℂ)
98	91, 97	addcld 11355	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ)
99	91, 97	subcld 11696	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
100	42	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝑄 ∈ ℝ)
101	100	recnd 11364	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝑄 ∈ ℂ)
102	47	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → 𝑄 ≠ 0)
103	101, 102	jca 521	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0))
104	103	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0))
105		div11 12029	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ ∧ ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ ∧ (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ↔ ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))))
106	98, 99, 104, 105	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ↔ ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))))
107		addsubeq0 48571	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ↔ (𝐵 · (√‘𝐷)) = 0))
108	91, 97, 107	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ↔ (𝐵 · (√‘𝐷)) = 0))
109	37, 69	resqrtcld 15614	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (√‘𝐷) ∈ ℝ)
110	109	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (√‘𝐷) ∈ ℂ)
111	92, 110	mul0ord 11991	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((𝐵 · (√‘𝐷)) = 0 ↔ (𝐵 = 0 ∨ (√‘𝐷) = 0)))
112	111	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((𝐵 · (√‘𝐷)) = 0 ↔ (𝐵 = 0 ∨ (√‘𝐷) = 0)))
113		eqneqall 2970	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 0 → (𝐵 ≠ 0 → 𝐷 = 0))
114	113	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ≠ 0 → (𝐵 = 0 → 𝐷 = 0))
115	114	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (𝐵 = 0 → 𝐷 = 0))
116		sqrt00 15459	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) → ((√‘𝐷) = 0 ↔ 𝐷 = 0))
117	37, 69, 116	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((√‘𝐷) = 0 ↔ 𝐷 = 0))
118	117	biimpd 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((√‘𝐷) = 0 → 𝐷 = 0))
119	118	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((√‘𝐷) = 0 → 𝐷 = 0))
120	115, 119	jaod 873	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((𝐵 = 0 ∨ (√‘𝐷) = 0) → 𝐷 = 0))
121	112, 120	sylbid 243	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((𝐵 · (√‘𝐷)) = 0 → 𝐷 = 0))
122	108, 121	sylbid 243	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) → 𝐷 = 0))
123	106, 122	sylbid 243	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → 𝐷 = 0))
124	123	necon3d 2980	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (𝐷 ≠ 0 → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
125	124	impancom 457	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → (𝐵 ≠ 0 → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
126	125	imp 412	. . . . . . . . . 10 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐵 ≠ 0) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
127	126	adantlr 728	. . . . . . . . 9 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) ∧ 𝐵 ≠ 0) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
128	20, 27	remulcld 11366	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝐵 · 𝐶) ∈ ℝ)
129	128	3adant3 1150	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐵 · 𝐶) ∈ ℝ)
130	129	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (𝐵 · 𝐶) ∈ ℝ)
131	13, 109	remulcld 11366	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℝ)
132	130, 131	resubcld 11771	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℝ)
133	132	recnd 11364	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
134	133	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
135	130, 131	readdcld 11365	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℝ)
136	135	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℝ)
137	136	recnd 11364	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
138	103	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0))
139		div11 12029	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ ∧ ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ ∧ (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ↔ ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))))
140	134, 137, 138, 139	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ↔ ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))))
141	130	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (𝐵 · 𝐶) ∈ ℂ)
142	131	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
143	141, 142	jca 521	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ))
144	143	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ))
145		eqcom 2770	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ↔ ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))
146		addsubeq0 48571	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ↔ (𝐴 · (√‘𝐷)) = 0))
147	145, 146	bitrid 286	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ↔ (𝐴 · (√‘𝐷)) = 0))
148	144, 147	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ↔ (𝐴 · (√‘𝐷)) = 0))
149	87, 110	mul0ord 11991	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ((𝐴 · (√‘𝐷)) = 0 ↔ (𝐴 = 0 ∨ (√‘𝐷) = 0)))
150	149	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐴 · (√‘𝐷)) = 0 ↔ (𝐴 = 0 ∨ (√‘𝐷) = 0)))
151		eqneqall 2970	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 = 0 → (𝐴 ≠ 0 → 𝐷 = 0))
152	151	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ≠ 0 → (𝐴 = 0 → 𝐷 = 0))
153	152	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → (𝐴 = 0 → 𝐷 = 0))
154	118	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((√‘𝐷) = 0 → 𝐷 = 0))
155	153, 154	jaod 873	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐴 = 0 ∨ (√‘𝐷) = 0) → 𝐷 = 0))
156	150, 155	sylbid 243	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐴 · (√‘𝐷)) = 0 → 𝐷 = 0))
157	148, 156	sylbid 243	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) → 𝐷 = 0))
158	140, 157	sylbid 243	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝐷 = 0))
159	158	necon3d 2980	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → (𝐷 ≠ 0 → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
160	159	impancom 457	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → (𝐴 ≠ 0 → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
161	160	imp 412	. . . . . . . . . 10 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐴 ≠ 0) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))
162	161	adantlr 728	. . . . . . . . 9 ⊢ ((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) ∧ 𝐴 ≠ 0) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))
163	43	ad3antrrr 743	. . . . . . . . 9 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → (𝐵 ≠ 0 ∨ 𝐴 ≠ 0))
164	127, 162, 163	orim12da 980	. . . . . . . 8 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∨ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
165		neorian 3054	. . . . . . . 8 ⊢ (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∨ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) ↔ ¬ ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
166	164, 165	sylib 221	. . . . . . 7 ⊢ (((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩) → ¬ ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
167	86, 166	pm2.65da 829	. . . . . 6 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ¬ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩)
168	167	neqned 2966	. . . . 5 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩)
169	77, 168	jca 521	. . . 4 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩} ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩))
170	57, 65, 169	3jca 1146	. . 3 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → (⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ∈ 𝑃 ∧ ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ∈ 𝑃 ∧ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩} ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩)))
171	2, 170	mpdan 700	. 2 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → (⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ∈ 𝑃 ∧ ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ∈ 𝑃 ∧ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩} ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩)))
172		preq1 4694	. . . . 5 ⊢ (𝑎 = ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ → {𝑎, 𝑏} = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, 𝑏})
173	172	eqeq2d 2774	. . . 4 ⊢ (𝑎 = ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ → ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ↔ (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, 𝑏}))
174		neeq1 3021	. . . 4 ⊢ (𝑎 = ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ → (𝑎 ≠ 𝑏 ↔ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ 𝑏))
175	173, 174	anbi12d 644	. . 3 ⊢ (𝑎 = ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ → (((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏) ↔ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, 𝑏} ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ 𝑏)))
176		preq2 4695	. . . . 5 ⊢ (𝑏 = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩ → {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, 𝑏} = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩})
177	176	eqeq2d 2774	. . . 4 ⊢ (𝑏 = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩ → ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, 𝑏} ↔ (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩}))
178		neeq2 3022	. . . 4 ⊢ (𝑏 = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩ → (⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ 𝑏 ↔ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩))
179	177, 178	anbi12d 644	. . 3 ⊢ (𝑏 = ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩ → (((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, 𝑏} ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ 𝑏) ↔ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩} ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩)))
180	175, 179	rspc2ev 3592	. 2 ⊢ ((⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ∈ 𝑃 ∧ ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ∈ 𝑃 ∧ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩, ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩} ∧ ⟨“(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)”⟩ ≠ ⟨“(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)”⟩)) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏))
181	171, 180	syl 18	1 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 < 𝐷)) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∃wrex 3090 ∩ cin 4092 {cpr 4590 class class class wbr 5106 ‘cfv 6558 (class class class)co 7443 ↑_m cmap 8875 ℂcc 11225 ℝcr 11226 0cc0 11227 1c1 11228 + caddc 11230 · cmul 11232 < clt 11370 ≤ cle 11371 − cmin 11568 / cdiv 12000 2c2 12424 ℝ⁺crp 13147 ..^cfzo 13815 ↑cexp 14231 ⟨“cs2 15020 √csqrt 15429 ℝ^crrx 25734 Line_Mcline 50045 Spherecsph 50046

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 7775 ax-inf2 9669 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305 ax-addf 11306 ax-mulf 11307

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 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-isom 6567 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7717 df-om 7902 df-1st 8025 df-2nd 8026 df-supp 8205 df-tpos 8271 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-2o 8505 df-oadd 8508 df-er 8745 df-map 8877 df-ixp 8954 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-fsupp 9382 df-sup 9461 df-oi 9531 df-dju 10009 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-5 12435 df-6 12436 df-7 12437 df-8 12438 df-9 12439 df-n0 12634 df-z 12721 df-dec 12842 df-uz 12993 df-rp 13148 df-xneg 13268 df-xadd 13269 df-xmul 13270 df-ico 13509 df-icc 13510 df-fz 13667 df-fzo 13816 df-seq 14172 df-exp 14232 df-hash 14502 df-word 14686 df-concat 14743 df-s1 14770 df-substr 14817 df-pfx 14849 df-s2 15027 df-cj 15295 df-re 15296 df-im 15297 df-sqrt 15431 df-abs 15432 df-clim 15684 df-sum 15883 df-struct 17354 df-sets 17371 df-slot 17389 df-ndx 17401 df-base 17417 df-ress 17438 df-plusg 17470 df-mulr 17471 df-starv 17472 df-sca 17473 df-vsca 17474 df-ip 17475 df-tset 17476 df-ple 17477 df-ds 17479 df-unif 17480 df-hom 17481 df-cco 17482 df-0g 17641 df-gsum 17642 df-prds 17647 df-pws 17649 df-mgm 18845 df-sgrp 18937 df-mnd 18953 df-mhm 19007 df-grp 19176 df-minusg 19177 df-sbg 19178 df-subg 19362 df-ghm 19457 df-cntz 19561 df-cmn 20026 df-abl 20027 df-mgp 20391 df-rng 20405 df-ur 20438 df-ring 20491 df-cring 20492 df-oppr 20597 df-dvdsr 20617 df-unit 20618 df-invr 20648 df-dvr 20661 df-rhm 20732 df-subrng 20828 df-subrg 20852 df-drng 21012 df-field 21013 df-staf 21126 df-srng 21127 df-lmod 21167 df-lss 21237 df-sra 21478 df-rgmod 21479 df-xmet 21701 df-met 21702 df-cnfld 21709 df-refld 21941 df-dsmm 22068 df-frlm 22083 df-nm 24931 df-tng 24933 df-tcph 25520 df-rrx 25736 df-ehl 25737 df-line 50047 df-sph 50048

This theorem is used by: inlinecirc02p 50104

W3C validator