inlinecirc02plem

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

	Ref	Expression
Hypotheses	inlinecirc02p.i	$⊢ I = (0 ..^2)$
	inlinecirc02p.e	$⊢ E = I$
	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 (1) - Y (1)$
	inlinecirc02plem.b	$⊢ B = Y (0) - X (0)$
	inlinecirc02plem.c	$⊢ C = X (1) Y (0) - X (0) Y (1)$
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 = (0 ..^2)$
2		inlinecirc02p.e	$⊢ E = I$
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 (1) - Y (1)$
10		inlinecirc02plem.b	$⊢ B = Y (0) - X (0)$
11		inlinecirc02plem.c	$⊢ C = X (1) Y (0) - X (0) Y (1)$
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 (1) \in ℝ$
15	14	adantr	$⊢ (X \in P \land Y \in P) \to X (1) \in ℝ$
16	1 3	rrx2pyel	$⊢ Y \in P \to Y (1) \in ℝ$
17	16	adantl	$⊢ (X \in P \land Y \in P) \to Y (1) \in ℝ$
18	15 17	resubcld	$⊢ (X \in P \land Y \in P) \to X (1) - Y (1) \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 (0) \in ℝ$
23	22	adantl	$⊢ (X \in P \land Y \in P) \to Y (0) \in ℝ$
24	1 3	rrx2pxel	$⊢ X \in P \to X (0) \in ℝ$
25	24	adantr	$⊢ (X \in P \land Y \in P) \to X (0) \in ℝ$
26	23 25	resubcld	$⊢ (X \in P \land Y \in P) \to Y (0) - X (0) \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 (1) Y (0) \in ℝ$
31	25 17	remulcld	$⊢ (X \in P \land Y \in P) \to X (0) Y (1) \in ℝ$
32	30 31	resubcld	$⊢ (X \in P \land Y \in P) \to X (1) Y (0) - X (0) Y (1) \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 ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\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 ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\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 ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\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 ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\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) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\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) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\}$
78	55	ad2antrr	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to \frac{A C + B \sqrt{D}}{Q} \in ℝ$
79	57	ad2antrr	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to \frac{B C - A \sqrt{D}}{Q} \in ℝ$
80	63	ad2antrr	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to \frac{A C - B \sqrt{D}}{Q} \in ℝ$
81	65	ad2antrr	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to \frac{B C + A \sqrt{D}}{Q} \in ℝ$
82	80 81	jca	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to (\frac{A C - B \sqrt{D}}{Q} \in ℝ \land \frac{B C + A \sqrt{D}}{Q} \in ℝ)$
83		simpr	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩$
84		s2eq2seq	$⊢ ((\frac{A C + B \sqrt{D}}{Q} \in ℝ \land \frac{B C - A \sqrt{D}}{Q} \in ℝ) \land (\frac{A C - B \sqrt{D}}{Q} \in ℝ \land \frac{B C + A \sqrt{D}}{Q} \in ℝ)) \to (⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩ \leftrightarrow (\frac{A C + B \sqrt{D}}{Q} = \frac{A C - B \sqrt{D}}{Q} \land \frac{B C - A \sqrt{D}}{Q} = \frac{B C + A \sqrt{D}}{Q}))$
85	84	biimpa	$⊢ (((\frac{A C + B \sqrt{D}}{Q} \in ℝ \land \frac{B C - A \sqrt{D}}{Q} \in ℝ) \land (\frac{A C - B \sqrt{D}}{Q} \in ℝ \land \frac{B C + A \sqrt{D}}{Q} \in ℝ)) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to (\frac{A C + B \sqrt{D}}{Q} = \frac{A C - B \sqrt{D}}{Q} \land \frac{B C - A \sqrt{D}}{Q} = \frac{B C + A \sqrt{D}}{Q})$
86	78 79 82 83 85	syl1111anc	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to (\frac{A C + B \sqrt{D}}{Q} = \frac{A C - B \sqrt{D}}{Q} \land \frac{B C - A \sqrt{D}}{Q} = \frac{B C + A \sqrt{D}}{Q})$
87	21	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to A \in ℂ$
88	87	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 ℂ$
89	35	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to C \in ℂ$
90	89	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 ℂ$
91	88 90	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 ℂ$
92	29	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B \in ℂ$
93	92	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 ℂ$
94	41	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to D \in ℂ$
95	94	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 ℂ$
96	95	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 ℂ$
97	93 96	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 ℂ$
98	91 97	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 ℂ$
99	91 97	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 ℂ$
100	46	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to Q \in ℝ$
101	100	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to Q \in ℂ$
102	51	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to Q \neq 0$
103	101 102	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)$
104	103	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)$
105		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})$
106	98 99 104 105	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})$
107		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)$
108	91 97 107	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)$
109	41 73	resqrtcld	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to \sqrt{D} \in ℝ$
110	109	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to \sqrt{D} \in ℂ$
111	92 110	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))$
112	111	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))$
113		eqneqall	$⊢ B = 0 \to (B \neq 0 \to D = 0)$
114	113	com12	$⊢ B \neq 0 \to (B = 0 \to D = 0)$
115	114	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)$
116		sqrt00	$⊢ (D \in ℝ \land 0 \leq D) \to (\sqrt{D} = 0 \leftrightarrow D = 0)$
117	41 73 116	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)$
118	117	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)$
119	118	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)$
120	115 119	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)$
121	112 120	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)$
122	108 121	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)$
123	106 122	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)$
124	123	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})$
125	124	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})$
126	125	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}$
127	126	adantlr	$⊢ (((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \land B \neq 0) \to \frac{A C + B \sqrt{D}}{Q} \neq \frac{A C - B \sqrt{D}}{Q}$
128	27 33	remulcld	$⊢ (X \in P \land Y \in P) \to B C \in ℝ$
129	128	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to B C \in ℝ$
130	129	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B C \in ℝ$
131	21 109	remulcld	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to A \sqrt{D} \in ℝ$
132	130 131	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 ℝ$
133	132	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 ℂ$
134	133	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 ℂ$
135	130 131	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 ℝ$
136	135	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 ℝ$
137	136	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 ℂ$
138	103	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)$
139		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})$
140	134 137 138 139	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})$
141	130	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to B C \in ℂ$
142	131	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \to A \sqrt{D} \in ℂ$
143	141 142	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 ℂ)$
144	143	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 ℂ)$
145		eqcom	$⊢ B C - A \sqrt{D} = B C + A \sqrt{D} \leftrightarrow B C + A \sqrt{D} = B C - A \sqrt{D}$
146		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)$
147	145 146	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)$
148	144 147	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)$
149	87 110	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))$
150	149	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))$
151		eqneqall	$⊢ A = 0 \to (A \neq 0 \to D = 0)$
152	151	com12	$⊢ A \neq 0 \to (A = 0 \to D = 0)$
153	152	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)$
154	118	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)$
155	153 154	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)$
156	150 155	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)$
157	148 156	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)$
158	140 157	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)$
159	158	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})$
160	159	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})$
161	160	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}$
162	161	adantlr	$⊢ (((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \land A \neq 0) \to \frac{B C - A \sqrt{D}}{Q} \neq \frac{B C + A \sqrt{D}}{Q}$
163	47	ad3antrrr	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to (B \neq 0 \lor A \neq 0)$
164	127 162 163	orim12da	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to (\frac{A C + B \sqrt{D}}{Q} \neq \frac{A C - B \sqrt{D}}{Q} \lor \frac{B C - A \sqrt{D}}{Q} \neq \frac{B C + A \sqrt{D}}{Q})$
165		neorian	$⊢ (\frac{A C + B \sqrt{D}}{Q} \neq \frac{A C - B \sqrt{D}}{Q} \lor \frac{B C - A \sqrt{D}}{Q} \neq \frac{B C + A \sqrt{D}}{Q}) \leftrightarrow \neg (\frac{A C + B \sqrt{D}}{Q} = \frac{A C - B \sqrt{D}}{Q} \land \frac{B C - A \sqrt{D}}{Q} = \frac{B C + A \sqrt{D}}{Q})$
166	164 165	sylib	$⊢ ((((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩) \to \neg (\frac{A C + B \sqrt{D}}{Q} = \frac{A C - B \sqrt{D}}{Q} \land \frac{B C - A \sqrt{D}}{Q} = \frac{B C + A \sqrt{D}}{Q})$
167	86 166	pm2.65da	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < D)) \land D \neq 0) \to \neg ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩$
168	167	neqned	$⊢ (((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}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩$
169	77 168	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) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\} \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩)$
170	61 69 169	3jca	$⊢ (((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}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \in P \land ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩ \in P \land ((\underset{˙}{0} S R) \cap (X L Y) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\} \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩))$
171	13 170	mpdan	$⊢ ((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}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \in P \land ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩ \in P \land ((\underset{˙}{0} S R) \cap (X L Y) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\} \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩))$
172		preq1	$⊢ a = ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \to \{a, b\} = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, b\}$
173	172	eqeq2d	$⊢ a = ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\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) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, b\})$
174		neeq1	$⊢ a = ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \to (a \neq b \leftrightarrow ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq b)$
175	173 174	anbi12d	$⊢ a = ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\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) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, b\} \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq b))$
176		preq2	$⊢ b = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩ \to \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, b\} = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\}$
177	176	eqeq2d	$⊢ b = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩ \to ((\underset{˙}{0} S R) \cap (X L Y) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, b\} \leftrightarrow (\underset{˙}{0} S R) \cap (X L Y) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\})$
178		neeq2	$⊢ b = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩ \to (⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq b \leftrightarrow ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩)$
179	177 178	anbi12d	$⊢ b = ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩ \to (((\underset{˙}{0} S R) \cap (X L Y) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, b\} \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq b) \leftrightarrow ((\underset{˙}{0} S R) \cap (X L Y) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\} \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩))$
180	175 179	rspc2ev	$⊢ (⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \in P \land ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩ \in P \land ((\underset{˙}{0} S R) \cap (X L Y) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\} \land ⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩ \neq ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\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)$
181	171 180	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