Metamath Proof Explorer

Theorem inlinecirc02plem

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

Ref Expression
Hypotheses inlinecirc02p.i 
|- I = { 1 , 2 }
inlinecirc02p.e 
|- E = ( RR^ ` I )
inlinecirc02p.p 
|- P = ( RR ^m I )
inlinecirc02p.s 
|- S = ( Sphere ` E )
inlinecirc02p.0 
|- .0. = ( I X. { 0 } )
inlinecirc02p.l 
|- L = ( LineM ` E )
inlinecirc02plem.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
inlinecirc02plem.d 
|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
inlinecirc02plem.a 
|- A = ( ( X ` 2 ) - ( Y ` 2 ) )
inlinecirc02plem.b 
|- B = ( ( Y ` 1 ) - ( X ` 1 ) )
inlinecirc02plem.c 
|- C = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
Assertion inlinecirc02plem 
|- ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 < D ) ) -> E. a e. P E. b e. P ( ( ( .0. S R ) i^i ( X L Y ) ) = { a , b } /\ a =/= b ) )

Proof

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