# Metamath Proof Explorer

## Theorem pellfund14b

Description: The positive Pell solutions are precisely the integer powers of the fundamental solution. To get the general solution set (which we will not be using), throw in a copy of Z/2Z. (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion pellfund14b
`|- ( D e. ( NN \ []NN ) -> ( A e. ( Pell14QR ` D ) <-> E. x e. ZZ A = ( ( PellFund ` D ) ^ x ) ) )`

### Proof

Step Hyp Ref Expression
1 pellfund14
` |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> E. x e. ZZ A = ( ( PellFund ` D ) ^ x ) )`
2 simpll
` |-  ( ( ( D e. ( NN \ []NN ) /\ x e. ZZ ) /\ A = ( ( PellFund ` D ) ^ x ) ) -> D e. ( NN \ []NN ) )`
` |-  ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) C_ ( Pell14QR ` D ) )`
4 pellfundex
` |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) )`
5 3 4 sseldd
` |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. ( Pell14QR ` D ) )`
` |-  ( ( ( D e. ( NN \ []NN ) /\ x e. ZZ ) /\ A = ( ( PellFund ` D ) ^ x ) ) -> ( PellFund ` D ) e. ( Pell14QR ` D ) )`
7 simplr
` |-  ( ( ( D e. ( NN \ []NN ) /\ x e. ZZ ) /\ A = ( ( PellFund ` D ) ^ x ) ) -> x e. ZZ )`
8 pell14qrexpcl
` |-  ( ( D e. ( NN \ []NN ) /\ ( PellFund ` D ) e. ( Pell14QR ` D ) /\ x e. ZZ ) -> ( ( PellFund ` D ) ^ x ) e. ( Pell14QR ` D ) )`
9 2 6 7 8 syl3anc
` |-  ( ( ( D e. ( NN \ []NN ) /\ x e. ZZ ) /\ A = ( ( PellFund ` D ) ^ x ) ) -> ( ( PellFund ` D ) ^ x ) e. ( Pell14QR ` D ) )`
10 eleq1
` |-  ( A = ( ( PellFund ` D ) ^ x ) -> ( A e. ( Pell14QR ` D ) <-> ( ( PellFund ` D ) ^ x ) e. ( Pell14QR ` D ) ) )`
` |-  ( ( ( D e. ( NN \ []NN ) /\ x e. ZZ ) /\ A = ( ( PellFund ` D ) ^ x ) ) -> ( A e. ( Pell14QR ` D ) <-> ( ( PellFund ` D ) ^ x ) e. ( Pell14QR ` D ) ) )`
` |-  ( ( ( D e. ( NN \ []NN ) /\ x e. ZZ ) /\ A = ( ( PellFund ` D ) ^ x ) ) -> A e. ( Pell14QR ` D ) )`
` |-  ( ( D e. ( NN \ []NN ) /\ E. x e. ZZ A = ( ( PellFund ` D ) ^ x ) ) -> A e. ( Pell14QR ` D ) )`
` |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell14QR ` D ) <-> E. x e. ZZ A = ( ( PellFund ` D ) ^ x ) ) )`