Metamath Proof Explorer

Theorem pell1qr1

Description: 1 is a Pell solution and in the first quadrant as one. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion pell1qr1 
|- ( D e. ( NN \ []NN ) -> 1 e. ( Pell1QR ` D ) )

Proof

Step Hyp Ref Expression
1 1red 
 |-  ( D e. ( NN \ []NN ) -> 1 e. RR )
2 1nn0 
 |-  1 e. NN0
3 2 a1i 
 |-  ( D e. ( NN \ []NN ) -> 1 e. NN0 )
4 0nn0 
 |-  0 e. NN0
5 4 a1i 
 |-  ( D e. ( NN \ []NN ) -> 0 e. NN0 )
6 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
7 6 nncnd 
 |-  ( D e. ( NN \ []NN ) -> D e. CC )
8 7 sqrtcld 
 |-  ( D e. ( NN \ []NN ) -> ( sqrt ` D ) e. CC )
9 8 mul01d 
 |-  ( D e. ( NN \ []NN ) -> ( ( sqrt ` D ) x. 0 ) = 0 )
10 9 oveq2d 
 |-  ( D e. ( NN \ []NN ) -> ( 1 + ( ( sqrt ` D ) x. 0 ) ) = ( 1 + 0 ) )
11 1p0e1 
 |-  ( 1 + 0 ) = 1
12 10 11 eqtr2di 
 |-  ( D e. ( NN \ []NN ) -> 1 = ( 1 + ( ( sqrt ` D ) x. 0 ) ) )
13 sq1 
 |-  ( 1 ^ 2 ) = 1
14 13 a1i 
 |-  ( D e. ( NN \ []NN ) -> ( 1 ^ 2 ) = 1 )
15 sq0 
 |-  ( 0 ^ 2 ) = 0
16 15 oveq2i 
 |-  ( D x. ( 0 ^ 2 ) ) = ( D x. 0 )
17 7 mul01d 
 |-  ( D e. ( NN \ []NN ) -> ( D x. 0 ) = 0 )
18 16 17 syl5eq 
 |-  ( D e. ( NN \ []NN ) -> ( D x. ( 0 ^ 2 ) ) = 0 )
19 14 18 oveq12d 
 |-  ( D e. ( NN \ []NN ) -> ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) = ( 1 - 0 ) )
20 1m0e1 
 |-  ( 1 - 0 ) = 1
21 19 20 eqtrdi 
 |-  ( D e. ( NN \ []NN ) -> ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) = 1 )
22 oveq1 
 |-  ( a = 1 -> ( a + ( ( sqrt ` D ) x. b ) ) = ( 1 + ( ( sqrt ` D ) x. b ) ) )
23 22 eqeq2d 
 |-  ( a = 1 -> ( 1 = ( a + ( ( sqrt ` D ) x. b ) ) <-> 1 = ( 1 + ( ( sqrt ` D ) x. b ) ) ) )
24 oveq1 
 |-  ( a = 1 -> ( a ^ 2 ) = ( 1 ^ 2 ) )
25 24 oveq1d 
 |-  ( a = 1 -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) )
26 25 eqeq1d 
 |-  ( a = 1 -> ( ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 <-> ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
27 23 26 anbi12d 
 |-  ( a = 1 -> ( ( 1 = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) <-> ( 1 = ( 1 + ( ( sqrt ` D ) x. b ) ) /\ ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) )
28 oveq2 
 |-  ( b = 0 -> ( ( sqrt ` D ) x. b ) = ( ( sqrt ` D ) x. 0 ) )
29 28 oveq2d 
 |-  ( b = 0 -> ( 1 + ( ( sqrt ` D ) x. b ) ) = ( 1 + ( ( sqrt ` D ) x. 0 ) ) )
30 29 eqeq2d 
 |-  ( b = 0 -> ( 1 = ( 1 + ( ( sqrt ` D ) x. b ) ) <-> 1 = ( 1 + ( ( sqrt ` D ) x. 0 ) ) ) )
31 oveq1 
 |-  ( b = 0 -> ( b ^ 2 ) = ( 0 ^ 2 ) )
32 31 oveq2d 
 |-  ( b = 0 -> ( D x. ( b ^ 2 ) ) = ( D x. ( 0 ^ 2 ) ) )
33 32 oveq2d 
 |-  ( b = 0 -> ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) )
34 33 eqeq1d 
 |-  ( b = 0 -> ( ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 <-> ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) = 1 ) )
35 30 34 anbi12d 
 |-  ( b = 0 -> ( ( 1 = ( 1 + ( ( sqrt ` D ) x. b ) ) /\ ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) <-> ( 1 = ( 1 + ( ( sqrt ` D ) x. 0 ) ) /\ ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) = 1 ) ) )
36 27 35 rspc2ev 
 |-  ( ( 1 e. NN0 /\ 0 e. NN0 /\ ( 1 = ( 1 + ( ( sqrt ` D ) x. 0 ) ) /\ ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) = 1 ) ) -> E. a e. NN0 E. b e. NN0 ( 1 = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
37 3 5 12 21 36 syl112anc 
 |-  ( D e. ( NN \ []NN ) -> E. a e. NN0 E. b e. NN0 ( 1 = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
38 elpell1qr 
 |-  ( D e. ( NN \ []NN ) -> ( 1 e. ( Pell1QR ` D ) <-> ( 1 e. RR /\ E. a e. NN0 E. b e. NN0 ( 1 = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
39 1 37 38 mpbir2and 
 |-  ( D e. ( NN \ []NN ) -> 1 e. ( Pell1QR ` D ) )