Step | Hyp | Ref
| Expression |
1 | | elpell1234qr 41203 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ (๐ด โ (Pell1234QRโ๐ท) โ (๐ด โ โ โง โ๐ โ โค โ๐ โ โค (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
2 | | simprl 770 |
. . . . . . 7
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ด = (๐ + ((โโ๐ท) ยท ๐))) |
3 | | ax-1ne0 11127 |
. . . . . . . . 9
โข 1 โ
0 |
4 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ท โ (โ โ
โปNN) โ ๐ท โ โ) |
5 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โ ๐ท โ โ) |
6 | 5 | nncnd 12176 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โ ๐ท โ โ) |
7 | 6 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ๐ท โ โ) |
8 | 7 | sqrtcld 15329 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ (โโ๐ท) โ
โ) |
9 | | zcn 12511 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ ๐ โ
โ) |
10 | 9 | ad2antll 728 |
. . . . . . . . . . . . . . . . 17
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
11 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ๐ โ โ) |
12 | 8, 11 | sqmuld 14070 |
. . . . . . . . . . . . . . 15
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ (((โโ๐ท) ยท ๐)โ2) = (((โโ๐ท)โ2) ยท (๐โ2))) |
13 | 7 | sqsqrtd 15331 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ((โโ๐ท)โ2) = ๐ท) |
14 | 13 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ (((โโ๐ท)โ2) ยท (๐โ2)) = (๐ท ยท (๐โ2))) |
15 | 12, 14 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ (๐ท ยท (๐โ2)) = (((โโ๐ท) ยท ๐)โ2)) |
16 | 15 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ((๐โ2) โ (๐ท ยท (๐โ2))) = ((๐โ2) โ (((โโ๐ท) ยท ๐)โ2))) |
17 | | zcn 12511 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ ๐ โ
โ) |
18 | 17 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ๐ โ โ) |
20 | 8, 11 | mulcld 11182 |
. . . . . . . . . . . . . 14
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ((โโ๐ท) ยท ๐) โ โ) |
21 | | subsq 14121 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง
((โโ๐ท) ยท
๐) โ โ) โ
((๐โ2) โ
(((โโ๐ท)
ยท ๐)โ2)) =
((๐ + ((โโ๐ท) ยท ๐)) ยท (๐ โ ((โโ๐ท) ยท ๐)))) |
22 | 19, 20, 21 | syl2anc 585 |
. . . . . . . . . . . . 13
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ((๐โ2) โ (((โโ๐ท) ยท ๐)โ2)) = ((๐ + ((โโ๐ท) ยท ๐)) ยท (๐ โ ((โโ๐ท) ยท ๐)))) |
23 | 16, 22 | eqtrd 2777 |
. . . . . . . . . . . 12
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ((๐โ2) โ (๐ท ยท (๐โ2))) = ((๐ + ((โโ๐ท) ยท ๐)) ยท (๐ โ ((โโ๐ท) ยท ๐)))) |
24 | | simplr 768 |
. . . . . . . . . . . 12
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) |
25 | | simpr 486 |
. . . . . . . . . . . . . 14
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ (๐ + ((โโ๐ท) ยท ๐)) = 0) |
26 | 25 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ((๐ + ((โโ๐ท) ยท ๐)) ยท (๐ โ ((โโ๐ท) ยท ๐))) = (0 ยท (๐ โ ((โโ๐ท) ยท ๐)))) |
27 | 19, 20 | subcld 11519 |
. . . . . . . . . . . . . 14
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ (๐ โ ((โโ๐ท) ยท ๐)) โ โ) |
28 | 27 | mul02d 11360 |
. . . . . . . . . . . . 13
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ (0 ยท (๐ โ ((โโ๐ท) ยท ๐))) = 0) |
29 | 26, 28 | eqtrd 2777 |
. . . . . . . . . . . 12
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ ((๐ + ((โโ๐ท) ยท ๐)) ยท (๐ โ ((โโ๐ท) ยท ๐))) = 0) |
30 | 23, 24, 29 | 3eqtr3d 2785 |
. . . . . . . . . . 11
โข
(((((๐ท โ
(โ โ โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โง (๐ + ((โโ๐ท) ยท ๐)) = 0) โ 1 = 0) |
31 | 30 | ex 414 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ((๐ + ((โโ๐ท) ยท ๐)) = 0 โ 1 = 0)) |
32 | 31 | necon3d 2965 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ (1 โ 0 โ
(๐ + ((โโ๐ท) ยท ๐)) โ 0)) |
33 | 3, 32 | mpi 20 |
. . . . . . . 8
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ (๐ + ((โโ๐ท) ยท ๐)) โ 0) |
34 | 33 | adantrl 715 |
. . . . . . 7
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ + ((โโ๐ท) ยท ๐)) โ 0) |
35 | 2, 34 | eqnetrd 3012 |
. . . . . 6
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ด โ 0) |
36 | 35 | ex 414 |
. . . . 5
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ๐ด โ 0)) |
37 | 36 | rexlimdvva 3206 |
. . . 4
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ) โ (โ๐ โ โค โ๐ โ โค (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ๐ด โ 0)) |
38 | 37 | expimpd 455 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ ((๐ด โ โ โง โ๐ โ โค โ๐ โ โค (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ด โ 0)) |
39 | 1, 38 | sylbid 239 |
. 2
โข (๐ท โ (โ โ
โปNN) โ (๐ด โ (Pell1234QRโ๐ท) โ ๐ด โ 0)) |
40 | 39 | imp 408 |
1
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ ๐ด โ 0) |