Step | Hyp | Ref
| Expression |
1 | | 2nn0 11309 |
. . . 4
|
2 | 1 | a1i 11 |
. . 3
Word |
3 | | lencl 13324 |
. . . 4
Word |
4 | 3 | adantr 481 |
. . 3
Word |
5 | | simpr 477 |
. . 3
Word |
6 | | elfz2nn0 12431 |
. . 3
|
7 | 2, 4, 5, 6 | syl3anbrc 1246 |
. 2
Word |
8 | | pfxlen 41391 |
. . . 4
Word
prefix |
9 | | s2len 13634 |
. . . . . . 7
|
10 | 9 | eqcomi 2631 |
. . . . . 6
|
11 | 10 | a1i 11 |
. . . . 5
Word
prefix |
12 | | simpl 473 |
. . . . . . . . . 10
Word
Word |
13 | | simpr 477 |
. . . . . . . . . 10
Word
|
14 | | 2nn 11185 |
. . . . . . . . . . . 12
|
15 | | lbfzo0 12507 |
. . . . . . . . . . . 12
..^ |
16 | 14, 15 | mpbir 221 |
. . . . . . . . . . 11
..^ |
17 | 16 | a1i 11 |
. . . . . . . . . 10
Word
..^ |
18 | 12, 13, 17 | 3jca 1242 |
. . . . . . . . 9
Word
Word
..^ |
19 | 18 | adantr 481 |
. . . . . . . 8
Word
prefix
Word ..^ |
20 | | pfxfv 41399 |
. . . . . . . 8
Word
..^
prefix |
21 | 19, 20 | syl 17 |
. . . . . . 7
Word
prefix prefix
|
22 | | fvex 6201 |
. . . . . . . 8
|
23 | | s2fv0 13632 |
. . . . . . . 8
|
24 | 22, 23 | ax-mp 5 |
. . . . . . 7
|
25 | 21, 24 | syl6eqr 2674 |
. . . . . 6
Word
prefix prefix
|
26 | | 1nn0 11308 |
. . . . . . . . . 10
|
27 | | 1lt2 11194 |
. . . . . . . . . 10
|
28 | | elfzo0 12508 |
. . . . . . . . . 10
..^
|
29 | 26, 14, 27, 28 | mpbir3an 1244 |
. . . . . . . . 9
..^ |
30 | | pfxfv 41399 |
. . . . . . . . 9
Word
..^
prefix |
31 | 29, 30 | mp3an3 1413 |
. . . . . . . 8
Word
prefix |
32 | | fvex 6201 |
. . . . . . . . 9
|
33 | | s2fv1 13633 |
. . . . . . . . 9
|
34 | 32, 33 | ax-mp 5 |
. . . . . . . 8
|
35 | 31, 34 | syl6eqr 2674 |
. . . . . . 7
Word
prefix |
36 | 35 | adantr 481 |
. . . . . 6
Word
prefix prefix
|
37 | | 0nn0 11307 |
. . . . . . . . 9
|
38 | 37, 26 | pm3.2i 471 |
. . . . . . . 8
|
39 | 38 | a1i 11 |
. . . . . . 7
Word
prefix
|
40 | | fveq2 6191 |
. . . . . . . . 9
prefix
prefix |
41 | | fveq2 6191 |
. . . . . . . . 9
|
42 | 40, 41 | eqeq12d 2637 |
. . . . . . . 8
prefix prefix |
43 | | fveq2 6191 |
. . . . . . . . 9
prefix
prefix |
44 | | fveq2 6191 |
. . . . . . . . 9
|
45 | 43, 44 | eqeq12d 2637 |
. . . . . . . 8
prefix prefix |
46 | 42, 45 | ralprg 4234 |
. . . . . . 7
prefix prefix
prefix |
47 | 39, 46 | syl 17 |
. . . . . 6
Word
prefix
prefix
prefix prefix |
48 | 25, 36, 47 | mpbir2and 957 |
. . . . 5
Word
prefix prefix |
49 | | eqeq1 2626 |
. . . . . . 7
prefix prefix
|
50 | | oveq2 6658 |
. . . . . . . . 9
prefix ..^ prefix ..^ |
51 | | fzo0to2pr 12553 |
. . . . . . . . 9
..^ |
52 | 50, 51 | syl6eq 2672 |
. . . . . . . 8
prefix ..^ prefix |
53 | 52 | raleqdv 3144 |
. . . . . . 7
prefix ..^ prefix prefix prefix
|
54 | 49, 53 | anbi12d 747 |
. . . . . 6
prefix prefix ..^ prefix prefix
prefix |
55 | 54 | adantl 482 |
. . . . 5
Word
prefix prefix ..^ prefix prefix prefix |
56 | 11, 48, 55 | mpbir2and 957 |
. . . 4
Word
prefix prefix ..^ prefix prefix |
57 | 8, 56 | mpdan 702 |
. . 3
Word
prefix ..^ prefix prefix |
58 | | pfxcl 41386 |
. . . . 5
Word prefix Word |
59 | 58 | adantr 481 |
. . . 4
Word
prefix
Word |
60 | | simp2 1062 |
. . . . . . . . . 10
|
61 | | 1red 10055 |
. . . . . . . . . . . . . . 15
|
62 | | 2re 11090 |
. . . . . . . . . . . . . . . 16
|
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . 15
|
64 | | nn0re 11301 |
. . . . . . . . . . . . . . 15
|
65 | 61, 63, 64 | 3jca 1242 |
. . . . . . . . . . . . . 14
|
66 | | ltleletr 10130 |
. . . . . . . . . . . . . 14
|
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . 13
|
68 | 27, 67 | mpani 712 |
. . . . . . . . . . . 12
|
69 | 68 | imp 445 |
. . . . . . . . . . 11
|
70 | 69 | 3adant1 1079 |
. . . . . . . . . 10
|
71 | 60, 70 | jca 554 |
. . . . . . . . 9
|
72 | | elnnnn0c 11338 |
. . . . . . . . 9
|
73 | 71, 72 | sylibr 224 |
. . . . . . . 8
|
74 | 6, 73 | sylbi 207 |
. . . . . . 7
|
75 | | lbfzo0 12507 |
. . . . . . 7
..^ |
76 | 74, 75 | sylibr 224 |
. . . . . 6
..^ |
77 | | wrdsymbcl 13318 |
. . . . . 6
Word
..^ |
78 | 76, 77 | sylan2 491 |
. . . . 5
Word
|
79 | 26 | a1i 11 |
. . . . . . 7
|
80 | 65 | adantl 482 |
. . . . . . . . . . 11
|
81 | | ltletr 10129 |
. . . . . . . . . . 11
|
82 | 80, 81 | syl 17 |
. . . . . . . . . 10
|
83 | 27, 82 | mpani 712 |
. . . . . . . . 9
|
84 | 83 | 3impia 1261 |
. . . . . . . 8
|
85 | 6, 84 | sylbi 207 |
. . . . . . 7
|
86 | | elfzo0 12508 |
. . . . . . 7
..^
|
87 | 79, 74, 85, 86 | syl3anbrc 1246 |
. . . . . 6
..^ |
88 | | wrdsymbcl 13318 |
. . . . . 6
Word
..^ |
89 | 87, 88 | sylan2 491 |
. . . . 5
Word
|
90 | 78, 89 | s2cld 13616 |
. . . 4
Word
Word
|
91 | | eqwrd 13346 |
. . . 4
prefix Word Word prefix
prefix ..^ prefix prefix |
92 | 59, 90, 91 | syl2anc 693 |
. . 3
Word
prefix
prefix ..^ prefix prefix |
93 | 57, 92 | mpbird 247 |
. 2
Word
prefix
|
94 | 7, 93 | syldan 487 |
1
Word prefix |