Step | Hyp | Ref
| Expression |
1 | | elpell14qr 37413 |
. . 3
◻NN Pell14QR
|
2 | | 0cnd 10033 |
. . . . . . . . . . . . . 14
◻NN
|
3 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . 19
◻NN
|
4 | 3 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
◻NN
|
5 | 4 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
◻NN
|
6 | 4 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . 18
◻NN
|
7 | 6 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . 17
◻NN
|
8 | 5, 7 | resqrtcld 14156 |
. . . . . . . . . . . . . . . 16
◻NN
|
9 | | zre 11381 |
. . . . . . . . . . . . . . . . . 18
|
10 | 9 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
11 | 10 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
◻NN
|
12 | 8, 11 | remulcld 10070 |
. . . . . . . . . . . . . . 15
◻NN
|
13 | 12 | recnd 10068 |
. . . . . . . . . . . . . 14
◻NN
|
14 | 2, 13 | abssubd 14192 |
. . . . . . . . . . . . 13
◻NN
|
15 | 13 | subid1d 10381 |
. . . . . . . . . . . . . 14
◻NN
|
16 | 15 | fveq2d 6195 |
. . . . . . . . . . . . 13
◻NN
|
17 | 14, 16 | eqtrd 2656 |
. . . . . . . . . . . 12
◻NN
|
18 | | absresq 14042 |
. . . . . . . . . . . . . . . 16
|
19 | 12, 18 | syl 17 |
. . . . . . . . . . . . . . 15
◻NN
|
20 | 5 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
◻NN
|
21 | 20 | sqrtcld 14176 |
. . . . . . . . . . . . . . . 16
◻NN
|
22 | 10 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
23 | 22 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
◻NN
|
24 | 21, 23 | sqmuld 13020 |
. . . . . . . . . . . . . . 15
◻NN
|
25 | 20 | sqsqrtd 14178 |
. . . . . . . . . . . . . . . 16
◻NN
|
26 | 25 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
◻NN
|
27 | 19, 24, 26 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
◻NN
|
28 | | 0lt1 10550 |
. . . . . . . . . . . . . . . 16
|
29 | | simpr 477 |
. . . . . . . . . . . . . . . 16
◻NN
|
30 | 28, 29 | syl5breqr 4691 |
. . . . . . . . . . . . . . 15
◻NN
|
31 | 11 | resqcld 13035 |
. . . . . . . . . . . . . . . . 17
◻NN
|
32 | 5, 31 | remulcld 10070 |
. . . . . . . . . . . . . . . 16
◻NN
|
33 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . 19
|
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
35 | 34 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
◻NN
|
36 | 35 | resqcld 13035 |
. . . . . . . . . . . . . . . 16
◻NN
|
37 | 32, 36 | posdifd 10614 |
. . . . . . . . . . . . . . 15
◻NN
|
38 | 30, 37 | mpbird 247 |
. . . . . . . . . . . . . 14
◻NN
|
39 | 27, 38 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
◻NN
|
40 | 13 | abscld 14175 |
. . . . . . . . . . . . . 14
◻NN
|
41 | 13 | absge0d 14183 |
. . . . . . . . . . . . . 14
◻NN
|
42 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . 16
|
43 | 42 | adantr 481 |
. . . . . . . . . . . . . . 15
|
44 | 43 | ad2antlr 763 |
. . . . . . . . . . . . . 14
◻NN
|
45 | 40, 35, 41, 44 | lt2sqd 13043 |
. . . . . . . . . . . . 13
◻NN
|
46 | 39, 45 | mpbird 247 |
. . . . . . . . . . . 12
◻NN
|
47 | 17, 46 | eqbrtrd 4675 |
. . . . . . . . . . 11
◻NN
|
48 | | 0red 10041 |
. . . . . . . . . . . 12
◻NN
|
49 | 48, 12, 35 | absdifltd 14172 |
. . . . . . . . . . 11
◻NN
|
50 | 47, 49 | mpbid 222 |
. . . . . . . . . 10
◻NN
|
51 | 50 | simprd 479 |
. . . . . . . . 9
◻NN
|
52 | | nn0cn 11302 |
. . . . . . . . . . . 12
|
53 | 52 | adantr 481 |
. . . . . . . . . . 11
|
54 | 53 | ad2antlr 763 |
. . . . . . . . . 10
◻NN
|
55 | 54, 13 | addcomd 10238 |
. . . . . . . . 9
◻NN
|
56 | 51, 55 | breqtrrd 4681 |
. . . . . . . 8
◻NN
|
57 | 56 | adantrl 752 |
. . . . . . 7
◻NN
|
58 | | simprl 794 |
. . . . . . 7
◻NN
|
59 | 57, 58 | breqtrrd 4681 |
. . . . . 6
◻NN
|
60 | 59 | ex 450 |
. . . . 5
◻NN
|
61 | 60 | rexlimdvva 3038 |
. . . 4
◻NN |
62 | 61 | expimpd 629 |
. . 3
◻NN
|
63 | 1, 62 | sylbid 230 |
. 2
◻NN Pell14QR |
64 | 63 | imp 445 |
1
◻NN Pell14QR
|