Theorem elpell1qr

Description: Membership in a first-quadrant Pell solution set. (Contributed by Stefan O'Rear, 17-Sep-2014)

	Ref	Expression
Assertion	elpell1qr	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left(A\in \mathrm{Pell1QR}\left(D\right)\leftrightarrow \left(A\in ℝ\wedge \exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(A=z+\sqrt{D}w\wedge z^2-D{w}^2=1\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pell1qrval	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{Pell1QR}\left(D\right)=\left\{a\in ℝ|\exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(a=z+\sqrt{D}w\wedge z^2-D{w}^2=1\right)\right\}$$
2	1	eleq2d	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left(A\in \mathrm{Pell1QR}\left(D\right)\leftrightarrow A\in \left\{a\in ℝ|\exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(a=z+\sqrt{D}w\wedge z^2-D{w}^2=1\right)\right\}\right)$$
3		eqeq1	$$⊢a=A\to \left(a=z+\sqrt{D}w\leftrightarrow A=z+\sqrt{D}w\right)$$
4	3	anbi1d	$$⊢a=A\to \left(\left(a=z+\sqrt{D}w\wedge z^2-D{w}^2=1\right)\leftrightarrow \left(A=z+\sqrt{D}w\wedge z^2-D{w}^2=1\right)\right)$$
5	4	2rexbidv	$$⊢a=A\to \left(\exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(a=z+\sqrt{D}w\wedge z^2-D{w}^2=1\right)\leftrightarrow \exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(A=z+\sqrt{D}w\wedge z^2-D{w}^2=1\right)\right)$$
6	5	elrab	$$⊢A\in \left\{a\in ℝ|\exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(a=z+\sqrt{D}w\wedge z^2-D{w}^2=1\right)\right\}\leftrightarrow \left(A\in ℝ\wedge \exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(A=z+\sqrt{D}w\wedge z^2-D{w}^2=1\right)\right)$$
7	2 6	bitrdi	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left(A\in \mathrm{Pell1QR}\left(D\right)\leftrightarrow \left(A\in ℝ\wedge \exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(A=z+\sqrt{D}w\wedge z^2-D{w}^2=1\right)\right)\right)$$