inlinecirc02plem

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

	Ref	Expression
Hypotheses	inlinecirc02p.i	$⊢ I = \{1, 2\}$
	inlinecirc02p.e	$⊢ E = msup$
	inlinecirc02p.p	$⊢ P = ℝ^{I}$
	inlinecirc02p.s	$⊢ S = Sphere (E)$
	inlinecirc02p.0	$⊢ \underset{˙}{0} = I \times \{0\}$
	inlinecirc02p.l	$⊢ L = {Line}_{M} (E)$
	inlinecirc02plem.q	$⊢ Q = A^{2} + B^{2}$
	inlinecirc02plem.d	$⊢ D = R^{2} Q - C^{2}$
	inlinecirc02plem.a	$⊢ A = X (2) - Y (2)$
	inlinecirc02plem.b	$⊢ B = Y (1) - X (1)$
	inlinecirc02plem.c	$⊢ C = X (2) Y (1) - X (1) Y (2)$
Assertion	inlinecirc02plem	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to \exists a \in P \exists b \in P ((\underset{˙}{0} S R) \cap (X L Y) = \{a, b\} \land a \neq b)$

Proof

Step	Hyp	Ref	Expression
1		inlinecirc02p.i	$⊢ I = \{1, 2\}$
2		inlinecirc02p.e	$⊢ E = msup$
3		inlinecirc02p.p	$⊢ P = ℝ^{I}$
4		inlinecirc02p.s	$⊢ S = Sphere (E)$
5		inlinecirc02p.0	$⊢ \underset{˙}{0} = I \times \{0\}$
6		inlinecirc02p.l	$⊢ L = {Line}_{M} (E)$
7		inlinecirc02plem.q	$⊢ Q = A^{2} + B^{2}$
8		inlinecirc02plem.d	$⊢ D = R^{2} Q - C^{2}$
9		inlinecirc02plem.a	$⊢ A = X (2) - Y (2)$
10		inlinecirc02plem.b	$⊢ B = Y (1) - X (1)$
11		inlinecirc02plem.c	$⊢ C = X (2) Y (1) - X (1) Y (2)$
12		simprr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to 0 < D$
13	12	gt0ne0d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to D \neq 0$
14	1 3	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
15	14	adantr	$⊢ (X \in P \land Y \in P) \to X (2) \in ℝ$
16	1 3	rrx2pyel	$⊢ Y \in P \to Y (2) \in ℝ$
17	16	adantl	$⊢ (X \in P \land Y \in P) \to Y (2) \in ℝ$
18	15 17	resubcld	$⊢ (X \in P \land Y \in P) \to X (2) - Y (2) \in ℝ$
19	9 18	eqeltrid	$⊢ (X \in P \land Y \in P) \to A \in ℝ$
20	19	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to A \in ℝ$
21	20	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to A \in ℝ$
22	1 3	rrx2pxel	$⊢ Y \in P \to Y (1) \in ℝ$
23	22	adantl	$⊢ (X \in P \land Y \in P) \to Y (1) \in ℝ$
24	1 3	rrx2pxel	$⊢ X \in P \to X (1) \in ℝ$
25	24	adantr	$⊢ (X \in P \land Y \in P) \to X (1) \in ℝ$
26	23 25	resubcld	$⊢ (X \in P \land Y \in P) \to Y (1) - X (1) \in ℝ$
27	10 26	eqeltrid	$⊢ (X \in P \land Y \in P) \to B \in ℝ$
28	27	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to B \in ℝ$
29	28	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B \in ℝ$
30	15 23	remulcld	$⊢ (X \in P \land Y \in P) \to X (2) Y (1) \in ℝ$
31	25 17	remulcld	$⊢ (X \in P \land Y \in P) \to X (1) Y (2) \in ℝ$
32	30 31	resubcld	$⊢ (X \in P \land Y \in P) \to X (2) Y (1) - X (1) Y (2) \in ℝ$
33	11 32	eqeltrid	$⊢ (X \in P \land Y \in P) \to C \in ℝ$
34	33	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to C \in ℝ$
35	34	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to C \in ℝ$
36	19 27 33	3jca	$⊢ (X \in P \land Y \in P) \to (A \in ℝ \land B \in ℝ \land C \in ℝ)$
37	36	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (A \in ℝ \land B \in ℝ \land C \in ℝ)$
38		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
39	38	adantr	$⊢ (R \in ℝ^{+} \land 0 < D) \to R \in ℝ$
40	7 8	itsclc0lem3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to D \in ℝ$
41	37 39 40	syl2an	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to D \in ℝ$
42	41 12	elrpd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to D \in ℝ^{+}$
43	42	rprege0d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (D \in ℝ \land 0 \leq D)$
44	7	resum2sqcl	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℝ$
45	19 27 44	syl2anc	$⊢ (X \in P \land Y \in P) \to Q \in ℝ$
46	45	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Q \in ℝ$
47	1 3 10 9	rrx2pnedifcoorneorr	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (B \neq 0 \lor A \neq 0)$
48	47	orcomd	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (A \neq 0 \lor B \neq 0)$
49	7	resum2sqorgt0	$⊢ (A \in ℝ \land B \in ℝ \land (A \neq 0 \lor B \neq 0)) \to 0 < Q$
50	20 28 48 49	syl3anc	$⊢ (X \in P \land Y \in P \land X \neq Y) \to 0 < Q$
51	50	gt0ne0d	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Q \neq 0$
52	46 51	jca	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Q \in ℝ \land Q \neq 0)$
53	52	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (Q \in ℝ \land Q \neq 0)$
54		itsclc0lem1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (D \in ℝ \land 0 \leq D) \land (Q \in ℝ \land Q \neq 0)) \to \frac{A C + B \sqrt{D}}{Q} \in ℝ$
55	21 29 35 43 53 54	syl311anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to \frac{A C + B \sqrt{D}}{Q} \in ℝ$
56		itsclc0lem2	$⊢ ((B \in ℝ \land A \in ℝ \land C \in ℝ) \land (D \in ℝ \land 0 \leq D) \land (Q \in ℝ \land Q \neq 0)) \to \frac{B C - A \sqrt{D}}{Q} \in ℝ$
57	29 21 35 43 53 56	syl311anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to \frac{B C - A \sqrt{D}}{Q} \in ℝ$
58	55 57	jca	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (\frac{A C + B \sqrt{D}}{Q} \in ℝ \land \frac{B C - A \sqrt{D}}{Q} \in ℝ)$
59	58	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to (\frac{A C + B \sqrt{D}}{Q} \in ℝ \land \frac{B C - A \sqrt{D}}{Q} \in ℝ)$
60	1 3	prelrrx2	$⊢ (\frac{A C + B \sqrt{D}}{Q} \in ℝ \land \frac{B C - A \sqrt{D}}{Q} \in ℝ) \to \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \in P$
61	59 60	syl	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \in P$
62		itsclc0lem2	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (D \in ℝ \land 0 \leq D) \land (Q \in ℝ \land Q \neq 0)) \to \frac{A C - B \sqrt{D}}{Q} \in ℝ$
63	21 29 35 43 53 62	syl311anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to \frac{A C - B \sqrt{D}}{Q} \in ℝ$
64		itsclc0lem1	$⊢ ((B \in ℝ \land A \in ℝ \land C \in ℝ) \land (D \in ℝ \land 0 \leq D) \land (Q \in ℝ \land Q \neq 0)) \to \frac{B C + A \sqrt{D}}{Q} \in ℝ$
65	29 21 35 43 53 64	syl311anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to \frac{B C + A \sqrt{D}}{Q} \in ℝ$
66	63 65	jca	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (\frac{A C - B \sqrt{D}}{Q} \in ℝ \land \frac{B C + A \sqrt{D}}{Q} \in ℝ)$
67	66	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to (\frac{A C - B \sqrt{D}}{Q} \in ℝ \land \frac{B C + A \sqrt{D}}{Q} \in ℝ)$
68	1 3	prelrrx2	$⊢ (\frac{A C - B \sqrt{D}}{Q} \in ℝ \land \frac{B C + A \sqrt{D}}{Q} \in ℝ) \to \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\} \in P$
69	67 68	syl	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\} \in P$
70		simpl	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (X \in P \land Y \in P \land X \neq Y)$
71		simprl	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to R \in ℝ^{+}$
72		0red	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to 0 \in ℝ$
73	72 41 12	ltled	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to 0 \leq D$
74	70 71 73	jca32	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D))$
75	74	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D))$
76	1 2 3 4 5 7 8 6 9 10 11	itsclinecirc0in	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\}$
77	75 76	syl	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to (\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\}$
78		opex	$⊢ ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \in V$
79		opex	$⊢ ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \in V$
80		opex	$⊢ ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \in V$
81		opex	$⊢ ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩ \in V$
82	80 81	pm3.2i	$⊢ (⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \in V \land ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩ \in V)$
83	48	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (A \neq 0 \lor B \neq 0)$
84	83	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to (A \neq 0 \lor B \neq 0)$
85		orcom	$⊢ (A \neq 0 \lor B \neq 0) \leftrightarrow (B \neq 0 \lor A \neq 0)$
86	21	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to A \in ℂ$
87	86	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to A \in ℂ$
88	35	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to C \in ℂ$
89	88	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to C \in ℂ$
90	87 89	mulcld	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to A C \in ℂ$
91	29	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B \in ℂ$
92	91	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to B \in ℂ$
93	41	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to D \in ℂ$
94	93	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to D \in ℂ$
95	94	sqrtcld	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to \sqrt{D} \in ℂ$
96	92 95	mulcld	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to B \sqrt{D} \in ℂ$
97	90 96	addcld	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to A C + B \sqrt{D} \in ℂ$
98	90 96	subcld	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to A C - B \sqrt{D} \in ℂ$
99	46	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to Q \in ℝ$
100	99	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to Q \in ℂ$
101	51	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to Q \neq 0$
102	100 101	jca	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (Q \in ℂ \land Q \neq 0)$
103	102	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to (Q \in ℂ \land Q \neq 0)$
104		div11	$⊢ (A C + B \sqrt{D} \in ℂ \land A C - B \sqrt{D} \in ℂ \land (Q \in ℂ \land Q \neq 0)) \to (\frac{A C + B \sqrt{D}}{Q} = \frac{A C - B \sqrt{D}}{Q} \leftrightarrow A C + B \sqrt{D} = A C - B \sqrt{D})$
105	97 98 103 104	syl3anc	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to (\frac{A C + B \sqrt{D}}{Q} = \frac{A C - B \sqrt{D}}{Q} \leftrightarrow A C + B \sqrt{D} = A C - B \sqrt{D})$
106		addsubeq0	$⊢ (A C \in ℂ \land B \sqrt{D} \in ℂ) \to (A C + B \sqrt{D} = A C - B \sqrt{D} \leftrightarrow B \sqrt{D} = 0)$
107	90 96 106	syl2anc	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to (A C + B \sqrt{D} = A C - B \sqrt{D} \leftrightarrow B \sqrt{D} = 0)$
108	41 73	resqrtcld	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to \sqrt{D} \in ℝ$
109	108	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to \sqrt{D} \in ℂ$
110	91 109	mul0ord	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (B \sqrt{D} = 0 \leftrightarrow (B = 0 \lor \sqrt{D} = 0))$
111	110	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to (B \sqrt{D} = 0 \leftrightarrow (B = 0 \lor \sqrt{D} = 0))$
112		eqneqall	$⊢ B = 0 \to (B \neq 0 \to D = 0)$
113	112	com12	$⊢ B \neq 0 \to (B = 0 \to D = 0)$
114	113	adantl	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to (B = 0 \to D = 0)$
115		sqrt00	$⊢ (D \in ℝ \land 0 \leq D) \to (\sqrt{D} = 0 \leftrightarrow D = 0)$
116	41 73 115	syl2anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (\sqrt{D} = 0 \leftrightarrow D = 0)$
117	116	biimpd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (\sqrt{D} = 0 \to D = 0)$
118	117	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to (\sqrt{D} = 0 \to D = 0)$
119	114 118	jaod	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to ((B = 0 \lor \sqrt{D} = 0) \to D = 0)$
120	111 119	sylbid	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to (B \sqrt{D} = 0 \to D = 0)$
121	107 120	sylbid	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to (A C + B \sqrt{D} = A C - B \sqrt{D} \to D = 0)$
122	105 121	sylbid	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to (\frac{A C + B \sqrt{D}}{Q} = \frac{A C - B \sqrt{D}}{Q} \to D = 0)$
123	122	necon3d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land B \neq 0) \to (D \neq 0 \to \frac{A C + B \sqrt{D}}{Q} \neq \frac{A C - B \sqrt{D}}{Q})$
124	123	impancom	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to (B \neq 0 \to \frac{A C + B \sqrt{D}}{Q} \neq \frac{A C - B \sqrt{D}}{Q})$
125	124	imp	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land B \neq 0) \to \frac{A C + B \sqrt{D}}{Q} \neq \frac{A C - B \sqrt{D}}{Q}$
126	125	olcd	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land B \neq 0) \to (1 \neq 1 \lor \frac{A C + B \sqrt{D}}{Q} \neq \frac{A C - B \sqrt{D}}{Q})$
127		1ex	$⊢ 1 \in V$
128		ovex	$⊢ \frac{A C + B \sqrt{D}}{Q} \in V$
129	127 128	opthne	$⊢ ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \leftrightarrow (1 \neq 1 \lor \frac{A C + B \sqrt{D}}{Q} \neq \frac{A C - B \sqrt{D}}{Q})$
130	126 129	sylibr	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land B \neq 0) \to ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩$
131		1ne2	$⊢ 1 \neq 2$
132	131	orci	$⊢ (1 \neq 2 \lor \frac{A C + B \sqrt{D}}{Q} \neq \frac{B C + A \sqrt{D}}{Q})$
133	127 128	opthne	$⊢ ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩ \leftrightarrow (1 \neq 2 \lor \frac{A C + B \sqrt{D}}{Q} \neq \frac{B C + A \sqrt{D}}{Q})$
134	132 133	mpbir	$⊢ ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩$
135	130 134	jctir	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land B \neq 0) \to (⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩)$
136	135	ex	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to (B \neq 0 \to (⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩))$
137	27 33	remulcld	$⊢ (X \in P \land Y \in P) \to B C \in ℝ$
138	137	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to B C \in ℝ$
139	138	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B C \in ℝ$
140	21 108	remulcld	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to A \sqrt{D} \in ℝ$
141	139 140	resubcld	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B C - A \sqrt{D} \in ℝ$
142	141	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B C - A \sqrt{D} \in ℂ$
143	142	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to B C - A \sqrt{D} \in ℂ$
144	29 35	remulcld	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B C \in ℝ$
145	144 140	readdcld	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B C + A \sqrt{D} \in ℝ$
146	145	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to B C + A \sqrt{D} \in ℝ$
147	146	recnd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to B C + A \sqrt{D} \in ℂ$
148	102	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (Q \in ℂ \land Q \neq 0)$
149		div11	$⊢ (B C - A \sqrt{D} \in ℂ \land B C + A \sqrt{D} \in ℂ \land (Q \in ℂ \land Q \neq 0)) \to (\frac{B C - A \sqrt{D}}{Q} = \frac{B C + A \sqrt{D}}{Q} \leftrightarrow B C - A \sqrt{D} = B C + A \sqrt{D})$
150	143 147 148 149	syl3anc	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (\frac{B C - A \sqrt{D}}{Q} = \frac{B C + A \sqrt{D}}{Q} \leftrightarrow B C - A \sqrt{D} = B C + A \sqrt{D})$
151	139	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B C \in ℂ$
152	140	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to A \sqrt{D} \in ℂ$
153	151 152	jca	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (B C \in ℂ \land A \sqrt{D} \in ℂ)$
154	153	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (B C \in ℂ \land A \sqrt{D} \in ℂ)$
155		eqcom	$⊢ B C - A \sqrt{D} = B C + A \sqrt{D} \leftrightarrow B C + A \sqrt{D} = B C - A \sqrt{D}$
156		addsubeq0	$⊢ (B C \in ℂ \land A \sqrt{D} \in ℂ) \to (B C + A \sqrt{D} = B C - A \sqrt{D} \leftrightarrow A \sqrt{D} = 0)$
157	155 156	bitrid	$⊢ (B C \in ℂ \land A \sqrt{D} \in ℂ) \to (B C - A \sqrt{D} = B C + A \sqrt{D} \leftrightarrow A \sqrt{D} = 0)$
158	154 157	syl	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (B C - A \sqrt{D} = B C + A \sqrt{D} \leftrightarrow A \sqrt{D} = 0)$
159	86 109	mul0ord	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (A \sqrt{D} = 0 \leftrightarrow (A = 0 \lor \sqrt{D} = 0))$
160	159	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (A \sqrt{D} = 0 \leftrightarrow (A = 0 \lor \sqrt{D} = 0))$
161		eqneqall	$⊢ A = 0 \to (A \neq 0 \to D = 0)$
162	161	com12	$⊢ A \neq 0 \to (A = 0 \to D = 0)$
163	162	adantl	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (A = 0 \to D = 0)$
164	117	adantr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (\sqrt{D} = 0 \to D = 0)$
165	163 164	jaod	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to ((A = 0 \lor \sqrt{D} = 0) \to D = 0)$
166	160 165	sylbid	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (A \sqrt{D} = 0 \to D = 0)$
167	158 166	sylbid	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (B C - A \sqrt{D} = B C + A \sqrt{D} \to D = 0)$
168	150 167	sylbid	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (\frac{B C - A \sqrt{D}}{Q} = \frac{B C + A \sqrt{D}}{Q} \to D = 0)$
169	168	necon3d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land A \neq 0) \to (D \neq 0 \to \frac{B C - A \sqrt{D}}{Q} \neq \frac{B C + A \sqrt{D}}{Q})$
170	169	impancom	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to (A \neq 0 \to \frac{B C - A \sqrt{D}}{Q} \neq \frac{B C + A \sqrt{D}}{Q})$
171	170	imp	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land A \neq 0) \to \frac{B C - A \sqrt{D}}{Q} \neq \frac{B C + A \sqrt{D}}{Q}$
172	171	olcd	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land A \neq 0) \to (2 \neq 2 \lor \frac{B C - A \sqrt{D}}{Q} \neq \frac{B C + A \sqrt{D}}{Q})$
173		2ex	$⊢ 2 \in V$
174		ovex	$⊢ \frac{B C - A \sqrt{D}}{Q} \in V$
175	173 174	opthne	$⊢ ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩ \leftrightarrow (2 \neq 2 \lor \frac{B C - A \sqrt{D}}{Q} \neq \frac{B C + A \sqrt{D}}{Q})$
176	172 175	sylibr	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land A \neq 0) \to ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩$
177	131	necomi	$⊢ 2 \neq 1$
178	177	orci	$⊢ (2 \neq 1 \lor \frac{B C - A \sqrt{D}}{Q} \neq \frac{A C - B \sqrt{D}}{Q})$
179	173 174	opthne	$⊢ ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \leftrightarrow (2 \neq 1 \lor \frac{B C - A \sqrt{D}}{Q} \neq \frac{A C - B \sqrt{D}}{Q})$
180	178 179	mpbir	$⊢ ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩$
181	176 180	jctil	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land A \neq 0) \to (⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩)$
182	181	ex	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to (A \neq 0 \to (⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩))$
183	136 182	orim12d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to ((B \neq 0 \lor A \neq 0) \to ((⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩) \lor (⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩)))$
184	85 183	biimtrid	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to ((A \neq 0 \lor B \neq 0) \to ((⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩) \lor (⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩)))$
185	84 184	mpd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to ((⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩) \lor (⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩))$
186		prneimg	$⊢ ((⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \in V \land ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \in V) \land (⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \in V \land ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩ \in V)) \to (((⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩) \lor (⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩)) \to \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\})$
187	186	imp	$⊢ (((⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \in V \land ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \in V) \land (⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \in V \land ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩ \in V)) \land ((⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨1, \frac{A C + B \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩) \lor (⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨1, \frac{A C - B \sqrt{D}}{Q}⟩ \land ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩ \neq ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩))) \to \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}$
188	78 79 82 185 187	mpsyl4anc	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}$
189	77 188	jca	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to ((\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\} \land \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\})$
190	61 69 189	3jca	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to (\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \in P \land \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\} \in P \land ((\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\} \land \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}))$
191	13 190	mpdan	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to (\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \in P \land \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\} \in P \land ((\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\} \land \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}))$
192		preq1	$⊢ a = \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \to \{a, b\} = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, b\}$
193	192	eqeq2d	$⊢ a = \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \to ((\underset{˙}{0} S R) \cap (X L Y) = \{a, b\} \leftrightarrow (\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, b\})$
194		neeq1	$⊢ a = \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \to (a \neq b \leftrightarrow \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq b)$
195	193 194	anbi12d	$⊢ a = \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \to (((\underset{˙}{0} S R) \cap (X L Y) = \{a, b\} \land a \neq b) \leftrightarrow ((\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, b\} \land \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq b))$
196		preq2	$⊢ b = \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\} \to \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, b\} = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\}$
197	196	eqeq2d	$⊢ b = \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\} \to ((\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, b\} \leftrightarrow (\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\})$
198		neeq2	$⊢ b = \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\} \to (\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq b \leftrightarrow \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\})$
199	197 198	anbi12d	$⊢ b = \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\} \to (((\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, b\} \land \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq b) \leftrightarrow ((\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\} \land \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}))$
200	195 199	rspc2ev	$⊢ (\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \in P \land \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\} \in P \land ((\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\} \land \{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\} \neq \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\})) \to \exists a \in P \exists b \in P ((\underset{˙}{0} S R) \cap (X L Y) = \{a, b\} \land a \neq b)$
201	191 200	syl	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to \exists a \in P \exists b \in P ((\underset{˙}{0} S R) \cap (X L Y) = \{a, b\} \land a \neq b)$

Metamath Proof Explorer

Theorem inlinecirc02plem

Proof