Metamath Proof Explorer

Theorem elpell14qr2

Description: A number is a positive Pell solution iff it is positive and a Pell solution, justifying our name choice. (Contributed by Stefan O'Rear, 19-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 pell14qrss1234 
 |-  ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) C_ ( Pell1234QR ` D ) )
2 1 sselda 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. ( Pell1234QR ` D ) )
3 pell14qrgt0 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 0 < A )
4 2 3 jca 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A e. ( Pell1234QR ` D ) /\ 0 < A ) )
5 0re 
 |-  0 e. RR
6 pell1234qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A e. RR )
7 ltnsym 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> -. A < 0 ) )
8 5 6 7 sylancr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( 0 < A -> -. A < 0 ) )
9 8 impr 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. ( Pell1234QR ` D ) /\ 0 < A ) ) -> -. A < 0 )
10 6 adantrr 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. ( Pell1234QR ` D ) /\ 0 < A ) ) -> A e. RR )
11 10 lt0neg1d 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. ( Pell1234QR ` D ) /\ 0 < A ) ) -> ( A < 0 <-> 0 < -u A ) )
12 9 11 mtbid 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. ( Pell1234QR ` D ) /\ 0 < A ) ) -> -. 0 < -u A )
13 pell14qrgt0 
 |-  ( ( D e. ( NN \ []NN ) /\ -u A e. ( Pell14QR ` D ) ) -> 0 < -u A )
14 13 ex 
 |-  ( D e. ( NN \ []NN ) -> ( -u A e. ( Pell14QR ` D ) -> 0 < -u A ) )
15 14 adantr 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. ( Pell1234QR ` D ) /\ 0 < A ) ) -> ( -u A e. ( Pell14QR ` D ) -> 0 < -u A ) )
16 12 15 mtod 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. ( Pell1234QR ` D ) /\ 0 < A ) ) -> -. -u A e. ( Pell14QR ` D ) )
17 pell1234qrdich 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) )
18 17 adantrr 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. ( Pell1234QR ` D ) /\ 0 < A ) ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) )
19 orel2 
 |-  ( -. -u A e. ( Pell14QR ` D ) -> ( ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) -> A e. ( Pell14QR ` D ) ) )
20 16 18 19 sylc 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A e. ( Pell1234QR ` D ) /\ 0 < A ) ) -> A e. ( Pell14QR ` D ) )
21 4 20 impbida 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell14QR ` D ) <-> ( A e. ( Pell1234QR ` D ) /\ 0 < A ) ) )