Metamath Proof Explorer

Theorem elpell1qr2

Description: The first quadrant solutions are precisely the positive Pell solutions which are at least one. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion elpell1qr2 
|- ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. ( Pell14QR ` D ) /\ 1 <_ A ) ) )

Proof

Step Hyp Ref Expression
1 pell1qrss14 
 |-  ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) C_ ( Pell14QR ` D ) )
2 1 sselda 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1QR ` D ) ) -> A e. ( Pell14QR ` D ) )
3 pell1qrge1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1QR ` D ) ) -> 1 <_ A )
4 2 3 jca 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1QR ` D ) ) -> ( A e. ( Pell14QR ` D ) /\ 1 <_ A ) )
5 1red 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 1 e. RR )
6 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR )
7 5 6 leloed 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( 1 <_ A <-> ( 1 < A \/ 1 = A ) ) )
8 5 6 ltnled 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( 1 < A <-> -. A <_ 1 ) )
9 8 biimpa 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> -. A <_ 1 )
10 1div1e1 
 |-  ( 1 / 1 ) = 1
11 10 eqcomi 
 |-  1 = ( 1 / 1 )
12 11 a1i 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> 1 = ( 1 / 1 ) )
13 12 breq2d 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> ( A <_ 1 <-> A <_ ( 1 / 1 ) ) )
14 6 adantr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> A e. RR )
15 pell14qrgt0 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 0 < A )
16 15 adantr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> 0 < A )
17 1red 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> 1 e. RR )
18 0lt1 
 |-  0 < 1
19 18 a1i 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> 0 < 1 )
20 lerec2 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 e. RR /\ 0 < 1 ) ) -> ( A <_ ( 1 / 1 ) <-> 1 <_ ( 1 / A ) ) )
21 14 16 17 19 20 syl22anc 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> ( A <_ ( 1 / 1 ) <-> 1 <_ ( 1 / A ) ) )
22 13 21 bitrd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> ( A <_ 1 <-> 1 <_ ( 1 / A ) ) )
23 9 22 mtbid 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> -. 1 <_ ( 1 / A ) )
24 simplll 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) /\ ( 1 / A ) e. ( Pell1QR ` D ) ) -> D e. ( NN \ []NN ) )
25 pell1qrge1 
 |-  ( ( D e. ( NN \ []NN ) /\ ( 1 / A ) e. ( Pell1QR ` D ) ) -> 1 <_ ( 1 / A ) )
26 24 25 sylancom 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) /\ ( 1 / A ) e. ( Pell1QR ` D ) ) -> 1 <_ ( 1 / A ) )
27 23 26 mtand 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> -. ( 1 / A ) e. ( Pell1QR ` D ) )
28 pell14qrdich 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A e. ( Pell1QR ` D ) \/ ( 1 / A ) e. ( Pell1QR ` D ) ) )
29 28 adantr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> ( A e. ( Pell1QR ` D ) \/ ( 1 / A ) e. ( Pell1QR ` D ) ) )
30 orel2 
 |-  ( -. ( 1 / A ) e. ( Pell1QR ` D ) -> ( ( A e. ( Pell1QR ` D ) \/ ( 1 / A ) e. ( Pell1QR ` D ) ) -> A e. ( Pell1QR ` D ) ) )
31 27 29 30 sylc 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 < A ) -> A e. ( Pell1QR ` D ) )
32 simpr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 = A ) -> 1 = A )
33 pell1qr1 
 |-  ( D e. ( NN \ []NN ) -> 1 e. ( Pell1QR ` D ) )
34 33 ad2antrr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 = A ) -> 1 e. ( Pell1QR ` D ) )
35 32 34 eqeltrrd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ 1 = A ) -> A e. ( Pell1QR ` D ) )
36 31 35 jaodan 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ ( 1 < A \/ 1 = A ) ) -> A e. ( Pell1QR ` D ) )
37 36 ex 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( 1 < A \/ 1 = A ) -> A e. ( Pell1QR ` D ) ) )
38 7 37 sylbid 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( 1 <_ A -> A e. ( Pell1QR ` D ) ) )
39 38 impr 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. ( Pell14QR ` D ) /\ 1 <_ A ) ) -> A e. ( Pell1QR ` D ) )
40 4 39 impbida 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. ( Pell14QR ` D ) /\ 1 <_ A ) ) )