Metamath Proof Explorer

Theorem pell14qrdivcl

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

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

Proof

Step Hyp Ref Expression
1 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR )
2 1 recnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. CC )
3 2 3adant3 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) -> A e. CC )
4 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ B e. ( Pell14QR ` D ) ) -> B e. RR )
5 4 recnd 
 |-  ( ( D e. ( NN \ []NN ) /\ B e. ( Pell14QR ` D ) ) -> B e. CC )
6 5 3adant2 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) -> B e. CC )
7 pell14qrne0 
 |-  ( ( D e. ( NN \ []NN ) /\ B e. ( Pell14QR ` D ) ) -> B =/= 0 )
8 7 3adant2 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) -> B =/= 0 )
9 3 6 8 divrecd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
10 pell14qrreccl 
 |-  ( ( D e. ( NN \ []NN ) /\ B e. ( Pell14QR ` D ) ) -> ( 1 / B ) e. ( Pell14QR ` D ) )
11 10 3adant2 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) -> ( 1 / B ) e. ( Pell14QR ` D ) )
12 pell14qrmulcl 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 / B ) e. ( Pell14QR ` D ) ) -> ( A x. ( 1 / B ) ) e. ( Pell14QR ` D ) )
13 11 12 syld3an3 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) -> ( A x. ( 1 / B ) ) e. ( Pell14QR ` D ) )
14 9 13 eqeltrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ( Pell14QR ` D ) ) -> ( A / B ) e. ( Pell14QR ` D ) )