Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pell1234qrmulcl Unicode version

Theorem pell1234qrmulcl 26940
Description: General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.)
Assertion
Ref Expression
pell1234qrmulcl  |-  ( ( D  e.  ( NN 
\NN )  /\  A  e.  (Pell1234QR `  D )  /\  B  e.  (Pell1234QR `  D ) )  ->  ( A  x.  B )  e.  (Pell1234QR `  D ) )

Proof of Theorem pell1234qrmulcl
Dummy variables  a 
b  c  d  e  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 731 . . . . . . . . . . . 12  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  ( A  e.  RR  /\  B  e.  RR ) )
21ad3antrrr 710 . . . . . . . . . . 11  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( A  e.  RR  /\  B  e.  RR ) )
3 remulcl 8822 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
42, 3syl 15 . . . . . . . . . 10  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( A  x.  B
)  e.  RR )
5 simprl 732 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  a  e.  ZZ )
65ad3antrrr 710 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
a  e.  ZZ )
7 simplrl 736 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
c  e.  ZZ )
86, 7zmulcld 10123 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( a  x.  c
)  e.  ZZ )
9 eldifi 3298 . . . . . . . . . . . . . . . 16  |-  ( D  e.  ( NN  \NN )  ->  D  e.  NN )
109ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  D  e.  NN )
1110nnzd 10116 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  D  e.  ZZ )
1211ad3antrrr 710 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  ->  D  e.  ZZ )
13 simplrr 737 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
d  e.  ZZ )
14 simprr 733 . . . . . . . . . . . . . . 15  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  b  e.  ZZ )
1514ad3antrrr 710 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
b  e.  ZZ )
1613, 15zmulcld 10123 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( d  x.  b
)  e.  ZZ )
1712, 16zmulcld 10123 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( D  x.  (
d  x.  b ) )  e.  ZZ )
188, 17zaddcld 10121 . . . . . . . . . . 11  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  e.  ZZ )
196, 13zmulcld 10123 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( a  x.  d
)  e.  ZZ )
207, 15zmulcld 10123 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( c  x.  b
)  e.  ZZ )
2119, 20zaddcld 10121 . . . . . . . . . . 11  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a  x.  d )  +  ( c  x.  b ) )  e.  ZZ )
22 simprl 732 . . . . . . . . . . . . . 14  |-  ( ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  ->  A  =  ( a  +  ( ( sqr `  D )  x.  b
) ) )
2322ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  ->  A  =  ( a  +  ( ( sqr `  D )  x.  b
) ) )
24 simprl 732 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  ->  B  =  ( c  +  ( ( sqr `  D )  x.  d
) ) )
2523, 24oveq12d 5876 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( A  x.  B
)  =  ( ( a  +  ( ( sqr `  D )  x.  b ) )  x.  ( c  +  ( ( sqr `  D
)  x.  d ) ) ) )
26 zcn 10029 . . . . . . . . . . . . . . 15  |-  ( a  e.  ZZ  ->  a  e.  CC )
2726ad2antrl 708 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  a  e.  CC )
2827ad3antrrr 710 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
a  e.  CC )
2910nncnd 9762 . . . . . . . . . . . . . . . 16  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  D  e.  CC )
3029ad3antrrr 710 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  ->  D  e.  CC )
3130sqrcld 11919 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( sqr `  D
)  e.  CC )
32 zcn 10029 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ZZ  ->  b  e.  CC )
3332ad2antll 709 . . . . . . . . . . . . . . 15  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  b  e.  CC )
3433ad3antrrr 710 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
b  e.  CC )
3531, 34mulcld 8855 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( sqr `  D
)  x.  b )  e.  CC )
36 zcn 10029 . . . . . . . . . . . . . . 15  |-  ( c  e.  ZZ  ->  c  e.  CC )
3736adantr 451 . . . . . . . . . . . . . 14  |-  ( ( c  e.  ZZ  /\  d  e.  ZZ )  ->  c  e.  CC )
3837ad2antlr 707 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
c  e.  CC )
39 zcn 10029 . . . . . . . . . . . . . . . 16  |-  ( d  e.  ZZ  ->  d  e.  CC )
4039adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( c  e.  ZZ  /\  d  e.  ZZ )  ->  d  e.  CC )
4140ad2antlr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
d  e.  CC )
4231, 41mulcld 8855 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( sqr `  D
)  x.  d )  e.  CC )
4328, 35, 38, 42muladdd 9237 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a  +  ( ( sqr `  D
)  x.  b ) )  x.  ( c  +  ( ( sqr `  D )  x.  d
) ) )  =  ( ( ( a  x.  c )  +  ( ( ( sqr `  D )  x.  d
)  x.  ( ( sqr `  D )  x.  b ) ) )  +  ( ( a  x.  ( ( sqr `  D )  x.  d ) )  +  ( c  x.  ( ( sqr `  D
)  x.  b ) ) ) ) )
4431, 41, 31, 34mul4d 9024 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( sqr `  D )  x.  d
)  x.  ( ( sqr `  D )  x.  b ) )  =  ( ( ( sqr `  D )  x.  ( sqr `  D
) )  x.  (
d  x.  b ) ) )
4530msqsqrd 11922 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( sqr `  D
)  x.  ( sqr `  D ) )  =  D )
4645oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( sqr `  D )  x.  ( sqr `  D ) )  x.  ( d  x.  b ) )  =  ( D  x.  (
d  x.  b ) ) )
4744, 46eqtrd 2315 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( sqr `  D )  x.  d
)  x.  ( ( sqr `  D )  x.  b ) )  =  ( D  x.  ( d  x.  b
) ) )
4847oveq2d 5874 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a  x.  c )  +  ( ( ( sqr `  D
)  x.  d )  x.  ( ( sqr `  D )  x.  b
) ) )  =  ( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) ) )
4928, 31, 41mul12d 9021 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( a  x.  (
( sqr `  D
)  x.  d ) )  =  ( ( sqr `  D )  x.  ( a  x.  d ) ) )
5038, 31, 34mul12d 9021 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( c  x.  (
( sqr `  D
)  x.  b ) )  =  ( ( sqr `  D )  x.  ( c  x.  b ) ) )
5149, 50oveq12d 5876 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a  x.  ( ( sqr `  D
)  x.  d ) )  +  ( c  x.  ( ( sqr `  D )  x.  b
) ) )  =  ( ( ( sqr `  D )  x.  (
a  x.  d ) )  +  ( ( sqr `  D )  x.  ( c  x.  b ) ) ) )
5228, 41mulcld 8855 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( a  x.  d
)  e.  CC )
5338, 34mulcld 8855 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( c  x.  b
)  e.  CC )
5431, 52, 53adddid 8859 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) )  =  ( ( ( sqr `  D )  x.  ( a  x.  d ) )  +  ( ( sqr `  D
)  x.  ( c  x.  b ) ) ) )
5551, 54eqtr4d 2318 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a  x.  ( ( sqr `  D
)  x.  d ) )  +  ( c  x.  ( ( sqr `  D )  x.  b
) ) )  =  ( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) )
5648, 55oveq12d 5876 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a  x.  c )  +  ( ( ( sqr `  D )  x.  d
)  x.  ( ( sqr `  D )  x.  b ) ) )  +  ( ( a  x.  ( ( sqr `  D )  x.  d ) )  +  ( c  x.  ( ( sqr `  D
)  x.  b ) ) ) )  =  ( ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  +  ( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) ) )
5725, 43, 563eqtrd 2319 . . . . . . . . . . 11  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( A  x.  B
)  =  ( ( ( a  x.  c
)  +  ( D  x.  ( d  x.  b ) ) )  +  ( ( sqr `  D )  x.  (
( a  x.  d
)  +  ( c  x.  b ) ) ) ) )
5852, 53addcld 8854 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a  x.  d )  +  ( c  x.  b ) )  e.  CC )
5931, 58sqmuld 11257 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( sqr `  D )  x.  (
( a  x.  d
)  +  ( c  x.  b ) ) ) ^ 2 )  =  ( ( ( sqr `  D ) ^ 2 )  x.  ( ( ( a  x.  d )  +  ( c  x.  b
) ) ^ 2 ) ) )
6030sqsqrd 11921 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( sqr `  D
) ^ 2 )  =  D )
6160oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( sqr `  D ) ^ 2 )  x.  ( ( ( a  x.  d
)  +  ( c  x.  b ) ) ^ 2 ) )  =  ( D  x.  ( ( ( a  x.  d )  +  ( c  x.  b
) ) ^ 2 ) ) )
6259, 61eqtr2d 2316 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( D  x.  (
( ( a  x.  d )  +  ( c  x.  b ) ) ^ 2 ) )  =  ( ( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) ^ 2 ) )
6362oveq2d 5874 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) ) ^
2 )  -  ( D  x.  ( (
( a  x.  d
)  +  ( c  x.  b ) ) ^ 2 ) ) )  =  ( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) ) ^ 2 )  -  ( ( ( sqr `  D )  x.  ( ( a  x.  d )  +  ( c  x.  b
) ) ) ^
2 ) ) )
6428, 38mulcld 8855 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( a  x.  c
)  e.  CC )
6541, 34mulcld 8855 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( d  x.  b
)  e.  CC )
6630, 65mulcld 8855 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( D  x.  (
d  x.  b ) )  e.  CC )
6764, 66addcld 8854 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  e.  CC )
6831, 58mulcld 8855 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) )  e.  CC )
69 subsq 11210 . . . . . . . . . . . . . 14  |-  ( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  e.  CC  /\  ( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) )  e.  CC )  -> 
( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) ) ^
2 )  -  (
( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) ^ 2 ) )  =  ( ( ( ( a  x.  c
)  +  ( D  x.  ( d  x.  b ) ) )  +  ( ( sqr `  D )  x.  (
( a  x.  d
)  +  ( c  x.  b ) ) ) )  x.  (
( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  -  ( ( sqr `  D )  x.  ( ( a  x.  d )  +  ( c  x.  b
) ) ) ) ) )
7067, 68, 69syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) ) ^
2 )  -  (
( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) ^ 2 ) )  =  ( ( ( ( a  x.  c
)  +  ( D  x.  ( d  x.  b ) ) )  +  ( ( sqr `  D )  x.  (
( a  x.  d
)  +  ( c  x.  b ) ) ) )  x.  (
( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  -  ( ( sqr `  D )  x.  ( ( a  x.  d )  +  ( c  x.  b
) ) ) ) ) )
7143, 56eqtr2d 2316 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  +  ( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) )  =  ( ( a  +  ( ( sqr `  D )  x.  b ) )  x.  ( c  +  ( ( sqr `  D
)  x.  d ) ) ) )
7228, 35, 38, 42mulsubd 9238 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a  -  ( ( sqr `  D
)  x.  b ) )  x.  ( c  -  ( ( sqr `  D )  x.  d
) ) )  =  ( ( ( a  x.  c )  +  ( ( ( sqr `  D )  x.  d
)  x.  ( ( sqr `  D )  x.  b ) ) )  -  ( ( a  x.  ( ( sqr `  D )  x.  d ) )  +  ( c  x.  ( ( sqr `  D
)  x.  b ) ) ) ) )
7348, 55oveq12d 5876 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a  x.  c )  +  ( ( ( sqr `  D )  x.  d
)  x.  ( ( sqr `  D )  x.  b ) ) )  -  ( ( a  x.  ( ( sqr `  D )  x.  d ) )  +  ( c  x.  ( ( sqr `  D
)  x.  b ) ) ) )  =  ( ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  -  (
( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) ) )
7472, 73eqtr2d 2316 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  -  (
( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) )  =  ( ( a  -  ( ( sqr `  D )  x.  b ) )  x.  ( c  -  ( ( sqr `  D
)  x.  d ) ) ) )
7571, 74oveq12d 5876 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) )  +  ( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) )  x.  ( ( ( a  x.  c
)  +  ( D  x.  ( d  x.  b ) ) )  -  ( ( sqr `  D )  x.  (
( a  x.  d
)  +  ( c  x.  b ) ) ) ) )  =  ( ( ( a  +  ( ( sqr `  D )  x.  b
) )  x.  (
c  +  ( ( sqr `  D )  x.  d ) ) )  x.  ( ( a  -  ( ( sqr `  D )  x.  b ) )  x.  ( c  -  ( ( sqr `  D
)  x.  d ) ) ) ) )
7663, 70, 753eqtrd 2319 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) ) ^
2 )  -  ( D  x.  ( (
( a  x.  d
)  +  ( c  x.  b ) ) ^ 2 ) ) )  =  ( ( ( a  +  ( ( sqr `  D
)  x.  b ) )  x.  ( c  +  ( ( sqr `  D )  x.  d
) ) )  x.  ( ( a  -  ( ( sqr `  D
)  x.  b ) )  x.  ( c  -  ( ( sqr `  D )  x.  d
) ) ) ) )
7728, 35addcld 8854 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( a  +  ( ( sqr `  D
)  x.  b ) )  e.  CC )
7838, 42addcld 8854 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( c  +  ( ( sqr `  D
)  x.  d ) )  e.  CC )
7928, 35subcld 9157 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( a  -  (
( sqr `  D
)  x.  b ) )  e.  CC )
8038, 42subcld 9157 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( c  -  (
( sqr `  D
)  x.  d ) )  e.  CC )
8177, 78, 79, 80mul4d 9024 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a  +  ( ( sqr `  D )  x.  b
) )  x.  (
c  +  ( ( sqr `  D )  x.  d ) ) )  x.  ( ( a  -  ( ( sqr `  D )  x.  b ) )  x.  ( c  -  ( ( sqr `  D
)  x.  d ) ) ) )  =  ( ( ( a  +  ( ( sqr `  D )  x.  b
) )  x.  (
a  -  ( ( sqr `  D )  x.  b ) ) )  x.  ( ( c  +  ( ( sqr `  D )  x.  d ) )  x.  ( c  -  ( ( sqr `  D
)  x.  d ) ) ) ) )
82 subsq 11210 . . . . . . . . . . . . . . 15  |-  ( ( a  e.  CC  /\  ( ( sqr `  D
)  x.  b )  e.  CC )  -> 
( ( a ^
2 )  -  (
( ( sqr `  D
)  x.  b ) ^ 2 ) )  =  ( ( a  +  ( ( sqr `  D )  x.  b
) )  x.  (
a  -  ( ( sqr `  D )  x.  b ) ) ) )
8328, 35, 82syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a ^
2 )  -  (
( ( sqr `  D
)  x.  b ) ^ 2 ) )  =  ( ( a  +  ( ( sqr `  D )  x.  b
) )  x.  (
a  -  ( ( sqr `  D )  x.  b ) ) ) )
84 subsq 11210 . . . . . . . . . . . . . . 15  |-  ( ( c  e.  CC  /\  ( ( sqr `  D
)  x.  d )  e.  CC )  -> 
( ( c ^
2 )  -  (
( ( sqr `  D
)  x.  d ) ^ 2 ) )  =  ( ( c  +  ( ( sqr `  D )  x.  d
) )  x.  (
c  -  ( ( sqr `  D )  x.  d ) ) ) )
8538, 42, 84syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( c ^
2 )  -  (
( ( sqr `  D
)  x.  d ) ^ 2 ) )  =  ( ( c  +  ( ( sqr `  D )  x.  d
) )  x.  (
c  -  ( ( sqr `  D )  x.  d ) ) ) )
8683, 85oveq12d 5876 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a ^ 2 )  -  ( ( ( sqr `  D )  x.  b
) ^ 2 ) )  x.  ( ( c ^ 2 )  -  ( ( ( sqr `  D )  x.  d ) ^
2 ) ) )  =  ( ( ( a  +  ( ( sqr `  D )  x.  b ) )  x.  ( a  -  ( ( sqr `  D
)  x.  b ) ) )  x.  (
( c  +  ( ( sqr `  D
)  x.  d ) )  x.  ( c  -  ( ( sqr `  D )  x.  d
) ) ) ) )
8731, 34sqmuld 11257 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( sqr `  D )  x.  b
) ^ 2 )  =  ( ( ( sqr `  D ) ^ 2 )  x.  ( b ^ 2 ) ) )
8887oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a ^
2 )  -  (
( ( sqr `  D
)  x.  b ) ^ 2 ) )  =  ( ( a ^ 2 )  -  ( ( ( sqr `  D ) ^ 2 )  x.  ( b ^ 2 ) ) ) )
8931, 41sqmuld 11257 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( sqr `  D )  x.  d
) ^ 2 )  =  ( ( ( sqr `  D ) ^ 2 )  x.  ( d ^ 2 ) ) )
9089oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( c ^
2 )  -  (
( ( sqr `  D
)  x.  d ) ^ 2 ) )  =  ( ( c ^ 2 )  -  ( ( ( sqr `  D ) ^ 2 )  x.  ( d ^ 2 ) ) ) )
9188, 90oveq12d 5876 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a ^ 2 )  -  ( ( ( sqr `  D )  x.  b
) ^ 2 ) )  x.  ( ( c ^ 2 )  -  ( ( ( sqr `  D )  x.  d ) ^
2 ) ) )  =  ( ( ( a ^ 2 )  -  ( ( ( sqr `  D ) ^ 2 )  x.  ( b ^ 2 ) ) )  x.  ( ( c ^
2 )  -  (
( ( sqr `  D
) ^ 2 )  x.  ( d ^
2 ) ) ) ) )
9281, 86, 913eqtr2d 2321 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a  +  ( ( sqr `  D )  x.  b
) )  x.  (
c  +  ( ( sqr `  D )  x.  d ) ) )  x.  ( ( a  -  ( ( sqr `  D )  x.  b ) )  x.  ( c  -  ( ( sqr `  D
)  x.  d ) ) ) )  =  ( ( ( a ^ 2 )  -  ( ( ( sqr `  D ) ^ 2 )  x.  ( b ^ 2 ) ) )  x.  ( ( c ^ 2 )  -  ( ( ( sqr `  D ) ^ 2 )  x.  ( d ^ 2 ) ) ) ) )
9360oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( sqr `  D ) ^ 2 )  x.  ( b ^ 2 ) )  =  ( D  x.  ( b ^ 2 ) ) )
9493oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a ^
2 )  -  (
( ( sqr `  D
) ^ 2 )  x.  ( b ^
2 ) ) )  =  ( ( a ^ 2 )  -  ( D  x.  (
b ^ 2 ) ) ) )
9560oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( sqr `  D ) ^ 2 )  x.  ( d ^ 2 ) )  =  ( D  x.  ( d ^ 2 ) ) )
9695oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( c ^
2 )  -  (
( ( sqr `  D
) ^ 2 )  x.  ( d ^
2 ) ) )  =  ( ( c ^ 2 )  -  ( D  x.  (
d ^ 2 ) ) ) )
9794, 96oveq12d 5876 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a ^ 2 )  -  ( ( ( sqr `  D ) ^ 2 )  x.  ( b ^ 2 ) ) )  x.  ( ( c ^ 2 )  -  ( ( ( sqr `  D ) ^ 2 )  x.  ( d ^ 2 ) ) ) )  =  ( ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  x.  ( ( c ^
2 )  -  ( D  x.  ( d ^ 2 ) ) ) ) )
98 simprr 733 . . . . . . . . . . . . . . 15  |-  ( ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  -> 
( ( a ^
2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 )
9998ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( a ^
2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 )
100 simprr 733 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( c ^
2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 )
10199, 100oveq12d 5876 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a ^ 2 )  -  ( D  x.  (
b ^ 2 ) ) )  x.  (
( c ^ 2 )  -  ( D  x.  ( d ^
2 ) ) ) )  =  ( 1  x.  1 ) )
102 1t1e1 9870 . . . . . . . . . . . . . 14  |-  ( 1  x.  1 )  =  1
103102a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( 1  x.  1 )  =  1 )
10497, 101, 1033eqtrd 2319 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( a ^ 2 )  -  ( ( ( sqr `  D ) ^ 2 )  x.  ( b ^ 2 ) ) )  x.  ( ( c ^ 2 )  -  ( ( ( sqr `  D ) ^ 2 )  x.  ( d ^ 2 ) ) ) )  =  1 )
10576, 92, 1043eqtrd 2319 . . . . . . . . . . 11  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) ) ^
2 )  -  ( D  x.  ( (
( a  x.  d
)  +  ( c  x.  b ) ) ^ 2 ) ) )  =  1 )
106 oveq1 5865 . . . . . . . . . . . . . 14  |-  ( e  =  ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  ->  (
e  +  ( ( sqr `  D )  x.  f ) )  =  ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) )  +  ( ( sqr `  D
)  x.  f ) ) )
107106eqeq2d 2294 . . . . . . . . . . . . 13  |-  ( e  =  ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  ->  (
( A  x.  B
)  =  ( e  +  ( ( sqr `  D )  x.  f
) )  <->  ( A  x.  B )  =  ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  +  ( ( sqr `  D )  x.  f ) ) ) )
108 oveq1 5865 . . . . . . . . . . . . . . 15  |-  ( e  =  ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  ->  (
e ^ 2 )  =  ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) ) ^
2 ) )
109108oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( e  =  ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  ->  (
( e ^ 2 )  -  ( D  x.  ( f ^
2 ) ) )  =  ( ( ( ( a  x.  c
)  +  ( D  x.  ( d  x.  b ) ) ) ^ 2 )  -  ( D  x.  (
f ^ 2 ) ) ) )
110109eqeq1d 2291 . . . . . . . . . . . . 13  |-  ( e  =  ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  ->  (
( ( e ^
2 )  -  ( D  x.  ( f ^ 2 ) ) )  =  1  <->  (
( ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) ) ^ 2 )  -  ( D  x.  ( f ^
2 ) ) )  =  1 ) )
111107, 110anbi12d 691 . . . . . . . . . . . 12  |-  ( e  =  ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  ->  (
( ( A  x.  B )  =  ( e  +  ( ( sqr `  D )  x.  f ) )  /\  ( ( e ^ 2 )  -  ( D  x.  (
f ^ 2 ) ) )  =  1 )  <->  ( ( A  x.  B )  =  ( ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  +  ( ( sqr `  D
)  x.  f ) )  /\  ( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) ) ^ 2 )  -  ( D  x.  ( f ^ 2 ) ) )  =  1 ) ) )
112 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  (
( sqr `  D
)  x.  f )  =  ( ( sqr `  D )  x.  (
( a  x.  d
)  +  ( c  x.  b ) ) ) )
113112oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  (
( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  +  ( ( sqr `  D )  x.  f ) )  =  ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) )  +  ( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) ) )
114113eqeq2d 2294 . . . . . . . . . . . . 13  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  (
( A  x.  B
)  =  ( ( ( a  x.  c
)  +  ( D  x.  ( d  x.  b ) ) )  +  ( ( sqr `  D )  x.  f
) )  <->  ( A  x.  B )  =  ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  +  ( ( sqr `  D )  x.  ( ( a  x.  d )  +  ( c  x.  b
) ) ) ) ) )
115 oveq1 5865 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  (
f ^ 2 )  =  ( ( ( a  x.  d )  +  ( c  x.  b ) ) ^
2 ) )
116115oveq2d 5874 . . . . . . . . . . . . . . 15  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  ( D  x.  ( f ^ 2 ) )  =  ( D  x.  ( ( ( a  x.  d )  +  ( c  x.  b
) ) ^ 2 ) ) )
117116oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  (
( ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) ) ^ 2 )  -  ( D  x.  ( f ^
2 ) ) )  =  ( ( ( ( a  x.  c
)  +  ( D  x.  ( d  x.  b ) ) ) ^ 2 )  -  ( D  x.  (
( ( a  x.  d )  +  ( c  x.  b ) ) ^ 2 ) ) ) )
118117eqeq1d 2291 . . . . . . . . . . . . 13  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  (
( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) ) ^
2 )  -  ( D  x.  ( f ^ 2 ) ) )  =  1  <->  (
( ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) ) ^ 2 )  -  ( D  x.  ( ( ( a  x.  d )  +  ( c  x.  b ) ) ^
2 ) ) )  =  1 ) )
119114, 118anbi12d 691 . . . . . . . . . . . 12  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  (
( ( A  x.  B )  =  ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  +  ( ( sqr `  D )  x.  f ) )  /\  ( ( ( ( a  x.  c
)  +  ( D  x.  ( d  x.  b ) ) ) ^ 2 )  -  ( D  x.  (
f ^ 2 ) ) )  =  1 )  <->  ( ( A  x.  B )  =  ( ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  +  ( ( sqr `  D
)  x.  ( ( a  x.  d )  +  ( c  x.  b ) ) ) )  /\  ( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) ) ^ 2 )  -  ( D  x.  ( ( ( a  x.  d )  +  ( c  x.  b
) ) ^ 2 ) ) )  =  1 ) ) )
120111, 119rspc2ev 2892 . . . . . . . . . . 11  |-  ( ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  e.  ZZ  /\  ( ( a  x.  d )  +  ( c  x.  b ) )  e.  ZZ  /\  ( ( A  x.  B )  =  ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b ) ) )  +  ( ( sqr `  D )  x.  ( ( a  x.  d )  +  ( c  x.  b
) ) ) )  /\  ( ( ( ( a  x.  c
)  +  ( D  x.  ( d  x.  b ) ) ) ^ 2 )  -  ( D  x.  (
( ( a  x.  d )  +  ( c  x.  b ) ) ^ 2 ) ) )  =  1 ) )  ->  E. e  e.  ZZ  E. f  e.  ZZ  ( ( A  x.  B )  =  ( e  +  ( ( sqr `  D
)  x.  f ) )  /\  ( ( e ^ 2 )  -  ( D  x.  ( f ^ 2 ) ) )  =  1 ) )
12118, 21, 57, 105, 120syl112anc 1186 . . . . . . . . . 10  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  ->  E. e  e.  ZZ  E. f  e.  ZZ  (
( A  x.  B
)  =  ( e  +  ( ( sqr `  D )  x.  f
) )  /\  (
( e ^ 2 )  -  ( D  x.  ( f ^
2 ) ) )  =  1 ) )
1224, 121jca 518 . . . . . . . . 9  |-  ( ( ( ( ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  /\  ( c  e.  ZZ  /\  d  e.  ZZ ) )  /\  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( A  x.  B )  e.  RR  /\ 
E. e  e.  ZZ  E. f  e.  ZZ  (
( A  x.  B
)  =  ( e  +  ( ( sqr `  D )  x.  f
) )  /\  (
( e ^ 2 )  -  ( D  x.  ( f ^
2 ) ) )  =  1 ) ) )
123122ex 423 . . . . . . . 8  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  (
a  +  ( ( sqr `  D )  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  (
b ^ 2 ) ) )  =  1 ) )  /\  (
c  e.  ZZ  /\  d  e.  ZZ )
)  ->  ( ( B  =  ( c  +  ( ( sqr `  D )  x.  d
) )  /\  (
( c ^ 2 )  -  ( D  x.  ( d ^
2 ) ) )  =  1 )  -> 
( ( A  x.  B )  e.  RR  /\ 
E. e  e.  ZZ  E. f  e.  ZZ  (
( A  x.  B
)  =  ( e  +  ( ( sqr `  D )  x.  f
) )  /\  (
( e ^ 2 )  -  ( D  x.  ( f ^
2 ) ) )  =  1 ) ) ) )
124123rexlimdvva 2674 . . . . . . 7  |-  ( ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  /\  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) )  -> 
( E. c  e.  ZZ  E. d  e.  ZZ  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 )  ->  (
( A  x.  B
)  e.  RR  /\  E. e  e.  ZZ  E. f  e.  ZZ  (
( A  x.  B
)  =  ( e  +  ( ( sqr `  D )  x.  f
) )  /\  (
( e ^ 2 )  -  ( D  x.  ( f ^
2 ) ) )  =  1 ) ) ) )
125124ex 423 . . . . . 6  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  ( ( A  =  ( a  +  ( ( sqr `  D )  x.  b
) )  /\  (
( a ^ 2 )  -  ( D  x.  ( b ^
2 ) ) )  =  1 )  -> 
( E. c  e.  ZZ  E. d  e.  ZZ  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 )  ->  (
( A  x.  B
)  e.  RR  /\  E. e  e.  ZZ  E. f  e.  ZZ  (
( A  x.  B
)  =  ( e  +  ( ( sqr `  D )  x.  f
) )  /\  (
( e ^ 2 )  -  ( D  x.  ( f ^
2 ) ) )  =  1 ) ) ) ) )
126125rexlimdvva 2674 . . . . 5  |-  ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  -> 
( E. a  e.  ZZ  E. b  e.  ZZ  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 )  ->  ( E. c  e.  ZZ  E. d  e.  ZZ  ( B  =  ( c  +  ( ( sqr `  D )  x.  d
) )  /\  (
( c ^ 2 )  -  ( D  x.  ( d ^
2 ) ) )  =  1 )  -> 
( ( A  x.  B )  e.  RR  /\ 
E. e  e.  ZZ  E. f  e.  ZZ  (
( A  x.  B
)  =  ( e  +  ( ( sqr `  D )  x.  f
) )  /\  (
( e ^ 2 )  -  ( D  x.  ( f ^
2 ) ) )  =  1 ) ) ) ) )
127126imp3a 420 . . . 4  |-  ( ( D  e.  ( NN 
\NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  -> 
( ( E. a  e.  ZZ  E. b  e.  ZZ  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 )  /\  E. c  e.  ZZ  E. d  e.  ZZ  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) )  -> 
( ( A  x.  B )  e.  RR  /\ 
E. e  e.  ZZ  E. f  e.  ZZ  (
( A  x.  B
)  =  ( e  +  ( ( sqr `  D )  x.  f
) )  /\  (
( e ^ 2 )  -  ( D  x.  ( f ^
2 ) ) )  =  1 ) ) ) )
128127expimpd 586 . . 3  |-  ( D  e.  ( NN  \NN )  -> 
( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( E. a  e.  ZZ  E. b  e.  ZZ  ( A  =  ( a  +  ( ( sqr `  D )  x.  b
) )  /\  (
( a ^ 2 )  -  ( D  x.  ( b ^
2 ) ) )  =  1 )  /\  E. c  e.  ZZ  E. d  e.  ZZ  ( B  =  ( c  +  ( ( sqr `  D )  x.  d
) )  /\  (
( c ^ 2 )  -  ( D  x.  ( d ^
2 ) ) )  =  1 ) ) )  ->  ( ( A  x.  B )  e.  RR  /\  E. e  e.  ZZ  E. f  e.  ZZ  ( ( A  x.  B )  =  ( e  +  ( ( sqr `  D
)  x.  f ) )  /\  ( ( e ^ 2 )  -  ( D  x.  ( f ^ 2 ) ) )  =  1 ) ) ) )
129 elpell1234qr 26936 . . . . 5  |-  ( D  e.  ( NN  \NN )  -> 
( A  e.  (Pell1234QR `  D )  <->  ( A  e.  RR  /\  E. a  e.  ZZ  E. b  e.  ZZ  ( A  =  ( a  +  ( ( sqr `  D
)  x.  b ) )  /\  ( ( a ^ 2 )  -  ( D  x.  ( b ^ 2 ) ) )  =  1 ) ) ) )
130 elpell1234qr 26936 . . . . 5  |-