# 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 \left(ℕ\setminus {◻}_{ℕ}\right)\to \left({A}\in \mathrm{Pell14QR}\left({D}\right)↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={\mathrm{PellFund}\left({D}\right)}^{{x}}\right)$

### Proof

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