Step | Hyp | Ref
| Expression |
1 | | oveq2 7421 |
. . . . . 6
โข (๐ = 0 โ (๐ดโ๐) = (๐ดโ0)) |
2 | 1 | eleq1d 2816 |
. . . . 5
โข (๐ = 0 โ ((๐ดโ๐) โ (Pell14QRโ๐ท) โ (๐ดโ0) โ (Pell14QRโ๐ท))) |
3 | 2 | imbi2d 339 |
. . . 4
โข (๐ = 0 โ (((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ0) โ (Pell14QRโ๐ท)))) |
4 | | oveq2 7421 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
5 | 4 | eleq1d 2816 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ๐) โ (Pell14QRโ๐ท) โ (๐ดโ๐) โ (Pell14QRโ๐ท))) |
6 | 5 | imbi2d 339 |
. . . 4
โข (๐ = ๐ โ (((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)))) |
7 | | oveq2 7421 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
8 | 7 | eleq1d 2816 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ดโ๐) โ (Pell14QRโ๐ท) โ (๐ดโ(๐ + 1)) โ (Pell14QRโ๐ท))) |
9 | 8 | imbi2d 339 |
. . . 4
โข (๐ = (๐ + 1) โ (((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ(๐ + 1)) โ (Pell14QRโ๐ท)))) |
10 | | oveq2 7421 |
. . . . . 6
โข (๐ = ๐ต โ (๐ดโ๐) = (๐ดโ๐ต)) |
11 | 10 | eleq1d 2816 |
. . . . 5
โข (๐ = ๐ต โ ((๐ดโ๐) โ (Pell14QRโ๐ท) โ (๐ดโ๐ต) โ (Pell14QRโ๐ท))) |
12 | 11 | imbi2d 339 |
. . . 4
โข (๐ = ๐ต โ (((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐ต) โ (Pell14QRโ๐ท)))) |
13 | | pell14qrre 41899 |
. . . . . . . 8
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ ๐ด โ โ) |
14 | 13 | recnd 11248 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ ๐ด โ โ) |
15 | 14 | exp0d 14111 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ0) = 1) |
16 | | pell14qrne0 41900 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ ๐ด โ 0) |
17 | 14, 16 | dividd 11994 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ด / ๐ด) = 1) |
18 | 15, 17 | eqtr4d 2773 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ0) = (๐ด / ๐ด)) |
19 | | pell14qrdivcl 41907 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ด / ๐ด) โ (Pell14QRโ๐ท)) |
20 | 19 | 3anidm23 1419 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ด / ๐ด) โ (Pell14QRโ๐ท)) |
21 | 18, 20 | eqeltrd 2831 |
. . . 4
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ0) โ (Pell14QRโ๐ท)) |
22 | 14 | 3ad2ant2 1132 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ๐ด โ โ) |
23 | | simp1 1134 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ๐ โ โ0) |
24 | 22, 23 | expp1d 14118 |
. . . . . . 7
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
25 | | simp2l 1197 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ๐ท โ (โ โ
โปNN)) |
26 | | simp3 1136 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) |
27 | | simp2r 1198 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ๐ด โ (Pell14QRโ๐ท)) |
28 | | pell14qrmulcl 41905 |
. . . . . . . 8
โข ((๐ท โ (โ โ
โปNN) โง (๐ดโ๐) โ (Pell14QRโ๐ท) โง ๐ด โ (Pell14QRโ๐ท)) โ ((๐ดโ๐) ยท ๐ด) โ (Pell14QRโ๐ท)) |
29 | 25, 26, 27, 28 | syl3anc 1369 |
. . . . . . 7
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ดโ๐) ยท ๐ด) โ (Pell14QRโ๐ท)) |
30 | 24, 29 | eqeltrd 2831 |
. . . . . 6
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ (๐ดโ(๐ + 1)) โ (Pell14QRโ๐ท)) |
31 | 30 | 3exp 1117 |
. . . . 5
โข (๐ โ โ0
โ ((๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ ((๐ดโ๐) โ (Pell14QRโ๐ท) โ (๐ดโ(๐ + 1)) โ (Pell14QRโ๐ท)))) |
32 | 31 | a2d 29 |
. . . 4
โข (๐ โ โ0
โ (((๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ(๐ + 1)) โ (Pell14QRโ๐ท)))) |
33 | 3, 6, 9, 12, 21, 32 | nn0ind 12663 |
. . 3
โข (๐ต โ โ0
โ ((๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐ต) โ (Pell14QRโ๐ท))) |
34 | 33 | expdcom 413 |
. 2
โข (๐ท โ (โ โ
โปNN) โ (๐ด โ (Pell14QRโ๐ท) โ (๐ต โ โ0 โ (๐ดโ๐ต) โ (Pell14QRโ๐ท)))) |
35 | 34 | 3imp 1109 |
1
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท) โง ๐ต โ โ0) โ (๐ดโ๐ต) โ (Pell14QRโ๐ท)) |