Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . . . . 10
β’ ((π₯ < ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β π₯ < ((β―βπ) β 2)) |
2 | | f1f1orn 6800 |
. . . . . . . . . . . . . 14
β’ (πΈ:dom πΈβ1-1βπ
β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
3 | 2 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
4 | 3 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
5 | 4 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π₯ < ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
6 | | elfzo0 13620 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β
(0..^((β―βπ)
β 1)) β (π₯
β β0 β§ ((β―βπ) β 1) β β β§ π₯ < ((β―βπ) β 1))) |
7 | | lencl 14428 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β Word π β (β―βπ) β
β0) |
8 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β π₯ β β0) |
9 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π₯ β β0
β§ (β―βπ)
β β0) β§ (π₯ < ((β―βπ) β 2) β§ 2 β€
(β―βπ))) β
π₯ β
β0) |
10 | | elnn0z 12519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π₯ β β0
β (π₯ β β€
β§ 0 β€ π₯)) |
11 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π₯ β β€ β§
(β―βπ) β
β0) β 0 β β) |
12 | | zre 12510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π₯ β β€ β π₯ β
β) |
13 | 12 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π₯ β β€ β§
(β―βπ) β
β0) β π₯ β β) |
14 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
((β―βπ)
β β0 β (β―βπ) β β) |
15 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ 2 β
β |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
((β―βπ)
β β0 β 2 β β) |
17 | 14, 16 | resubcld 11590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’
((β―βπ)
β β0 β ((β―βπ) β 2) β
β) |
18 | 17 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π₯ β β€ β§
(β―βπ) β
β0) β ((β―βπ) β 2) β
β) |
19 | | lelttr 11252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((0
β β β§ π₯
β β β§ ((β―βπ) β 2) β β) β ((0 β€
π₯ β§ π₯ < ((β―βπ) β 2)) β 0 <
((β―βπ) β
2))) |
20 | 11, 13, 18, 19 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π₯ β β€ β§
(β―βπ) β
β0) β ((0 β€ π₯ β§ π₯ < ((β―βπ) β 2)) β 0 <
((β―βπ) β
2))) |
21 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’
((β―βπ)
β β0 β (β―βπ) β β€) |
22 | | 2z 12542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’ 2 β
β€ |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’
((β―βπ)
β β0 β 2 β β€) |
24 | 21, 23 | zsubcld 12619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’
((β―βπ)
β β0 β ((β―βπ) β 2) β
β€) |
25 | 24 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’
(((β―βπ)
β β0 β§ 0 < ((β―βπ) β 2)) β (((β―βπ) β 2) β β€
β§ 0 < ((β―βπ) β 2))) |
26 | | elnnz 12516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’
(((β―βπ)
β 2) β β β (((β―βπ) β 2) β β€ β§ 0 <
((β―βπ) β
2))) |
27 | 25, 26 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
(((β―βπ)
β β0 β§ 0 < ((β―βπ) β 2)) β ((β―βπ) β 2) β
β) |
28 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
β’
((β―βπ)
β β0 β (β―βπ) β β) |
29 | | peano2cnm 11474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
β’
((β―βπ)
β β β ((β―βπ) β 1) β
β) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
β’
((β―βπ)
β β0 β ((β―βπ) β 1) β
β) |
31 | 30 | subid1d 11508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’
((β―βπ)
β β0 β (((β―βπ) β 1) β 0) =
((β―βπ) β
1)) |
32 | 31 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’
((β―βπ)
β β0 β ((((β―βπ) β 1) β 0) β 1) =
(((β―βπ) β
1) β 1)) |
33 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
β’
((β―βπ)
β β0 β 1 β β) |
34 | 28, 33, 33 | subsub4d 11550 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’
((β―βπ)
β β0 β (((β―βπ) β 1) β 1) =
((β―βπ) β
(1 + 1))) |
35 | | 1p1e2 12285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
β’ (1 + 1) =
2 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
β’
((β―βπ)
β β0 β (1 + 1) = 2) |
37 | 36 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’
((β―βπ)
β β0 β ((β―βπ) β (1 + 1)) = ((β―βπ) β 2)) |
38 | 34, 37 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’
((β―βπ)
β β0 β (((β―βπ) β 1) β 1) =
((β―βπ) β
2)) |
39 | 32, 38 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’
((β―βπ)
β β0 β ((((β―βπ) β 1) β 0) β 1) =
((β―βπ) β
2)) |
40 | 39 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’
((β―βπ)
β β0 β (((((β―βπ) β 1) β 0) β 1) β
β β ((β―βπ) β 2) β
β)) |
41 | 40 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
(((β―βπ)
β β0 β§ 0 < ((β―βπ) β 2)) β
(((((β―βπ)
β 1) β 0) β 1) β β β ((β―βπ) β 2) β
β)) |
42 | 27, 41 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’
(((β―βπ)
β β0 β§ 0 < ((β―βπ) β 2)) β ((((β―βπ) β 1) β 0) β
1) β β) |
43 | 42 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’
((β―βπ)
β β0 β (0 < ((β―βπ) β 2) β ((((β―βπ) β 1) β 0) β
1) β β)) |
44 | 43 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π₯ β β€ β§
(β―βπ) β
β0) β (0 < ((β―βπ) β 2) β ((((β―βπ) β 1) β 0) β
1) β β)) |
45 | 20, 44 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π₯ β β€ β§
(β―βπ) β
β0) β ((0 β€ π₯ β§ π₯ < ((β―βπ) β 2)) β ((((β―βπ) β 1) β 0) β
1) β β)) |
46 | 45 | exp4b 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π₯ β β€ β
((β―βπ) β
β0 β (0 β€ π₯ β (π₯ < ((β―βπ) β 2) β ((((β―βπ) β 1) β 0) β
1) β β)))) |
47 | 46 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π₯ β β€ β (0 β€
π₯ β
((β―βπ) β
β0 β (π₯ < ((β―βπ) β 2) β ((((β―βπ) β 1) β 0) β
1) β β)))) |
48 | 47 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π₯ β β€ β§ 0 β€
π₯) β
((β―βπ) β
β0 β (π₯ < ((β―βπ) β 2) β ((((β―βπ) β 1) β 0) β
1) β β))) |
49 | 10, 48 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π₯ β β0
β ((β―βπ)
β β0 β (π₯ < ((β―βπ) β 2) β ((((β―βπ) β 1) β 0) β
1) β β))) |
50 | 49 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (π₯ < ((β―βπ) β 2) β ((((β―βπ) β 1) β 0) β
1) β β)) |
51 | 50 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π₯ < ((β―βπ) β 2) β ((π₯ β β0
β§ (β―βπ)
β β0) β ((((β―βπ) β 1) β 0) β 1) β
β)) |
52 | 51 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π₯ < ((β―βπ) β 2) β§ 2 β€
(β―βπ)) β
((π₯ β
β0 β§ (β―βπ) β β0) β
((((β―βπ)
β 1) β 0) β 1) β β)) |
53 | 52 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π₯ β β0
β§ (β―βπ)
β β0) β§ (π₯ < ((β―βπ) β 2) β§ 2 β€
(β―βπ))) β
((((β―βπ)
β 1) β 0) β 1) β β) |
54 | | df-2 12223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ 2 = (1 +
1) |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((β―βπ)
β β0 β 2 = (1 + 1)) |
56 | 55 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((β―βπ)
β β0 β ((β―βπ) β 2) = ((β―βπ) β (1 +
1))) |
57 | 31 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((β―βπ)
β β0 β ((β―βπ) β 1) = (((β―βπ) β 1) β
0)) |
58 | 57 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((β―βπ)
β β0 β (((β―βπ) β 1) β 1) =
((((β―βπ)
β 1) β 0) β 1)) |
59 | 56, 34, 58 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((β―βπ)
β β0 β ((β―βπ) β 2) = ((((β―βπ) β 1) β 0) β
1)) |
60 | 59 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β ((β―βπ) β 2) = ((((β―βπ) β 1) β 0) β
1)) |
61 | 60 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (π₯ < ((β―βπ) β 2) β π₯ < ((((β―βπ) β 1) β 0) β
1))) |
62 | 61 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π₯ < ((β―βπ) β 2) β ((π₯ β β0
β§ (β―βπ)
β β0) β π₯ < ((((β―βπ) β 1) β 0) β
1))) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π₯ < ((β―βπ) β 2) β§ 2 β€
(β―βπ)) β
((π₯ β
β0 β§ (β―βπ) β β0) β π₯ < ((((β―βπ) β 1) β 0) β
1))) |
64 | 63 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π₯ β β0
β§ (β―βπ)
β β0) β§ (π₯ < ((β―βπ) β 2) β§ 2 β€
(β―βπ))) β
π₯ <
((((β―βπ)
β 1) β 0) β 1)) |
65 | | elfzo0 13620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1)) β (π₯ β β0 β§
((((β―βπ)
β 1) β 0) β 1) β β β§ π₯ < ((((β―βπ) β 1) β 0) β
1))) |
66 | 9, 53, 64, 65 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π₯ β β0
β§ (β―βπ)
β β0) β§ (π₯ < ((β―βπ) β 2) β§ 2 β€
(β―βπ))) β
π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1))) |
67 | 66 | exp32 422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (π₯ < ((β―βπ) β 2) β (2 β€
(β―βπ) β
π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1))))) |
68 | 67 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (π₯ < ((β―βπ) β 1) β (π₯ < ((β―βπ) β 2) β (2 β€
(β―βπ) β
π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1)))))) |
69 | 68 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (2 β€ (β―βπ) β (π₯ < ((β―βπ) β 2) β (π₯ < ((β―βπ) β 1) β π₯ β (0..^((((β―βπ) β 1) β 0) β
1)))))) |
70 | 69 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π₯ β β0
β ((β―βπ)
β β0 β (2 β€ (β―βπ) β (π₯ < ((β―βπ) β 2) β (π₯ < ((β―βπ) β 1) β π₯ β (0..^((((β―βπ) β 1) β 0) β
1))))))) |
71 | 70 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ β β0
β (π₯ <
((β―βπ) β
1) β (2 β€ (β―βπ) β (π₯ < ((β―βπ) β 2) β ((β―βπ) β β0
β π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1))))))) |
72 | 71 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β (2 β€ (β―βπ) β (π₯ < ((β―βπ) β 2) β ((β―βπ) β β0
β π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1)))))) |
73 | 72 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π₯ β β0
β§ ((β―βπ)
β 1) β β β§ π₯ < ((β―βπ) β 1)) β (2 β€
(β―βπ) β
(π₯ <
((β―βπ) β
2) β ((β―βπ) β β0 β π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1)))))) |
74 | 73 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ)
β β0 β (2 β€ (β―βπ) β (π₯ < ((β―βπ) β 2) β ((π₯ β β0 β§
((β―βπ) β
1) β β β§ π₯
< ((β―βπ)
β 1)) β π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1)))))) |
75 | 7, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β Word π β (2 β€ (β―βπ) β (π₯ < ((β―βπ) β 2) β ((π₯ β β0 β§
((β―βπ) β
1) β β β§ π₯
< ((β―βπ)
β 1)) β π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1)))))) |
76 | 75 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (π₯ < ((β―βπ) β 2) β ((π₯ β β0 β§
((β―βπ) β
1) β β β§ π₯
< ((β―βπ)
β 1)) β π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1))))) |
77 | 76 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (π₯ < ((β―βπ) β 2) β ((π₯ β β0 β§
((β―βπ) β
1) β β β§ π₯
< ((β―βπ)
β 1)) β π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1))))) |
78 | 6, 77 | syl7bi 255 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (π₯ < ((β―βπ) β 2) β (π₯ β (0..^((β―βπ) β 1)) β π₯ β
(0..^((((β―βπ)
β 1) β 0) β 1))))) |
79 | 78 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β
(0..^((β―βπ)
β 1)) β (π₯ <
((β―βπ) β
2) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β π₯ β (0..^((((β―βπ) β 1) β 0) β
1))))) |
80 | 79 | imp31 419 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β
(0..^((β―βπ)
β 1)) β§ π₯ <
((β―βπ) β
2)) β§ (πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ))) β π₯ β (0..^((((β―βπ) β 1) β 0) β
1))) |
81 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π₯ β (πβπ) = (πβπ₯)) |
82 | | fvoveq1 7385 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π₯ β (πβ(π + 1)) = (πβ(π₯ + 1))) |
83 | 81, 82 | preq12d 4707 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π₯ β {(πβπ), (πβ(π + 1))} = {(πβπ₯), (πβ(π₯ + 1))}) |
84 | 83 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π₯ β ({(πβπ), (πβ(π + 1))} β ran πΈ β {(πβπ₯), (πβ(π₯ + 1))} β ran πΈ)) |
85 | 84 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π₯ β
(0..^((β―βπ)
β 1)) β§ π₯ <
((β―βπ) β
2)) β§ (πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ))) β§ π = π₯) β ({(πβπ), (πβ(π + 1))} β ran πΈ β {(πβπ₯), (πβ(π₯ + 1))} β ran πΈ)) |
86 | 80, 85 | rspcdv 3576 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β
(0..^((β―βπ)
β 1)) β§ π₯ <
((β―βπ) β
2)) β§ (πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ))) β (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β {(πβπ₯), (πβ(π₯ + 1))} β ran πΈ)) |
87 | 86 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β
(0..^((β―βπ)
β 1)) β§ π₯ <
((β―βπ) β
2)) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β {(πβπ₯), (πβ(π₯ + 1))} β ran πΈ))) |
88 | 87 | com13 88 |
. . . . . . . . . . . . . . 15
β’
(βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β ((π₯ β (0..^((β―βπ) β 1)) β§ π₯ < ((β―βπ) β 2)) β {(πβπ₯), (πβ(π₯ + 1))} β ran πΈ))) |
89 | 88 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’
(((lastSβπ) =
(πβ0) β§
(βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β ((π₯ β (0..^((β―βπ) β 1)) β§ π₯ < ((β―βπ) β 2)) β {(πβπ₯), (πβ(π₯ + 1))} β ran πΈ))) |
90 | 89 | impcom 409 |
. . . . . . . . . . . . 13
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β ((π₯ β (0..^((β―βπ) β 1)) β§ π₯ < ((β―βπ) β 2)) β {(πβπ₯), (πβ(π₯ + 1))} β ran πΈ)) |
91 | 90 | expdimp 454 |
. . . . . . . . . . . 12
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1))) β (π₯ < ((β―βπ) β 2) β {(πβπ₯), (πβ(π₯ + 1))} β ran πΈ)) |
92 | 91 | impcom 409 |
. . . . . . . . . . 11
β’ ((π₯ < ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β {(πβπ₯), (πβ(π₯ + 1))} β ran πΈ) |
93 | | f1ocnvdm 7236 |
. . . . . . . . . . 11
β’ ((πΈ:dom πΈβ1-1-ontoβran
πΈ β§ {(πβπ₯), (πβ(π₯ + 1))} β ran πΈ) β (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}) β dom πΈ) |
94 | 5, 92, 93 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π₯ < ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}) β dom πΈ) |
95 | 1, 94 | jca 513 |
. . . . . . . . 9
β’ ((π₯ < ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β (π₯ < ((β―βπ) β 2) β§ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}) β dom πΈ)) |
96 | 95 | orcd 872 |
. . . . . . . 8
β’ ((π₯ < ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β ((π₯ < ((β―βπ) β 2) β§ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}) β dom πΈ) β¨ (Β¬ π₯ < ((β―βπ) β 2) β§ (β‘πΈβ{(πβπ₯), (πβ0)}) β dom πΈ))) |
97 | | simpl 484 |
. . . . . . . . . 10
β’ ((Β¬
π₯ <
((β―βπ) β
2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β Β¬
π₯ <
((β―βπ) β
2)) |
98 | 4 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((Β¬
π₯ <
((β―βπ) β
2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
99 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π₯ β β0
β π₯ β
β€) |
100 | | peano2zm 12553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((β―βπ)
β β€ β ((β―βπ) β 1) β
β€) |
101 | 21, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((β―βπ)
β β0 β ((β―βπ) β 1) β
β€) |
102 | 99, 101 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (π₯ β β€ β§ ((β―βπ) β 1) β
β€)) |
103 | | zltlem1 12563 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π₯ β β€ β§
((β―βπ) β
1) β β€) β (π₯ < ((β―βπ) β 1) β π₯ β€ (((β―βπ) β 1) β 1))) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (π₯ < ((β―βπ) β 1) β π₯ β€ (((β―βπ) β 1) β 1))) |
105 | 38 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (((β―βπ) β 1) β 1) =
((β―βπ) β
2)) |
106 | 105 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (π₯ β€ (((β―βπ) β 1) β 1) β π₯ β€ ((β―βπ) β 2))) |
107 | 106 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (π₯ β€ (((β―βπ) β 1) β 1) β π₯ β€ ((β―βπ) β 2))) |
108 | 104, 107 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π₯ β β0
β§ (β―βπ)
β β0) β (π₯ < ((β―βπ) β 1) β π₯ β€ ((β―βπ) β 2))) |
109 | 108 | impancom 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β ((β―βπ) β β0 β π₯ β€ ((β―βπ) β 2))) |
110 | 109 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β§ (β―βπ)
β β0) β π₯ β€ ((β―βπ) β 2)) |
111 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π₯ β β0
β π₯ β
β) |
112 | 111 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β π₯ β
β) |
113 | 112, 17 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β§ (β―βπ)
β β0) β (π₯ β β β§ ((β―βπ) β 2) β
β)) |
114 | | lenlt 11240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π₯ β β β§
((β―βπ) β
2) β β) β (π₯ β€ ((β―βπ) β 2) β Β¬
((β―βπ) β
2) < π₯)) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β§ (β―βπ)
β β0) β (π₯ β€ ((β―βπ) β 2) β Β¬
((β―βπ) β
2) < π₯)) |
116 | 110, 115 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β§ (β―βπ)
β β0) β Β¬ ((β―βπ) β 2) < π₯) |
117 | 116 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β§ (β―βπ)
β β0) β§ Β¬ π₯ < ((β―βπ) β 2)) β (Β¬
((β―βπ) β
2) < π₯ β§ Β¬ π₯ < ((β―βπ) β 2))) |
118 | 113 | ancomd 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β§ (β―βπ)
β β0) β (((β―βπ) β 2) β β β§ π₯ β
β)) |
119 | 118 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β§ (β―βπ)
β β0) β§ Β¬ π₯ < ((β―βπ) β 2)) β (((β―βπ) β 2) β β
β§ π₯ β
β)) |
120 | | lttri3 11245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((β―βπ)
β 2) β β β§ π₯ β β) β
(((β―βπ) β
2) = π₯ β (Β¬
((β―βπ) β
2) < π₯ β§ Β¬ π₯ < ((β―βπ) β 2)))) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β§ (β―βπ)
β β0) β§ Β¬ π₯ < ((β―βπ) β 2)) β (((β―βπ) β 2) = π₯ β (Β¬
((β―βπ) β
2) < π₯ β§ Β¬ π₯ < ((β―βπ) β 2)))) |
122 | 117, 121 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β§ (β―βπ)
β β0) β§ Β¬ π₯ < ((β―βπ) β 2)) β ((β―βπ) β 2) = π₯) |
123 | 122 | exp31 421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β ((β―βπ) β β0 β (Β¬
π₯ <
((β―βπ) β
2) β ((β―βπ) β 2) = π₯))) |
124 | 123 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π₯ β β0
β§ π₯ <
((β―βπ) β
1)) β (Β¬ π₯ <
((β―βπ) β
2) β ((β―βπ) β β0 β
((β―βπ) β
2) = π₯))) |
125 | 124 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π₯ β β0
β§ ((β―βπ)
β 1) β β β§ π₯ < ((β―βπ) β 1)) β (Β¬ π₯ < ((β―βπ) β 2) β
((β―βπ) β
β0 β ((β―βπ) β 2) = π₯))) |
126 | 6, 125 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ β
(0..^((β―βπ)
β 1)) β (Β¬ π₯
< ((β―βπ)
β 2) β ((β―βπ) β β0 β
((β―βπ) β
2) = π₯))) |
127 | 126 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((Β¬
π₯ <
((β―βπ) β
2) β§ π₯ β
(0..^((β―βπ)
β 1))) β ((β―βπ) β β0 β
((β―βπ) β
2) = π₯)) |
128 | 7, 127 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β Word π β ((Β¬ π₯ < ((β―βπ) β 2) β§ π₯ β (0..^((β―βπ) β 1))) β
((β―βπ) β
2) = π₯)) |
129 | 128 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β ((Β¬ π₯ < ((β―βπ) β 2) β§ π₯ β
(0..^((β―βπ)
β 1))) β ((β―βπ) β 2) = π₯)) |
130 | 129 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ (Β¬ π₯ < ((β―βπ) β 2) β§ π₯ β
(0..^((β―βπ)
β 1)))) β ((β―βπ) β 2) = π₯) |
131 | 130 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ (Β¬ π₯ < ((β―βπ) β 2) β§ π₯ β
(0..^((β―βπ)
β 1)))) β (πβ((β―βπ) β 2)) = (πβπ₯)) |
132 | 131 | preq1d 4705 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ (Β¬ π₯ < ((β―βπ) β 2) β§ π₯ β
(0..^((β―βπ)
β 1)))) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβπ₯), (πβ0)}) |
133 | 132 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ (Β¬ π₯ < ((β―βπ) β 2) β§ π₯ β
(0..^((β―βπ)
β 1)))) β ({(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ β {(πβπ₯), (πβ0)} β ran πΈ)) |
134 | 133 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ (Β¬ π₯ < ((β―βπ) β 2) β§ π₯ β
(0..^((β―βπ)
β 1)))) β ({(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ β {(πβπ₯), (πβ0)} β ran πΈ)) |
135 | 134 | exp32 422 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (Β¬ π₯ < ((β―βπ) β 2) β (π₯ β
(0..^((β―βπ)
β 1)) β ({(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ β {(πβπ₯), (πβ0)} β ran πΈ)))) |
136 | 135 | com12 32 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π₯ <
((β―βπ) β
2) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (π₯ β (0..^((β―βπ) β 1)) β ({(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ β {(πβπ₯), (πβ0)} β ran πΈ)))) |
137 | 136 | com14 96 |
. . . . . . . . . . . . . . . 16
β’ ({(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (π₯ β (0..^((β―βπ) β 1)) β (Β¬
π₯ <
((β―βπ) β
2) β {(πβπ₯), (πβ0)} β ran πΈ)))) |
138 | 137 | adantl 483 |
. . . . . . . . . . . . . . 15
β’
((βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (π₯ β (0..^((β―βπ) β 1)) β (Β¬
π₯ <
((β―βπ) β
2) β {(πβπ₯), (πβ0)} β ran πΈ)))) |
139 | 138 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((lastSβπ) =
(πβ0) β§
(βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (π₯ β (0..^((β―βπ) β 1)) β (Β¬
π₯ <
((β―βπ) β
2) β {(πβπ₯), (πβ0)} β ran πΈ)))) |
140 | 139 | com12 32 |
. . . . . . . . . . . . 13
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β (π₯ β (0..^((β―βπ) β 1)) β (Β¬
π₯ <
((β―βπ) β
2) β {(πβπ₯), (πβ0)} β ran πΈ)))) |
141 | 140 | imp31 419 |
. . . . . . . . . . . 12
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1))) β (Β¬
π₯ <
((β―βπ) β
2) β {(πβπ₯), (πβ0)} β ran πΈ)) |
142 | 141 | impcom 409 |
. . . . . . . . . . 11
β’ ((Β¬
π₯ <
((β―βπ) β
2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β {(πβπ₯), (πβ0)} β ran πΈ) |
143 | | f1ocnvdm 7236 |
. . . . . . . . . . 11
β’ ((πΈ:dom πΈβ1-1-ontoβran
πΈ β§ {(πβπ₯), (πβ0)} β ran πΈ) β (β‘πΈβ{(πβπ₯), (πβ0)}) β dom πΈ) |
144 | 98, 142, 143 | syl2anc 585 |
. . . . . . . . . 10
β’ ((Β¬
π₯ <
((β―βπ) β
2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β (β‘πΈβ{(πβπ₯), (πβ0)}) β dom πΈ) |
145 | 97, 144 | jca 513 |
. . . . . . . . 9
β’ ((Β¬
π₯ <
((β―βπ) β
2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β (Β¬
π₯ <
((β―βπ) β
2) β§ (β‘πΈβ{(πβπ₯), (πβ0)}) β dom πΈ)) |
146 | 145 | olcd 873 |
. . . . . . . 8
β’ ((Β¬
π₯ <
((β―βπ) β
2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1)))) β ((π₯ < ((β―βπ) β 2) β§ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}) β dom πΈ) β¨ (Β¬ π₯ < ((β―βπ) β 2) β§ (β‘πΈβ{(πβπ₯), (πβ0)}) β dom πΈ))) |
147 | 96, 146 | pm2.61ian 811 |
. . . . . . 7
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1))) β ((π₯ < ((β―βπ) β 2) β§ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}) β dom πΈ) β¨ (Β¬ π₯ < ((β―βπ) β 2) β§ (β‘πΈβ{(πβπ₯), (πβ0)}) β dom πΈ))) |
148 | | ifel 4535 |
. . . . . . 7
β’ (if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})) β dom πΈ β ((π₯ < ((β―βπ) β 2) β§ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}) β dom πΈ) β¨ (Β¬ π₯ < ((β―βπ) β 2) β§ (β‘πΈβ{(πβπ₯), (πβ0)}) β dom πΈ))) |
149 | 147, 148 | sylibr 233 |
. . . . . 6
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β§ π₯ β (0..^((β―βπ) β 1))) β if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})) β dom πΈ) |
150 | | clwlkclwwlklem2.f |
. . . . . 6
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) |
151 | 149, 150 | fmptd 7067 |
. . . . 5
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β πΉ:(0..^((β―βπ) β 1))βΆdom πΈ) |
152 | | iswrdi 14413 |
. . . . 5
β’ (πΉ:(0..^((β―βπ) β 1))βΆdom πΈ β πΉ β Word dom πΈ) |
153 | 151, 152 | syl 17 |
. . . 4
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β πΉ β Word dom πΈ) |
154 | | wrdf 14414 |
. . . . . . . 8
β’ (π β Word π β π:(0..^(β―βπ))βΆπ) |
155 | 154 | adantr 482 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ (β―βπ)) β π:(0..^(β―βπ))βΆπ) |
156 | 150 | clwlkclwwlklem2a2 28979 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (β―βπΉ) = ((β―βπ) β 1)) |
157 | | fzoval 13580 |
. . . . . . . . . . 11
β’
((β―βπ)
β β€ β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
158 | 7, 21, 157 | 3syl 18 |
. . . . . . . . . 10
β’ (π β Word π β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
159 | | oveq2 7370 |
. . . . . . . . . . 11
β’
(((β―βπ)
β 1) = (β―βπΉ) β (0...((β―βπ) β 1)) =
(0...(β―βπΉ))) |
160 | 159 | eqcoms 2745 |
. . . . . . . . . 10
β’
((β―βπΉ) =
((β―βπ) β
1) β (0...((β―βπ) β 1)) = (0...(β―βπΉ))) |
161 | 158, 160 | sylan9eq 2797 |
. . . . . . . . 9
β’ ((π β Word π β§ (β―βπΉ) = ((β―βπ) β 1)) β
(0..^(β―βπ)) =
(0...(β―βπΉ))) |
162 | 156, 161 | syldan 592 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ (β―βπ)) β
(0..^(β―βπ)) =
(0...(β―βπΉ))) |
163 | 162 | feq2d 6659 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (π:(0..^(β―βπ))βΆπ β π:(0...(β―βπΉ))βΆπ)) |
164 | 155, 163 | mpbid 231 |
. . . . . 6
β’ ((π β Word π β§ 2 β€ (β―βπ)) β π:(0...(β―βπΉ))βΆπ) |
165 | 164 | 3adant1 1131 |
. . . . 5
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β π:(0...(β―βπΉ))βΆπ) |
166 | 165 | adantr 482 |
. . . 4
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β π:(0...(β―βπΉ))βΆπ) |
167 | | clwlkclwwlklem2a1 28978 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ)) |
168 | 167 | 3adant1 1131 |
. . . . . 6
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ)) |
169 | 168 | imp 408 |
. . . . 5
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ) |
170 | 156 | 3adant1 1131 |
. . . . . . . 8
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (β―βπΉ) = ((β―βπ) β 1)) |
171 | 170 | adantr 482 |
. . . . . . 7
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β (β―βπΉ) = ((β―βπ) β 1)) |
172 | 150 | clwlkclwwlklem2a4 28983 |
. . . . . . . . . 10
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ π β (0..^((β―βπ) β 1))) β ({(πβπ), (πβ(π + 1))} β ran πΈ β (πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
173 | 172 | impl 457 |
. . . . . . . . 9
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β§ π β (0..^((β―βπ) β 1))) β ({(πβπ), (πβ(π + 1))} β ran πΈ β (πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
174 | 173 | ralimdva 3165 |
. . . . . . . 8
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^((β―βπ) β 1))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
175 | | oveq2 7370 |
. . . . . . . . . 10
β’
((β―βπΉ) =
((β―βπ) β
1) β (0..^(β―βπΉ)) = (0..^((β―βπ) β 1))) |
176 | 175 | raleqdv 3316 |
. . . . . . . . 9
β’
((β―βπΉ) =
((β―βπ) β
1) β (βπ β
(0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β βπ β (0..^((β―βπ) β 1))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
177 | 176 | imbi2d 341 |
. . . . . . . 8
β’
((β―βπΉ) =
((β―βπ) β
1) β ((βπ
β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^((β―βπ) β 1))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
178 | 174, 177 | syl5ibr 246 |
. . . . . . 7
β’
((β―βπΉ) =
((β―βπ) β
1) β (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
179 | 171, 178 | mpcom 38 |
. . . . . 6
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ (lastSβπ) = (πβ0)) β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
180 | 179 | adantrr 716 |
. . . . 5
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
181 | 169, 180 | mpd 15 |
. . . 4
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
182 | 153, 166,
181 | 3jca 1129 |
. . 3
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β (πΉ β Word dom πΈ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
183 | 150 | clwlkclwwlklem2a3 28980 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (πβ(β―βπΉ)) = (lastSβπ)) |
184 | 183 | 3adant1 1131 |
. . . . . . . . 9
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (πβ(β―βπΉ)) = (lastSβπ)) |
185 | 184 | eqcomd 2743 |
. . . . . . . 8
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (lastSβπ) = (πβ(β―βπΉ))) |
186 | 185 | eqeq2d 2748 |
. . . . . . 7
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β ((πβ0) = (lastSβπ) β (πβ0) = (πβ(β―βπΉ)))) |
187 | 186 | biimpcd 249 |
. . . . . 6
β’ ((πβ0) = (lastSβπ) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (πβ0) = (πβ(β―βπΉ)))) |
188 | 187 | eqcoms 2745 |
. . . . 5
β’
((lastSβπ) =
(πβ0) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (πβ0) = (πβ(β―βπΉ)))) |
189 | 188 | adantr 482 |
. . . 4
β’
(((lastSβπ) =
(πβ0) β§
(βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (πβ0) = (πβ(β―βπΉ)))) |
190 | 189 | impcom 409 |
. . 3
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β (πβ0) = (πβ(β―βπΉ))) |
191 | 182, 190 | jca 513 |
. 2
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) β ((πΉ β Word dom πΈ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπΉ)))) |
192 | 191 | ex 414 |
1
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((πΉ β Word dom πΈ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπΉ))))) |