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	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ∃ 𝑥 ∈ ℤ 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pellfund14	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ∃ 𝑥 ∈ ℤ 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) )
2		simpll	⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑥 ∈ ℤ ) ∧ 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) )
3		pell1qrss14	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) )
4		pellfundex	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) )
5	3 4	sseldd	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell14QR ‘ 𝐷 ) )
6	5	ad2antrr	⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑥 ∈ ℤ ) ∧ 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell14QR ‘ 𝐷 ) )
7		simplr	⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑥 ∈ ℤ ) ∧ 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ) → 𝑥 ∈ ℤ )
8		pell14qrexpcl	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( PellFund ‘ 𝐷 ) ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝑥 ∈ ℤ ) → ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ∈ ( Pell14QR ‘ 𝐷 ) )
9	2 6 7 8	syl3anc	⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑥 ∈ ℤ ) ∧ 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ) → ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ∈ ( Pell14QR ‘ 𝐷 ) )
10		eleq1	⊢ ( 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
11	10	adantl	⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑥 ∈ ℤ ) ∧ 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
12	9 11	mpbird	⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑥 ∈ ℤ ) ∧ 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ) → 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) )
13	12	r19.29an	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ∃ 𝑥 ∈ ℤ 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ) → 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) )
14	1 13	impbida	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ∃ 𝑥 ∈ ℤ 𝐴 = ( ( PellFund ‘ 𝐷 ) ↑ 𝑥 ) ) )