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 ) )
3		pell1qrss14	|- ( 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 ) )
6	5	ad2antrr	|- ( ( ( 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 ) ) )
11	10	adantl	|- ( ( ( D e. ( NN \ []NN ) /\ x e. ZZ ) /\ A = ( ( PellFund ` D ) ^ x ) ) -> ( A e. ( Pell14QR ` D ) <-> ( ( PellFund ` D ) ^ x ) e. ( Pell14QR ` D ) ) )
12	9 11	mpbird	|- ( ( ( D e. ( NN \ []NN ) /\ x e. ZZ ) /\ A = ( ( PellFund ` D ) ^ x ) ) -> A e. ( Pell14QR ` D ) )
13	12	r19.29an	|- ( ( D e. ( NN \ []NN ) /\ E. x e. ZZ A = ( ( PellFund ` D ) ^ x ) ) -> A e. ( Pell14QR ` D ) )
14	1 13	impbida	|- ( D e. ( NN \ []NN ) -> ( A e. ( Pell14QR ` D ) <-> E. x e. ZZ A = ( ( PellFund ` D ) ^ x ) ) )