# 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 ( 𝐷 ∈ ( ℕ ∖ ◻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 ‘ 𝐷 ) ↑ 𝑥 ) ) )