Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . 8
Word |
2 | | efgval.r |
. . . . . . . 8
~FG |
3 | | efgval2.m |
. . . . . . . 8
|
4 | | efgval2.t |
. . . . . . . 8
splice |
5 | | efgred.d |
. . . . . . . 8
|
6 | | efgred.s |
. . . . . . . 8
Word ..^ |
7 | 1, 2, 3, 4, 5, 6 | efgsdm 18143 |
. . . . . . 7
Word
..^ |
8 | 7 | simp1bi 1076 |
. . . . . 6
Word |
9 | 8 | adantr 481 |
. . . . 5
Word |
10 | 9 | eldifad 3586 |
. . . 4
Word |
11 | 1, 2, 3, 4, 5, 6 | efgsf 18142 |
. . . . . . . . . . . 12
Word
..^ |
12 | 11 | fdmi 6052 |
. . . . . . . . . . . . 13
Word
..^ |
13 | 12 | feq2i 6037 |
. . . . . . . . . . . 12
Word
..^ |
14 | 11, 13 | mpbir 221 |
. . . . . . . . . . 11
|
15 | 14 | ffvelrni 6358 |
. . . . . . . . . 10
|
16 | 15 | adantr 481 |
. . . . . . . . 9
|
17 | 1, 2, 3, 4 | efgtf 18135 |
. . . . . . . . 9
splice |
18 | 16, 17 | syl 17 |
. . . . . . . 8
splice
|
19 | 18 | simprd 479 |
. . . . . . 7
|
20 | | frn 6053 |
. . . . . . 7
|
21 | 19, 20 | syl 17 |
. . . . . 6
|
22 | | simpr 477 |
. . . . . 6
|
23 | 21, 22 | sseldd 3604 |
. . . . 5
|
24 | 23 | s1cld 13383 |
. . . 4
Word
|
25 | | ccatcl 13359 |
. . . 4
Word Word ++
Word |
26 | 10, 24, 25 | syl2anc 693 |
. . 3
++
Word |
27 | | ccatlen 13360 |
. . . . . . 7
Word Word ++ |
28 | 10, 24, 27 | syl2anc 693 |
. . . . . 6
++ |
29 | | s1len 13385 |
. . . . . . 7
|
30 | 29 | oveq2i 6661 |
. . . . . 6
|
31 | 28, 30 | syl6eq 2672 |
. . . . 5
++ |
32 | | lencl 13324 |
. . . . . 6
Word |
33 | | nn0p1nn 11332 |
. . . . . 6
|
34 | 10, 32, 33 | 3syl 18 |
. . . . 5
|
35 | 31, 34 | eqeltrd 2701 |
. . . 4
++ |
36 | | wrdfin 13323 |
. . . . 5
++
Word ++ |
37 | | hashnncl 13157 |
. . . . 5
++
++ ++
|
38 | 26, 36, 37 | 3syl 18 |
. . . 4
++
++ |
39 | 35, 38 | mpbid 222 |
. . 3
++ |
40 | | eldifsn 4317 |
. . 3
++
Word ++ Word ++ |
41 | 26, 39, 40 | sylanbrc 698 |
. 2
++
Word |
42 | | eldifsni 4320 |
. . . . . . 7
Word |
43 | 9, 42 | syl 17 |
. . . . . 6
|
44 | | wrdfin 13323 |
. . . . . . 7
Word |
45 | | hashnncl 13157 |
. . . . . . 7
|
46 | 10, 44, 45 | 3syl 18 |
. . . . . 6
|
47 | 43, 46 | mpbird 247 |
. . . . 5
|
48 | | lbfzo0 12507 |
. . . . 5
..^ |
49 | 47, 48 | sylibr 224 |
. . . 4
..^ |
50 | | ccatval1 13361 |
. . . 4
Word Word ..^ ++ |
51 | 10, 24, 49, 50 | syl3anc 1326 |
. . 3
++ |
52 | 7 | simp2bi 1077 |
. . . 4
|
53 | 52 | adantr 481 |
. . 3
|
54 | 51, 53 | eqeltrd 2701 |
. 2
++ |
55 | 7 | simp3bi 1078 |
. . . . . 6
..^ |
56 | 55 | adantr 481 |
. . . . 5
..^ |
57 | | fzo0ss1 12498 |
. . . . . . . . . . 11
..^ ..^ |
58 | 57 | sseli 3599 |
. . . . . . . . . 10
..^
..^ |
59 | | ccatval1 13361 |
. . . . . . . . . 10
Word Word ..^ ++ |
60 | 58, 59 | syl3an3 1361 |
. . . . . . . . 9
Word Word ..^ ++ |
61 | | elfzoel2 12469 |
. . . . . . . . . . . . . . . 16
..^
|
62 | | peano2zm 11420 |
. . . . . . . . . . . . . . . 16
|
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
..^
|
64 | 61 | zred 11482 |
. . . . . . . . . . . . . . . 16
..^
|
65 | 64 | lem1d 10957 |
. . . . . . . . . . . . . . 15
..^
|
66 | | eluz2 11693 |
. . . . . . . . . . . . . . 15
|
67 | 63, 61, 65, 66 | syl3anbrc 1246 |
. . . . . . . . . . . . . 14
..^
|
68 | | fzoss2 12496 |
. . . . . . . . . . . . . 14
..^ ..^ |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . 13
..^
..^
..^ |
70 | | elfzoelz 12470 |
. . . . . . . . . . . . . . 15
..^
|
71 | | elfzom1b 12567 |
. . . . . . . . . . . . . . 15
..^
..^ |
72 | 70, 61, 71 | syl2anc 693 |
. . . . . . . . . . . . . 14
..^
..^
..^ |
73 | 72 | ibi 256 |
. . . . . . . . . . . . 13
..^
..^ |
74 | 69, 73 | sseldd 3604 |
. . . . . . . . . . . 12
..^
..^ |
75 | | ccatval1 13361 |
. . . . . . . . . . . 12
Word Word ..^ ++ |
76 | 74, 75 | syl3an3 1361 |
. . . . . . . . . . 11
Word Word ..^ ++ |
77 | 76 | fveq2d 6195 |
. . . . . . . . . 10
Word Word ..^ ++ |
78 | 77 | rneqd 5353 |
. . . . . . . . 9
Word Word ..^
++ |
79 | 60, 78 | eleq12d 2695 |
. . . . . . . 8
Word Word ..^ ++ ++ |
80 | 79 | 3expa 1265 |
. . . . . . 7
Word Word
..^ ++ ++
|
81 | 80 | ralbidva 2985 |
. . . . . 6
Word Word
..^ ++ ++ ..^ |
82 | 10, 24, 81 | syl2anc 693 |
. . . . 5
..^ ++ ++ ..^ |
83 | 56, 82 | mpbird 247 |
. . . 4
..^ ++ ++ |
84 | 10, 32 | syl 17 |
. . . . . . . . . 10
|
85 | 84 | nn0cnd 11353 |
. . . . . . . . 9
|
86 | 85 | addid2d 10237 |
. . . . . . . 8
|
87 | 86 | fveq2d 6195 |
. . . . . . 7
++ ++ |
88 | | 1nn 11031 |
. . . . . . . . . . 11
|
89 | 29, 88 | eqeltri 2697 |
. . . . . . . . . 10
|
90 | 89 | a1i 11 |
. . . . . . . . 9
|
91 | | lbfzo0 12507 |
. . . . . . . . 9
..^
|
92 | 90, 91 | sylibr 224 |
. . . . . . . 8
..^ |
93 | | ccatval3 13363 |
. . . . . . . 8
Word Word ..^ ++ |
94 | 10, 24, 92, 93 | syl3anc 1326 |
. . . . . . 7
++ |
95 | 87, 94 | eqtr3d 2658 |
. . . . . 6
++ |
96 | | s1fv 13390 |
. . . . . . . 8
|
97 | 96 | adantl 482 |
. . . . . . 7
|
98 | | fzo0end 12560 |
. . . . . . . . . . . 12
..^ |
99 | 47, 98 | syl 17 |
. . . . . . . . . . 11
..^ |
100 | | ccatval1 13361 |
. . . . . . . . . . 11
Word Word ..^ ++ |
101 | 10, 24, 99, 100 | syl3anc 1326 |
. . . . . . . . . 10
++ |
102 | 1, 2, 3, 4, 5, 6 | efgsval 18144 |
. . . . . . . . . . 11
|
103 | 102 | adantr 481 |
. . . . . . . . . 10
|
104 | 101, 103 | eqtr4d 2659 |
. . . . . . . . 9
++ |
105 | 104 | fveq2d 6195 |
. . . . . . . 8
++ |
106 | 105 | rneqd 5353 |
. . . . . . 7
++ |
107 | 22, 97, 106 | 3eltr4d 2716 |
. . . . . 6
++ |
108 | 95, 107 | eqeltrd 2701 |
. . . . 5
++ ++ |
109 | | fvex 6201 |
. . . . . 6
|
110 | | fveq2 6191 |
. . . . . . 7
++ ++ |
111 | | oveq1 6657 |
. . . . . . . . . 10
|
112 | 111 | fveq2d 6195 |
. . . . . . . . 9
++ ++ |
113 | 112 | fveq2d 6195 |
. . . . . . . 8
++ ++ |
114 | 113 | rneqd 5353 |
. . . . . . 7
++ ++ |
115 | 110, 114 | eleq12d 2695 |
. . . . . 6
++ ++ ++ ++ |
116 | 109, 115 | ralsn 4222 |
. . . . 5
++ ++ ++ ++ |
117 | 108, 116 | sylibr 224 |
. . . 4
++ ++ |
118 | | ralunb 3794 |
. . . 4
..^ ++ ++ ..^ ++ ++ ++ ++ |
119 | 83, 117, 118 | sylanbrc 698 |
. . 3
..^ ++ ++ |
120 | 31 | oveq2d 6666 |
. . . . 5
..^ ++ ..^ |
121 | | nnuz 11723 |
. . . . . . 7
|
122 | 47, 121 | syl6eleq 2711 |
. . . . . 6
|
123 | | fzosplitsn 12576 |
. . . . . 6
..^ ..^ |
124 | 122, 123 | syl 17 |
. . . . 5
..^ ..^ |
125 | 120, 124 | eqtrd 2656 |
. . . 4
..^ ++ ..^ |
126 | 125 | raleqdv 3144 |
. . 3
..^ ++ ++ ++ ..^ ++ ++ |
127 | 119, 126 | mpbird 247 |
. 2
..^ ++ ++ ++ |
128 | 1, 2, 3, 4, 5, 6 | efgsdm 18143 |
. 2
++
++ Word ++ ..^ ++ ++ ++ |
129 | 41, 54, 127, 128 | syl3anbrc 1246 |
1
++
|