Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) โ ๐ท โ (โ โ
โปNN)) |
2 | | simprll 778 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) โ ๐ด โ (Pell1234QRโ๐ท)) |
3 | | simprrl 780 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) โ ๐ต โ (Pell1234QRโ๐ท)) |
4 | | pell1234qrmulcl 41221 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท) โง ๐ต โ (Pell1234QRโ๐ท)) โ (๐ด ยท ๐ต) โ (Pell1234QRโ๐ท)) |
5 | 1, 2, 3, 4 | syl3anc 1372 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) โ (๐ด ยท ๐ต) โ (Pell1234QRโ๐ท)) |
6 | | pell1234qrre 41218 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ ๐ด โ โ) |
7 | 2, 6 | syldan 592 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) โ ๐ด โ โ) |
8 | | pell1234qrre 41218 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง ๐ต โ (Pell1234QRโ๐ท)) โ ๐ต โ โ) |
9 | 3, 8 | syldan 592 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) โ ๐ต โ โ) |
10 | | simprlr 779 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) โ 0 < ๐ด) |
11 | | simprrr 781 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) โ 0 < ๐ต) |
12 | 7, 9, 10, 11 | mulgt0d 11315 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) โ 0 < (๐ด ยท ๐ต)) |
13 | 5, 12 | jca 513 |
. . . 4
โข ((๐ท โ (โ โ
โปNN) โง ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) โ ((๐ด ยท ๐ต) โ (Pell1234QRโ๐ท) โง 0 < (๐ด ยท ๐ต))) |
14 | 13 | ex 414 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ (((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต)) โ ((๐ด ยท ๐ต) โ (Pell1234QRโ๐ท) โง 0 < (๐ด ยท ๐ต)))) |
15 | | elpell14qr2 41228 |
. . . 4
โข (๐ท โ (โ โ
โปNN) โ (๐ด โ (Pell14QRโ๐ท) โ (๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด))) |
16 | | elpell14qr2 41228 |
. . . 4
โข (๐ท โ (โ โ
โปNN) โ (๐ต โ (Pell14QRโ๐ท) โ (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต))) |
17 | 15, 16 | anbi12d 632 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ ((๐ด โ (Pell14QRโ๐ท) โง ๐ต โ (Pell14QRโ๐ท)) โ ((๐ด โ (Pell1234QRโ๐ท) โง 0 < ๐ด) โง (๐ต โ (Pell1234QRโ๐ท) โง 0 < ๐ต)))) |
18 | | elpell14qr2 41228 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ ((๐ด ยท ๐ต) โ (Pell14QRโ๐ท) โ ((๐ด ยท ๐ต) โ (Pell1234QRโ๐ท) โง 0 < (๐ด ยท ๐ต)))) |
19 | 14, 17, 18 | 3imtr4d 294 |
. 2
โข (๐ท โ (โ โ
โปNN) โ ((๐ด โ (Pell14QRโ๐ท) โง ๐ต โ (Pell14QRโ๐ท)) โ (๐ด ยท ๐ต) โ (Pell14QRโ๐ท))) |
20 | 19 | 3impib 1117 |
1
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท) โง ๐ต โ (Pell14QRโ๐ท)) โ (๐ด ยท ๐ต) โ (Pell14QRโ๐ท)) |