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