Step | Hyp | Ref
| Expression |
1 | | lencl 14430 |
. . . . . . . . . . . 12
β’ (π β Word π β (β―βπ) β
β0) |
2 | | nn0cn 12431 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β0 β (β―βπ) β β) |
3 | | peano2cnm 11475 |
. . . . . . . . . . . . . . 15
β’
((β―βπ)
β β β ((β―βπ) β 1) β
β) |
4 | 3 | subid1d 11509 |
. . . . . . . . . . . . . 14
β’
((β―βπ)
β β β (((β―βπ) β 1) β 0) =
((β―βπ) β
1)) |
5 | 4 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β β ((((β―βπ) β 1) β 0) β 1) =
(((β―βπ) β
1) β 1)) |
6 | | sub1m1 12413 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β β (((β―βπ) β 1) β 1) =
((β―βπ) β
2)) |
7 | 5, 6 | eqtrd 2773 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β β ((((β―βπ) β 1) β 0) β 1) =
((β―βπ) β
2)) |
8 | 1, 2, 7 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β Word π β ((((β―βπ) β 1) β 0) β 1) =
((β―βπ) β
2)) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ (β―βπ)) β
((((β―βπ)
β 1) β 0) β 1) = ((β―βπ) β 2)) |
10 | 9 | oveq2d 7377 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ (β―βπ)) β
(0..^((((β―βπ)
β 1) β 0) β 1)) = (0..^((β―βπ) β 2))) |
11 | 10 | raleqdv 3312 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^((β―βπ) β 2)){(πβπ), (πβ(π + 1))} β ran πΈ)) |
12 | 11 | biimpcd 249 |
. . . . . . 7
β’
(βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β ((π β Word π β§ 2 β€ (β―βπ)) β βπ β
(0..^((β―βπ)
β 2)){(πβπ), (πβ(π + 1))} β ran πΈ)) |
13 | 12 | adantr 482 |
. . . . . 6
β’
((βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ) β ((π β Word π β§ 2 β€ (β―βπ)) β βπ β
(0..^((β―βπ)
β 2)){(πβπ), (πβ(π + 1))} β ran πΈ)) |
14 | 13 | adantl 483 |
. . . . 5
β’
(((lastSβπ) =
(πβ0) β§
(βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((π β Word π β§ 2 β€ (β―βπ)) β βπ β
(0..^((β―βπ)
β 2)){(πβπ), (πβ(π + 1))} β ran πΈ)) |
15 | 14 | impcom 409 |
. . . 4
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β βπ β (0..^((β―βπ) β 2)){(πβπ), (πβ(π + 1))} β ran πΈ) |
16 | | lsw 14461 |
. . . . . . . . . . . . . . . 16
β’ (π β Word π β (lastSβπ) = (πβ((β―βπ) β 1))) |
17 | | 2m1e1 12287 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (2
β 1) = 1 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Word π β (2 β 1) = 1) |
19 | 18 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Word π β 1 = (2 β 1)) |
20 | 19 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Word π β ((β―βπ) β 1) = ((β―βπ) β (2 β
1))) |
21 | 1, 2 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Word π β (β―βπ) β β) |
22 | | 2cnd 12239 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Word π β 2 β β) |
23 | | 1cnd 11158 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Word π β 1 β β) |
24 | 21, 22, 23 | subsubd 11548 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Word π β ((β―βπ) β (2 β 1)) =
(((β―βπ) β
2) + 1)) |
25 | 20, 24 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word π β ((β―βπ) β 1) = (((β―βπ) β 2) +
1)) |
26 | 25 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ (π β Word π β (πβ((β―βπ) β 1)) = (πβ(((β―βπ) β 2) + 1))) |
27 | 16, 26 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (π β Word π β (lastSβπ) = (πβ(((β―βπ) β 2) + 1))) |
28 | 27 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (lastSβπ) = (πβ(((β―βπ) β 2) + 1))) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β (lastSβπ) = (πβ(((β―βπ) β 2) + 1))) |
30 | | eqeq1 2737 |
. . . . . . . . . . . . . 14
β’
((lastSβπ) =
(πβ0) β
((lastSβπ) = (πβ(((β―βπ) β 2) + 1)) β (πβ0) = (πβ(((β―βπ) β 2) + 1)))) |
31 | 30 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β ((lastSβπ) = (πβ(((β―βπ) β 2) + 1)) β (πβ0) = (πβ(((β―βπ) β 2) + 1)))) |
32 | 29, 31 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β (πβ0) = (πβ(((β―βπ) β 2) + 1))) |
33 | 32 | preq2d 4705 |
. . . . . . . . . . 11
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))}) |
34 | 33 | eleq1d 2819 |
. . . . . . . . . 10
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β ({(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} β ran πΈ)) |
35 | 34 | biimpd 228 |
. . . . . . . . 9
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β ({(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} β ran πΈ)) |
36 | 35 | ex 414 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((lastSβπ) = (πβ0) β ({(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} β ran πΈ))) |
37 | 36 | com13 88 |
. . . . . . 7
β’ ({(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ β ((lastSβπ) = (πβ0) β ((π β Word π β§ 2 β€ (β―βπ)) β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} β ran πΈ))) |
38 | 37 | adantl 483 |
. . . . . 6
β’
((βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ) β ((lastSβπ) = (πβ0) β ((π β Word π β§ 2 β€ (β―βπ)) β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} β ran πΈ))) |
39 | 38 | impcom 409 |
. . . . 5
β’
(((lastSβπ) =
(πβ0) β§
(βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((π β Word π β§ 2 β€ (β―βπ)) β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} β ran πΈ)) |
40 | 39 | impcom 409 |
. . . 4
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} β ran πΈ) |
41 | | ovexd 7396 |
. . . . 5
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β ((β―βπ) β 2) β V) |
42 | | fveq2 6846 |
. . . . . . . 8
β’ (π = ((β―βπ) β 2) β (πβπ) = (πβ((β―βπ) β 2))) |
43 | | fvoveq1 7384 |
. . . . . . . 8
β’ (π = ((β―βπ) β 2) β (πβ(π + 1)) = (πβ(((β―βπ) β 2) + 1))) |
44 | 42, 43 | preq12d 4706 |
. . . . . . 7
β’ (π = ((β―βπ) β 2) β {(πβπ), (πβ(π + 1))} = {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))}) |
45 | 44 | eleq1d 2819 |
. . . . . 6
β’ (π = ((β―βπ) β 2) β ({(πβπ), (πβ(π + 1))} β ran πΈ β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} β ran πΈ)) |
46 | 45 | ralunsn 4855 |
. . . . 5
β’
(((β―βπ)
β 2) β V β (βπ β ((0..^((β―βπ) β 2)) βͺ
{((β―βπ) β
2)}){(πβπ), (πβ(π + 1))} β ran πΈ β (βπ β (0..^((β―βπ) β 2)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} β ran πΈ))) |
47 | 41, 46 | syl 17 |
. . . 4
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β (βπ β ((0..^((β―βπ) β 2)) βͺ
{((β―βπ) β
2)}){(πβπ), (πβ(π + 1))} β ran πΈ β (βπ β (0..^((β―βπ) β 2)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} β ran πΈ))) |
48 | 15, 40, 47 | mpbir2and 712 |
. . 3
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β βπ β ((0..^((β―βπ) β 2)) βͺ
{((β―βπ) β
2)}){(πβπ), (πβ(π + 1))} β ran πΈ) |
49 | | 1e2m1 12288 |
. . . . . . . . . . 11
β’ 1 = (2
β 1) |
50 | 49 | a1i 11 |
. . . . . . . . . 10
β’ (π β Word π β 1 = (2 β 1)) |
51 | 50 | oveq2d 7377 |
. . . . . . . . 9
β’ (π β Word π β ((β―βπ) β 1) = ((β―βπ) β (2 β
1))) |
52 | 51, 24 | eqtrd 2773 |
. . . . . . . 8
β’ (π β Word π β ((β―βπ) β 1) = (((β―βπ) β 2) +
1)) |
53 | 52 | oveq2d 7377 |
. . . . . . 7
β’ (π β Word π β (0..^((β―βπ) β 1)) =
(0..^(((β―βπ)
β 2) + 1))) |
54 | 53 | adantr 482 |
. . . . . 6
β’ ((π β Word π β§ 2 β€ (β―βπ)) β
(0..^((β―βπ)
β 1)) = (0..^(((β―βπ) β 2) + 1))) |
55 | | nn0re 12430 |
. . . . . . . . . . . . . 14
β’
((β―βπ)
β β0 β (β―βπ) β β) |
56 | | 2re 12235 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . 14
β’
((β―βπ)
β β0 β 2 β β) |
58 | 55, 57 | subge0d 11753 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β0 β (0 β€ ((β―βπ) β 2) β 2 β€
(β―βπ))) |
59 | 58 | biimprd 248 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β0 β (2 β€ (β―βπ) β 0 β€ ((β―βπ) β 2))) |
60 | | nn0z 12532 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β0 β (β―βπ) β β€) |
61 | | 2z 12543 |
. . . . . . . . . . . . . 14
β’ 2 β
β€ |
62 | 61 | a1i 11 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β0 β 2 β β€) |
63 | 60, 62 | zsubcld 12620 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β0 β ((β―βπ) β 2) β
β€) |
64 | 59, 63 | jctild 527 |
. . . . . . . . . . 11
β’
((β―βπ)
β β0 β (2 β€ (β―βπ) β (((β―βπ) β 2) β β€ β§ 0 β€
((β―βπ) β
2)))) |
65 | 1, 64 | syl 17 |
. . . . . . . . . 10
β’ (π β Word π β (2 β€ (β―βπ) β (((β―βπ) β 2) β β€
β§ 0 β€ ((β―βπ) β 2)))) |
66 | 65 | imp 408 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (((β―βπ) β 2) β β€
β§ 0 β€ ((β―βπ) β 2))) |
67 | | elnn0z 12520 |
. . . . . . . . 9
β’
(((β―βπ)
β 2) β β0 β (((β―βπ) β 2) β β€ β§ 0 β€
((β―βπ) β
2))) |
68 | 66, 67 | sylibr 233 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((β―βπ) β 2) β
β0) |
69 | | elnn0uz 12816 |
. . . . . . . 8
β’
(((β―βπ)
β 2) β β0 β ((β―βπ) β 2) β
(β€β₯β0)) |
70 | 68, 69 | sylib 217 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((β―βπ) β 2) β
(β€β₯β0)) |
71 | | fzosplitsn 13689 |
. . . . . . 7
β’
(((β―βπ)
β 2) β (β€β₯β0) β
(0..^(((β―βπ)
β 2) + 1)) = ((0..^((β―βπ) β 2)) βͺ {((β―βπ) β 2)})) |
72 | 70, 71 | syl 17 |
. . . . . 6
β’ ((π β Word π β§ 2 β€ (β―βπ)) β
(0..^(((β―βπ)
β 2) + 1)) = ((0..^((β―βπ) β 2)) βͺ {((β―βπ) β 2)})) |
73 | 54, 72 | eqtrd 2773 |
. . . . 5
β’ ((π β Word π β§ 2 β€ (β―βπ)) β
(0..^((β―βπ)
β 1)) = ((0..^((β―βπ) β 2)) βͺ {((β―βπ) β 2)})) |
74 | 73 | adantr 482 |
. . . 4
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β (0..^((β―βπ) β 1)) =
((0..^((β―βπ)
β 2)) βͺ {((β―βπ) β 2)})) |
75 | 74 | raleqdv 3312 |
. . 3
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β ((0..^((β―βπ) β 2)) βͺ
{((β―βπ) β
2)}){(πβπ), (πβ(π + 1))} β ran πΈ)) |
76 | 48, 75 | mpbird 257 |
. 2
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ) |
77 | 76 | ex 414 |
1
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ)) |