Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ ((π β Word π β§ 1 < (β―βπ)) β π β Word π) |
2 | | lencl 14428 |
. . . . 5
β’ (π β Word π β (β―βπ) β
β0) |
3 | | 1z 12540 |
. . . . . . . . 9
β’ 1 β
β€ |
4 | | nn0z 12531 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β (β―βπ) β β€) |
5 | | zltp1le 12560 |
. . . . . . . . 9
β’ ((1
β β€ β§ (β―βπ) β β€) β (1 <
(β―βπ) β (1
+ 1) β€ (β―βπ))) |
6 | 3, 4, 5 | sylancr 588 |
. . . . . . . 8
β’
((β―βπ)
β β0 β (1 < (β―βπ) β (1 + 1) β€ (β―βπ))) |
7 | | 1p1e2 12285 |
. . . . . . . . . . 11
β’ (1 + 1) =
2 |
8 | 7 | a1i 11 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β (1 + 1) = 2) |
9 | 8 | breq1d 5120 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β ((1 + 1) β€ (β―βπ) β 2 β€
(β―βπ))) |
10 | 9 | biimpd 228 |
. . . . . . . 8
β’
((β―βπ)
β β0 β ((1 + 1) β€ (β―βπ) β 2 β€
(β―βπ))) |
11 | 6, 10 | sylbid 239 |
. . . . . . 7
β’
((β―βπ)
β β0 β (1 < (β―βπ) β 2 β€ (β―βπ))) |
12 | 11 | imp 408 |
. . . . . 6
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β 2 β€ (β―βπ)) |
13 | | 2nn0 12437 |
. . . . . . . . 9
β’ 2 β
β0 |
14 | 13 | jctl 525 |
. . . . . . . 8
β’
((β―βπ)
β β0 β (2 β β0 β§
(β―βπ) β
β0)) |
15 | 14 | adantr 482 |
. . . . . . 7
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β (2 β β0
β§ (β―βπ)
β β0)) |
16 | | nn0sub 12470 |
. . . . . . 7
β’ ((2
β β0 β§ (β―βπ) β β0) β (2 β€
(β―βπ) β
((β―βπ) β
2) β β0)) |
17 | 15, 16 | syl 17 |
. . . . . 6
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β (2 β€ (β―βπ) β ((β―βπ) β 2) β
β0)) |
18 | 12, 17 | mpbid 231 |
. . . . 5
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β ((β―βπ) β 2) β
β0) |
19 | 2, 18 | sylan 581 |
. . . 4
β’ ((π β Word π β§ 1 < (β―βπ)) β ((β―βπ) β 2) β
β0) |
20 | | 0red 11165 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β€ β 0 β β) |
21 | | 1red 11163 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β€ β 1 β β) |
22 | | zre 12510 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β€ β (β―βπ) β β) |
23 | 20, 21, 22 | 3jca 1129 |
. . . . . . . . . . 11
β’
((β―βπ)
β β€ β (0 β β β§ 1 β β β§
(β―βπ) β
β)) |
24 | | 0lt1 11684 |
. . . . . . . . . . 11
β’ 0 <
1 |
25 | | lttr 11238 |
. . . . . . . . . . . 12
β’ ((0
β β β§ 1 β β β§ (β―βπ) β β) β ((0 < 1 β§ 1
< (β―βπ))
β 0 < (β―βπ))) |
26 | 25 | expd 417 |
. . . . . . . . . . 11
β’ ((0
β β β§ 1 β β β§ (β―βπ) β β) β (0 < 1 β (1
< (β―βπ)
β 0 < (β―βπ)))) |
27 | 23, 24, 26 | mpisyl 21 |
. . . . . . . . . 10
β’
((β―βπ)
β β€ β (1 < (β―βπ) β 0 < (β―βπ))) |
28 | | elnnz 12516 |
. . . . . . . . . . 11
β’
((β―βπ)
β β β ((β―βπ) β β€ β§ 0 <
(β―βπ))) |
29 | 28 | simplbi2 502 |
. . . . . . . . . 10
β’
((β―βπ)
β β€ β (0 < (β―βπ) β (β―βπ) β β)) |
30 | 27, 29 | syld 47 |
. . . . . . . . 9
β’
((β―βπ)
β β€ β (1 < (β―βπ) β (β―βπ) β β)) |
31 | 4, 30 | syl 17 |
. . . . . . . 8
β’
((β―βπ)
β β0 β (1 < (β―βπ) β (β―βπ) β β)) |
32 | 31 | imp 408 |
. . . . . . 7
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β (β―βπ) β β) |
33 | | fzo0end 13671 |
. . . . . . 7
β’
((β―βπ)
β β β ((β―βπ) β 1) β
(0..^(β―βπ))) |
34 | 32, 33 | syl 17 |
. . . . . 6
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β ((β―βπ) β 1) β
(0..^(β―βπ))) |
35 | | nn0cn 12430 |
. . . . . . . . . . 11
β’
((β―βπ)
β β0 β (β―βπ) β β) |
36 | | 2cn 12235 |
. . . . . . . . . . . 12
β’ 2 β
β |
37 | 36 | a1i 11 |
. . . . . . . . . . 11
β’
((β―βπ)
β β0 β 2 β β) |
38 | | 1cnd 11157 |
. . . . . . . . . . 11
β’
((β―βπ)
β β0 β 1 β β) |
39 | 35, 37, 38 | 3jca 1129 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β ((β―βπ) β β β§ 2 β β
β§ 1 β β)) |
40 | | 1e2m1 12287 |
. . . . . . . . . . . . 13
β’ 1 = (2
β 1) |
41 | 40 | a1i 11 |
. . . . . . . . . . . 12
β’
(((β―βπ)
β β β§ 2 β β β§ 1 β β) β 1 = (2
β 1)) |
42 | 41 | oveq2d 7378 |
. . . . . . . . . . 11
β’
(((β―βπ)
β β β§ 2 β β β§ 1 β β) β
((β―βπ) β
1) = ((β―βπ)
β (2 β 1))) |
43 | | subsub 11438 |
. . . . . . . . . . 11
β’
(((β―βπ)
β β β§ 2 β β β§ 1 β β) β
((β―βπ) β
(2 β 1)) = (((β―βπ) β 2) + 1)) |
44 | 42, 43 | eqtrd 2777 |
. . . . . . . . . 10
β’
(((β―βπ)
β β β§ 2 β β β§ 1 β β) β
((β―βπ) β
1) = (((β―βπ)
β 2) + 1)) |
45 | 39, 44 | syl 17 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β ((β―βπ) β 1) = (((β―βπ) β 2) +
1)) |
46 | 45 | eqcomd 2743 |
. . . . . . . 8
β’
((β―βπ)
β β0 β (((β―βπ) β 2) + 1) = ((β―βπ) β 1)) |
47 | 46 | eleq1d 2823 |
. . . . . . 7
β’
((β―βπ)
β β0 β ((((β―βπ) β 2) + 1) β
(0..^(β―βπ))
β ((β―βπ)
β 1) β (0..^(β―βπ)))) |
48 | 47 | adantr 482 |
. . . . . 6
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β ((((β―βπ) β 2) + 1) β
(0..^(β―βπ))
β ((β―βπ)
β 1) β (0..^(β―βπ)))) |
49 | 34, 48 | mpbird 257 |
. . . . 5
β’
(((β―βπ)
β β0 β§ 1 < (β―βπ)) β (((β―βπ) β 2) + 1) β
(0..^(β―βπ))) |
50 | 2, 49 | sylan 581 |
. . . 4
β’ ((π β Word π β§ 1 < (β―βπ)) β (((β―βπ) β 2) + 1) β
(0..^(β―βπ))) |
51 | 1, 19, 50 | 3jca 1129 |
. . 3
β’ ((π β Word π β§ 1 < (β―βπ)) β (π β Word π β§ ((β―βπ) β 2) β β0
β§ (((β―βπ)
β 2) + 1) β (0..^(β―βπ)))) |
52 | | swrds2 14836 |
. . 3
β’ ((π β Word π β§ ((β―βπ) β 2) β β0
β§ (((β―βπ)
β 2) + 1) β (0..^(β―βπ))) β (π substr β¨((β―βπ) β 2),
(((β―βπ) β
2) + 2)β©) = β¨β(πβ((β―βπ) β 2))(πβ(((β―βπ) β 2) +
1))ββ©) |
53 | 51, 52 | syl 17 |
. 2
β’ ((π β Word π β§ 1 < (β―βπ)) β (π substr β¨((β―βπ) β 2),
(((β―βπ) β
2) + 2)β©) = β¨β(πβ((β―βπ) β 2))(πβ(((β―βπ) β 2) +
1))ββ©) |
54 | 35, 36 | jctir 522 |
. . . . . 6
β’
((β―βπ)
β β0 β ((β―βπ) β β β§ 2 β
β)) |
55 | | npcan 11417 |
. . . . . . 7
β’
(((β―βπ)
β β β§ 2 β β) β (((β―βπ) β 2) + 2) =
(β―βπ)) |
56 | 55 | eqcomd 2743 |
. . . . . 6
β’
(((β―βπ)
β β β§ 2 β β) β (β―βπ) = (((β―βπ) β 2) + 2)) |
57 | 2, 54, 56 | 3syl 18 |
. . . . 5
β’ (π β Word π β (β―βπ) = (((β―βπ) β 2) + 2)) |
58 | 57 | adantr 482 |
. . . 4
β’ ((π β Word π β§ 1 < (β―βπ)) β (β―βπ) = (((β―βπ) β 2) +
2)) |
59 | 58 | opeq2d 4842 |
. . 3
β’ ((π β Word π β§ 1 < (β―βπ)) β
β¨((β―βπ)
β 2), (β―βπ)β© = β¨((β―βπ) β 2),
(((β―βπ) β
2) + 2)β©) |
60 | 59 | oveq2d 7378 |
. 2
β’ ((π β Word π β§ 1 < (β―βπ)) β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 2), (((β―βπ) β 2) + 2)β©)) |
61 | | eqidd 2738 |
. . 3
β’ ((π β Word π β§ 1 < (β―βπ)) β (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2))) |
62 | | lsw 14459 |
. . . . 5
β’ (π β Word π β (lastSβπ) = (πβ((β―βπ) β 1))) |
63 | 39, 43 | syl 17 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β ((β―βπ) β (2 β 1)) =
(((β―βπ) β
2) + 1)) |
64 | 63 | eqcomd 2743 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β (((β―βπ) β 2) + 1) = ((β―βπ) β (2 β
1))) |
65 | | 2m1e1 12286 |
. . . . . . . . . . 11
β’ (2
β 1) = 1 |
66 | 65 | a1i 11 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β (2 β 1) = 1) |
67 | 66 | oveq2d 7378 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β ((β―βπ) β (2 β 1)) =
((β―βπ) β
1)) |
68 | 64, 67 | eqtrd 2777 |
. . . . . . . 8
β’
((β―βπ)
β β0 β (((β―βπ) β 2) + 1) = ((β―βπ) β 1)) |
69 | 2, 68 | syl 17 |
. . . . . . 7
β’ (π β Word π β (((β―βπ) β 2) + 1) = ((β―βπ) β 1)) |
70 | 69 | eqcomd 2743 |
. . . . . 6
β’ (π β Word π β ((β―βπ) β 1) = (((β―βπ) β 2) +
1)) |
71 | 70 | fveq2d 6851 |
. . . . 5
β’ (π β Word π β (πβ((β―βπ) β 1)) = (πβ(((β―βπ) β 2) + 1))) |
72 | 62, 71 | eqtrd 2777 |
. . . 4
β’ (π β Word π β (lastSβπ) = (πβ(((β―βπ) β 2) + 1))) |
73 | 72 | adantr 482 |
. . 3
β’ ((π β Word π β§ 1 < (β―βπ)) β (lastSβπ) = (πβ(((β―βπ) β 2) + 1))) |
74 | 61, 73 | s2eqd 14759 |
. 2
β’ ((π β Word π β§ 1 < (β―βπ)) β β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ© =
β¨β(πβ((β―βπ) β 2))(πβ(((β―βπ) β 2) +
1))ββ©) |
75 | 53, 60, 74 | 3eqtr4d 2787 |
1
β’ ((π β Word π β§ 1 < (β―βπ)) β (π substr β¨((β―βπ) β 2),
(β―βπ)β©) =
β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©) |