Step | Hyp | Ref
| Expression |
1 | | lencl 14428 |
. . . . 5
β’ (π β Word π β (β―βπ) β
β0) |
2 | | 1z 12540 |
. . . . . . . . . 10
β’ 1 β
β€ |
3 | | nn0z 12531 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β (β―βπ) β β€) |
4 | | zltp1le 12560 |
. . . . . . . . . 10
β’ ((1
β β€ β§ (β―βπ) β β€) β (1 <
(β―βπ) β (1
+ 1) β€ (β―βπ))) |
5 | 2, 3, 4 | sylancr 588 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β (1 < (β―βπ) β (1 + 1) β€ (β―βπ))) |
6 | | 1p1e2 12285 |
. . . . . . . . . . . 12
β’ (1 + 1) =
2 |
7 | 6 | a1i 11 |
. . . . . . . . . . 11
β’
((β―βπ)
β β0 β (1 + 1) = 2) |
8 | 7 | breq1d 5120 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β ((1 + 1) β€ (β―βπ) β 2 β€
(β―βπ))) |
9 | 8 | biimpd 228 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β ((1 + 1) β€ (β―βπ) β 2 β€
(β―βπ))) |
10 | 5, 9 | sylbid 239 |
. . . . . . . 8
β’
((β―βπ)
β β0 β (1 < (β―βπ) β 2 β€ (β―βπ))) |
11 | 10 | imp 408 |
. . . . . . 7
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β 2 β€ (β―βπ)) |
12 | | 2nn0 12437 |
. . . . . . . 8
β’ 2 β
β0 |
13 | | simpl 484 |
. . . . . . . 8
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β (β―βπ) β
β0) |
14 | | nn0sub 12470 |
. . . . . . . 8
β’ ((2
β β0 β§ (β―βπ) β β0) β (2 β€
(β―βπ) β
((β―βπ) β
2) β β0)) |
15 | 12, 13, 14 | sylancr 588 |
. . . . . . 7
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β (2 β€ (β―βπ) β ((β―βπ) β 2) β
β0)) |
16 | 11, 15 | mpbid 231 |
. . . . . 6
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β ((β―βπ) β 2) β
β0) |
17 | 3 | adantr 482 |
. . . . . . 7
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β (β―βπ) β β€) |
18 | | 0red 11165 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β 0 β β) |
19 | | 1red 11163 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β 1 β β) |
20 | | nn0re 12429 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β (β―βπ) β β) |
21 | 18, 19, 20 | 3jca 1129 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β (0 β β β§ 1 β β
β§ (β―βπ)
β β)) |
22 | | 0lt1 11684 |
. . . . . . . . 9
β’ 0 <
1 |
23 | | lttr 11238 |
. . . . . . . . . 10
β’ ((0
β β β§ 1 β β β§ (β―βπ) β β) β ((0 < 1 β§ 1
< (β―βπ))
β 0 < (β―βπ))) |
24 | 23 | expd 417 |
. . . . . . . . 9
β’ ((0
β β β§ 1 β β β§ (β―βπ) β β) β (0 < 1 β (1
< (β―βπ)
β 0 < (β―βπ)))) |
25 | 21, 22, 24 | mpisyl 21 |
. . . . . . . 8
β’
((β―βπ)
β β0 β (1 < (β―βπ) β 0 < (β―βπ))) |
26 | 25 | imp 408 |
. . . . . . 7
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β 0 < (β―βπ)) |
27 | | elnnz 12516 |
. . . . . . 7
β’
((β―βπ)
β β β ((β―βπ) β β€ β§ 0 <
(β―βπ))) |
28 | 17, 26, 27 | sylanbrc 584 |
. . . . . 6
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β (β―βπ) β β) |
29 | | 2rp 12927 |
. . . . . . . . 9
β’ 2 β
β+ |
30 | 29 | a1i 11 |
. . . . . . . 8
β’
((β―βπ)
β β0 β 2 β
β+) |
31 | 20, 30 | ltsubrpd 12996 |
. . . . . . 7
β’
((β―βπ)
β β0 β ((β―βπ) β 2) < (β―βπ)) |
32 | 31 | adantr 482 |
. . . . . 6
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β ((β―βπ) β 2) < (β―βπ)) |
33 | | elfzo0 13620 |
. . . . . 6
β’
(((β―βπ)
β 2) β (0..^(β―βπ)) β (((β―βπ) β 2) β β0
β§ (β―βπ)
β β β§ ((β―βπ) β 2) < (β―βπ))) |
34 | 16, 28, 32, 33 | syl3anbrc 1344 |
. . . . 5
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β ((β―βπ) β 2) β
(0..^(β―βπ))) |
35 | 1, 34 | sylan 581 |
. . . 4
β’ ((π β Word π β§ 1 < (β―βπ)) β ((β―βπ) β 2) β
(0..^(β―βπ))) |
36 | 35 | 3adant2 1132 |
. . 3
β’ ((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β ((β―βπ) β 2) β
(0..^(β―βπ))) |
37 | | pfxsuffeqwrdeq 14593 |
. . 3
β’ ((π β Word π β§ π β Word π β§ ((β―βπ) β 2) β
(0..^(β―βπ)))
β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 2), (β―βπ)β©))))) |
38 | 36, 37 | syld3an3 1410 |
. 2
β’ ((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 2), (β―βπ)β©))))) |
39 | | swrd2lsw 14848 |
. . . . . . . . 9
β’ ((π β Word π β§ 1 < (β―βπ)) β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©) |
40 | 39 | 3adant2 1132 |
. . . . . . . 8
β’ ((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©) |
41 | 40 | adantr 482 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©) |
42 | | breq2 5114 |
. . . . . . . . . . 11
β’
((β―βπ) =
(β―βπ) β (1
< (β―βπ)
β 1 < (β―βπ))) |
43 | 42 | 3anbi3d 1443 |
. . . . . . . . . 10
β’
((β―βπ) =
(β―βπ) β
((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β (π β Word π β§ π β Word π β§ 1 < (β―βπ)))) |
44 | | swrd2lsw 14848 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 1 < (β―βπ)) β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©) |
45 | 44 | 3adant1 1131 |
. . . . . . . . . 10
β’ ((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©) |
46 | 43, 45 | syl6bi 253 |
. . . . . . . . 9
β’
((β―βπ) =
(β―βπ) β
((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©)) |
47 | 46 | impcom 409 |
. . . . . . . 8
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©) |
48 | | oveq1 7369 |
. . . . . . . . . . . 12
β’
((β―βπ) =
(β―βπ) β
((β―βπ) β
2) = ((β―βπ)
β 2)) |
49 | | id 22 |
. . . . . . . . . . . 12
β’
((β―βπ) =
(β―βπ) β
(β―βπ) =
(β―βπ)) |
50 | 48, 49 | opeq12d 4843 |
. . . . . . . . . . 11
β’
((β―βπ) =
(β―βπ) β
β¨((β―βπ)
β 2), (β―βπ)β© = β¨((β―βπ) β 2),
(β―βπ)β©) |
51 | 50 | oveq2d 7378 |
. . . . . . . . . 10
β’
((β―βπ) =
(β―βπ) β
(π substr
β¨((β―βπ)
β 2), (β―βπ)β©) = (π substr β¨((β―βπ) β 2),
(β―βπ)β©)) |
52 | 51 | eqeq1d 2739 |
. . . . . . . . 9
β’
((β―βπ) =
(β―βπ) β
((π substr
β¨((β―βπ)
β 2), (β―βπ)β©) = β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ© β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©)) |
53 | 52 | adantl 483 |
. . . . . . . 8
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β ((π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ© β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©)) |
54 | 47, 53 | mpbird 257 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©) |
55 | 41, 54 | eqeq12d 2753 |
. . . . . 6
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β ((π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 2), (β―βπ)β©) β β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ© =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©)) |
56 | | fvexd 6862 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (πβ((β―βπ) β 2)) β V) |
57 | | fvexd 6862 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (lastSβπ) β V) |
58 | | fvexd 6862 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (πβ((β―βπ) β 2)) β V) |
59 | | fvexd 6862 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (lastSβπ) β V) |
60 | | s2eq2s1eq 14832 |
. . . . . . 7
β’ ((((πβ((β―βπ) β 2)) β V β§
(lastSβπ) β V)
β§ ((πβ((β―βπ) β 2)) β V β§
(lastSβπ) β V))
β (β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ© = β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ© β
(β¨β(πβ((β―βπ) β 2))ββ© =
β¨β(πβ((β―βπ) β 2))ββ© β§
β¨β(lastSβπ)ββ© =
β¨β(lastSβπ)ββ©))) |
61 | 56, 57, 58, 59, 60 | syl22anc 838 |
. . . . . 6
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ© =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ© β (β¨β(πβ((β―βπ) β 2))ββ© =
β¨β(πβ((β―βπ) β 2))ββ© β§
β¨β(lastSβπ)ββ© =
β¨β(lastSβπ)ββ©))) |
62 | | fvex 6860 |
. . . . . . . . 9
β’ (πβ((β―βπ) β 2)) β
V |
63 | | s111 14510 |
. . . . . . . . 9
β’ (((πβ((β―βπ) β 2)) β V β§
(πβ((β―βπ) β 2)) β V) β
(β¨β(πβ((β―βπ) β 2))ββ© =
β¨β(πβ((β―βπ) β 2))ββ© β (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)))) |
64 | 62, 58, 63 | sylancr 588 |
. . . . . . . 8
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (β¨β(πβ((β―βπ) β 2))ββ© =
β¨β(πβ((β―βπ) β 2))ββ© β (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)))) |
65 | | fvoveq1 7385 |
. . . . . . . . . . 11
β’
((β―βπ) =
(β―βπ) β
(πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2))) |
66 | 65 | eqcoms 2745 |
. . . . . . . . . 10
β’
((β―βπ) =
(β―βπ) β
(πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2))) |
67 | 66 | adantl 483 |
. . . . . . . . 9
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2))) |
68 | 67 | eqeq2d 2748 |
. . . . . . . 8
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β ((πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)))) |
69 | 64, 68 | bitrd 279 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (β¨β(πβ((β―βπ) β 2))ββ© =
β¨β(πβ((β―βπ) β 2))ββ© β (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)))) |
70 | | fvex 6860 |
. . . . . . . 8
β’
(lastSβπ)
β V |
71 | | s111 14510 |
. . . . . . . 8
β’
(((lastSβπ)
β V β§ (lastSβπ) β V) β
(β¨β(lastSβπ)ββ© =
β¨β(lastSβπ)ββ© β (lastSβπ) = (lastSβπ))) |
72 | 70, 59, 71 | sylancr 588 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β
(β¨β(lastSβπ)ββ© =
β¨β(lastSβπ)ββ© β (lastSβπ) = (lastSβπ))) |
73 | 69, 72 | anbi12d 632 |
. . . . . 6
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β ((β¨β(πβ((β―βπ) β 2))ββ© =
β¨β(πβ((β―βπ) β 2))ββ© β§
β¨β(lastSβπ)ββ© =
β¨β(lastSβπ)ββ©) β ((πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ)))) |
74 | 55, 61, 73 | 3bitrd 305 |
. . . . 5
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β ((π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 2), (β―βπ)β©) β ((πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ)))) |
75 | 74 | anbi2d 630 |
. . . 4
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 2), (β―βπ)β©)) β ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ ((πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ))))) |
76 | | 3anass 1096 |
. . . 4
β’ (((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§
(lastSβπ) =
(lastSβπ)) β
((π prefix
((β―βπ) β
2)) = (π prefix
((β―βπ) β
2)) β§ ((πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ)))) |
77 | 75, 76 | bitr4di 289 |
. . 3
β’ (((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 2), (β―βπ)β©)) β ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ)))) |
78 | 77 | pm5.32da 580 |
. 2
β’ ((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β (((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 2), (β―βπ)β©))) β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ))))) |
79 | 38, 78 | bitrd 279 |
1
β’ ((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ))))) |