Step | Hyp | Ref
| Expression |
1 | | 1red 11164 |
. 2
โข (๐ท โ (โ โ
โปNN) โ 1 โ โ) |
2 | | 1nn0 12437 |
. . . 4
โข 1 โ
โ0 |
3 | 2 | a1i 11 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ 1 โ
โ0) |
4 | | 0nn0 12436 |
. . . 4
โข 0 โ
โ0 |
5 | 4 | a1i 11 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ 0 โ
โ0) |
6 | | eldifi 4090 |
. . . . . . . 8
โข (๐ท โ (โ โ
โปNN) โ ๐ท โ โ) |
7 | 6 | nncnd 12177 |
. . . . . . 7
โข (๐ท โ (โ โ
โปNN) โ ๐ท โ โ) |
8 | 7 | sqrtcld 15331 |
. . . . . 6
โข (๐ท โ (โ โ
โปNN) โ (โโ๐ท) โ โ) |
9 | 8 | mul01d 11362 |
. . . . 5
โข (๐ท โ (โ โ
โปNN) โ ((โโ๐ท) ยท 0) = 0) |
10 | 9 | oveq2d 7377 |
. . . 4
โข (๐ท โ (โ โ
โปNN) โ (1 + ((โโ๐ท) ยท 0)) = (1 + 0)) |
11 | | 1p0e1 12285 |
. . . 4
โข (1 + 0) =
1 |
12 | 10, 11 | eqtr2di 2790 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ 1 = (1 + ((โโ๐ท) ยท 0))) |
13 | | sq1 14108 |
. . . . . 6
โข
(1โ2) = 1 |
14 | 13 | a1i 11 |
. . . . 5
โข (๐ท โ (โ โ
โปNN) โ (1โ2) = 1) |
15 | | sq0 14105 |
. . . . . . 7
โข
(0โ2) = 0 |
16 | 15 | oveq2i 7372 |
. . . . . 6
โข (๐ท ยท (0โ2)) = (๐ท ยท 0) |
17 | 7 | mul01d 11362 |
. . . . . 6
โข (๐ท โ (โ โ
โปNN) โ (๐ท ยท 0) = 0) |
18 | 16, 17 | eqtrid 2785 |
. . . . 5
โข (๐ท โ (โ โ
โปNN) โ (๐ท ยท (0โ2)) = 0) |
19 | 14, 18 | oveq12d 7379 |
. . . 4
โข (๐ท โ (โ โ
โปNN) โ ((1โ2) โ (๐ท ยท (0โ2))) = (1 โ
0)) |
20 | | 1m0e1 12282 |
. . . 4
โข (1
โ 0) = 1 |
21 | 19, 20 | eqtrdi 2789 |
. . 3
โข (๐ท โ (โ โ
โปNN) โ ((1โ2) โ (๐ท ยท (0โ2))) = 1) |
22 | | oveq1 7368 |
. . . . . 6
โข (๐ = 1 โ (๐ + ((โโ๐ท) ยท ๐)) = (1 + ((โโ๐ท) ยท ๐))) |
23 | 22 | eqeq2d 2744 |
. . . . 5
โข (๐ = 1 โ (1 = (๐ + ((โโ๐ท) ยท ๐)) โ 1 = (1 + ((โโ๐ท) ยท ๐)))) |
24 | | oveq1 7368 |
. . . . . . 7
โข (๐ = 1 โ (๐โ2) = (1โ2)) |
25 | 24 | oveq1d 7376 |
. . . . . 6
โข (๐ = 1 โ ((๐โ2) โ (๐ท ยท (๐โ2))) = ((1โ2) โ (๐ท ยท (๐โ2)))) |
26 | 25 | eqeq1d 2735 |
. . . . 5
โข (๐ = 1 โ (((๐โ2) โ (๐ท ยท (๐โ2))) = 1 โ ((1โ2) โ
(๐ท ยท (๐โ2))) =
1)) |
27 | 23, 26 | anbi12d 632 |
. . . 4
โข (๐ = 1 โ ((1 = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ (1 = (1 +
((โโ๐ท) ยท
๐)) โง ((1โ2)
โ (๐ท ยท (๐โ2))) =
1))) |
28 | | oveq2 7369 |
. . . . . . 7
โข (๐ = 0 โ
((โโ๐ท) ยท
๐) = ((โโ๐ท) ยท 0)) |
29 | 28 | oveq2d 7377 |
. . . . . 6
โข (๐ = 0 โ (1 +
((โโ๐ท) ยท
๐)) = (1 +
((โโ๐ท) ยท
0))) |
30 | 29 | eqeq2d 2744 |
. . . . 5
โข (๐ = 0 โ (1 = (1 +
((โโ๐ท) ยท
๐)) โ 1 = (1 +
((โโ๐ท) ยท
0)))) |
31 | | oveq1 7368 |
. . . . . . . 8
โข (๐ = 0 โ (๐โ2) = (0โ2)) |
32 | 31 | oveq2d 7377 |
. . . . . . 7
โข (๐ = 0 โ (๐ท ยท (๐โ2)) = (๐ท ยท (0โ2))) |
33 | 32 | oveq2d 7377 |
. . . . . 6
โข (๐ = 0 โ ((1โ2) โ
(๐ท ยท (๐โ2))) = ((1โ2) โ
(๐ท ยท
(0โ2)))) |
34 | 33 | eqeq1d 2735 |
. . . . 5
โข (๐ = 0 โ (((1โ2) โ
(๐ท ยท (๐โ2))) = 1 โ
((1โ2) โ (๐ท
ยท (0โ2))) = 1)) |
35 | 30, 34 | anbi12d 632 |
. . . 4
โข (๐ = 0 โ ((1 = (1 +
((โโ๐ท) ยท
๐)) โง ((1โ2)
โ (๐ท ยท (๐โ2))) = 1) โ (1 = (1 +
((โโ๐ท) ยท
0)) โง ((1โ2) โ (๐ท ยท (0โ2))) =
1))) |
36 | 27, 35 | rspc2ev 3594 |
. . 3
โข ((1
โ โ0 โง 0 โ โ0 โง (1 = (1 +
((โโ๐ท) ยท
0)) โง ((1โ2) โ (๐ท ยท (0โ2))) = 1)) โ
โ๐ โ
โ0 โ๐ โ โ0 (1 = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) |
37 | 3, 5, 12, 21, 36 | syl112anc 1375 |
. 2
โข (๐ท โ (โ โ
โปNN) โ โ๐ โ โ0 โ๐ โ โ0 (1 =
(๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) |
38 | | elpell1qr 41217 |
. 2
โข (๐ท โ (โ โ
โปNN) โ (1 โ (Pell1QRโ๐ท) โ (1 โ โ โง
โ๐ โ
โ0 โ๐ โ โ0 (1 = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
39 | 1, 37, 38 | mpbir2and 712 |
1
โข (๐ท โ (โ โ
โปNN) โ 1 โ (Pell1QRโ๐ท)) |