Step | Hyp | Ref
| Expression |
1 | | lsw 14461 |
. . 3
β’ (π β Word π β (lastSβπ) = (πβ((β―βπ) β 1))) |
2 | 1 | 3ad2ant1 1134 |
. 2
β’ ((π β Word π β§ β
β π β§ (β―βπ) β 0) β (lastSβπ) = (πβ((β―βπ) β 1))) |
3 | | wrdf 14416 |
. . . . . 6
β’ (π β Word π β π:(0..^(β―βπ))βΆπ) |
4 | | lencl 14430 |
. . . . . 6
β’ (π β Word π β (β―βπ) β
β0) |
5 | | simpll 766 |
. . . . . . . 8
β’ (((π:(0..^(β―βπ))βΆπ β§ (β―βπ) β β0) β§
(β―βπ) β 0)
β π:(0..^(β―βπ))βΆπ) |
6 | | elnnne0 12435 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β β ((β―βπ) β β0 β§
(β―βπ) β
0)) |
7 | 6 | biimpri 227 |
. . . . . . . . . . 11
β’
(((β―βπ)
β β0 β§ (β―βπ) β 0) β (β―βπ) β
β) |
8 | | nnm1nn0 12462 |
. . . . . . . . . . 11
β’
((β―βπ)
β β β ((β―βπ) β 1) β
β0) |
9 | 7, 8 | syl 17 |
. . . . . . . . . 10
β’
(((β―βπ)
β β0 β§ (β―βπ) β 0) β ((β―βπ) β 1) β
β0) |
10 | | nn0re 12430 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β0 β (β―βπ) β β) |
11 | 10 | ltm1d 12095 |
. . . . . . . . . . 11
β’
((β―βπ)
β β0 β ((β―βπ) β 1) < (β―βπ)) |
12 | 11 | adantr 482 |
. . . . . . . . . 10
β’
(((β―βπ)
β β0 β§ (β―βπ) β 0) β ((β―βπ) β 1) <
(β―βπ)) |
13 | | elfzo0 13622 |
. . . . . . . . . 10
β’
(((β―βπ)
β 1) β (0..^(β―βπ)) β (((β―βπ) β 1) β β0
β§ (β―βπ)
β β β§ ((β―βπ) β 1) < (β―βπ))) |
14 | 9, 7, 12, 13 | syl3anbrc 1344 |
. . . . . . . . 9
β’
(((β―βπ)
β β0 β§ (β―βπ) β 0) β ((β―βπ) β 1) β
(0..^(β―βπ))) |
15 | 14 | adantll 713 |
. . . . . . . 8
β’ (((π:(0..^(β―βπ))βΆπ β§ (β―βπ) β β0) β§
(β―βπ) β 0)
β ((β―βπ)
β 1) β (0..^(β―βπ))) |
16 | 5, 15 | ffvelcdmd 7040 |
. . . . . . 7
β’ (((π:(0..^(β―βπ))βΆπ β§ (β―βπ) β β0) β§
(β―βπ) β 0)
β (πβ((β―βπ) β 1)) β π) |
17 | 16 | ex 414 |
. . . . . 6
β’ ((π:(0..^(β―βπ))βΆπ β§ (β―βπ) β β0) β
((β―βπ) β 0
β (πβ((β―βπ) β 1)) β π)) |
18 | 3, 4, 17 | syl2anc 585 |
. . . . 5
β’ (π β Word π β ((β―βπ) β 0 β (πβ((β―βπ) β 1)) β π)) |
19 | | eleq1a 2829 |
. . . . . . . . . 10
β’ ((πβ((β―βπ) β 1)) β π β (β
= (πβ((β―βπ) β 1)) β β
β π)) |
20 | 19 | com12 32 |
. . . . . . . . 9
β’ (β
= (πβ((β―βπ) β 1)) β ((πβ((β―βπ) β 1)) β π β β
β π)) |
21 | 20 | eqcoms 2741 |
. . . . . . . 8
β’ ((πβ((β―βπ) β 1)) = β
β
((πβ((β―βπ) β 1)) β π β β
β π)) |
22 | 21 | com12 32 |
. . . . . . 7
β’ ((πβ((β―βπ) β 1)) β π β ((πβ((β―βπ) β 1)) = β
β β
β π)) |
23 | | nnel 3055 |
. . . . . . 7
β’ (Β¬
β
β π β
β
β π) |
24 | 22, 23 | syl6ibr 252 |
. . . . . 6
β’ ((πβ((β―βπ) β 1)) β π β ((πβ((β―βπ) β 1)) = β
β Β¬ β
β π)) |
25 | 24 | necon2ad 2955 |
. . . . 5
β’ ((πβ((β―βπ) β 1)) β π β (β
β π β (πβ((β―βπ) β 1)) β
β
)) |
26 | 18, 25 | syl6 35 |
. . . 4
β’ (π β Word π β ((β―βπ) β 0 β (β
β π β (πβ((β―βπ) β 1)) β
β
))) |
27 | 26 | com23 86 |
. . 3
β’ (π β Word π β (β
β π β ((β―βπ) β 0 β (πβ((β―βπ) β 1)) β
β
))) |
28 | 27 | 3imp 1112 |
. 2
β’ ((π β Word π β§ β
β π β§ (β―βπ) β 0) β (πβ((β―βπ) β 1)) β β
) |
29 | 2, 28 | eqnetrd 3008 |
1
β’ ((π β Word π β§ β
β π β§ (β―βπ) β 0) β (lastSβπ) β β
) |