Step | Hyp | Ref
| Expression |
1 | | fof 6115 |
. . 3
|
2 | | fargshift.g |
. . . 4
..^ |
3 | 2 | fargshiftf 41376 |
. . 3
..^ |
4 | 1, 3 | sylan2 491 |
. 2
..^ |
5 | 2 | rnmpt 5371 |
. . 3
..^ |
6 | | fofn 6117 |
. . . . . 6
|
7 | | fnrnfv 6242 |
. . . . . 6
|
8 | 6, 7 | syl 17 |
. . . . 5
|
9 | 8 | adantl 482 |
. . . 4
|
10 | | df-fo 5894 |
. . . . . . 7
|
11 | 10 | biimpi 206 |
. . . . . 6
|
12 | 11 | adantl 482 |
. . . . 5
|
13 | | eqeq1 2626 |
. . . . . . . . 9
|
14 | | eqcom 2629 |
. . . . . . . . 9
|
15 | 13, 14 | syl6bb 276 |
. . . . . . . 8
|
16 | | ffn 6045 |
. . . . . . . . . . . . . 14
|
17 | | fseq1hash 13165 |
. . . . . . . . . . . . . 14
|
18 | 16, 17 | sylan2 491 |
. . . . . . . . . . . . 13
|
19 | 1, 18 | sylan2 491 |
. . . . . . . . . . . 12
|
20 | | fz0add1fz1 12537 |
. . . . . . . . . . . . . . 15
..^ |
21 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . 21
|
22 | | fzval3 12536 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
24 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . 22
|
25 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . 22
|
26 | 24, 25 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . . 21
|
27 | 26 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
28 | 23, 27 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
..^ |
29 | 28 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . 18
..^ |
30 | 29 | biimpa 501 |
. . . . . . . . . . . . . . . . 17
..^ |
31 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
32 | | fzosubel3 12528 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
33 | 30, 31, 32 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
..^ |
34 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
35 | 34 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
36 | 35 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
37 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | 37 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 38 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
40 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . 18
|
41 | 39, 40 | npcand 10396 |
. . . . . . . . . . . . . . . . 17
|
42 | 41 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
|
43 | 33, 36, 42 | rspcedvd 3317 |
. . . . . . . . . . . . . . 15
..^ |
44 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
45 | 44 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
46 | 45 | adantl 482 |
. . . . . . . . . . . . . . 15
|
47 | 20, 43, 46 | rexxfrd 4881 |
. . . . . . . . . . . . . 14
..^ |
48 | 47 | adantr 481 |
. . . . . . . . . . . . 13
..^
|
49 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
50 | 49 | rexeqdv 3145 |
. . . . . . . . . . . . . . 15
..^ ..^
|
51 | 50 | bibi2d 332 |
. . . . . . . . . . . . . 14
..^
..^ |
52 | 51 | adantl 482 |
. . . . . . . . . . . . 13
..^
..^ |
53 | 48, 52 | mpbird 247 |
. . . . . . . . . . . 12
..^ |
54 | 19, 53 | syldan 487 |
. . . . . . . . . . 11
..^
|
55 | 54 | abbidv 2741 |
. . . . . . . . . 10
..^ |
56 | 55 | eqeq1d 2624 |
. . . . . . . . 9
..^
|
57 | 56 | biimpcd 239 |
. . . . . . . 8
..^ |
58 | 15, 57 | syl6bi 243 |
. . . . . . 7
..^
|
59 | 58 | com23 86 |
. . . . . 6
..^
|
60 | 59 | adantl 482 |
. . . . 5
..^ |
61 | 12, 60 | mpcom 38 |
. . . 4
..^ |
62 | 9, 61 | mpd 15 |
. . 3
..^ |
63 | 5, 62 | syl5eq 2668 |
. 2
|
64 | | dffo2 6119 |
. 2
..^
..^
|
65 | 4, 63, 64 | sylanbrc 698 |
1
..^ |