Metamath Proof Explorer

Theorem pell14qrgt0

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

Ref Expression
Assertion pell14qrgt0 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 0 < A )

Proof

Step Hyp Ref Expression
1 elpell14qr 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell14QR ` D ) <-> ( A e. RR /\ E. a e. NN0 E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
2 0cnd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 e. CC )
3 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
4 3 ad3antrrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> D e. NN )
5 4 nnred 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> D e. RR )
6 4 nnnn0d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> D e. NN0 )
7 6 nn0ge0d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 <_ D )
8 5 7 resqrtcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( sqrt ` D ) e. RR )
9 zre 
 |-  ( b e. ZZ -> b e. RR )
10 9 adantl 
 |-  ( ( a e. NN0 /\ b e. ZZ ) -> b e. RR )
11 10 ad2antlr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> b e. RR )
12 8 11 remulcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( sqrt ` D ) x. b ) e. RR )
13 12 recnd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( sqrt ` D ) x. b ) e. CC )
14 2 13 abssubd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( abs ` ( 0 - ( ( sqrt ` D ) x. b ) ) ) = ( abs ` ( ( ( sqrt ` D ) x. b ) - 0 ) ) )
15 13 subid1d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( ( sqrt ` D ) x. b ) - 0 ) = ( ( sqrt ` D ) x. b ) )
16 15 fveq2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( abs ` ( ( ( sqrt ` D ) x. b ) - 0 ) ) = ( abs ` ( ( sqrt ` D ) x. b ) ) )
17 14 16 eqtrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( abs ` ( 0 - ( ( sqrt ` D ) x. b ) ) ) = ( abs ` ( ( sqrt ` D ) x. b ) ) )
18 absresq 
 |-  ( ( ( sqrt ` D ) x. b ) e. RR -> ( ( abs ` ( ( sqrt ` D ) x. b ) ) ^ 2 ) = ( ( ( sqrt ` D ) x. b ) ^ 2 ) )
19 12 18 syl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( abs ` ( ( sqrt ` D ) x. b ) ) ^ 2 ) = ( ( ( sqrt ` D ) x. b ) ^ 2 ) )
20 5 recnd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> D e. CC )
21 20 sqrtcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( sqrt ` D ) e. CC )
22 10 recnd 
 |-  ( ( a e. NN0 /\ b e. ZZ ) -> b e. CC )
23 22 ad2antlr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> b e. CC )
24 21 23 sqmuld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( ( sqrt ` D ) x. b ) ^ 2 ) = ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) )
25 20 sqsqrtd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( sqrt ` D ) ^ 2 ) = D )
26 25 oveq1d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) = ( D x. ( b ^ 2 ) ) )
27 19 24 26 3eqtrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( abs ` ( ( sqrt ` D ) x. b ) ) ^ 2 ) = ( D x. ( b ^ 2 ) ) )
28 0lt1 
 |-  0 < 1
29 simpr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 )
30 28 29 breqtrrid 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 < ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) )
31 11 resqcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( b ^ 2 ) e. RR )
32 5 31 remulcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( D x. ( b ^ 2 ) ) e. RR )
33 nn0re 
 |-  ( a e. NN0 -> a e. RR )
34 33 adantr 
 |-  ( ( a e. NN0 /\ b e. ZZ ) -> a e. RR )
35 34 ad2antlr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> a e. RR )
36 35 resqcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( a ^ 2 ) e. RR )
37 32 36 posdifd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( D x. ( b ^ 2 ) ) < ( a ^ 2 ) <-> 0 < ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) ) )
38 30 37 mpbird 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( D x. ( b ^ 2 ) ) < ( a ^ 2 ) )
39 27 38 eqbrtrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( abs ` ( ( sqrt ` D ) x. b ) ) ^ 2 ) < ( a ^ 2 ) )
40 13 abscld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( abs ` ( ( sqrt ` D ) x. b ) ) e. RR )
41 13 absge0d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 <_ ( abs ` ( ( sqrt ` D ) x. b ) ) )
42 nn0ge0 
 |-  ( a e. NN0 -> 0 <_ a )
43 42 adantr 
 |-  ( ( a e. NN0 /\ b e. ZZ ) -> 0 <_ a )
44 43 ad2antlr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 <_ a )
45 40 35 41 44 lt2sqd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( abs ` ( ( sqrt ` D ) x. b ) ) < a <-> ( ( abs ` ( ( sqrt ` D ) x. b ) ) ^ 2 ) < ( a ^ 2 ) ) )
46 39 45 mpbird 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( abs ` ( ( sqrt ` D ) x. b ) ) < a )
47 17 46 eqbrtrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( abs ` ( 0 - ( ( sqrt ` D ) x. b ) ) ) < a )
48 0red 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 e. RR )
49 48 12 35 absdifltd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( abs ` ( 0 - ( ( sqrt ` D ) x. b ) ) ) < a <-> ( ( ( ( sqrt ` D ) x. b ) - a ) < 0 /\ 0 < ( ( ( sqrt ` D ) x. b ) + a ) ) ) )
50 47 49 mpbid 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( ( ( sqrt ` D ) x. b ) - a ) < 0 /\ 0 < ( ( ( sqrt ` D ) x. b ) + a ) ) )
51 50 simprd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 < ( ( ( sqrt ` D ) x. b ) + a ) )
52 nn0cn 
 |-  ( a e. NN0 -> a e. CC )
53 52 adantr 
 |-  ( ( a e. NN0 /\ b e. ZZ ) -> a e. CC )
54 53 ad2antlr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> a e. CC )
55 54 13 addcomd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( a + ( ( sqrt ` D ) x. b ) ) = ( ( ( sqrt ` D ) x. b ) + a ) )
56 51 55 breqtrrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 < ( a + ( ( sqrt ` D ) x. b ) ) )
57 56 adantrl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 0 < ( a + ( ( sqrt ` D ) x. b ) ) )
58 simprl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A = ( a + ( ( sqrt ` D ) x. b ) ) )
59 57 58 breqtrrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 0 < A )
60 59 ex 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 < A ) )
61 60 rexlimdvva 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR ) -> ( E. a e. NN0 E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 < A ) )
62 61 expimpd 
 |-  ( D e. ( NN \ []NN ) -> ( ( A e. RR /\ E. a e. NN0 E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 0 < A ) )
63 1 62 sylbid 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell14QR ` D ) -> 0 < A ) )
64 63 imp 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 0 < A )