Metamath Proof Explorer


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 1 Pell1QR D

Proof

Step Hyp Ref Expression
1 1red D 1
2 1nn0 1 0
3 2 a1i D 1 0
4 0nn0 0 0
5 4 a1i D 0 0
6 eldifi D D
7 6 nncnd D D
8 7 sqrtcld D D
9 8 mul01d D D 0 = 0
10 9 oveq2d D 1 + D 0 = 1 + 0
11 1p0e1 1 + 0 = 1
12 10 11 eqtr2di D 1 = 1 + D 0
13 sq1 1 2 = 1
14 13 a1i D 1 2 = 1
15 sq0 0 2 = 0
16 15 oveq2i D 0 2 = D 0
17 7 mul01d D D 0 = 0
18 16 17 syl5eq D D 0 2 = 0
19 14 18 oveq12d D 1 2 D 0 2 = 1 0
20 1m0e1 1 0 = 1
21 19 20 eqtrdi D 1 2 D 0 2 = 1
22 oveq1 a = 1 a + D b = 1 + D b
23 22 eqeq2d a = 1 1 = a + D b 1 = 1 + D b
24 oveq1 a = 1 a 2 = 1 2
25 24 oveq1d a = 1 a 2 D b 2 = 1 2 D b 2
26 25 eqeq1d a = 1 a 2 D b 2 = 1 1 2 D b 2 = 1
27 23 26 anbi12d a = 1 1 = a + D b a 2 D b 2 = 1 1 = 1 + D b 1 2 D b 2 = 1
28 oveq2 b = 0 D b = D 0
29 28 oveq2d b = 0 1 + D b = 1 + D 0
30 29 eqeq2d b = 0 1 = 1 + D b 1 = 1 + D 0
31 oveq1 b = 0 b 2 = 0 2
32 31 oveq2d b = 0 D b 2 = D 0 2
33 32 oveq2d b = 0 1 2 D b 2 = 1 2 D 0 2
34 33 eqeq1d b = 0 1 2 D b 2 = 1 1 2 D 0 2 = 1
35 30 34 anbi12d b = 0 1 = 1 + D b 1 2 D b 2 = 1 1 = 1 + D 0 1 2 D 0 2 = 1
36 27 35 rspc2ev 1 0 0 0 1 = 1 + D 0 1 2 D 0 2 = 1 a 0 b 0 1 = a + D b a 2 D b 2 = 1
37 3 5 12 21 36 syl112anc D a 0 b 0 1 = a + D b a 2 D b 2 = 1
38 elpell1qr D 1 Pell1QR D 1 a 0 b 0 1 = a + D b a 2 D b 2 = 1
39 1 37 38 mpbir2and D 1 Pell1QR D