Metamath Proof Explorer

Theorem pell1234qrmulcl

Description: General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell1234qrmulcl 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) /\ B e. ( Pell1234QR ` D ) ) -> ( A x. B ) e. ( Pell1234QR ` D ) )

Proof

Step Hyp Ref Expression
1 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
2 1 ad5antlr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( A x. B ) e. RR )
3 simprl 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ )
4 3 ad3antrrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> a e. ZZ )
5 simplrl 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> c e. ZZ )
6 4 5 zmulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( a x. c ) e. ZZ )
7 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
8 7 ad2antrr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> D e. NN )
9 8 nnzd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> D e. ZZ )
10 9 ad3antrrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> D e. ZZ )
11 simplrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> d e. ZZ )
12 simprr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. ZZ )
13 12 ad3antrrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> b e. ZZ )
14 11 13 zmulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( d x. b ) e. ZZ )
15 10 14 zmulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( D x. ( d x. b ) ) e. ZZ )
16 6 15 zaddcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a x. c ) + ( D x. ( d x. b ) ) ) e. ZZ )
17 4 11 zmulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( a x. d ) e. ZZ )
18 5 13 zmulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( c x. b ) e. ZZ )
19 17 18 zaddcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a x. d ) + ( c x. b ) ) e. ZZ )
20 simprl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A = ( a + ( ( sqrt ` D ) x. b ) ) )
21 20 ad2antrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> A = ( a + ( ( sqrt ` D ) x. b ) ) )
22 simprl 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> B = ( c + ( ( sqrt ` D ) x. d ) ) )
23 21 22 oveq12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( A x. B ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( c + ( ( sqrt ` D ) x. d ) ) ) )
24 zcn 
 |-  ( a e. ZZ -> a e. CC )
25 24 ad2antrl 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC )
26 25 ad3antrrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> a e. CC )
27 8 nncnd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> D e. CC )
28 27 ad3antrrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> D e. CC )
29 28 sqrtcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( sqrt ` D ) e. CC )
30 zcn 
 |-  ( b e. ZZ -> b e. CC )
31 30 ad2antll 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
32 31 ad3antrrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> b e. CC )
33 29 32 mulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) x. b ) e. CC )
34 zcn 
 |-  ( c e. ZZ -> c e. CC )
35 34 adantr 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> c e. CC )
36 35 ad2antlr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> c e. CC )
37 zcn 
 |-  ( d e. ZZ -> d e. CC )
38 37 adantl 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> d e. CC )
39 38 ad2antlr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> d e. CC )
40 29 39 mulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) x. d ) e. CC )
41 26 33 36 40 muladdd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( c + ( ( sqrt ` D ) x. d ) ) ) = ( ( ( a x. c ) + ( ( ( sqrt ` D ) x. d ) x. ( ( sqrt ` D ) x. b ) ) ) + ( ( a x. ( ( sqrt ` D ) x. d ) ) + ( c x. ( ( sqrt ` D ) x. b ) ) ) ) )
42 29 39 29 32 mul4d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) x. d ) x. ( ( sqrt ` D ) x. b ) ) = ( ( ( sqrt ` D ) x. ( sqrt ` D ) ) x. ( d x. b ) ) )
43 28 msqsqrtd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) x. ( sqrt ` D ) ) = D )
44 43 oveq1d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) x. ( sqrt ` D ) ) x. ( d x. b ) ) = ( D x. ( d x. b ) ) )
45 42 44 eqtrd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) x. d ) x. ( ( sqrt ` D ) x. b ) ) = ( D x. ( d x. b ) ) )
46 45 oveq2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a x. c ) + ( ( ( sqrt ` D ) x. d ) x. ( ( sqrt ` D ) x. b ) ) ) = ( ( a x. c ) + ( D x. ( d x. b ) ) ) )
47 26 29 39 mul12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( a x. ( ( sqrt ` D ) x. d ) ) = ( ( sqrt ` D ) x. ( a x. d ) ) )
48 36 29 32 mul12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( c x. ( ( sqrt ` D ) x. b ) ) = ( ( sqrt ` D ) x. ( c x. b ) ) )
49 47 48 oveq12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a x. ( ( sqrt ` D ) x. d ) ) + ( c x. ( ( sqrt ` D ) x. b ) ) ) = ( ( ( sqrt ` D ) x. ( a x. d ) ) + ( ( sqrt ` D ) x. ( c x. b ) ) ) )
50 26 39 mulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( a x. d ) e. CC )
51 36 32 mulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( c x. b ) e. CC )
52 29 50 51 adddid 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) = ( ( ( sqrt ` D ) x. ( a x. d ) ) + ( ( sqrt ` D ) x. ( c x. b ) ) ) )
53 49 52 eqtr4d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a x. ( ( sqrt ` D ) x. d ) ) + ( c x. ( ( sqrt ` D ) x. b ) ) ) = ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) )
54 46 53 oveq12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( a x. c ) + ( ( ( sqrt ` D ) x. d ) x. ( ( sqrt ` D ) x. b ) ) ) + ( ( a x. ( ( sqrt ` D ) x. d ) ) + ( c x. ( ( sqrt ` D ) x. b ) ) ) ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) )
55 23 41 54 3eqtrd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( A x. B ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) )
56 50 51 addcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a x. d ) + ( c x. b ) ) e. CC )
57 29 56 sqmuld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ^ 2 ) = ( ( ( sqrt ` D ) ^ 2 ) x. ( ( ( a x. d ) + ( c x. b ) ) ^ 2 ) ) )
58 28 sqsqrtd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) ^ 2 ) = D )
59 58 oveq1d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) ^ 2 ) x. ( ( ( a x. d ) + ( c x. b ) ) ^ 2 ) ) = ( D x. ( ( ( a x. d ) + ( c x. b ) ) ^ 2 ) ) )
60 57 59 eqtr2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( D x. ( ( ( a x. d ) + ( c x. b ) ) ^ 2 ) ) = ( ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ^ 2 ) )
61 60 oveq2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` 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 ) - ( ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ^ 2 ) ) )
62 26 36 mulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( a x. c ) e. CC )
63 39 32 mulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( d x. b ) e. CC )
64 28 63 mulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( D x. ( d x. b ) ) e. CC )
65 62 64 addcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a x. c ) + ( D x. ( d x. b ) ) ) e. CC )
66 29 56 mulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) e. CC )
67 subsq 
 |-  ( ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) e. CC /\ ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) e. CC ) -> ( ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) ^ 2 ) - ( ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ^ 2 ) ) = ( ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) x. ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) - ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) ) )
68 65 66 67 syl2anc 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) ^ 2 ) - ( ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ^ 2 ) ) = ( ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) x. ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) - ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) ) )
69 41 54 eqtr2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( c + ( ( sqrt ` D ) x. d ) ) ) )
70 26 33 36 40 mulsubd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a - ( ( sqrt ` D ) x. b ) ) x. ( c - ( ( sqrt ` D ) x. d ) ) ) = ( ( ( a x. c ) + ( ( ( sqrt ` D ) x. d ) x. ( ( sqrt ` D ) x. b ) ) ) - ( ( a x. ( ( sqrt ` D ) x. d ) ) + ( c x. ( ( sqrt ` D ) x. b ) ) ) ) )
71 46 53 oveq12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( a x. c ) + ( ( ( sqrt ` D ) x. d ) x. ( ( sqrt ` D ) x. b ) ) ) - ( ( a x. ( ( sqrt ` D ) x. d ) ) + ( c x. ( ( sqrt ` D ) x. b ) ) ) ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) - ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) )
72 70 71 eqtr2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) - ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) = ( ( a - ( ( sqrt ` D ) x. b ) ) x. ( c - ( ( sqrt ` D ) x. d ) ) ) )
73 69 72 oveq12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) x. ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) - ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) ) = ( ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( c + ( ( sqrt ` D ) x. d ) ) ) x. ( ( a - ( ( sqrt ` D ) x. b ) ) x. ( c - ( ( sqrt ` D ) x. d ) ) ) ) )
74 61 68 73 3eqtrd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` 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 + ( ( sqrt ` D ) x. b ) ) x. ( c + ( ( sqrt ` D ) x. d ) ) ) x. ( ( a - ( ( sqrt ` D ) x. b ) ) x. ( c - ( ( sqrt ` D ) x. d ) ) ) ) )
75 26 33 addcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( a + ( ( sqrt ` D ) x. b ) ) e. CC )
76 36 40 addcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( c + ( ( sqrt ` D ) x. d ) ) e. CC )
77 26 33 subcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( a - ( ( sqrt ` D ) x. b ) ) e. CC )
78 36 40 subcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( c - ( ( sqrt ` D ) x. d ) ) e. CC )
79 75 76 77 78 mul4d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( c + ( ( sqrt ` D ) x. d ) ) ) x. ( ( a - ( ( sqrt ` D ) x. b ) ) x. ( c - ( ( sqrt ` D ) x. d ) ) ) ) = ( ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) x. ( ( c + ( ( sqrt ` D ) x. d ) ) x. ( c - ( ( sqrt ` D ) x. d ) ) ) ) )
80 subsq 
 |-  ( ( a e. CC /\ ( ( sqrt ` D ) x. b ) e. CC ) -> ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
81 26 33 80 syl2anc 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
82 subsq 
 |-  ( ( c e. CC /\ ( ( sqrt ` D ) x. d ) e. CC ) -> ( ( c ^ 2 ) - ( ( ( sqrt ` D ) x. d ) ^ 2 ) ) = ( ( c + ( ( sqrt ` D ) x. d ) ) x. ( c - ( ( sqrt ` D ) x. d ) ) ) )
83 36 40 82 syl2anc 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( c ^ 2 ) - ( ( ( sqrt ` D ) x. d ) ^ 2 ) ) = ( ( c + ( ( sqrt ` D ) x. d ) ) x. ( c - ( ( sqrt ` D ) x. d ) ) ) )
84 81 83 oveq12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) x. ( ( c ^ 2 ) - ( ( ( sqrt ` D ) x. d ) ^ 2 ) ) ) = ( ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) x. ( ( c + ( ( sqrt ` D ) x. d ) ) x. ( c - ( ( sqrt ` D ) x. d ) ) ) ) )
85 29 32 sqmuld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) x. b ) ^ 2 ) = ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) )
86 85 oveq2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) = ( ( a ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) ) )
87 29 39 sqmuld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) x. d ) ^ 2 ) = ( ( ( sqrt ` D ) ^ 2 ) x. ( d ^ 2 ) ) )
88 87 oveq2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( c ^ 2 ) - ( ( ( sqrt ` D ) x. d ) ^ 2 ) ) = ( ( c ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( d ^ 2 ) ) ) )
89 86 88 oveq12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) x. ( ( c ^ 2 ) - ( ( ( sqrt ` D ) x. d ) ^ 2 ) ) ) = ( ( ( a ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) ) x. ( ( c ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( d ^ 2 ) ) ) ) )
90 79 84 89 3eqtr2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( c + ( ( sqrt ` D ) x. d ) ) ) x. ( ( a - ( ( sqrt ` D ) x. b ) ) x. ( c - ( ( sqrt ` D ) x. d ) ) ) ) = ( ( ( a ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) ) x. ( ( c ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( d ^ 2 ) ) ) ) )
91 58 oveq1d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) = ( D x. ( b ^ 2 ) ) )
92 91 oveq2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) ) = ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) )
93 58 oveq1d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) ^ 2 ) x. ( d ^ 2 ) ) = ( D x. ( d ^ 2 ) ) )
94 93 oveq2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( c ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( d ^ 2 ) ) ) = ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) )
95 92 94 oveq12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( a ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) ) x. ( ( c ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( d ^ 2 ) ) ) ) = ( ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) x. ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) ) )
96 simprr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 )
97 96 ad2antrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 )
98 simprr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 )
99 97 98 oveq12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` 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 
 |-  ( 1 x. 1 ) = 1
101 100 a1i 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( 1 x. 1 ) = 1 )
102 95 99 101 3eqtrd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> ( ( ( a ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) ) x. ( ( c ^ 2 ) - ( ( ( sqrt ` D ) ^ 2 ) x. ( d ^ 2 ) ) ) ) = 1 )
103 74 90 102 3eqtrd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` 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 
 |-  ( e = ( ( a x. c ) + ( D x. ( d x. b ) ) ) -> ( e + ( ( sqrt ` D ) x. f ) ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. f ) ) )
105 104 eqeq2d 
 |-  ( e = ( ( a x. c ) + ( D x. ( d x. b ) ) ) -> ( ( A x. B ) = ( e + ( ( sqrt ` D ) x. f ) ) <-> ( A x. B ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. f ) ) ) )
106 oveq1 
 |-  ( e = ( ( a x. c ) + ( D x. ( d x. b ) ) ) -> ( e ^ 2 ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) ^ 2 ) )
107 106 oveq1d 
 |-  ( 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 ) ) ) )
108 107 eqeq1d 
 |-  ( 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 ) )
109 105 108 anbi12d 
 |-  ( e = ( ( a x. c ) + ( D x. ( d x. b ) ) ) -> ( ( ( A x. B ) = ( e + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) <-> ( ( A x. B ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. f ) ) /\ ( ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) ) )
110 oveq2 
 |-  ( f = ( ( a x. d ) + ( c x. b ) ) -> ( ( sqrt ` D ) x. f ) = ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) )
111 110 oveq2d 
 |-  ( f = ( ( a x. d ) + ( c x. b ) ) -> ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. f ) ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) )
112 111 eqeq2d 
 |-  ( f = ( ( a x. d ) + ( c x. b ) ) -> ( ( A x. B ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. f ) ) <-> ( A x. B ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` D ) x. ( ( a x. d ) + ( c x. b ) ) ) ) ) )
113 oveq1 
 |-  ( f = ( ( a x. d ) + ( c x. b ) ) -> ( f ^ 2 ) = ( ( ( a x. d ) + ( c x. b ) ) ^ 2 ) )
114 113 oveq2d 
 |-  ( f = ( ( a x. d ) + ( c x. b ) ) -> ( D x. ( f ^ 2 ) ) = ( D x. ( ( ( a x. d ) + ( c x. b ) ) ^ 2 ) ) )
115 114 oveq2d 
 |-  ( 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 ) ) ) )
116 115 eqeq1d 
 |-  ( 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 ) )
117 112 116 anbi12d 
 |-  ( f = ( ( a x. d ) + ( c x. b ) ) -> ( ( ( A x. B ) = ( ( ( a x. c ) + ( D x. ( d x. b ) ) ) + ( ( sqrt ` 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 ) ) ) + ( ( sqrt ` 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 ) ) )
118 109 117 rspc2ev 
 |-  ( ( ( ( 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 ) ) ) + ( ( sqrt ` 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 + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) )
119 16 19 55 103 118 syl112anc 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) -> E. e e. ZZ E. f e. ZZ ( ( A x. B ) = ( e + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) )
120 2 119 jca 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( ( sqrt ` 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 + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) ) )
121 120 ex 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( B = ( c + ( ( sqrt ` 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 + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) ) ) )
122 121 rexlimdvva 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( E. c e. ZZ E. d e. ZZ ( B = ( c + ( ( sqrt ` 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 + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) ) ) )
123 122 ex 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( E. c e. ZZ E. d e. ZZ ( B = ( c + ( ( sqrt ` 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 + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) ) ) ) )
124 123 rexlimdvva 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) -> ( E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( E. c e. ZZ E. d e. ZZ ( B = ( c + ( ( sqrt ` 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 + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) ) ) ) )
125 124 impd 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. RR /\ B e. RR ) ) -> ( ( E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ E. c e. ZZ E. d e. ZZ ( B = ( c + ( ( sqrt ` 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 + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) ) ) )
126 125 expimpd 
 |-  ( D e. ( NN \ []NN ) -> ( ( ( A e. RR /\ B e. RR ) /\ ( E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ E. c e. ZZ E. d e. ZZ ( B = ( c + ( ( sqrt ` 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 + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) ) ) )
127 elpell1234qr 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1234QR ` D ) <-> ( A e. RR /\ E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
128 elpell1234qr 
 |-  ( D e. ( NN \ []NN ) -> ( B e. ( Pell1234QR ` D ) <-> ( B e. RR /\ E. c e. ZZ E. d e. ZZ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) )
129 127 128 anbi12d 
 |-  ( 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 + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( B e. RR /\ E. c e. ZZ E. d e. ZZ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) ) )
130 an4 
 |-  ( ( ( A e. RR /\ E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ ( B e. RR /\ E. c e. ZZ E. d e. ZZ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) <-> ( ( A e. RR /\ B e. RR ) /\ ( E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ E. c e. ZZ E. d e. ZZ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) )
131 129 130 bitrdi 
 |-  ( D e. ( NN \ []NN ) -> ( ( A e. ( Pell1234QR ` D ) /\ B e. ( Pell1234QR ` D ) ) <-> ( ( A e. RR /\ B e. RR ) /\ ( E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ E. c e. ZZ E. d e. ZZ ( B = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) ) )
132 elpell1234qr 
 |-  ( D e. ( NN \ []NN ) -> ( ( A x. B ) e. ( Pell1234QR ` D ) <-> ( ( A x. B ) e. RR /\ E. e e. ZZ E. f e. ZZ ( ( A x. B ) = ( e + ( ( sqrt ` D ) x. f ) ) /\ ( ( e ^ 2 ) - ( D x. ( f ^ 2 ) ) ) = 1 ) ) ) )
133 126 131 132 3imtr4d 
 |-  ( D e. ( NN \ []NN ) -> ( ( A e. ( Pell1234QR ` D ) /\ B e. ( Pell1234QR ` D ) ) -> ( A x. B ) e. ( Pell1234QR ` D ) ) )
134 133 3impib 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) /\ B e. ( Pell1234QR ` D ) ) -> ( A x. B ) e. ( Pell1234QR ` D ) )