Step | Hyp | Ref
| Expression |
1 | | elpell1qr 41199 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ (๐ด โ (Pell1QRโ๐ท) โ (๐ด โ โ โง โ๐ โ โ0
โ๐ โ
โ0 (๐ด =
(๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
2 | | 1red 11163 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 1 โ
โ) |
3 | | simplrl 776 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ ๐ โ
โ0) |
4 | 3 | nn0red 12481 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ ๐ โ
โ) |
5 | | eldifi 4091 |
. . . . . . . . . . . . . . 15
โข (๐ท โ (โ โ
โปNN) โ ๐ท โ โ) |
6 | 5 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ ๐ท โ
โ) |
7 | 6 | nnnn0d 12480 |
. . . . . . . . . . . . 13
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ ๐ท โ
โ0) |
8 | 7 | nn0red 12481 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ ๐ท โ
โ) |
9 | 7 | nn0ge0d 12483 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 0 โค
๐ท) |
10 | 8, 9 | resqrtcld 15309 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ
(โโ๐ท) โ
โ) |
11 | | simplrr 777 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ ๐ โ
โ0) |
12 | 11 | nn0red 12481 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ ๐ โ
โ) |
13 | 10, 12 | remulcld 11192 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ
((โโ๐ท) ยท
๐) โ
โ) |
14 | 4, 13 | readdcld 11191 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ (๐ + ((โโ๐ท) ยท ๐)) โ โ) |
15 | | 2nn0 12437 |
. . . . . . . . . . . . . . . 16
โข 2 โ
โ0 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 2 โ
โ0) |
17 | 11, 16 | nn0expcld 14156 |
. . . . . . . . . . . . . 14
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ (๐โ2) โ
โ0) |
18 | 7, 17 | nn0mulcld 12485 |
. . . . . . . . . . . . 13
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ (๐ท ยท (๐โ2)) โ
โ0) |
19 | 18 | nn0ge0d 12483 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 0 โค
(๐ท ยท (๐โ2))) |
20 | 18 | nn0red 12481 |
. . . . . . . . . . . . 13
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ (๐ท ยท (๐โ2)) โ โ) |
21 | 2, 20 | addge02d 11751 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ (0 โค
(๐ท ยท (๐โ2)) โ 1 โค ((๐ท ยท (๐โ2)) + 1))) |
22 | 19, 21 | mpbid 231 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 1 โค
((๐ท ยท (๐โ2)) + 1)) |
23 | | sq1 14106 |
. . . . . . . . . . . 12
โข
(1โ2) = 1 |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ
(1โ2) = 1) |
25 | | nn0cn 12430 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ ๐ โ
โ) |
26 | 25 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ ๐ โ
โ) |
27 | 26 | sqcld 14056 |
. . . . . . . . . . . . . 14
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ (๐โ2) โ
โ) |
28 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ ๐ท โ
โ) |
29 | 28 | nncnd 12176 |
. . . . . . . . . . . . . . 15
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ ๐ท โ
โ) |
30 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ ๐ โ
โ) |
31 | 30 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ ๐ โ
โ) |
32 | 31 | sqcld 14056 |
. . . . . . . . . . . . . . 15
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ (๐โ2) โ
โ) |
33 | 29, 32 | mulcld 11182 |
. . . . . . . . . . . . . 14
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ (๐ท ยท (๐โ2)) โ
โ) |
34 | | 1cnd 11157 |
. . . . . . . . . . . . . 14
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ 1 โ โ) |
35 | 27, 33, 34 | subaddd 11537 |
. . . . . . . . . . . . 13
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ (((๐โ2) โ
(๐ท ยท (๐โ2))) = 1 โ ((๐ท ยท (๐โ2)) + 1) = (๐โ2))) |
36 | 35 | biimpa 478 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ ((๐ท ยท (๐โ2)) + 1) = (๐โ2)) |
37 | 36 | eqcomd 2743 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ (๐โ2) = ((๐ท ยท (๐โ2)) + 1)) |
38 | 22, 24, 37 | 3brtr4d 5142 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ
(1โ2) โค (๐โ2)) |
39 | | 0le1 11685 |
. . . . . . . . . . . 12
โข 0 โค
1 |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 0 โค
1) |
41 | 3 | nn0ge0d 12483 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 0 โค
๐) |
42 | 2, 4, 40, 41 | le2sqd 14167 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ (1 โค
๐ โ (1โ2) โค
(๐โ2))) |
43 | 38, 42 | mpbird 257 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 1 โค
๐) |
44 | 8, 9 | sqrtge0d 15312 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 0 โค
(โโ๐ท)) |
45 | 11 | nn0ge0d 12483 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 0 โค
๐) |
46 | 10, 12, 44, 45 | mulge0d 11739 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 0 โค
((โโ๐ท) ยท
๐)) |
47 | 4, 13 | addge01d 11750 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ (0 โค
((โโ๐ท) ยท
๐) โ ๐ โค (๐ + ((โโ๐ท) ยท ๐)))) |
48 | 46, 47 | mpbid 231 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ ๐ โค (๐ + ((โโ๐ท) ยท ๐))) |
49 | 2, 4, 14, 43, 48 | letrd 11319 |
. . . . . . . 8
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ 1 โค
(๐ + ((โโ๐ท) ยท ๐))) |
50 | 49 | adantrl 715 |
. . . . . . 7
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ 1 โค (๐ + ((โโ๐ท) ยท ๐))) |
51 | | simprl 770 |
. . . . . . 7
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ด = (๐ + ((โโ๐ท) ยท ๐))) |
52 | 50, 51 | breqtrrd 5138 |
. . . . . 6
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ 1 โค ๐ด) |
53 | 52 | ex 414 |
. . . . 5
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ ((๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ 1 โค ๐ด)) |
54 | 53 | rexlimdvva 3206 |
. . . 4
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โ (โ๐ โ โ0
โ๐ โ
โ0 (๐ด =
(๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ 1 โค ๐ด)) |
55 | 54 | expimpd 455 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ ((๐ด โ โ โง โ๐ โ โ0
โ๐ โ
โ0 (๐ด =
(๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ 1 โค ๐ด)) |
56 | 1, 55 | sylbid 239 |
. 2
โข (๐ท โ (โ โ
โปNN) โ (๐ด โ (Pell1QRโ๐ท) โ 1 โค ๐ด)) |
57 | 56 | imp 408 |
1
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1QRโ๐ท)) โ 1 โค ๐ด) |