Proof of Theorem inlinecirc02plem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simprr 772 | . . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 0 < 𝐷) | 
| 2 | 1 | gt0ne0d 11828 | . . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝐷 ≠ 0) | 
| 3 |  | inlinecirc02plem.a | . . . . . . . . . . 11
⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) | 
| 4 |  | inlinecirc02p.i | . . . . . . . . . . . . . 14
⊢ 𝐼 = {1, 2} | 
| 5 |  | inlinecirc02p.p | . . . . . . . . . . . . . 14
⊢ 𝑃 = (ℝ ↑m
𝐼) | 
| 6 | 4, 5 | rrx2pyel 48638 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) | 
| 7 | 6 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋‘2) ∈ ℝ) | 
| 8 | 4, 5 | rrx2pyel 48638 | . . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝑃 → (𝑌‘2) ∈ ℝ) | 
| 9 | 8 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑌‘2) ∈ ℝ) | 
| 10 | 7, 9 | resubcld 11692 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘2) − (𝑌‘2)) ∈ ℝ) | 
| 11 | 3, 10 | eqeltrid 2844 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐴 ∈ ℝ) | 
| 12 | 11 | 3adant3 1132 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐴 ∈ ℝ) | 
| 13 | 12 | adantr 480 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝐴 ∈
ℝ) | 
| 14 |  | inlinecirc02plem.b | . . . . . . . . . . 11
⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) | 
| 15 | 4, 5 | rrx2pxel 48637 | . . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ) | 
| 16 | 15 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑌‘1) ∈ ℝ) | 
| 17 | 4, 5 | rrx2pxel 48637 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ) | 
| 18 | 17 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋‘1) ∈ ℝ) | 
| 19 | 16, 18 | resubcld 11692 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑌‘1) − (𝑋‘1)) ∈ ℝ) | 
| 20 | 14, 19 | eqeltrid 2844 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐵 ∈ ℝ) | 
| 21 | 20 | 3adant3 1132 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐵 ∈ ℝ) | 
| 22 | 21 | adantr 480 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝐵 ∈
ℝ) | 
| 23 |  | inlinecirc02plem.c | . . . . . . . . . . 11
⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) | 
| 24 | 7, 16 | remulcld 11292 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘2) · (𝑌‘1)) ∈ ℝ) | 
| 25 | 18, 9 | remulcld 11292 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘1) · (𝑌‘2)) ∈ ℝ) | 
| 26 | 24, 25 | resubcld 11692 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ∈ ℝ) | 
| 27 | 23, 26 | eqeltrid 2844 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐶 ∈ ℝ) | 
| 28 | 27 | 3adant3 1132 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐶 ∈ ℝ) | 
| 29 | 28 | adantr 480 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝐶 ∈
ℝ) | 
| 30 | 11, 20, 27 | 3jca 1128 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) | 
| 31 | 30 | 3adant3 1132 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) | 
| 32 |  | rpre 13044 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 0 < 𝐷) →
𝑅 ∈
ℝ) | 
| 34 |  | inlinecirc02plem.q | . . . . . . . . . . . 12
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) | 
| 35 |  | inlinecirc02plem.d | . . . . . . . . . . . 12
⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) | 
| 36 | 34, 35 | itsclc0lem3 48684 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → 𝐷 ∈
ℝ) | 
| 37 | 31, 33, 36 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝐷 ∈
ℝ) | 
| 38 | 37, 1 | elrpd 13075 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝐷 ∈
ℝ+) | 
| 39 | 38 | rprege0d 13085 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (𝐷 ∈ ℝ ∧ 0 ≤
𝐷)) | 
| 40 | 34 | resum2sqcl 48632 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈
ℝ) | 
| 41 | 11, 20, 40 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝑄 ∈ ℝ) | 
| 42 | 41 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝑄 ∈ ℝ) | 
| 43 | 4, 5, 14, 3 | rrx2pnedifcoorneorr 48643 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐵 ≠ 0 ∨ 𝐴 ≠ 0)) | 
| 44 | 43 | orcomd 871 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) | 
| 45 | 34 | resum2sqorgt0 48635 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < 𝑄) | 
| 46 | 12, 21, 44, 45 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 0 < 𝑄) | 
| 47 | 46 | gt0ne0d 11828 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝑄 ≠ 0) | 
| 48 | 42, 47 | jca 511 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) | 
| 49 | 48 | adantr 480 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) | 
| 50 |  | itsclc0lem1 48682 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 51 | 13, 22, 29, 39, 49, 50 | syl311anc 1385 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 52 |  | itsclc0lem2 48683 | . . . . . . . 8
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 53 | 22, 13, 29, 39, 49, 52 | syl311anc 1385 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 54 | 51, 53 | jca 511 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)) | 
| 55 | 54 | adantr 480 | . . . . 5
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)) | 
| 56 | 4, 5 | prelrrx2 48639 | . . . . 5
⊢
(((((𝐴 ·
𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) → {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ∈ 𝑃) | 
| 57 | 55, 56 | syl 17 | . . . 4
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ∈ 𝑃) | 
| 58 |  | itsclc0lem2 48683 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 59 | 13, 22, 29, 39, 49, 58 | syl311anc 1385 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 60 |  | itsclc0lem1 48682 | . . . . . . . 8
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 61 | 22, 13, 29, 39, 49, 60 | syl311anc 1385 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 62 | 59, 61 | jca 511 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)) | 
| 63 | 62 | adantr 480 | . . . . 5
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)) | 
| 64 | 4, 5 | prelrrx2 48639 | . . . . 5
⊢
(((((𝐴 ·
𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) → {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉} ∈ 𝑃) | 
| 65 | 63, 64 | syl 17 | . . . 4
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉} ∈ 𝑃) | 
| 66 |  | simpl 482 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) | 
| 67 |  | simprl 770 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝑅 ∈
ℝ+) | 
| 68 |  | 0red 11265 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 0 ∈
ℝ) | 
| 69 | 68, 37, 1 | ltled 11410 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 0 ≤ 𝐷) | 
| 70 | 66, 67, 69 | jca32 515 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷))) | 
| 71 | 70 | adantr 480 | . . . . . 6
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷))) | 
| 72 |  | inlinecirc02p.e | . . . . . . 7
⊢ 𝐸 = (ℝ^‘𝐼) | 
| 73 |  | inlinecirc02p.s | . . . . . . 7
⊢ 𝑆 = (Sphere‘𝐸) | 
| 74 |  | inlinecirc02p.0 | . . . . . . 7
⊢  0 = (𝐼 × {0}) | 
| 75 |  | inlinecirc02p.l | . . . . . . 7
⊢ 𝐿 = (LineM‘𝐸) | 
| 76 | 4, 72, 5, 73, 74, 34, 35, 75, 3, 14, 23 | itsclinecirc0in 48701 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}}) | 
| 77 | 71, 76 | syl 17 | . . . . 5
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}}) | 
| 78 |  | opex 5468 | . . . . . 6
⊢ 〈1,
(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ∈ V | 
| 79 |  | opex 5468 | . . . . . 6
⊢ 〈2,
(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ∈ V | 
| 80 |  | opex 5468 | . . . . . . 7
⊢ 〈1,
(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∈ V | 
| 81 |  | opex 5468 | . . . . . . 7
⊢ 〈2,
(((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉 ∈ V | 
| 82 | 80, 81 | pm3.2i 470 | . . . . . 6
⊢ (〈1,
(((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∈ V ∧ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉 ∈ V) | 
| 83 | 44 | adantr 480 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) | 
| 84 | 83 | adantr 480 | . . . . . . 7
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) | 
| 85 |  | orcom 870 | . . . . . . . 8
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ (𝐵 ≠ 0 ∨ 𝐴 ≠ 0)) | 
| 86 | 13 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝐴 ∈
ℂ) | 
| 87 | 86 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → 𝐴 ∈ ℂ) | 
| 88 | 29 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝐶 ∈
ℂ) | 
| 89 | 88 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → 𝐶 ∈ ℂ) | 
| 90 | 87, 89 | mulcld 11282 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → (𝐴 · 𝐶) ∈ ℂ) | 
| 91 | 22 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝐵 ∈
ℂ) | 
| 92 | 91 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ) | 
| 93 | 37 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝐷 ∈
ℂ) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → 𝐷 ∈ ℂ) | 
| 95 | 94 | sqrtcld 15477 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → (√‘𝐷) ∈
ℂ) | 
| 96 | 92, 95 | mulcld 11282 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → (𝐵 · (√‘𝐷)) ∈ ℂ) | 
| 97 | 90, 96 | addcld 11281 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ) | 
| 98 | 90, 96 | subcld 11621 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ) | 
| 99 | 42 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝑄 ∈
ℝ) | 
| 100 | 99 | recnd 11290 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝑄 ∈
ℂ) | 
| 101 | 47 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → 𝑄 ≠ 0) | 
| 102 | 100, 101 | jca 511 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) | 
| 103 | 102 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) | 
| 104 |  | div11 11951 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ ∧ ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ ∧ (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ↔ ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))))) | 
| 105 | 97, 98, 103, 104 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ↔ ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))))) | 
| 106 |  | addsubeq0 47313 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ↔ (𝐵 · (√‘𝐷)) = 0)) | 
| 107 | 90, 96, 106 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ↔ (𝐵 · (√‘𝐷)) = 0)) | 
| 108 | 37, 69 | resqrtcld 15457 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) →
(√‘𝐷) ∈
ℝ) | 
| 109 | 108 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) →
(√‘𝐷) ∈
ℂ) | 
| 110 | 91, 109 | mul0ord 11914 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ((𝐵 · (√‘𝐷)) = 0 ↔ (𝐵 = 0 ∨ (√‘𝐷) = 0))) | 
| 111 | 110 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → ((𝐵 · (√‘𝐷)) = 0 ↔ (𝐵 = 0 ∨ (√‘𝐷) = 0))) | 
| 112 |  | eqneqall 2950 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 = 0 → (𝐵 ≠ 0 → 𝐷 = 0)) | 
| 113 | 112 | com12 32 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ≠ 0 → (𝐵 = 0 → 𝐷 = 0)) | 
| 114 | 113 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → (𝐵 = 0 → 𝐷 = 0)) | 
| 115 |  | sqrt00 15303 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ ℝ ∧ 0 ≤
𝐷) →
((√‘𝐷) = 0
↔ 𝐷 =
0)) | 
| 116 | 37, 69, 115 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) →
((√‘𝐷) = 0
↔ 𝐷 =
0)) | 
| 117 | 116 | biimpd 229 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) →
((√‘𝐷) = 0
→ 𝐷 =
0)) | 
| 118 | 117 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → ((√‘𝐷) = 0 → 𝐷 = 0)) | 
| 119 | 114, 118 | jaod 859 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → ((𝐵 = 0 ∨ (√‘𝐷) = 0) → 𝐷 = 0)) | 
| 120 | 111, 119 | sylbid 240 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → ((𝐵 · (√‘𝐷)) = 0 → 𝐷 = 0)) | 
| 121 | 107, 120 | sylbid 240 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) → 𝐷 = 0)) | 
| 122 | 105, 121 | sylbid 240 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → 𝐷 = 0)) | 
| 123 | 122 | necon3d 2960 | . . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐵 ≠ 0) → (𝐷 ≠ 0 → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))) | 
| 124 | 123 | impancom 451 | . . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → (𝐵 ≠ 0 → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))) | 
| 125 | 124 | imp 406 | . . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐵 ≠ 0) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) | 
| 126 | 125 | olcd 874 | . . . . . . . . . . . 12
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐵 ≠ 0) → (1 ≠ 1 ∨ (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))) | 
| 127 |  | 1ex 11258 | . . . . . . . . . . . . 13
⊢ 1 ∈
V | 
| 128 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ V | 
| 129 | 127, 128 | opthne 5486 | . . . . . . . . . . . 12
⊢ (〈1,
(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ↔ (1 ≠ 1 ∨ (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))) | 
| 130 | 126, 129 | sylibr 234 | . . . . . . . . . . 11
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐵 ≠ 0) → 〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉) | 
| 131 |  | 1ne2 12475 | . . . . . . . . . . . . 13
⊢ 1 ≠
2 | 
| 132 | 131 | orci 865 | . . . . . . . . . . . 12
⊢ (1 ≠ 2
∨ (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) | 
| 133 | 127, 128 | opthne 5486 | . . . . . . . . . . . 12
⊢ (〈1,
(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉 ↔ (1 ≠ 2 ∨ (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) | 
| 134 | 132, 133 | mpbir 231 | . . . . . . . . . . 11
⊢ 〈1,
(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉 | 
| 135 | 130, 134 | jctir 520 | . . . . . . . . . 10
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐵 ≠ 0) → (〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉)) | 
| 136 | 135 | ex 412 | . . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → (𝐵 ≠ 0 → (〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉))) | 
| 137 | 20, 27 | remulcld 11292 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝐵 · 𝐶) ∈ ℝ) | 
| 138 | 137 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐵 · 𝐶) ∈ ℝ) | 
| 139 | 138 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (𝐵 · 𝐶) ∈ ℝ) | 
| 140 | 13, 108 | remulcld 11292 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (𝐴 · (√‘𝐷)) ∈
ℝ) | 
| 141 | 139, 140 | resubcld 11692 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℝ) | 
| 142 | 141 | recnd 11290 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ) | 
| 143 | 142 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ) | 
| 144 | 22, 29 | remulcld 11292 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (𝐵 · 𝐶) ∈ ℝ) | 
| 145 | 144, 140 | readdcld 11291 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℝ) | 
| 146 | 145 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℝ) | 
| 147 | 146 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ) | 
| 148 | 102 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) | 
| 149 |  | div11 11951 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ ∧ ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ ∧ (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ↔ ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) | 
| 150 | 143, 147,
148, 149 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ↔ ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) | 
| 151 | 139 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (𝐵 · 𝐶) ∈ ℂ) | 
| 152 | 140 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → (𝐴 · (√‘𝐷)) ∈
ℂ) | 
| 153 | 151, 152 | jca 511 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ)) | 
| 154 | 153 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → ((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ)) | 
| 155 |  | eqcom 2743 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ↔ ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) | 
| 156 |  | addsubeq0 47313 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ↔ (𝐴 · (√‘𝐷)) = 0)) | 
| 157 | 155, 156 | bitrid 283 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ↔ (𝐴 · (√‘𝐷)) = 0)) | 
| 158 | 154, 157 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ↔ (𝐴 · (√‘𝐷)) = 0)) | 
| 159 | 86, 109 | mul0ord 11914 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ((𝐴 · (√‘𝐷)) = 0 ↔ (𝐴 = 0 ∨ (√‘𝐷) = 0))) | 
| 160 | 159 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → ((𝐴 · (√‘𝐷)) = 0 ↔ (𝐴 = 0 ∨ (√‘𝐷) = 0))) | 
| 161 |  | eqneqall 2950 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 = 0 → (𝐴 ≠ 0 → 𝐷 = 0)) | 
| 162 | 161 | com12 32 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ≠ 0 → (𝐴 = 0 → 𝐷 = 0)) | 
| 163 | 162 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → (𝐴 = 0 → 𝐷 = 0)) | 
| 164 | 117 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → ((√‘𝐷) = 0 → 𝐷 = 0)) | 
| 165 | 163, 164 | jaod 859 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → ((𝐴 = 0 ∨ (√‘𝐷) = 0) → 𝐷 = 0)) | 
| 166 | 160, 165 | sylbid 240 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → ((𝐴 · (√‘𝐷)) = 0 → 𝐷 = 0)) | 
| 167 | 158, 166 | sylbid 240 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) → 𝐷 = 0)) | 
| 168 | 150, 167 | sylbid 240 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝐷 = 0)) | 
| 169 | 168 | necon3d 2960 | . . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐴 ≠ 0) → (𝐷 ≠ 0 → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) | 
| 170 | 169 | impancom 451 | . . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → (𝐴 ≠ 0 → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) | 
| 171 | 170 | imp 406 | . . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐴 ≠ 0) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) | 
| 172 | 171 | olcd 874 | . . . . . . . . . . . 12
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐴 ≠ 0) → (2 ≠ 2 ∨ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) | 
| 173 |  | 2ex 12344 | . . . . . . . . . . . . 13
⊢ 2 ∈
V | 
| 174 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ V | 
| 175 | 173, 174 | opthne 5486 | . . . . . . . . . . . 12
⊢ (〈2,
(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉 ↔ (2 ≠ 2 ∨ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) | 
| 176 | 172, 175 | sylibr 234 | . . . . . . . . . . 11
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐴 ≠ 0) → 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉) | 
| 177 | 131 | necomi 2994 | . . . . . . . . . . . . 13
⊢ 2 ≠
1 | 
| 178 | 177 | orci 865 | . . . . . . . . . . . 12
⊢ (2 ≠ 1
∨ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) | 
| 179 | 173, 174 | opthne 5486 | . . . . . . . . . . . 12
⊢ (〈2,
(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ↔ (2 ≠ 1 ∨ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ≠ (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))) | 
| 180 | 178, 179 | mpbir 231 | . . . . . . . . . . 11
⊢ 〈2,
(((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 | 
| 181 | 176, 180 | jctil 519 | . . . . . . . . . 10
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) ∧ 𝐴 ≠ 0) → (〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉)) | 
| 182 | 181 | ex 412 | . . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → (𝐴 ≠ 0 → (〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉))) | 
| 183 | 136, 182 | orim12d 966 | . . . . . . . 8
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → ((𝐵 ≠ 0 ∨ 𝐴 ≠ 0) → ((〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉) ∨ (〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉)))) | 
| 184 | 85, 183 | biimtrid 242 | . . . . . . 7
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → ((〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉) ∨ (〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉)))) | 
| 185 | 84, 184 | mpd 15 | . . . . . 6
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → ((〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉) ∨ (〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉))) | 
| 186 |  | prneimg 4853 | . . . . . . 7
⊢
(((〈1, (((𝐴
· 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ∈ V ∧ 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ∈ V) ∧ (〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∈ V ∧ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉 ∈ V)) → (((〈1,
(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉) ∨ (〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉)) → {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉})) | 
| 187 | 186 | imp 406 | . . . . . 6
⊢
((((〈1, (((𝐴
· 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ∈ V ∧ 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ∈ V) ∧ (〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∈ V ∧ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉 ∈ V)) ∧ ((〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉) ∨ (〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉 ∧ 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉 ≠ 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉))) → {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}) | 
| 188 | 78, 79, 82, 185, 187 | mpsyl4anc 842 | . . . . 5
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}) | 
| 189 | 77, 188 | jca 511 | . . . 4
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}} ∧ {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉})) | 
| 190 | 57, 65, 189 | 3jca 1128 | . . 3
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) ∧ 𝐷 ≠ 0) → ({〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ∈ 𝑃 ∧ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉} ∈ 𝑃 ∧ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}} ∧ {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}))) | 
| 191 | 2, 190 | mpdan 687 | . 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ({〈1,
(((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ∈ 𝑃 ∧ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉} ∈ 𝑃 ∧ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}} ∧ {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}))) | 
| 192 |  | preq1 4732 | . . . . 5
⊢ (𝑎 = {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} → {𝑎, 𝑏} = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, 𝑏}) | 
| 193 | 192 | eqeq2d 2747 | . . . 4
⊢ (𝑎 = {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} → ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ↔ (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, 𝑏})) | 
| 194 |  | neeq1 3002 | . . . 4
⊢ (𝑎 = {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} → (𝑎 ≠ 𝑏 ↔ {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ 𝑏)) | 
| 195 | 193, 194 | anbi12d 632 | . . 3
⊢ (𝑎 = {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} → (((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏) ↔ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, 𝑏} ∧ {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ 𝑏))) | 
| 196 |  | preq2 4733 | . . . . 5
⊢ (𝑏 = {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉} → {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, 𝑏} = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}}) | 
| 197 | 196 | eqeq2d 2747 | . . . 4
⊢ (𝑏 = {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉} → ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, 𝑏} ↔ (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}})) | 
| 198 |  | neeq2 3003 | . . . 4
⊢ (𝑏 = {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉} → ({〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ 𝑏 ↔ {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉})) | 
| 199 | 197, 198 | anbi12d 632 | . . 3
⊢ (𝑏 = {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉} → (((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, 𝑏} ∧ {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ 𝑏) ↔ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}} ∧ {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}))) | 
| 200 | 195, 199 | rspc2ev 3634 | . 2
⊢
(({〈1, (((𝐴
· 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ∈ 𝑃 ∧ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉} ∈ 𝑃 ∧ ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}} ∧ {〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉} ≠ {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉})) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) | 
| 201 | 191, 200 | syl 17 | 1
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 <
𝐷)) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) |