Step | Hyp | Ref
| Expression |
1 | | elpell1234qr 41221 |
. . . 4
โข (๐ท โ (โ โ
โปNN) โ (๐ด โ (Pell1234QRโ๐ท) โ (๐ด โ โ โง โ๐ โ โค โ๐ โ โค (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
2 | 1 | biimpa 478 |
. . 3
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ (๐ด โ โ โง โ๐ โ โค โ๐ โ โค (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1))) |
3 | | pell1234qrre 41222 |
. . . . . . . . 9
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ ๐ด โ โ) |
4 | | pell1234qrne0 41223 |
. . . . . . . . 9
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ ๐ด โ 0) |
5 | 3, 4 | rereccld 11990 |
. . . . . . . 8
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ (1 / ๐ด) โ โ) |
6 | 5 | ad2antrr 725 |
. . . . . . 7
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (1 / ๐ด) โ
โ) |
7 | | simplrl 776 |
. . . . . . . 8
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ โ โค) |
8 | | simplrr 777 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ โ โค) |
9 | 8 | znegcld 12617 |
. . . . . . . 8
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ -๐ โ โค) |
10 | 5 | recnd 11191 |
. . . . . . . . . 10
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ (1 / ๐ด) โ โ) |
11 | 10 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (1 / ๐ด) โ
โ) |
12 | | zcn 12512 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
13 | 12 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
14 | 13 | ad2antlr 726 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ โ โ) |
15 | | eldifi 4090 |
. . . . . . . . . . . . . 14
โข (๐ท โ (โ โ
โปNN) โ ๐ท โ โ) |
16 | 15 | nncnd 12177 |
. . . . . . . . . . . . 13
โข (๐ท โ (โ โ
โปNN) โ ๐ท โ โ) |
17 | 16 | ad3antrrr 729 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ท โ โ) |
18 | 17 | sqrtcld 15331 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (โโ๐ท) โ
โ) |
19 | 8 | zcnd 12616 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ โ โ) |
20 | 19 | negcld 11507 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ -๐ โ โ) |
21 | 18, 20 | mulcld 11183 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((โโ๐ท) ยท -๐) โ โ) |
22 | 14, 21 | addcld 11182 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ + ((โโ๐ท) ยท -๐)) โ โ) |
23 | 3 | recnd 11191 |
. . . . . . . . . 10
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ ๐ด โ โ) |
24 | 23 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ด โ โ) |
25 | 4 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ด โ 0) |
26 | 18, 19 | sqmuld 14072 |
. . . . . . . . . . . . 13
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ
(((โโ๐ท)
ยท ๐)โ2) =
(((โโ๐ท)โ2)
ยท (๐โ2))) |
27 | 17 | sqsqrtd 15333 |
. . . . . . . . . . . . . 14
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((โโ๐ท)โ2) = ๐ท) |
28 | 27 | oveq1d 7376 |
. . . . . . . . . . . . 13
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ
(((โโ๐ท)โ2)
ยท (๐โ2)) =
(๐ท ยท (๐โ2))) |
29 | 26, 28 | eqtr2d 2774 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ท ยท (๐โ2)) = (((โโ๐ท) ยท ๐)โ2)) |
30 | 29 | oveq2d 7377 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((๐โ2) โ (๐ท ยท (๐โ2))) = ((๐โ2) โ (((โโ๐ท) ยท ๐)โ2))) |
31 | | simprr 772 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) |
32 | 18, 19 | mulcld 11183 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((โโ๐ท) ยท ๐) โ โ) |
33 | | subsq 14123 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
((โโ๐ท) ยท
๐) โ โ) โ
((๐โ2) โ
(((โโ๐ท)
ยท ๐)โ2)) =
((๐ + ((โโ๐ท) ยท ๐)) ยท (๐ โ ((โโ๐ท) ยท ๐)))) |
34 | 14, 32, 33 | syl2anc 585 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((๐โ2) โ (((โโ๐ท) ยท ๐)โ2)) = ((๐ + ((โโ๐ท) ยท ๐)) ยท (๐ โ ((โโ๐ท) ยท ๐)))) |
35 | 30, 31, 34 | 3eqtr3d 2781 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ 1 = ((๐ + ((โโ๐ท) ยท ๐)) ยท (๐ โ ((โโ๐ท) ยท ๐)))) |
36 | 24, 25 | recidd 11934 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ด ยท (1 / ๐ด)) = 1) |
37 | | simprl 770 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ๐ด = (๐ + ((โโ๐ท) ยท ๐))) |
38 | 18, 19 | mulneg2d 11617 |
. . . . . . . . . . . . 13
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((โโ๐ท) ยท -๐) = -((โโ๐ท) ยท ๐)) |
39 | 38 | oveq2d 7377 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ + ((โโ๐ท) ยท -๐)) = (๐ + -((โโ๐ท) ยท ๐))) |
40 | 14, 32 | negsubd 11526 |
. . . . . . . . . . . 12
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ + -((โโ๐ท) ยท ๐)) = (๐ โ ((โโ๐ท) ยท ๐))) |
41 | 39, 40 | eqtrd 2773 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ + ((โโ๐ท) ยท -๐)) = (๐ โ ((โโ๐ท) ยท ๐))) |
42 | 37, 41 | oveq12d 7379 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ด ยท (๐ + ((โโ๐ท) ยท -๐))) = ((๐ + ((โโ๐ท) ยท ๐)) ยท (๐ โ ((โโ๐ท) ยท ๐)))) |
43 | 35, 36, 42 | 3eqtr4d 2783 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ด ยท (1 / ๐ด)) = (๐ด ยท (๐ + ((โโ๐ท) ยท -๐)))) |
44 | 11, 22, 24, 25, 43 | mulcanad 11798 |
. . . . . . . 8
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (1 / ๐ด) = (๐ + ((โโ๐ท) ยท -๐))) |
45 | | sqneg 14030 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (-๐โ2) = (๐โ2)) |
46 | 19, 45 | syl 17 |
. . . . . . . . . . 11
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (-๐โ2) = (๐โ2)) |
47 | 46 | oveq2d 7377 |
. . . . . . . . . 10
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ (๐ท ยท (-๐โ2)) = (๐ท ยท (๐โ2))) |
48 | 47 | oveq2d 7377 |
. . . . . . . . 9
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((๐โ2) โ (๐ท ยท (-๐โ2))) = ((๐โ2) โ (๐ท ยท (๐โ2)))) |
49 | 48, 31 | eqtrd 2773 |
. . . . . . . 8
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((๐โ2) โ (๐ท ยท (-๐โ2))) = 1) |
50 | | oveq1 7368 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ + ((โโ๐ท) ยท ๐)) = (๐ + ((โโ๐ท) ยท ๐))) |
51 | 50 | eqeq2d 2744 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โ (1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)))) |
52 | | oveq1 7368 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐โ2) = (๐โ2)) |
53 | 52 | oveq1d 7376 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐โ2) โ (๐ท ยท (๐โ2))) = ((๐โ2) โ (๐ท ยท (๐โ2)))) |
54 | 53 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ = ๐ โ (((๐โ2) โ (๐ท ยท (๐โ2))) = 1 โ ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) |
55 | 51, 54 | anbi12d 632 |
. . . . . . . . 9
โข (๐ = ๐ โ (((1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ((1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1))) |
56 | | oveq2 7369 |
. . . . . . . . . . . 12
โข (๐ = -๐ โ ((โโ๐ท) ยท ๐) = ((โโ๐ท) ยท -๐)) |
57 | 56 | oveq2d 7377 |
. . . . . . . . . . 11
โข (๐ = -๐ โ (๐ + ((โโ๐ท) ยท ๐)) = (๐ + ((โโ๐ท) ยท -๐))) |
58 | 57 | eqeq2d 2744 |
. . . . . . . . . 10
โข (๐ = -๐ โ ((1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โ (1 / ๐ด) = (๐ + ((โโ๐ท) ยท -๐)))) |
59 | | oveq1 7368 |
. . . . . . . . . . . . 13
โข (๐ = -๐ โ (๐โ2) = (-๐โ2)) |
60 | 59 | oveq2d 7377 |
. . . . . . . . . . . 12
โข (๐ = -๐ โ (๐ท ยท (๐โ2)) = (๐ท ยท (-๐โ2))) |
61 | 60 | oveq2d 7377 |
. . . . . . . . . . 11
โข (๐ = -๐ โ ((๐โ2) โ (๐ท ยท (๐โ2))) = ((๐โ2) โ (๐ท ยท (-๐โ2)))) |
62 | 61 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ = -๐ โ (((๐โ2) โ (๐ท ยท (๐โ2))) = 1 โ ((๐โ2) โ (๐ท ยท (-๐โ2))) = 1)) |
63 | 58, 62 | anbi12d 632 |
. . . . . . . . 9
โข (๐ = -๐ โ (((1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ((1 / ๐ด) = (๐ + ((โโ๐ท) ยท -๐)) โง ((๐โ2) โ (๐ท ยท (-๐โ2))) = 1))) |
64 | 55, 63 | rspc2ev 3594 |
. . . . . . . 8
โข ((๐ โ โค โง -๐ โ โค โง ((1 /
๐ด) = (๐ + ((โโ๐ท) ยท -๐)) โง ((๐โ2) โ (๐ท ยท (-๐โ2))) = 1)) โ โ๐ โ โค โ๐ โ โค ((1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) |
65 | 7, 9, 44, 49, 64 | syl112anc 1375 |
. . . . . . 7
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ โ๐ โ โค โ๐ โ โค ((1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) |
66 | 6, 65 | jca 513 |
. . . . . 6
โข ((((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((1 / ๐ด) โ โ โง
โ๐ โ โค
โ๐ โ โค ((1
/ ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1))) |
67 | 66 | ex 414 |
. . . . 5
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ((1 / ๐ด) โ โ โง
โ๐ โ โค
โ๐ โ โค ((1
/ ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
68 | 67 | rexlimdvva 3202 |
. . . 4
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ (โ๐ โ โค โ๐ โ โค (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ((1 / ๐ด) โ โ โง
โ๐ โ โค
โ๐ โ โค ((1
/ ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
69 | 68 | adantld 492 |
. . 3
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ ((๐ด โ โ โง โ๐ โ โค โ๐ โ โค (๐ด = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) โ ((1 / ๐ด) โ โ โง
โ๐ โ โค
โ๐ โ โค ((1
/ ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
70 | 2, 69 | mpd 15 |
. 2
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ ((1 / ๐ด) โ โ โง โ๐ โ โค โ๐ โ โค ((1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1))) |
71 | | elpell1234qr 41221 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ ((1 / ๐ด) โ (Pell1234QRโ๐ท) โ ((1 / ๐ด) โ โ โง โ๐ โ โค โ๐ โ โค ((1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
72 | 71 | adantr 482 |
. 2
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ ((1 / ๐ด) โ (Pell1234QRโ๐ท) โ ((1 / ๐ด) โ โ โง โ๐ โ โค โ๐ โ โค ((1 / ๐ด) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
73 | 70, 72 | mpbird 257 |
1
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell1234QRโ๐ท)) โ (1 / ๐ด) โ (Pell1234QRโ๐ท)) |