Metamath Proof Explorer

Theorem pell14qrss1234

Description: A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell14qrss1234 
|- ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) C_ ( Pell1234QR ` D ) )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( b e. NN0 -> b e. ZZ )
2 1 a1i 
 |-  ( D e. ( NN \ []NN ) -> ( b e. NN0 -> b e. ZZ ) )
3 2 anim1d 
 |-  ( D e. ( NN \ []NN ) -> ( ( b e. NN0 /\ E. c e. ZZ ( a = ( b + ( ( sqrt ` D ) x. c ) ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) -> ( b e. ZZ /\ E. c e. ZZ ( a = ( b + ( ( sqrt ` D ) x. c ) ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) ) )
4 3 reximdv2 
 |-  ( D e. ( NN \ []NN ) -> ( E. b e. NN0 E. c e. ZZ ( a = ( b + ( ( sqrt ` D ) x. c ) ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) -> E. b e. ZZ E. c e. ZZ ( a = ( b + ( ( sqrt ` D ) x. c ) ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) )
5 4 anim2d 
 |-  ( D e. ( NN \ []NN ) -> ( ( a e. RR /\ E. b e. NN0 E. c e. ZZ ( a = ( b + ( ( sqrt ` D ) x. c ) ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) -> ( a e. RR /\ E. b e. ZZ E. c e. ZZ ( a = ( b + ( ( sqrt ` D ) x. c ) ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) ) )
6 elpell14qr 
 |-  ( D e. ( NN \ []NN ) -> ( a e. ( Pell14QR ` D ) <-> ( a e. RR /\ E. b e. NN0 E. c e. ZZ ( a = ( b + ( ( sqrt ` D ) x. c ) ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) ) )
7 elpell1234qr 
 |-  ( D e. ( NN \ []NN ) -> ( a e. ( Pell1234QR ` D ) <-> ( a e. RR /\ E. b e. ZZ E. c e. ZZ ( a = ( b + ( ( sqrt ` D ) x. c ) ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) ) )
8 5 6 7 3imtr4d 
 |-  ( D e. ( NN \ []NN ) -> ( a e. ( Pell14QR ` D ) -> a e. ( Pell1234QR ` D ) ) )
9 8 ssrdv 
 |-  ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) C_ ( Pell1234QR ` D ) )