Theorem pellqrexplicit

Description: Condition for a calculated real to be a Pell solution. (Contributed by Stefan O'Rear, 19-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
2	1	3ad2ant2	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to A\in ℝ$$
3		eldifi	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to D\in \mathbb{N}$$
4	3	3ad2ant1	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to D\in \mathbb{N}$$
5	4	nnrpd	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to D\in {ℝ}^{+}$$
6	5	rpsqrtcld	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \sqrt{D}\in {ℝ}^{+}$$
7	6	rpred	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \sqrt{D}\in ℝ$$
8		nn0re	$$⊢B\in {\mathbb{N}}_0\to B\in ℝ$$
9	8	3ad2ant3	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to B\in ℝ$$
10	7 9	remulcld	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \sqrt{D}B\in ℝ$$
11	2 10	readdcld	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to A+\sqrt{D}B\in ℝ$$
12	11	adantr	$$⊢\left(\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge A^2-D{B}^2=1\right)\to A+\sqrt{D}B\in ℝ$$
13		simpl2	$$⊢\left(\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge A^2-D{B}^2=1\right)\to A\in {\mathbb{N}}_0$$
14		simpl3	$$⊢\left(\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge A^2-D{B}^2=1\right)\to B\in {\mathbb{N}}_0$$
15		eqidd	$$⊢\left(\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge A^2-D{B}^2=1\right)\to A+\sqrt{D}B=A+\sqrt{D}B$$
16		simpr	$$⊢\left(\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge A^2-D{B}^2=1\right)\to A^2-D{B}^2=1$$
17		oveq1	$$⊢a=A\to a+\sqrt{D}b=A+\sqrt{D}b$$
18	17	eqeq2d	$$⊢a=A\to \left(A+\sqrt{D}B=a+\sqrt{D}b\leftrightarrow A+\sqrt{D}B=A+\sqrt{D}b\right)$$
19		oveq1	$$⊢a=A\to a^2=A^2$$
20	19	oveq1d	$$⊢a=A\to a^2-D{b}^2=A^2-D{b}^2$$
21	20	eqeq1d	$$⊢a=A\to \left(a^2-D{b}^2=1\leftrightarrow A^2-D{b}^2=1\right)$$
22	18 21	anbi12d	$$⊢a=A\to \left(\left(A+\sqrt{D}B=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)\leftrightarrow \left(A+\sqrt{D}B=A+\sqrt{D}b\wedge A^2-D{b}^2=1\right)\right)$$
23		oveq2	$$⊢b=B\to \sqrt{D}b=\sqrt{D}B$$
24	23	oveq2d	$$⊢b=B\to A+\sqrt{D}b=A+\sqrt{D}B$$
25	24	eqeq2d	$$⊢b=B\to \left(A+\sqrt{D}B=A+\sqrt{D}b\leftrightarrow A+\sqrt{D}B=A+\sqrt{D}B\right)$$
26		oveq1	$$⊢b=B\to b^2=B^2$$
27	26	oveq2d	$$⊢b=B\to D{b}^2=D{B}^2$$
28	27	oveq2d	$$⊢b=B\to A^2-D{b}^2=A^2-D{B}^2$$
29	28	eqeq1d	$$⊢b=B\to \left(A^2-D{b}^2=1\leftrightarrow A^2-D{B}^2=1\right)$$
30	25 29	anbi12d	$$⊢b=B\to \left(\left(A+\sqrt{D}B=A+\sqrt{D}b\wedge A^2-D{b}^2=1\right)\leftrightarrow \left(A+\sqrt{D}B=A+\sqrt{D}B\wedge A^2-D{B}^2=1\right)\right)$$
31	22 30	rspc2ev	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge \left(A+\sqrt{D}B=A+\sqrt{D}B\wedge A^2-D{B}^2=1\right)\right)\to \exists a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(A+\sqrt{D}B=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)$$
32	13 14 15 16 31	syl112anc	$$⊢\left(\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge A^2-D{B}^2=1\right)\to \exists a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(A+\sqrt{D}B=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)$$
33		elpell1qr	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left(A+\sqrt{D}B\in \mathrm{Pell1QR}\left(D\right)\leftrightarrow \left(A+\sqrt{D}B\in ℝ\wedge \exists a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(A+\sqrt{D}B=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)\right)\right)$$
34	33	3ad2ant1	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A+\sqrt{D}B\in \mathrm{Pell1QR}\left(D\right)\leftrightarrow \left(A+\sqrt{D}B\in ℝ\wedge \exists a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(A+\sqrt{D}B=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)\right)\right)$$
35	34	adantr	$$⊢\left(\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge A^2-D{B}^2=1\right)\to \left(A+\sqrt{D}B\in \mathrm{Pell1QR}\left(D\right)\leftrightarrow \left(A+\sqrt{D}B\in ℝ\wedge \exists a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(A+\sqrt{D}B=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)\right)\right)$$
36	12 32 35	mpbir2and	$$⊢\left(\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge A^2-D{B}^2=1\right)\to A+\sqrt{D}B\in \mathrm{Pell1QR}\left(D\right)$$