Theorem pell1234qrre

Description: General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014)

	Ref	Expression
Assertion	pell1234qrre	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in \mathrm{Pell1234QR}\left(D\right)\right)\to A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		elpell1234qr	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left(A\in \mathrm{Pell1234QR}\left(D\right)\leftrightarrow \left(A\in ℝ\wedge \exists a\in \mathbb{Z}\exists b\in \mathbb{Z}\left(A=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)\right)\right)$$
2	1	simprbda	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in \mathrm{Pell1234QR}\left(D\right)\right)\to A\in ℝ$$