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 ∈ ℕ ∖ ◻ ℕ → A ∈ Pell14QR ⁡ D ↔ ∃ x ∈ ℤ A = PellFund ⁡ D x

Proof

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