Theorem pell1qr1

Description: 1 is a Pell solution and in the first quadrant as one. (Contributed by Stefan O'Rear, 17-Sep-2014)

	Ref	Expression
Assertion	pell1qr1	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1\in \mathrm{Pell1QR}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		1red	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1\in ℝ$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3	2	a1i	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1\in {\mathbb{N}}_0$$
4		0nn0	$$⊢0\in {\mathbb{N}}_0$$
5	4	a1i	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 0\in {\mathbb{N}}_0$$
6		eldifi	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to D\in \mathbb{N}$$
7	6	nncnd	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to D\in ℂ$$
8	7	sqrtcld	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \sqrt{D}\in ℂ$$
9	8	mul01d	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \sqrt{D}\cdot 0=0$$
10	9	oveq2d	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1+\sqrt{D}\cdot 0=1+0$$
11		1p0e1	$$⊢1+0=1$$
12	10 11	eqtr2di	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1=1+\sqrt{D}\cdot 0$$
13		sq1	$$⊢1^2=1$$
14	13	a1i	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1^2=1$$
15		sq0	$$⊢0^2=0$$
16	15	oveq2i	$$⊢D{0}^2=D\cdot 0$$
17	7	mul01d	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to D\cdot 0=0$$
18	16 17	syl5eq	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to D{0}^2=0$$
19	14 18	oveq12d	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1^2-D{0}^2=1-0$$
20		1m0e1	$$⊢1-0=1$$
21	19 20	eqtrdi	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1^2-D{0}^2=1$$
22		oveq1	$$⊢a=1\to a+\sqrt{D}b=1+\sqrt{D}b$$
23	22	eqeq2d	$$⊢a=1\to \left(1=a+\sqrt{D}b\leftrightarrow 1=1+\sqrt{D}b\right)$$
24		oveq1	$$⊢a=1\to a^2=1^2$$
25	24	oveq1d	$$⊢a=1\to a^2-D{b}^2=1^2-D{b}^2$$
26	25	eqeq1d	$$⊢a=1\to \left(a^2-D{b}^2=1\leftrightarrow 1^2-D{b}^2=1\right)$$
27	23 26	anbi12d	$$⊢a=1\to \left(\left(1=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)\leftrightarrow \left(1=1+\sqrt{D}b\wedge 1^2-D{b}^2=1\right)\right)$$
28		oveq2	$$⊢b=0\to \sqrt{D}b=\sqrt{D}\cdot 0$$
29	28	oveq2d	$$⊢b=0\to 1+\sqrt{D}b=1+\sqrt{D}\cdot 0$$
30	29	eqeq2d	$$⊢b=0\to \left(1=1+\sqrt{D}b\leftrightarrow 1=1+\sqrt{D}\cdot 0\right)$$
31		oveq1	$$⊢b=0\to b^2=0^2$$
32	31	oveq2d	$$⊢b=0\to D{b}^2=D{0}^2$$
33	32	oveq2d	$$⊢b=0\to 1^2-D{b}^2=1^2-D{0}^2$$
34	33	eqeq1d	$$⊢b=0\to \left(1^2-D{b}^2=1\leftrightarrow 1^2-D{0}^2=1\right)$$
35	30 34	anbi12d	$$⊢b=0\to \left(\left(1=1+\sqrt{D}b\wedge 1^2-D{b}^2=1\right)\leftrightarrow \left(1=1+\sqrt{D}\cdot 0\wedge 1^2-D{0}^2=1\right)\right)$$
36	27 35	rspc2ev	$$⊢\left(1\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\wedge \left(1=1+\sqrt{D}\cdot 0\wedge 1^2-D{0}^2=1\right)\right)\to \exists a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(1=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)$$
37	3 5 12 21 36	syl112anc	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \exists a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(1=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)$$
38		elpell1qr	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left(1\in \mathrm{Pell1QR}\left(D\right)\leftrightarrow \left(1\in ℝ\wedge \exists a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(1=a+\sqrt{D}b\wedge a^2-D{b}^2=1\right)\right)\right)$$
39	1 37 38	mpbir2and	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1\in \mathrm{Pell1QR}\left(D\right)$$