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

Theorem pell1234qrmulcl 26956
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 remulcl 9106 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
21ad5antlr 717 . . . . . . . . . 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 )
3 simprl 734 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  a  e.  ZZ )
43ad3antrrr 712 . . . . . . . . . . . . 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 )
5 simplrl 738 . . . . . . . . . . . . 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 )
64, 5zmulcld 10412 . . . . . . . . . . . 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 )
7 eldifi 3455 . . . . . . . . . . . . . . . 16  |-  ( D  e.  ( NN  \NN )  ->  D  e.  NN )
87ad2antrr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  D  e.  NN )
98nnzd 10405 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  D  e.  ZZ )
109ad3antrrr 712 . . . . . . . . . . . . 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 )
11 simplrr 739 . . . . . . . . . . . . . 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 )
12 simprr 735 . . . . . . . . . . . . . . 15  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  b  e.  ZZ )
1312ad3antrrr 712 . . . . . . . . . . . . . 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 )
1411, 13zmulcld 10412 . . . . . . . . . . . . 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 )
1510, 14zmulcld 10412 . . . . . . . . . . . 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 )
166, 15zaddcld 10410 . . . . . . . . . . 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 )
174, 11zmulcld 10412 . . . . . . . . . . . 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 )
185, 13zmulcld 10412 . . . . . . . . . . . 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 )
1917, 18zaddcld 10410 . . . . . . . . . . 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 )
20 simprl 734 . . . . . . . . . . . . . 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
) ) )
2120ad2antrr 708 . . . . . . . . . . . . 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
) ) )
22 simprl 734 . . . . . . . . . . . . 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
) ) )
2321, 22oveq12d 6128 . . . . . . . . . . . 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 ) ) ) )
24 zcn 10318 . . . . . . . . . . . . . . 15  |-  ( a  e.  ZZ  ->  a  e.  CC )
2524ad2antrl 710 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  a  e.  CC )
2625ad3antrrr 712 . . . . . . . . . . . . 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 )
278nncnd 10047 . . . . . . . . . . . . . . . 16  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  D  e.  CC )
2827ad3antrrr 712 . . . . . . . . . . . . . . 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 )
2928sqrcld 12270 . . . . . . . . . . . . . 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 )
30 zcn 10318 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ZZ  ->  b  e.  CC )
3130ad2antll 711 . . . . . . . . . . . . . . 15  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( A  e.  RR  /\  B  e.  RR ) )  /\  ( a  e.  ZZ  /\  b  e.  ZZ ) )  ->  b  e.  CC )
3231ad3antrrr 712 . . . . . . . . . . . . . 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 )
3329, 32mulcld 9139 . . . . . . . . . . . . 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 )
34 zcn 10318 . . . . . . . . . . . . . . 15  |-  ( c  e.  ZZ  ->  c  e.  CC )
3534adantr 453 . . . . . . . . . . . . . 14  |-  ( ( c  e.  ZZ  /\  d  e.  ZZ )  ->  c  e.  CC )
3635ad2antlr 709 . . . . . . . . . . . . 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 )
37 zcn 10318 . . . . . . . . . . . . . . . 16  |-  ( d  e.  ZZ  ->  d  e.  CC )
3837adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( c  e.  ZZ  /\  d  e.  ZZ )  ->  d  e.  CC )
3938ad2antlr 709 . . . . . . . . . . . . . 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 )
4029, 39mulcld 9139 . . . . . . . . . . . . 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 )
4126, 33, 36, 40muladdd 9522 . . . . . . . . . . . 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 ) ) ) ) )
4229, 39, 29, 32mul4d 9309 . . . . . . . . . . . . . . 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 ) ) )
4328msqsqrd 12273 . . . . . . . . . . . . . . . 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 )
4443oveq1d 6125 . . . . . . . . . . . . . . 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 ) ) )
4542, 44eqtrd 2474 . . . . . . . . . . . . . 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
) ) )
4645oveq2d 6126 . . . . . . . . . . . . 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 ) ) ) )
4726, 29, 39mul12d 9306 . . . . . . . . . . . . . . 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 ) ) )
4836, 29, 32mul12d 9306 . . . . . . . . . . . . . . 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 ) ) )
4947, 48oveq12d 6128 . . . . . . . . . . . . . 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 ) ) ) )
5026, 39mulcld 9139 . . . . . . . . . . . . . . 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 )
5136, 32mulcld 9139 . . . . . . . . . . . . . . 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 )
5229, 50, 51adddid 9143 . . . . . . . . . . . . . 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 ) ) ) )
5349, 52eqtr4d 2477 . . . . . . . . . . . . 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 ) ) ) )
5446, 53oveq12d 6128 . . . . . . . . . . . 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 ) ) ) ) )
5523, 41, 543eqtrd 2478 . . . . . . . . . . 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 ) ) ) ) )
5650, 51addcld 9138 . . . . . . . . . . . . . . . 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 )
5729, 56sqmuld 11566 . . . . . . . . . . . . . . 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 ) ) )
5828sqsqrd 12272 . . . . . . . . . . . . . . . 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 )
5958oveq1d 6125 . . . . . . . . . . . . . . 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 ) ) )
6057, 59eqtr2d 2475 . . . . . . . . . . . . . 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 ) )
6160oveq2d 6126 . . . . . . . . . . . . 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 ) ) )
6226, 36mulcld 9139 . . . . . . . . . . . . . . 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 )
6339, 32mulcld 9139 . . . . . . . . . . . . . . . 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 )
6428, 63mulcld 9139 . . . . . . . . . . . . . . 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 )
6562, 64addcld 9138 . . . . . . . . . . . . . 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 )
6629, 56mulcld 9139 . . . . . . . . . . . . . 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 )
67 subsq 11519 . . . . . . . . . . . . . 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
) ) ) ) ) )
6865, 66, 67syl2anc 644 . . . . . . . . . . . . 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
) ) ) ) ) )
6941, 54eqtr2d 2475 . . . . . . . . . . . . . 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 ) ) ) )
7026, 33, 36, 40mulsubd 9523 . . . . . . . . . . . . . . 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 ) ) ) ) )
7146, 53oveq12d 6128 . . . . . . . . . . . . . . 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 ) ) ) ) )
7270, 71eqtr2d 2475 . . . . . . . . . . . . . 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 ) ) ) )
7369, 72oveq12d 6128 . . . . . . . . . . . . 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 ) ) ) ) )
7461, 68, 733eqtrd 2478 . . . . . . . . . . . 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
) ) ) ) )
7526, 33addcld 9138 . . . . . . . . . . . . . 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 )
7636, 40addcld 9138 . . . . . . . . . . . . . 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 )
7726, 33subcld 9442 . . . . . . . . . . . . . 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 )
7836, 40subcld 9442 . . . . . . . . . . . . . 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 )
7975, 76, 77, 78mul4d 9309 . . . . . . . . . . . . 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 ) ) ) ) )
80 subsq 11519 . . . . . . . . . . . . . . 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 ) ) ) )
8126, 33, 80syl2anc 644 . . . . . . . . . . . . . 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 ) ) ) )
82 subsq 11519 . . . . . . . . . . . . . . 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 ) ) ) )
8336, 40, 82syl2anc 644 . . . . . . . . . . . . . 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 ) ) ) )
8481, 83oveq12d 6128 . . . . . . . . . . . . 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
) ) ) ) )
8529, 32sqmuld 11566 . . . . . . . . . . . . . . 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 ) ) )
8685oveq2d 6126 . . . . . . . . . . . . . 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 ) ) ) )
8729, 39sqmuld 11566 . . . . . . . . . . . . . . 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 ) ) )
8887oveq2d 6126 . . . . . . . . . . . . . 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 ) ) ) )
8986, 88oveq12d 6128 . . . . . . . . . . . . 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 ) ) ) ) )
9079, 84, 893eqtr2d 2480 . . . . . . . . . . . 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 ) ) ) ) )
9158oveq1d 6125 . . . . . . . . . . . . . . 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 ) ) )
9291oveq2d 6126 . . . . . . . . . . . . . 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 ) ) ) )
9358oveq1d 6125 . . . . . . . . . . . . . . 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 ) ) )
9493oveq2d 6126 . . . . . . . . . . . . . 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 ) ) ) )
9592, 94oveq12d 6128 . . . . . . . . . . . . 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 ) ) ) ) )
96 simprr 735 . . . . . . . . . . . . . . 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 )
9796ad2antrr 708 . . . . . . . . . . . . . 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 )
98 simprr 735 . . . . . . . . . . . . . 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 )
9997, 98oveq12d 6128 . . . . . . . . . . . . 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 ) )
100 1t1e1 10157 . . . . . . . . . . . . . 14  |-  ( 1  x.  1 )  =  1
101100a1i 11 . . . . . . . . . . . . 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 )
10295, 99, 1013eqtrd 2478 . . . . . . . . . . . 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 )
10374, 90, 1023eqtrd 2478 . . . . . . . . . . 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 )
104 oveq1 6117 . . . . . . . . . . . . . 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 ) ) )
105104eqeq2d 2453 . . . . . . . . . . . . 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 ) ) ) )
106 oveq1 6117 . . . . . . . . . . . . . . 15  |-  ( e  =  ( ( a  x.  c )  +  ( D  x.  (
d  x.  b ) ) )  ->  (
e ^ 2 )  =  ( ( ( a  x.  c )  +  ( D  x.  ( d  x.  b
) ) ) ^
2 ) )
107106oveq1d 6125 . . . . . . . . . . . . . 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 ) ) ) )
108107eqeq1d 2450 . . . . . . . . . . . . 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 ) )
109105, 108anbi12d 693 . . . . . . . . . . . 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 ) ) )
110 oveq2 6118 . . . . . . . . . . . . . . 15  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  (
( sqr `  D
)  x.  f )  =  ( ( sqr `  D )  x.  (
( a  x.  d
)  +  ( c  x.  b ) ) ) )
111110oveq2d 6126 . . . . . . . . . . . . . 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 ) ) ) ) )
112111eqeq2d 2453 . . . . . . . . . . . . 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
) ) ) ) ) )
113 oveq1 6117 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  (
f ^ 2 )  =  ( ( ( a  x.  d )  +  ( c  x.  b ) ) ^
2 ) )
114113oveq2d 6126 . . . . . . . . . . . . . . 15  |-  ( f  =  ( ( a  x.  d )  +  ( c  x.  b
) )  ->  ( D  x.  ( f ^ 2 ) )  =  ( D  x.  ( ( ( a  x.  d )  +  ( c  x.  b
) ) ^ 2 ) ) )
115114oveq2d 6126 . . . . . . . . . . . . . 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 ) ) ) )
116115eqeq1d 2450 . . . . . . . . . . . . 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 ) )
117112, 116anbi12d 693 . . . . . . . . . . . 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 ) ) )
118109, 117rspc2ev 3066 . . . . . . . . . . 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 ) )
11916, 19, 55, 103, 118syl112anc 1189 . . . . . . . . . 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 ) )
1202, 119jca 520 . . . . . . . . 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 ) ) )
121120ex 425 . . . . . . . 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 ) ) ) )
122121rexlimdvva 2843 . . . . . . 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 ) ) ) )
123122ex 425 . . . . . 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 ) ) ) ) )
124123rexlimdvva 2843 . . . . 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 ) ) ) ) )
125124imp3a 422 . . . 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 ) ) ) )
126125expimpd 588 . . 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 ) ) ) )
127 elpell1234qr 26952 . . . . 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 ) ) ) )
128 elpell1234qr 26952 . . . . 5  |-  ( D  e.  ( NN  \NN )  -> 
( B  e.  (Pell1234QR `  D )  <->  ( B  e.  RR  /\  E. c  e.  ZZ  E. d  e.  ZZ  ( B  =  ( c  +  ( ( sqr `  D
)  x.  d ) )  /\  ( ( c ^ 2 )  -  ( D  x.  ( d ^ 2 ) ) )  =  1 ) ) ) )
129127, 128anbi12d 693 . . . 4  |-  ( D  e.  ( NN  \NN )  -> 
( ( A  e.  (Pell1234QR `  D )  /\  B  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 ) )  /\  ( B  e.  RR  /\ 
E. c  e.  ZZ  E. d  e.  ZZ  ( B  =  ( c  +  ( ( sqr `  D )  x.  d
) )  /\  (
( c ^ 2 )  -  ( D  x.  ( d ^
2 ) ) )  =  1 ) ) ) ) )