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 \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell14QR (D) \leftrightarrow \exists x \in ℤ A = {PellFund (D)}^{x})$

Proof

Step	Hyp	Ref	Expression
1		pellfund14	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \exists x \in ℤ A = {PellFund (D)}^{x}$
2		simpll	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land x \in ℤ) \land A = {PellFund (D)}^{x}) \to D \in (ℕ ∖ ◻_{ℕ})$
3		pell1qrss14	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to Pell1QR (D) \subseteq Pell14QR (D)$
4		pellfundex	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in Pell1QR (D)$
5	3 4	sseldd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in Pell14QR (D)$
6	5	ad2antrr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land x \in ℤ) \land A = {PellFund (D)}^{x}) \to PellFund (D) \in Pell14QR (D)$
7		simplr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land x \in ℤ) \land A = {PellFund (D)}^{x}) \to x \in ℤ$
8		pell14qrexpcl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land PellFund (D) \in Pell14QR (D) \land x \in ℤ) \to {PellFund (D)}^{x} \in Pell14QR (D)$
9	2 6 7 8	syl3anc	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land x \in ℤ) \land A = {PellFund (D)}^{x}) \to {PellFund (D)}^{x} \in Pell14QR (D)$
10		eleq1	$⊢ A = {PellFund (D)}^{x} \to (A \in Pell14QR (D) \leftrightarrow {PellFund (D)}^{x} \in Pell14QR (D))$
11	10	adantl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land x \in ℤ) \land A = {PellFund (D)}^{x}) \to (A \in Pell14QR (D) \leftrightarrow {PellFund (D)}^{x} \in Pell14QR (D))$
12	9 11	mpbird	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land x \in ℤ) \land A = {PellFund (D)}^{x}) \to A \in Pell14QR (D)$
13	12	r19.29an	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land \exists x \in ℤ A = {PellFund (D)}^{x}) \to A \in Pell14QR (D)$
14	1 13	impbida	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell14QR (D) \leftrightarrow \exists x \in ℤ A = {PellFund (D)}^{x})$