Step | Hyp | Ref
| Expression |
1 | | elpell1qr 41217 |
. . . . . 6
โข (๐ท โ (โ โ
โปNN) โ (๐ด โ (Pell1QRโ๐ท) โ (๐ด โ โ โง โ๐ โ โ0
โ๐ โ
โ0 (๐ด =
(๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
2 | 1 | adantr 482 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง 1 < ๐ด) โ (๐ด โ (Pell1QRโ๐ท) โ (๐ด โ โ โง โ๐ โ โ0
โ๐ โ
โ0 (๐ด =
(๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
3 | | eldifi 4090 |
. . . . . . . . . . 11
โข (๐ท โ (โ โ
โปNN) โ ๐ท โ โ) |
4 | 3 | ad4antr 731 |
. . . . . . . . . 10
โข
(((((๐ท โ
(โ โ โปNN) โง 1 < ๐ด) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ท โ โ) |
5 | | simplr 768 |
. . . . . . . . . 10
โข
(((((๐ท โ
(โ โ โปNN) โง 1 < ๐ด) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ โ โ0 โง ๐ โ
โ0)) |
6 | | simp-4r 783 |
. . . . . . . . . . 11
โข
(((((๐ท โ
(โ โ โปNN) โง 1 < ๐ด) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ 1 < ๐ด) |
7 | | simprl 770 |
. . . . . . . . . . 11
โข
(((((๐ท โ
(โ โ โปNN) โง 1 < ๐ด) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ด = (๐ + ((โโ๐ท) ยท ๐))) |
8 | 6, 7 | breqtrd 5135 |
. . . . . . . . . 10
โข
(((((๐ท โ
(โ โ โปNN) โง 1 < ๐ด) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ 1 < (๐ + ((โโ๐ท) ยท ๐))) |
9 | | simprr 772 |
. . . . . . . . . 10
โข
(((((๐ท โ
(โ โ โปNN) โง 1 < ๐ด) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) |
10 | | pell1qrgaplem 41243 |
. . . . . . . . . 10
โข (((๐ท โ โ โง (๐ โ โ0
โง ๐ โ
โ0)) โง (1 < (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ
((โโ(๐ท + 1)) +
(โโ๐ท)) โค
(๐ + ((โโ๐ท) ยท ๐))) |
11 | 4, 5, 8, 9, 10 | syl22anc 838 |
. . . . . . . . 9
โข
(((((๐ท โ
(โ โ โปNN) โง 1 < ๐ด) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ
((โโ(๐ท + 1)) +
(โโ๐ท)) โค
(๐ + ((โโ๐ท) ยท ๐))) |
12 | 11, 7 | breqtrrd 5137 |
. . . . . . . 8
โข
(((((๐ท โ
(โ โ โปNN) โง 1 < ๐ด) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ
((โโ(๐ท + 1)) +
(โโ๐ท)) โค
๐ด) |
13 | 12 | ex 414 |
. . . . . . 7
โข ((((๐ท โ (โ โ
โปNN) โง 1 < ๐ด) โง ๐ด โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ ((๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ((โโ(๐ท + 1)) + (โโ๐ท)) โค ๐ด)) |
14 | 13 | rexlimdvva 3202 |
. . . . . 6
โข (((๐ท โ (โ โ
โปNN) โง 1 < ๐ด) โง ๐ด โ โ) โ (โ๐ โ โ0
โ๐ โ
โ0 (๐ด =
(๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ((โโ(๐ท + 1)) + (โโ๐ท)) โค ๐ด)) |
15 | 14 | expimpd 455 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง 1 < ๐ด) โ ((๐ด โ โ โง โ๐ โ โ0
โ๐ โ
โ0 (๐ด =
(๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ
((โโ(๐ท + 1)) +
(โโ๐ท)) โค
๐ด)) |
16 | 2, 15 | sylbid 239 |
. . . 4
โข ((๐ท โ (โ โ
โปNN) โง 1 < ๐ด) โ (๐ด โ (Pell1QRโ๐ท) โ ((โโ(๐ท + 1)) + (โโ๐ท)) โค ๐ด)) |
17 | 16 | ex 414 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ (1 < ๐ด โ (๐ด โ (Pell1QRโ๐ท) โ ((โโ(๐ท + 1)) + (โโ๐ท)) โค ๐ด))) |
18 | 17 | com23 86 |
. 2
โข (๐ท โ (โ โ
โปNN) โ (๐ด โ (Pell1QRโ๐ท) โ (1 < ๐ด โ ((โโ(๐ท + 1)) + (โโ๐ท)) โค ๐ด))) |
19 | 18 | 3imp 1112 |
1
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1QRโ๐ท) โง 1 < ๐ด) โ ((โโ(๐ท + 1)) + (โโ๐ท)) โค ๐ด) |