Step | Hyp | Ref
| Expression |
1 | | eldifi 4091 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ ๐ท โ โ) |
2 | | eldifn 4092 |
. . . 4
โข (๐ท โ (โ โ
โปNN) โ ยฌ ๐ท โ
โปNN) |
3 | 1 | anim1i 616 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง (โโ๐ท) โ โ) โ (๐ท โ โ โง (โโ๐ท) โ
โ)) |
4 | | fveq2 6847 |
. . . . . . 7
โข (๐ = ๐ท โ (โโ๐) = (โโ๐ท)) |
5 | 4 | eleq1d 2823 |
. . . . . 6
โข (๐ = ๐ท โ ((โโ๐) โ โ โ (โโ๐ท) โ
โ)) |
6 | | df-squarenn 41193 |
. . . . . 6
โข
โปNN = {๐ โ โ โฃ (โโ๐) โ
โ} |
7 | 5, 6 | elrab2 3653 |
. . . . 5
โข (๐ท โ
โปNN โ (๐ท โ โ โง (โโ๐ท) โ
โ)) |
8 | 3, 7 | sylibr 233 |
. . . 4
โข ((๐ท โ (โ โ
โปNN) โง (โโ๐ท) โ โ) โ ๐ท โ
โปNN) |
9 | 2, 8 | mtand 815 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ ยฌ (โโ๐ท) โ โ) |
10 | | pellex 41187 |
. . 3
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ โ๐
โ โ โ๐
โ โ ((๐โ2)
โ (๐ท ยท (๐โ2))) = 1) |
11 | 1, 9, 10 | syl2anc 585 |
. 2
โข (๐ท โ (โ โ
โปNN) โ โ๐ โ โ โ๐ โ โ ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) |
12 | | simpll 766 |
. . . . . 6
โข (((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ๐ท โ (โ โ
โปNN)) |
13 | | nnnn0 12427 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ0) |
14 | 13 | adantr 482 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ0) |
15 | 14 | ad2antlr 726 |
. . . . . 6
โข (((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ๐ โ โ0) |
16 | | nnnn0 12427 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ0) |
17 | 16 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ0) |
18 | 17 | ad2antlr 726 |
. . . . . 6
โข (((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ๐ โ โ0) |
19 | | simpr 486 |
. . . . . 6
โข (((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) |
20 | | pellqrexplicit 41229 |
. . . . . 6
โข (((๐ท โ (โ โ
โปNN) โง ๐ โ โ0 โง ๐ โ โ0)
โง ((๐โ2) โ
(๐ท ยท (๐โ2))) = 1) โ (๐ + ((โโ๐ท) ยท ๐)) โ (Pell1QRโ๐ท)) |
21 | 12, 15, 18, 19, 20 | syl31anc 1374 |
. . . . 5
โข (((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ (๐ + ((โโ๐ท) ยท ๐)) โ (Pell1QRโ๐ท)) |
22 | | 1re 11162 |
. . . . . . . 8
โข 1 โ
โ |
23 | 22 | a1i 11 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ 1 โ
โ) |
24 | 22, 22 | readdcli 11177 |
. . . . . . . 8
โข (1 + 1)
โ โ |
25 | 24 | a1i 11 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ (1 + 1) โ
โ) |
26 | | nnre 12167 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
27 | 26 | ad2antrl 727 |
. . . . . . . 8
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
28 | 1 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ ๐ท โ โ) |
29 | 28 | nnrpd 12962 |
. . . . . . . . . . 11
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ ๐ท โ
โ+) |
30 | 29 | rpsqrtcld 15303 |
. . . . . . . . . 10
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ (โโ๐ท) โ
โ+) |
31 | 30 | rpred 12964 |
. . . . . . . . 9
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ (โโ๐ท) โ
โ) |
32 | | nnre 12167 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
33 | 32 | ad2antll 728 |
. . . . . . . . 9
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
34 | 31, 33 | remulcld 11192 |
. . . . . . . 8
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ
((โโ๐ท) ยท
๐) โ
โ) |
35 | 27, 34 | readdcld 11191 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ (๐ + ((โโ๐ท) ยท ๐)) โ โ) |
36 | 22 | ltp1i 12066 |
. . . . . . . 8
โข 1 < (1
+ 1) |
37 | 36 | a1i 11 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ 1 < (1 +
1)) |
38 | | nnge1 12188 |
. . . . . . . . 9
โข (๐ โ โ โ 1 โค
๐) |
39 | 38 | ad2antrl 727 |
. . . . . . . 8
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ 1 โค ๐) |
40 | | 1t1e1 12322 |
. . . . . . . . 9
โข (1
ยท 1) = 1 |
41 | | nnge1 12188 |
. . . . . . . . . . . . 13
โข (๐ท โ โ โ 1 โค
๐ท) |
42 | | sq1 14106 |
. . . . . . . . . . . . . 14
โข
(1โ2) = 1 |
43 | 42 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ท โ โ โ
(1โ2) = 1) |
44 | | nncn 12168 |
. . . . . . . . . . . . . 14
โข (๐ท โ โ โ ๐ท โ
โ) |
45 | 44 | sqsqrtd 15331 |
. . . . . . . . . . . . 13
โข (๐ท โ โ โ
((โโ๐ท)โ2)
= ๐ท) |
46 | 41, 43, 45 | 3brtr4d 5142 |
. . . . . . . . . . . 12
โข (๐ท โ โ โ
(1โ2) โค ((โโ๐ท)โ2)) |
47 | 22 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ท โ โ โ 1 โ
โ) |
48 | | nnrp 12933 |
. . . . . . . . . . . . . . 15
โข (๐ท โ โ โ ๐ท โ
โ+) |
49 | 48 | rpsqrtcld 15303 |
. . . . . . . . . . . . . 14
โข (๐ท โ โ โ
(โโ๐ท) โ
โ+) |
50 | 49 | rpred 12964 |
. . . . . . . . . . . . 13
โข (๐ท โ โ โ
(โโ๐ท) โ
โ) |
51 | | 0le1 11685 |
. . . . . . . . . . . . . 14
โข 0 โค
1 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ท โ โ โ 0 โค
1) |
53 | 49 | rpge0d 12968 |
. . . . . . . . . . . . 13
โข (๐ท โ โ โ 0 โค
(โโ๐ท)) |
54 | 47, 50, 52, 53 | le2sqd 14167 |
. . . . . . . . . . . 12
โข (๐ท โ โ โ (1 โค
(โโ๐ท) โ
(1โ2) โค ((โโ๐ท)โ2))) |
55 | 46, 54 | mpbird 257 |
. . . . . . . . . . 11
โข (๐ท โ โ โ 1 โค
(โโ๐ท)) |
56 | 28, 55 | syl 17 |
. . . . . . . . . 10
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ 1 โค
(โโ๐ท)) |
57 | | nnge1 12188 |
. . . . . . . . . . 11
โข (๐ โ โ โ 1 โค
๐) |
58 | 57 | ad2antll 728 |
. . . . . . . . . 10
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ 1 โค ๐) |
59 | 23, 51 | jctir 522 |
. . . . . . . . . . 11
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ (1 โ โ
โง 0 โค 1)) |
60 | | lemul12a 12020 |
. . . . . . . . . . 11
โข ((((1
โ โ โง 0 โค 1) โง (โโ๐ท) โ โ) โง ((1 โ โ
โง 0 โค 1) โง ๐
โ โ)) โ ((1 โค (โโ๐ท) โง 1 โค ๐) โ (1 ยท 1) โค
((โโ๐ท) ยท
๐))) |
61 | 59, 31, 59, 33, 60 | syl22anc 838 |
. . . . . . . . . 10
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ ((1 โค
(โโ๐ท) โง 1
โค ๐) โ (1 ยท
1) โค ((โโ๐ท)
ยท ๐))) |
62 | 56, 58, 61 | mp2and 698 |
. . . . . . . . 9
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ (1 ยท 1) โค
((โโ๐ท) ยท
๐)) |
63 | 40, 62 | eqbrtrrid 5146 |
. . . . . . . 8
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ 1 โค
((โโ๐ท) ยท
๐)) |
64 | 23, 23, 27, 34, 39, 63 | le2addd 11781 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ (1 + 1) โค (๐ + ((โโ๐ท) ยท ๐))) |
65 | 23, 25, 35, 37, 64 | ltletrd 11322 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ 1 < (๐ + ((โโ๐ท) ยท ๐))) |
66 | 65 | adantr 482 |
. . . . 5
โข (((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ 1 < (๐ + ((โโ๐ท) ยท ๐))) |
67 | | breq2 5114 |
. . . . . 6
โข (๐ฅ = (๐ + ((โโ๐ท) ยท ๐)) โ (1 < ๐ฅ โ 1 < (๐ + ((โโ๐ท) ยท ๐)))) |
68 | 67 | rspcev 3584 |
. . . . 5
โข (((๐ + ((โโ๐ท) ยท ๐)) โ (Pell1QRโ๐ท) โง 1 < (๐ + ((โโ๐ท) ยท ๐))) โ โ๐ฅ โ (Pell1QRโ๐ท)1 < ๐ฅ) |
69 | 21, 66, 68 | syl2anc 585 |
. . . 4
โข (((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ โ๐ฅ โ (Pell1QRโ๐ท)1 < ๐ฅ) |
70 | 69 | ex 414 |
. . 3
โข ((๐ท โ (โ โ
โปNN) โง (๐ โ โ โง ๐ โ โ)) โ (((๐โ2) โ (๐ท ยท (๐โ2))) = 1 โ โ๐ฅ โ (Pell1QRโ๐ท)1 < ๐ฅ)) |
71 | 70 | rexlimdvva 3206 |
. 2
โข (๐ท โ (โ โ
โปNN) โ (โ๐ โ โ โ๐ โ โ ((๐โ2) โ (๐ท ยท (๐โ2))) = 1 โ โ๐ฅ โ (Pell1QRโ๐ท)1 < ๐ฅ)) |
72 | 11, 71 | mpd 15 |
1
โข (๐ท โ (โ โ
โปNN) โ โ๐ฅ โ (Pell1QRโ๐ท)1 < ๐ฅ) |