Metamath Proof Explorer

Theorem pell1qrss14

Description: First-quadrant Pell solutions are a subset of the positive solutions. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell1qrss14 
|- ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) C_ ( Pell14QR ` 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 /\ ( a = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( b e. ZZ /\ ( a = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
4 3 reximdv2 
 |-  ( D e. ( NN \ []NN ) -> ( E. b e. NN0 ( a = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> E. b e. ZZ ( a = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) )
5 4 reximdv 
 |-  ( D e. ( NN \ []NN ) -> ( E. c e. NN0 E. b e. NN0 ( a = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> E. c e. NN0 E. b e. ZZ ( a = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) )
6 5 anim2d 
 |-  ( D e. ( NN \ []NN ) -> ( ( a e. RR /\ E. c e. NN0 E. b e. NN0 ( a = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( a e. RR /\ E. c e. NN0 E. b e. ZZ ( a = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
7 elpell1qr 
 |-  ( D e. ( NN \ []NN ) -> ( a e. ( Pell1QR ` D ) <-> ( a e. RR /\ E. c e. NN0 E. b e. NN0 ( a = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
8 elpell14qr 
 |-  ( D e. ( NN \ []NN ) -> ( a e. ( Pell14QR ` D ) <-> ( a e. RR /\ E. c e. NN0 E. b e. ZZ ( a = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
9 6 7 8 3imtr4d 
 |-  ( D e. ( NN \ []NN ) -> ( a e. ( Pell1QR ` D ) -> a e. ( Pell14QR ` D ) ) )
10 9 ssrdv 
 |-  ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) C_ ( Pell14QR ` D ) )