Metamath Proof Explorer

Theorem pell14qrmulcl

Description: Positive Pell solutions are closed under multiplication. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion pell14qrmulcl 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) -> ( A x. B ) e. ( Pell14QR ` D ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( D e. ( NN \ []NN ) /\ ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) -> D e. ( NN \ []NN ) )
2 simprll 
 |-  ( ( D e. ( NN \ []NN ) /\ ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) -> A e. ( Pell1234QR ` D ) )
3 simprrl 
 |-  ( ( D e. ( NN \ []NN ) /\ ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) -> B e. ( Pell1234QR ` D ) )
4 pell1234qrmulcl 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) /\ B e. ( Pell1234QR ` D ) ) -> ( A x. B ) e. ( Pell1234QR ` D ) )
5 1 2 3 4 syl3anc 
 |-  ( ( D e. ( NN \ []NN ) /\ ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) -> ( A x. B ) e. ( Pell1234QR ` D ) )
6 pell1234qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A e. RR )
7 2 6 syldan 
 |-  ( ( D e. ( NN \ []NN ) /\ ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) -> A e. RR )
8 pell1234qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ B e. ( Pell1234QR ` D ) ) -> B e. RR )
9 3 8 syldan 
 |-  ( ( D e. ( NN \ []NN ) /\ ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) -> B e. RR )
10 simprlr 
 |-  ( ( D e. ( NN \ []NN ) /\ ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) -> 0 < A )
11 simprrr 
 |-  ( ( D e. ( NN \ []NN ) /\ ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) -> 0 < B )
12 7 9 10 11 mulgt0d 
 |-  ( ( D e. ( NN \ []NN ) /\ ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) -> 0 < ( A x. B ) )
13 5 12 jca 
 |-  ( ( D e. ( NN \ []NN ) /\ ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) -> ( ( A x. B ) e. ( Pell1234QR ` D ) /\ 0 < ( A x. B ) ) )
14 13 ex 
 |-  ( D e. ( NN \ []NN ) -> ( ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) -> ( ( A x. B ) e. ( Pell1234QR ` D ) /\ 0 < ( A x. B ) ) ) )
15 elpell14qr2 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell14QR ` D ) <-> ( A e. ( Pell1234QR ` D ) /\ 0 < A ) ) )
16 elpell14qr2 
 |-  ( D e. ( NN \ []NN ) -> ( B e. ( Pell14QR ` D ) <-> ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) )
17 15 16 anbi12d 
 |-  ( D e. ( NN \ []NN ) -> ( ( A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) <-> ( ( A e. ( Pell1234QR ` D ) /\ 0 < A ) /\ ( B e. ( Pell1234QR ` D ) /\ 0 < B ) ) ) )
18 elpell14qr2 
 |-  ( D e. ( NN \ []NN ) -> ( ( A x. B ) e. ( Pell14QR ` D ) <-> ( ( A x. B ) e. ( Pell1234QR ` D ) /\ 0 < ( A x. B ) ) ) )
19 14 17 18 3imtr4d 
 |-  ( D e. ( NN \ []NN ) -> ( ( A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) -> ( A x. B ) e. ( Pell14QR ` D ) ) )
20 19 3impib 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) -> ( A x. B ) e. ( Pell14QR ` D ) )