Users' Mathboxes 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 46862
Description: Lemma for inlinecirc02p 46863. (Contributed by AV, 7-May-2023.) (Revised by AV, 15-May-2023.)
Hypotheses
Ref Expression
inlinecirc02p.i 𝐼 = {1, 2}
inlinecirc02p.e 𝐸 = (ℝ^‘𝐼)
inlinecirc02p.p 𝑃 = (ℝ ↑m 𝐼)
inlinecirc02p.s 𝑆 = (Sphere‘𝐸)
inlinecirc02p.0 0 = (𝐼 × {0})
inlinecirc02p.l 𝐿 = (LineM𝐸)
inlinecirc02plem.q 𝑄 = ((𝐴↑2) + (𝐵↑2))
inlinecirc02plem.d 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
inlinecirc02plem.a 𝐴 = ((𝑋‘2) − (𝑌‘2))
inlinecirc02plem.b 𝐵 = ((𝑌‘1) − (𝑋‘1))
inlinecirc02plem.c 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))
Assertion
Ref Expression
inlinecirc02plem (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ∃𝑎𝑃𝑏𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎𝑏))
Distinct variable groups:   𝐿,𝑎,𝑏   𝑃,𝑎,𝑏   𝑅,𝑎,𝑏   𝑆,𝑎,𝑏   𝑋,𝑎,𝑏   𝑌,𝑎,𝑏   0 ,𝑎,𝑏   𝐴,𝑎,𝑏   𝐵,𝑎,𝑏   𝐶,𝑎,𝑏   𝐷,𝑎,𝑏   𝑄,𝑎,𝑏
Allowed substitution hints:   𝐸(𝑎,𝑏)   𝐼(𝑎,𝑏)

Proof of Theorem inlinecirc02plem
StepHypRef Expression
1 simprr 771 . . . 4 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 0 < 𝐷)
21gt0ne0d 11719 . . 3 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝐷 ≠ 0)
3 inlinecirc02plem.a . . . . . . . . . . 11 𝐴 = ((𝑋‘2) − (𝑌‘2))
4 inlinecirc02p.i . . . . . . . . . . . . . 14 𝐼 = {1, 2}
5 inlinecirc02p.p . . . . . . . . . . . . . 14 𝑃 = (ℝ ↑m 𝐼)
64, 5rrx2pyel 46788 . . . . . . . . . . . . 13 (𝑋𝑃 → (𝑋‘2) ∈ ℝ)
76adantr 481 . . . . . . . . . . . 12 ((𝑋𝑃𝑌𝑃) → (𝑋‘2) ∈ ℝ)
84, 5rrx2pyel 46788 . . . . . . . . . . . . 13 (𝑌𝑃 → (𝑌‘2) ∈ ℝ)
98adantl 482 . . . . . . . . . . . 12 ((𝑋𝑃𝑌𝑃) → (𝑌‘2) ∈ ℝ)
107, 9resubcld 11583 . . . . . . . . . . 11 ((𝑋𝑃𝑌𝑃) → ((𝑋‘2) − (𝑌‘2)) ∈ ℝ)
113, 10eqeltrid 2842 . . . . . . . . . 10 ((𝑋𝑃𝑌𝑃) → 𝐴 ∈ ℝ)
12113adant3 1132 . . . . . . . . 9 ((𝑋𝑃𝑌𝑃𝑋𝑌) → 𝐴 ∈ ℝ)
1312adantr 481 . . . . . . . 8 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝐴 ∈ ℝ)
14 inlinecirc02plem.b . . . . . . . . . . 11 𝐵 = ((𝑌‘1) − (𝑋‘1))
154, 5rrx2pxel 46787 . . . . . . . . . . . . 13 (𝑌𝑃 → (𝑌‘1) ∈ ℝ)
1615adantl 482 . . . . . . . . . . . 12 ((𝑋𝑃𝑌𝑃) → (𝑌‘1) ∈ ℝ)
174, 5rrx2pxel 46787 . . . . . . . . . . . . 13 (𝑋𝑃 → (𝑋‘1) ∈ ℝ)
1817adantr 481 . . . . . . . . . . . 12 ((𝑋𝑃𝑌𝑃) → (𝑋‘1) ∈ ℝ)
1916, 18resubcld 11583 . . . . . . . . . . 11 ((𝑋𝑃𝑌𝑃) → ((𝑌‘1) − (𝑋‘1)) ∈ ℝ)
2014, 19eqeltrid 2842 . . . . . . . . . 10 ((𝑋𝑃𝑌𝑃) → 𝐵 ∈ ℝ)
21203adant3 1132 . . . . . . . . 9 ((𝑋𝑃𝑌𝑃𝑋𝑌) → 𝐵 ∈ ℝ)
2221adantr 481 . . . . . . . 8 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝐵 ∈ ℝ)
23 inlinecirc02plem.c . . . . . . . . . . 11 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))
247, 16remulcld 11185 . . . . . . . . . . . 12 ((𝑋𝑃𝑌𝑃) → ((𝑋‘2) · (𝑌‘1)) ∈ ℝ)
2518, 9remulcld 11185 . . . . . . . . . . . 12 ((𝑋𝑃𝑌𝑃) → ((𝑋‘1) · (𝑌‘2)) ∈ ℝ)
2624, 25resubcld 11583 . . . . . . . . . . 11 ((𝑋𝑃𝑌𝑃) → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ∈ ℝ)
2723, 26eqeltrid 2842 . . . . . . . . . 10 ((𝑋𝑃𝑌𝑃) → 𝐶 ∈ ℝ)
28273adant3 1132 . . . . . . . . 9 ((𝑋𝑃𝑌𝑃𝑋𝑌) → 𝐶 ∈ ℝ)
2928adantr 481 . . . . . . . 8 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝐶 ∈ ℝ)
3011, 20, 273jca 1128 . . . . . . . . . . . 12 ((𝑋𝑃𝑌𝑃) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ))
31303adant3 1132 . . . . . . . . . . 11 ((𝑋𝑃𝑌𝑃𝑋𝑌) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ))
32 rpre 12923 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
3332adantr 481 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+ ∧ 0 < 𝐷) → 𝑅 ∈ ℝ)
34 inlinecirc02plem.q . . . . . . . . . . . 12 𝑄 = ((𝐴↑2) + (𝐵↑2))
35 inlinecirc02plem.d . . . . . . . . . . . 12 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
3634, 35itsclc0lem3 46834 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → 𝐷 ∈ ℝ)
3731, 33, 36syl2an 596 . . . . . . . . . 10 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝐷 ∈ ℝ)
3837, 1elrpd 12954 . . . . . . . . 9 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝐷 ∈ ℝ+)
3938rprege0d 12964 . . . . . . . 8 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))
4034resum2sqcl 46782 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
4111, 20, 40syl2anc 584 . . . . . . . . . . 11 ((𝑋𝑃𝑌𝑃) → 𝑄 ∈ ℝ)
42413adant3 1132 . . . . . . . . . 10 ((𝑋𝑃𝑌𝑃𝑋𝑌) → 𝑄 ∈ ℝ)
434, 5, 14, 3rrx2pnedifcoorneorr 46793 . . . . . . . . . . . . 13 ((𝑋𝑃𝑌𝑃𝑋𝑌) → (𝐵 ≠ 0 ∨ 𝐴 ≠ 0))
4443orcomd 869 . . . . . . . . . . . 12 ((𝑋𝑃𝑌𝑃𝑋𝑌) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0))
4534resum2sqorgt0 46785 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < 𝑄)
4612, 21, 44, 45syl3anc 1371 . . . . . . . . . . 11 ((𝑋𝑃𝑌𝑃𝑋𝑌) → 0 < 𝑄)
4746gt0ne0d 11719 . . . . . . . . . 10 ((𝑋𝑃𝑌𝑃𝑋𝑌) → 𝑄 ≠ 0)
4842, 47jca 512 . . . . . . . . 9 ((𝑋𝑃𝑌𝑃𝑋𝑌) → (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0))
4948adantr 481 . . . . . . . 8 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0))
50 itsclc0lem1 46832 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ)
5113, 22, 29, 39, 49, 50syl311anc 1384 . . . . . . 7 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ)
52 itsclc0lem2 46833 . . . . . . . 8 (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)
5322, 13, 29, 39, 49, 52syl311anc 1384 . . . . . . 7 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)
5451, 53jca 512 . . . . . 6 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ))
5554adantr 481 . . . . 5 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ))
564, 5prelrrx2 46789 . . . . 5 (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) → {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ∈ 𝑃)
5755, 56syl 17 . . . 4 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ∈ 𝑃)
58 itsclc0lem2 46833 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ)
5913, 22, 29, 39, 49, 58syl311anc 1384 . . . . . . 7 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ)
60 itsclc0lem1 46832 . . . . . . . 8 (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)
6122, 13, 29, 39, 49, 60syl311anc 1384 . . . . . . 7 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)
6259, 61jca 512 . . . . . 6 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ))
6362adantr 481 . . . . 5 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ))
644, 5prelrrx2 46789 . . . . 5 (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) → {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩} ∈ 𝑃)
6563, 64syl 17 . . . 4 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩} ∈ 𝑃)
66 simpl 483 . . . . . . . 8 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (𝑋𝑃𝑌𝑃𝑋𝑌))
67 simprl 769 . . . . . . . 8 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝑅 ∈ ℝ+)
68 0red 11158 . . . . . . . . 9 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 0 ∈ ℝ)
6968, 37, 1ltled 11303 . . . . . . . 8 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 0 ≤ 𝐷)
7066, 67, 69jca32 516 . . . . . . 7 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)))
7170adantr 481 . . . . . 6 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)))
72 inlinecirc02p.e . . . . . . 7 𝐸 = (ℝ^‘𝐼)
73 inlinecirc02p.s . . . . . . 7 𝑆 = (Sphere‘𝐸)
74 inlinecirc02p.0 . . . . . . 7 0 = (𝐼 × {0})
75 inlinecirc02p.l . . . . . . 7 𝐿 = (LineM𝐸)
764, 72, 5, 73, 74, 34, 35, 75, 3, 14, 23itsclinecirc0in 46851 . . . . . 6 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}})
7771, 76syl 17 . . . . 5 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}})
78 opex 5421 . . . . . 6 ⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∈ V
79 opex 5421 . . . . . 6 ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ∈ V
80 opex 5421 . . . . . . 7 ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∈ V
81 opex 5421 . . . . . . 7 ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩ ∈ V
8280, 81pm3.2i 471 . . . . . 6 (⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∈ V ∧ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩ ∈ V)
8344adantr 481 . . . . . . . 8 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0))
8483adantr 481 . . . . . . 7 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0))
85 orcom 868 . . . . . . . 8 ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ (𝐵 ≠ 0 ∨ 𝐴 ≠ 0))
8613recnd 11183 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝐴 ∈ ℂ)
8786adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → 𝐴 ∈ ℂ)
8829recnd 11183 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝐶 ∈ ℂ)
8988adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → 𝐶 ∈ ℂ)
9087, 89mulcld 11175 . . . . . . . . . . . . . . . . . . 19 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (𝐴 · 𝐶) ∈ ℂ)
9122recnd 11183 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝐵 ∈ ℂ)
9291adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
9337recnd 11183 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝐷 ∈ ℂ)
9493adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → 𝐷 ∈ ℂ)
9594sqrtcld 15322 . . . . . . . . . . . . . . . . . . . 20 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (√‘𝐷) ∈ ℂ)
9692, 95mulcld 11175 . . . . . . . . . . . . . . . . . . 19 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (𝐵 · (√‘𝐷)) ∈ ℂ)
9790, 96addcld 11174 . . . . . . . . . . . . . . . . . 18 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ)
9890, 96subcld 11512 . . . . . . . . . . . . . . . . . 18 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
9942adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝑄 ∈ ℝ)
10099recnd 11183 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝑄 ∈ ℂ)
10147adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → 𝑄 ≠ 0)
102100, 101jca 512 . . . . . . . . . . . . . . . . . . 19 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0))
103102adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0))
104 div11 11841 . . . . . . . . . . . . . . . . . 18 ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ ∧ ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ ∧ (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ↔ ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))))
10597, 98, 103, 104syl3anc 1371 . . . . . . . . . . . . . . . . 17 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ↔ ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))))
106 addsubeq0 45518 . . . . . . . . . . . . . . . . . . 19 (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ↔ (𝐵 · (√‘𝐷)) = 0))
10790, 96, 106syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ↔ (𝐵 · (√‘𝐷)) = 0))
10837, 69resqrtcld 15302 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (√‘𝐷) ∈ ℝ)
109108recnd 11183 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (√‘𝐷) ∈ ℂ)
11091, 109mul0ord 11805 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((𝐵 · (√‘𝐷)) = 0 ↔ (𝐵 = 0 ∨ (√‘𝐷) = 0)))
111110adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((𝐵 · (√‘𝐷)) = 0 ↔ (𝐵 = 0 ∨ (√‘𝐷) = 0)))
112 eqneqall 2954 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 = 0 → (𝐵 ≠ 0 → 𝐷 = 0))
113112com12 32 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ≠ 0 → (𝐵 = 0 → 𝐷 = 0))
114113adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (𝐵 = 0 → 𝐷 = 0))
115 sqrt00 15148 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) → ((√‘𝐷) = 0 ↔ 𝐷 = 0))
11637, 69, 115syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((√‘𝐷) = 0 ↔ 𝐷 = 0))
117116biimpd 228 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((√‘𝐷) = 0 → 𝐷 = 0))
118117adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((√‘𝐷) = 0 → 𝐷 = 0))
119114, 118jaod 857 . . . . . . . . . . . . . . . . . . 19 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((𝐵 = 0 ∨ (√‘𝐷) = 0) → 𝐷 = 0))
120111, 119sylbid 239 . . . . . . . . . . . . . . . . . 18 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((𝐵 · (√‘𝐷)) = 0 → 𝐷 = 0))
121107, 120sylbid 239 . . . . . . . . . . . . . . . . 17 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) → 𝐷 = 0))
122105, 121sylbid 239 . . . . . . . . . . . . . . . 16 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → 𝐷 = 0))
123122necon3d 2964 . . . . . . . . . . . . . . 15 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐵 ≠ 0) → (𝐷 ≠ 0 → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
124123impancom 452 . . . . . . . . . . . . . 14 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → (𝐵 ≠ 0 → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
125124imp 407 . . . . . . . . . . . . 13 (((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐵 ≠ 0) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
126125olcd 872 . . . . . . . . . . . 12 (((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐵 ≠ 0) → (1 ≠ 1 ∨ (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
127 1ex 11151 . . . . . . . . . . . . 13 1 ∈ V
128 ovex 7390 . . . . . . . . . . . . 13 (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ V
129127, 128opthne 5439 . . . . . . . . . . . 12 (⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ↔ (1 ≠ 1 ∨ (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
130126, 129sylibr 233 . . . . . . . . . . 11 (((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐵 ≠ 0) → ⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩)
131 1ne2 12361 . . . . . . . . . . . . 13 1 ≠ 2
132131orci 863 . . . . . . . . . . . 12 (1 ≠ 2 ∨ (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))
133127, 128opthne 5439 . . . . . . . . . . . 12 (⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩ ↔ (1 ≠ 2 ∨ (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
134132, 133mpbir 230 . . . . . . . . . . 11 ⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩
135130, 134jctir 521 . . . . . . . . . 10 (((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐵 ≠ 0) → (⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩))
136135ex 413 . . . . . . . . 9 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → (𝐵 ≠ 0 → (⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩)))
13720, 27remulcld 11185 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝑃𝑌𝑃) → (𝐵 · 𝐶) ∈ ℝ)
1381373adant3 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝑃𝑌𝑃𝑋𝑌) → (𝐵 · 𝐶) ∈ ℝ)
139138adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (𝐵 · 𝐶) ∈ ℝ)
14013, 108remulcld 11185 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℝ)
141139, 140resubcld 11583 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℝ)
142141recnd 11183 . . . . . . . . . . . . . . . . . . 19 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
143142adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
14422, 29remulcld 11185 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (𝐵 · 𝐶) ∈ ℝ)
145144, 140readdcld 11184 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℝ)
146145adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℝ)
147146recnd 11183 . . . . . . . . . . . . . . . . . 18 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
148102adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0))
149 div11 11841 . . . . . . . . . . . . . . . . . 18 ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ ∧ ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ ∧ (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ↔ ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))))
150143, 147, 148, 149syl3anc 1371 . . . . . . . . . . . . . . . . 17 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ↔ ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))))
151139recnd 11183 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (𝐵 · 𝐶) ∈ ℂ)
152140recnd 11183 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
153151, 152jca 512 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ))
154153adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ))
155 eqcom 2743 . . . . . . . . . . . . . . . . . . . 20 (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ↔ ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))
156 addsubeq0 45518 . . . . . . . . . . . . . . . . . . . 20 (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ↔ (𝐴 · (√‘𝐷)) = 0))
157155, 156bitrid 282 . . . . . . . . . . . . . . . . . . 19 (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ↔ (𝐴 · (√‘𝐷)) = 0))
158154, 157syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ↔ (𝐴 · (√‘𝐷)) = 0))
15986, 109mul0ord 11805 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ((𝐴 · (√‘𝐷)) = 0 ↔ (𝐴 = 0 ∨ (√‘𝐷) = 0)))
160159adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐴 · (√‘𝐷)) = 0 ↔ (𝐴 = 0 ∨ (√‘𝐷) = 0)))
161 eqneqall 2954 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 = 0 → (𝐴 ≠ 0 → 𝐷 = 0))
162161com12 32 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ≠ 0 → (𝐴 = 0 → 𝐷 = 0))
163162adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → (𝐴 = 0 → 𝐷 = 0))
164117adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((√‘𝐷) = 0 → 𝐷 = 0))
165163, 164jaod 857 . . . . . . . . . . . . . . . . . . 19 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐴 = 0 ∨ (√‘𝐷) = 0) → 𝐷 = 0))
166160, 165sylbid 239 . . . . . . . . . . . . . . . . . 18 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((𝐴 · (√‘𝐷)) = 0 → 𝐷 = 0))
167158, 166sylbid 239 . . . . . . . . . . . . . . . . 17 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) → 𝐷 = 0))
168150, 167sylbid 239 . . . . . . . . . . . . . . . 16 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝐷 = 0))
169168necon3d 2964 . . . . . . . . . . . . . . 15 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐴 ≠ 0) → (𝐷 ≠ 0 → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
170169impancom 452 . . . . . . . . . . . . . 14 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → (𝐴 ≠ 0 → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
171170imp 407 . . . . . . . . . . . . 13 (((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐴 ≠ 0) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))
172171olcd 872 . . . . . . . . . . . 12 (((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐴 ≠ 0) → (2 ≠ 2 ∨ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
173 2ex 12230 . . . . . . . . . . . . 13 2 ∈ V
174 ovex 7390 . . . . . . . . . . . . 13 (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ V
175173, 174opthne 5439 . . . . . . . . . . . 12 (⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩ ↔ (2 ≠ 2 ∨ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
176172, 175sylibr 233 . . . . . . . . . . 11 (((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐴 ≠ 0) → ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩)
177131necomi 2998 . . . . . . . . . . . . 13 2 ≠ 1
178177orci 863 . . . . . . . . . . . 12 (2 ≠ 1 ∨ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
179173, 174opthne 5439 . . . . . . . . . . . 12 (⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ↔ (2 ≠ 1 ∨ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
180178, 179mpbir 230 . . . . . . . . . . 11 ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩
181176, 180jctil 520 . . . . . . . . . 10 (((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐴 ≠ 0) → (⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩))
182181ex 413 . . . . . . . . 9 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → (𝐴 ≠ 0 → (⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩)))
183136, 182orim12d 963 . . . . . . . 8 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((𝐵 ≠ 0 ∨ 𝐴 ≠ 0) → ((⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩) ∨ (⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩))))
18485, 183biimtrid 241 . . . . . . 7 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → ((⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩) ∨ (⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩))))
18584, 184mpd 15 . . . . . 6 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩) ∨ (⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩)))
186 prneimg 4812 . . . . . . 7 (((⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∈ V ∧ ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ∈ V) ∧ (⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∈ V ∧ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩ ∈ V)) → (((⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩) ∨ (⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩)) → {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}))
187186imp 407 . . . . . 6 ((((⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∈ V ∧ ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ∈ V) ∧ (⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∈ V ∧ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩ ∈ V)) ∧ ((⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩) ∨ (⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩ ∧ ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩ ≠ ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩))) → {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩})
18878, 79, 82, 185, 187mpsyl4anc 840 . . . . 5 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩})
18977, 188jca 512 . . . 4 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}} ∧ {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}))
19057, 65, 1893jca 1128 . . 3 ((((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) ∧ 𝐷 ≠ 0) → ({⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ∈ 𝑃 ∧ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩} ∈ 𝑃 ∧ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}} ∧ {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩})))
1912, 190mpdan 685 . 2 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ({⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ∈ 𝑃 ∧ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩} ∈ 𝑃 ∧ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}} ∧ {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩})))
192 preq1 4694 . . . . 5 (𝑎 = {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} → {𝑎, 𝑏} = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, 𝑏})
193192eqeq2d 2747 . . . 4 (𝑎 = {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} → ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ↔ (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, 𝑏}))
194 neeq1 3006 . . . 4 (𝑎 = {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} → (𝑎𝑏 ↔ {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ 𝑏))
195193, 194anbi12d 631 . . 3 (𝑎 = {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} → (((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎𝑏) ↔ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, 𝑏} ∧ {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ 𝑏)))
196 preq2 4695 . . . . 5 (𝑏 = {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩} → {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, 𝑏} = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}})
197196eqeq2d 2747 . . . 4 (𝑏 = {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩} → ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, 𝑏} ↔ (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}}))
198 neeq2 3007 . . . 4 (𝑏 = {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩} → ({⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ 𝑏 ↔ {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}))
199197, 198anbi12d 631 . . 3 (𝑏 = {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩} → (((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, 𝑏} ∧ {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ 𝑏) ↔ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}} ∧ {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩})))
200195, 199rspc2ev 3592 . 2 (({⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ∈ 𝑃 ∧ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩} ∈ 𝑃 ∧ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩}, {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩}} ∧ {⟨1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)⟩} ≠ {⟨1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)⟩, ⟨2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)⟩})) → ∃𝑎𝑃𝑏𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎𝑏))
201191, 200syl 17 1 (((𝑋𝑃𝑌𝑃𝑋𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ∃𝑎𝑃𝑏𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎𝑏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wrex 3073  Vcvv 3445  cin 3909  {csn 4586  {cpr 4588  cop 4592   class class class wbr 5105   × cxp 5631  cfv 6496  (class class class)co 7357  m cmap 8765  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  2c2 12208  +crp 12915  cexp 13967  csqrt 15118  ℝ^crrx 24747  LineMcline 46803  Spherecsph 46804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-tpos 8157  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-0g 17323  df-gsum 17324  df-prds 17329  df-pws 17331  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-grp 18751  df-minusg 18752  df-sbg 18753  df-subg 18925  df-ghm 19006  df-cntz 19097  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-ring 19966  df-cring 19967  df-oppr 20049  df-dvdsr 20070  df-unit 20071  df-invr 20101  df-dvr 20112  df-rnghom 20146  df-drng 20187  df-field 20188  df-subrg 20220  df-staf 20304  df-srng 20305  df-lmod 20324  df-lss 20393  df-sra 20633  df-rgmod 20634  df-xmet 20789  df-met 20790  df-cnfld 20797  df-refld 21009  df-dsmm 21138  df-frlm 21153  df-nm 23938  df-tng 23940  df-tcph 24533  df-rrx 24749  df-ehl 24750  df-line 46805  df-sph 46806
This theorem is referenced by:  inlinecirc02p  46863
  Copyright terms: Public domain W3C validator