Step | Hyp | Ref
| Expression |
1 | | nn0re 12430 |
. . . . 5
โข (๐ด โ โ0
โ ๐ด โ
โ) |
2 | 1 | 3ad2ant2 1135 |
. . . 4
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โ ๐ด โ
โ) |
3 | | eldifi 4090 |
. . . . . . . . 9
โข (๐ท โ (โ โ
โปNN) โ ๐ท โ โ) |
4 | 3 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โ ๐ท โ
โ) |
5 | 4 | nnrpd 12963 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โ ๐ท โ
โ+) |
6 | 5 | rpsqrtcld 15305 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โ (โโ๐ท)
โ โ+) |
7 | 6 | rpred 12965 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โ (โโ๐ท)
โ โ) |
8 | | nn0re 12430 |
. . . . . 6
โข (๐ต โ โ0
โ ๐ต โ
โ) |
9 | 8 | 3ad2ant3 1136 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โ ๐ต โ
โ) |
10 | 7, 9 | remulcld 11193 |
. . . 4
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โ ((โโ๐ท)
ยท ๐ต) โ
โ) |
11 | 2, 10 | readdcld 11192 |
. . 3
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โ (๐ด +
((โโ๐ท) ยท
๐ต)) โ
โ) |
12 | 11 | adantr 482 |
. 2
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โง ((๐ดโ2) โ
(๐ท ยท (๐ตโ2))) = 1) โ (๐ด + ((โโ๐ท) ยท ๐ต)) โ โ) |
13 | | simpl2 1193 |
. . 3
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โง ((๐ดโ2) โ
(๐ท ยท (๐ตโ2))) = 1) โ ๐ด โ
โ0) |
14 | | simpl3 1194 |
. . 3
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โง ((๐ดโ2) โ
(๐ท ยท (๐ตโ2))) = 1) โ ๐ต โ
โ0) |
15 | | eqidd 2734 |
. . 3
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โง ((๐ดโ2) โ
(๐ท ยท (๐ตโ2))) = 1) โ (๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ด + ((โโ๐ท) ยท ๐ต))) |
16 | | simpr 486 |
. . 3
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โง ((๐ดโ2) โ
(๐ท ยท (๐ตโ2))) = 1) โ ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1) |
17 | | oveq1 7368 |
. . . . . 6
โข (๐ = ๐ด โ (๐ + ((โโ๐ท) ยท ๐)) = (๐ด + ((โโ๐ท) ยท ๐))) |
18 | 17 | eqeq2d 2744 |
. . . . 5
โข (๐ = ๐ด โ ((๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ + ((โโ๐ท) ยท ๐)) โ (๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ด + ((โโ๐ท) ยท ๐)))) |
19 | | oveq1 7368 |
. . . . . . 7
โข (๐ = ๐ด โ (๐โ2) = (๐ดโ2)) |
20 | 19 | oveq1d 7376 |
. . . . . 6
โข (๐ = ๐ด โ ((๐โ2) โ (๐ท ยท (๐โ2))) = ((๐ดโ2) โ (๐ท ยท (๐โ2)))) |
21 | 20 | eqeq1d 2735 |
. . . . 5
โข (๐ = ๐ด โ (((๐โ2) โ (๐ท ยท (๐โ2))) = 1 โ ((๐ดโ2) โ (๐ท ยท (๐โ2))) = 1)) |
22 | 18, 21 | anbi12d 632 |
. . . 4
โข (๐ = ๐ด โ (((๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1) โ ((๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ด + ((โโ๐ท) ยท ๐)) โง ((๐ดโ2) โ (๐ท ยท (๐โ2))) = 1))) |
23 | | oveq2 7369 |
. . . . . . 7
โข (๐ = ๐ต โ ((โโ๐ท) ยท ๐) = ((โโ๐ท) ยท ๐ต)) |
24 | 23 | oveq2d 7377 |
. . . . . 6
โข (๐ = ๐ต โ (๐ด + ((โโ๐ท) ยท ๐)) = (๐ด + ((โโ๐ท) ยท ๐ต))) |
25 | 24 | eqeq2d 2744 |
. . . . 5
โข (๐ = ๐ต โ ((๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ด + ((โโ๐ท) ยท ๐)) โ (๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ด + ((โโ๐ท) ยท ๐ต)))) |
26 | | oveq1 7368 |
. . . . . . . 8
โข (๐ = ๐ต โ (๐โ2) = (๐ตโ2)) |
27 | 26 | oveq2d 7377 |
. . . . . . 7
โข (๐ = ๐ต โ (๐ท ยท (๐โ2)) = (๐ท ยท (๐ตโ2))) |
28 | 27 | oveq2d 7377 |
. . . . . 6
โข (๐ = ๐ต โ ((๐ดโ2) โ (๐ท ยท (๐โ2))) = ((๐ดโ2) โ (๐ท ยท (๐ตโ2)))) |
29 | 28 | eqeq1d 2735 |
. . . . 5
โข (๐ = ๐ต โ (((๐ดโ2) โ (๐ท ยท (๐โ2))) = 1 โ ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) |
30 | 25, 29 | anbi12d 632 |
. . . 4
โข (๐ = ๐ต โ (((๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ด + ((โโ๐ท) ยท ๐)) โง ((๐ดโ2) โ (๐ท ยท (๐โ2))) = 1) โ ((๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1))) |
31 | 22, 30 | rspc2ev 3594 |
. . 3
โข ((๐ด โ โ0
โง ๐ต โ
โ0 โง ((๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ โ๐ โ โ0
โ๐ โ
โ0 ((๐ด +
((โโ๐ท) ยท
๐ต)) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) |
32 | 13, 14, 15, 16, 31 | syl112anc 1375 |
. 2
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โง ((๐ดโ2) โ
(๐ท ยท (๐ตโ2))) = 1) โ
โ๐ โ
โ0 โ๐ โ โ0 ((๐ด + ((โโ๐ท) ยท ๐ต)) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)) |
33 | | elpell1qr 41217 |
. . . 4
โข (๐ท โ (โ โ
โปNN) โ ((๐ด + ((โโ๐ท) ยท ๐ต)) โ (Pell1QRโ๐ท) โ ((๐ด + ((โโ๐ท) ยท ๐ต)) โ โ โง โ๐ โ โ0
โ๐ โ
โ0 ((๐ด +
((โโ๐ท) ยท
๐ต)) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
34 | 33 | 3ad2ant1 1134 |
. . 3
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โ ((๐ด +
((โโ๐ท) ยท
๐ต)) โ
(Pell1QRโ๐ท) โ
((๐ด + ((โโ๐ท) ยท ๐ต)) โ โ โง โ๐ โ โ0
โ๐ โ
โ0 ((๐ด +
((โโ๐ท) ยท
๐ต)) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
35 | 34 | adantr 482 |
. 2
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โง ((๐ดโ2) โ
(๐ท ยท (๐ตโ2))) = 1) โ ((๐ด + ((โโ๐ท) ยท ๐ต)) โ (Pell1QRโ๐ท) โ ((๐ด + ((โโ๐ท) ยท ๐ต)) โ โ โง โ๐ โ โ0
โ๐ โ
โ0 ((๐ด +
((โโ๐ท) ยท
๐ต)) = (๐ + ((โโ๐ท) ยท ๐)) โง ((๐โ2) โ (๐ท ยท (๐โ2))) = 1)))) |
36 | 12, 32, 35 | mpbir2and 712 |
1
โข (((๐ท โ (โ โ
โปNN) โง ๐ด โ โ0 โง ๐ต โ โ0)
โง ((๐ดโ2) โ
(๐ท ยท (๐ตโ2))) = 1) โ (๐ด + ((โโ๐ท) ยท ๐ต)) โ (Pell1QRโ๐ท)) |