Step | Hyp | Ref
| Expression |
1 | | oveq2 7417 |
. . . . . 6
โข (๐ = 0 โ (๐ดโ๐) = (๐ดโ0)) |
2 | 1 | eleq1d 2819 |
. . . . 5
โข (๐ = 0 โ ((๐ดโ๐) โ (Pell14QRโ๐ท) โ (๐ดโ0) โ (Pell14QRโ๐ท))) |
3 | 2 | imbi2d 341 |
. . . 4
โข (๐ = 0 โ (((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ0) โ (Pell14QRโ๐ท)))) |
4 | | oveq2 7417 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
5 | 4 | eleq1d 2819 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ๐) โ (Pell14QRโ๐ท) โ (๐ดโ๐) โ (Pell14QRโ๐ท))) |
6 | 5 | imbi2d 341 |
. . . 4
โข (๐ = ๐ โ (((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)))) |
7 | | oveq2 7417 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
8 | 7 | eleq1d 2819 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ดโ๐) โ (Pell14QRโ๐ท) โ (๐ดโ(๐ + 1)) โ (Pell14QRโ๐ท))) |
9 | 8 | imbi2d 341 |
. . . 4
โข (๐ = (๐ + 1) โ (((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ(๐ + 1)) โ (Pell14QRโ๐ท)))) |
10 | | oveq2 7417 |
. . . . . 6
โข (๐ = ๐ต โ (๐ดโ๐) = (๐ดโ๐ต)) |
11 | 10 | eleq1d 2819 |
. . . . 5
โข (๐ = ๐ต โ ((๐ดโ๐) โ (Pell14QRโ๐ท) โ (๐ดโ๐ต) โ (Pell14QRโ๐ท))) |
12 | 11 | imbi2d 341 |
. . . 4
โข (๐ = ๐ต โ (((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐ต) โ (Pell14QRโ๐ท)))) |
13 | | pell14qrre 41595 |
. . . . . . . 8
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ ๐ด โ โ) |
14 | 13 | recnd 11242 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ ๐ด โ โ) |
15 | 14 | exp0d 14105 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ0) = 1) |
16 | | pell14qrne0 41596 |
. . . . . . 7
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ ๐ด โ 0) |
17 | 14, 16 | dividd 11988 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ด / ๐ด) = 1) |
18 | 15, 17 | eqtr4d 2776 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ0) = (๐ด / ๐ด)) |
19 | | pell14qrdivcl 41603 |
. . . . . 6
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ด / ๐ด) โ (Pell14QRโ๐ท)) |
20 | 19 | 3anidm23 1422 |
. . . . 5
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ด / ๐ด) โ (Pell14QRโ๐ท)) |
21 | 18, 20 | eqeltrd 2834 |
. . . 4
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ0) โ (Pell14QRโ๐ท)) |
22 | 14 | 3ad2ant2 1135 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ๐ด โ โ) |
23 | | simp1 1137 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ๐ โ โ0) |
24 | 22, 23 | expp1d 14112 |
. . . . . . 7
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
25 | | simp2l 1200 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ๐ท โ (โ โ
โปNN)) |
26 | | simp3 1139 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ (๐ดโ๐) โ (Pell14QRโ๐ท)) |
27 | | simp2r 1201 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ๐ด โ (Pell14QRโ๐ท)) |
28 | | pell14qrmulcl 41601 |
. . . . . . . 8
โข ((๐ท โ (โ โ
โปNN) โง (๐ดโ๐) โ (Pell14QRโ๐ท) โง ๐ด โ (Pell14QRโ๐ท)) โ ((๐ดโ๐) ยท ๐ด) โ (Pell14QRโ๐ท)) |
29 | 25, 26, 27, 28 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ ((๐ดโ๐) ยท ๐ด) โ (Pell14QRโ๐ท)) |
30 | 24, 29 | eqeltrd 2834 |
. . . . . 6
โข ((๐ โ โ0
โง (๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โง (๐ดโ๐) โ (Pell14QRโ๐ท)) โ (๐ดโ(๐ + 1)) โ (Pell14QRโ๐ท)) |
31 | 30 | 3exp 1120 |
. . . . 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 12657 |
. . 3
โข (๐ต โ โ0
โ ((๐ท โ (โ
โ โปNN) โง ๐ด โ (Pell14QRโ๐ท)) โ (๐ดโ๐ต) โ (Pell14QRโ๐ท))) |
34 | 33 | expdcom 416 |
. 2
โข (๐ท โ (โ โ
โปNN) โ (๐ด โ (Pell14QRโ๐ท) โ (๐ต โ โ0 โ (๐ดโ๐ต) โ (Pell14QRโ๐ท)))) |
35 | 34 | 3imp 1112 |
1
โข ((๐ท โ (โ โ
โปNN) โง ๐ด โ (Pell14QRโ๐ท) โง ๐ต โ โ0) โ (๐ดโ๐ต) โ (Pell14QRโ๐ท)) |