Step | Hyp | Ref
| Expression |
1 | | fveq2 6842 |
. . . . . . . . . 10
β’ (πΌ = ((β―βπ) β 2) β (πΉβπΌ) = (πΉβ((β―βπ) β 2))) |
2 | | lencl 14421 |
. . . . . . . . . . 11
β’ (π β Word π β (β―βπ) β
β0) |
3 | | clwlkclwwlklem2.f |
. . . . . . . . . . . 12
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) |
4 | 3 | clwlkclwwlklem2fv2 28940 |
. . . . . . . . . . 11
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β (πΉβ((β―βπ) β 2)) = (β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)})) |
5 | 2, 4 | sylan 580 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (πΉβ((β―βπ) β 2)) = (β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)})) |
6 | 1, 5 | sylan9eqr 2798 |
. . . . . . . . 9
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ πΌ = ((β―βπ) β 2)) β (πΉβπΌ) = (β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)})) |
7 | 6 | ex 413 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (πΌ = ((β―βπ) β 2) β (πΉβπΌ) = (β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)}))) |
8 | 7 | 3adant1 1130 |
. . . . . . 7
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (πΌ = ((β―βπ) β 2) β (πΉβπΌ) = (β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)}))) |
9 | 8 | ad2antrr 724 |
. . . . . 6
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ) β (πΌ = ((β―βπ) β 2) β (πΉβπΌ) = (β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)}))) |
10 | 9 | impcom 408 |
. . . . 5
β’ ((πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β (πΉβπΌ) = (β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)})) |
11 | 10 | fveq2d 6846 |
. . . 4
β’ ((πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β (πΈβ(πΉβπΌ)) = (πΈβ(β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)}))) |
12 | | f1f1orn 6795 |
. . . . . . 7
β’ (πΈ:dom πΈβ1-1βπ
β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
13 | 12 | 3ad2ant1 1133 |
. . . . . 6
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
14 | 13 | ad2antrr 724 |
. . . . 5
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ) β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
15 | | lsw 14452 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Word π β (lastSβπ) = (πβ((β―βπ) β 1))) |
16 | 15 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word π β ((lastSβπ) = (πβ0) β (πβ((β―βπ) β 1)) = (πβ0))) |
17 | | nn0cn 12423 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ)
β β0 β (β―βπ) β β) |
18 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ)
β β β (β―βπ) β β) |
19 | | 2cnd 12231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ)
β β β 2 β β) |
20 | | 1cnd 11150 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ)
β β β 1 β β) |
21 | 18, 19, 20 | subsubd 11540 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ)
β β β ((β―βπ) β (2 β 1)) =
(((β―βπ) β
2) + 1)) |
22 | | 2m1e1 12279 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (2
β 1) = 1 |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ)
β β β (2 β 1) = 1) |
24 | 23 | oveq2d 7373 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ)
β β β ((β―βπ) β (2 β 1)) =
((β―βπ) β
1)) |
25 | 21, 24 | eqtr3d 2778 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ)
β β β (((β―βπ) β 2) + 1) = ((β―βπ) β 1)) |
26 | 2, 17, 25 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Word π β (((β―βπ) β 2) + 1) = ((β―βπ) β 1)) |
27 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Word π β§ (πβ((β―βπ) β 1)) = (πβ0)) β (((β―βπ) β 2) + 1) =
((β―βπ) β
1)) |
28 | 27 | fveq2d 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Word π β§ (πβ((β―βπ) β 1)) = (πβ0)) β (πβ(((β―βπ) β 2) + 1)) = (πβ((β―βπ) β 1))) |
29 | | eqeq2 2748 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβ0) = (πβ((β―βπ) β 1)) β ((πβ(((β―βπ) β 2) + 1)) = (πβ0) β (πβ(((β―βπ) β 2) + 1)) = (πβ((β―βπ) β 1)))) |
30 | 29 | eqcoms 2744 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβ((β―βπ) β 1)) = (πβ0) β ((πβ(((β―βπ) β 2) + 1)) = (πβ0) β (πβ(((β―βπ) β 2) + 1)) = (πβ((β―βπ) β 1)))) |
31 | 30 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Word π β§ (πβ((β―βπ) β 1)) = (πβ0)) β ((πβ(((β―βπ) β 2) + 1)) = (πβ0) β (πβ(((β―βπ) β 2) + 1)) = (πβ((β―βπ) β 1)))) |
32 | 28, 31 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Word π β§ (πβ((β―βπ) β 1)) = (πβ0)) β (πβ(((β―βπ) β 2) + 1)) = (πβ0)) |
33 | 32 | ex 413 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word π β ((πβ((β―βπ) β 1)) = (πβ0) β (πβ(((β―βπ) β 2) + 1)) = (πβ0))) |
34 | 16, 33 | sylbid 239 |
. . . . . . . . . . . . . . . 16
β’ (π β Word π β ((lastSβπ) = (πβ0) β (πβ(((β―βπ) β 2) + 1)) = (πβ0))) |
35 | 34 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . 15
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β ((lastSβπ) = (πβ0) β (πβ(((β―βπ) β 2) + 1)) = (πβ0))) |
36 | 35 | com12 32 |
. . . . . . . . . . . . . 14
β’
((lastSβπ) =
(πβ0) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (πβ(((β―βπ) β 2) + 1)) = (πβ0))) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . 13
β’
(((lastSβπ) =
(πβ0) β§ πΌ β
(0..^((β―βπ)
β 1))) β ((πΈ:dom
πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (πβ(((β―βπ) β 2) + 1)) = (πβ0))) |
38 | 37 | impcom 408 |
. . . . . . . . . . . 12
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β (πβ(((β―βπ) β 2) + 1)) = (πβ0)) |
39 | 38 | adantr 481 |
. . . . . . . . . . 11
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ πΌ = ((β―βπ) β 2)) β (πβ(((β―βπ) β 2) + 1)) = (πβ0)) |
40 | 39 | preq2d 4701 |
. . . . . . . . . 10
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ πΌ = ((β―βπ) β 2)) β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} = {(πβ((β―βπ) β 2)), (πβ0)}) |
41 | | fveq2 6842 |
. . . . . . . . . . . . 13
β’ (πΌ = ((β―βπ) β 2) β (πβπΌ) = (πβ((β―βπ) β 2))) |
42 | | fvoveq1 7380 |
. . . . . . . . . . . . 13
β’ (πΌ = ((β―βπ) β 2) β (πβ(πΌ + 1)) = (πβ(((β―βπ) β 2) + 1))) |
43 | 41, 42 | preq12d 4702 |
. . . . . . . . . . . 12
β’ (πΌ = ((β―βπ) β 2) β {(πβπΌ), (πβ(πΌ + 1))} = {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))}) |
44 | 43 | eqeq1d 2738 |
. . . . . . . . . . 11
β’ (πΌ = ((β―βπ) β 2) β ({(πβπΌ), (πβ(πΌ + 1))} = {(πβ((β―βπ) β 2)), (πβ0)} β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} = {(πβ((β―βπ) β 2)), (πβ0)})) |
45 | 44 | adantl 482 |
. . . . . . . . . 10
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ πΌ = ((β―βπ) β 2)) β ({(πβπΌ), (πβ(πΌ + 1))} = {(πβ((β―βπ) β 2)), (πβ0)} β {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))} = {(πβ((β―βπ) β 2)), (πβ0)})) |
46 | 40, 45 | mpbird 256 |
. . . . . . . . 9
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ πΌ = ((β―βπ) β 2)) β {(πβπΌ), (πβ(πΌ + 1))} = {(πβ((β―βπ) β 2)), (πβ0)}) |
47 | 46 | eleq1d 2822 |
. . . . . . . 8
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ πΌ = ((β―βπ) β 2)) β ({(πβπΌ), (πβ(πΌ + 1))} β ran πΈ β {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) |
48 | 47 | biimpd 228 |
. . . . . . 7
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ πΌ = ((β―βπ) β 2)) β ({(πβπΌ), (πβ(πΌ + 1))} β ran πΈ β {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) |
49 | 48 | impancom 452 |
. . . . . 6
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ) β (πΌ = ((β―βπ) β 2) β {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) |
50 | 49 | impcom 408 |
. . . . 5
β’ ((πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ) |
51 | | f1ocnvfv2 7223 |
. . . . 5
β’ ((πΈ:dom πΈβ1-1-ontoβran
πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ) β (πΈβ(β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)})) = {(πβ((β―βπ) β 2)), (πβ0)}) |
52 | 14, 50, 51 | syl2an2 684 |
. . . 4
β’ ((πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β (πΈβ(β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)})) = {(πβ((β―βπ) β 2)), (πβ0)}) |
53 | | eqcom 2743 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβ((β―βπ) β 1)) = (πβ0) β (πβ0) = (πβ((β―βπ) β 1))) |
54 | 53 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβ((β―βπ) β 1)) = (πβ0) β (πβ0) = (πβ((β―βπ) β 1))) |
55 | | 1e2m1 12280 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 = (2
β 1) |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Word π β 1 = (2 β 1)) |
57 | 56 | oveq2d 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Word π β ((β―βπ) β 1) = ((β―βπ) β (2 β
1))) |
58 | 2, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Word π β (β―βπ) β β) |
59 | | 2cnd 12231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Word π β 2 β β) |
60 | | 1cnd 11150 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Word π β 1 β β) |
61 | 58, 59, 60 | subsubd 11540 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Word π β ((β―βπ) β (2 β 1)) =
(((β―βπ) β
2) + 1)) |
62 | 57, 61 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Word π β ((β―βπ) β 1) = (((β―βπ) β 2) +
1)) |
63 | 62 | fveq2d 6846 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Word π β (πβ((β―βπ) β 1)) = (πβ(((β―βπ) β 2) + 1))) |
64 | 54, 63 | sylan9eqr 2798 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Word π β§ (πβ((β―βπ) β 1)) = (πβ0)) β (πβ0) = (πβ(((β―βπ) β 2) + 1))) |
65 | 64 | ex 413 |
. . . . . . . . . . . . . . . 16
β’ (π β Word π β ((πβ((β―βπ) β 1)) = (πβ0) β (πβ0) = (πβ(((β―βπ) β 2) + 1)))) |
66 | 16, 65 | sylbid 239 |
. . . . . . . . . . . . . . 15
β’ (π β Word π β ((lastSβπ) = (πβ0) β (πβ0) = (πβ(((β―βπ) β 2) + 1)))) |
67 | 66 | imp 407 |
. . . . . . . . . . . . . 14
β’ ((π β Word π β§ (lastSβπ) = (πβ0)) β (πβ0) = (πβ(((β―βπ) β 2) + 1))) |
68 | 67 | preq2d 4701 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ (lastSβπ) = (πβ0)) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))}) |
69 | 68 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β Word π β§ (lastSβπ) = (πβ0)) β§ πΌ = ((β―βπ) β 2)) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))}) |
70 | 43 | adantl 482 |
. . . . . . . . . . . 12
β’ (((π β Word π β§ (lastSβπ) = (πβ0)) β§ πΌ = ((β―βπ) β 2)) β {(πβπΌ), (πβ(πΌ + 1))} = {(πβ((β―βπ) β 2)), (πβ(((β―βπ) β 2) + 1))}) |
71 | 69, 70 | eqtr4d 2779 |
. . . . . . . . . . 11
β’ (((π β Word π β§ (lastSβπ) = (πβ0)) β§ πΌ = ((β―βπ) β 2)) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβπΌ), (πβ(πΌ + 1))}) |
72 | 71 | exp31 420 |
. . . . . . . . . 10
β’ (π β Word π β ((lastSβπ) = (πβ0) β (πΌ = ((β―βπ) β 2) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβπΌ), (πβ(πΌ + 1))}))) |
73 | 72 | 3ad2ant2 1134 |
. . . . . . . . 9
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β ((lastSβπ) = (πβ0) β (πΌ = ((β―βπ) β 2) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβπΌ), (πβ(πΌ + 1))}))) |
74 | 73 | com12 32 |
. . . . . . . 8
β’
((lastSβπ) =
(πβ0) β ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (πΌ = ((β―βπ) β 2) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβπΌ), (πβ(πΌ + 1))}))) |
75 | 74 | adantr 481 |
. . . . . . 7
β’
(((lastSβπ) =
(πβ0) β§ πΌ β
(0..^((β―βπ)
β 1))) β ((πΈ:dom
πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (πΌ = ((β―βπ) β 2) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβπΌ), (πβ(πΌ + 1))}))) |
76 | 75 | impcom 408 |
. . . . . 6
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β (πΌ = ((β―βπ) β 2) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβπΌ), (πβ(πΌ + 1))})) |
77 | 76 | adantr 481 |
. . . . 5
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ) β (πΌ = ((β―βπ) β 2) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβπΌ), (πβ(πΌ + 1))})) |
78 | 77 | impcom 408 |
. . . 4
β’ ((πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβπΌ), (πβ(πΌ + 1))}) |
79 | 11, 52, 78 | 3eqtrd 2780 |
. . 3
β’ ((πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β (πΈβ(πΉβπΌ)) = {(πβπΌ), (πβ(πΌ + 1))}) |
80 | | simpll 765 |
. . . . . . . . . . . . . . . . 17
β’
((((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β§ (πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2))) β
(β―βπ) β
β0) |
81 | | oveq1 7364 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ) =
2 β ((β―βπ)
β 1) = (2 β 1)) |
82 | 81, 22 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ) =
2 β ((β―βπ)
β 1) = 1) |
83 | 82 | oveq2d 7373 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ) =
2 β (0..^((β―βπ) β 1)) = (0..^1)) |
84 | 83 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ) =
2 β (πΌ β
(0..^((β―βπ)
β 1)) β πΌ β
(0..^1))) |
85 | | oveq1 7364 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ) =
2 β ((β―βπ)
β 2) = (2 β 2)) |
86 | | 2cn 12228 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 2 β
β |
87 | 86 | subidi 11472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (2
β 2) = 0 |
88 | 85, 87 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ) =
2 β ((β―βπ)
β 2) = 0) |
89 | 88 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ) =
2 β (πΌ =
((β―βπ) β
2) β πΌ =
0)) |
90 | 89 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ) =
2 β (Β¬ πΌ =
((β―βπ) β
2) β Β¬ πΌ =
0)) |
91 | 84, 90 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπ) =
2 β ((πΌ β
(0..^((β―βπ)
β 1)) β§ Β¬ πΌ =
((β―βπ) β
2)) β (πΌ β
(0..^1) β§ Β¬ πΌ =
0))) |
92 | | elsni 4603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πΌ β {0} β πΌ = 0) |
93 | 92 | pm2.24d 151 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΌ β {0} β (Β¬ πΌ = 0 β (πΌ β β0 β§
((β―βπ) β
2) β β β§ πΌ
< ((β―βπ)
β 2)))) |
94 | | fzo01 13654 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (0..^1) =
{0} |
95 | 93, 94 | eleq2s 2855 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΌ β (0..^1) β (Β¬
πΌ = 0 β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2)))) |
96 | 95 | imp 407 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΌ β (0..^1) β§ Β¬
πΌ = 0) β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2))) |
97 | 91, 96 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπ) =
2 β ((πΌ β
(0..^((β―βπ)
β 1)) β§ Β¬ πΌ =
((β―βπ) β
2)) β (πΌ β
β0 β§ ((β―βπ) β 2) β β β§ πΌ < ((β―βπ) β 2)))) |
98 | 97 | adantld 491 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―βπ) =
2 β ((((β―βπ) β β0 β§ 2 β€
(β―βπ)) β§
(πΌ β
(0..^((β―βπ)
β 1)) β§ Β¬ πΌ =
((β―βπ) β
2))) β (πΌ β
β0 β§ ((β―βπ) β 2) β β β§ πΌ < ((β―βπ) β 2)))) |
99 | | df-ne 2944 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ)
β 2 β Β¬ (β―βπ) = 2) |
100 | | 2re 12227 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 2 β
β |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β 2 β β) |
102 | | nn0re 12422 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―βπ)
β β0 β (β―βπ) β β) |
103 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β (β―βπ) β β) |
104 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β 2 β€ (β―βπ)) |
105 | 101, 103,
104 | leltned 11308 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β (2 < (β―βπ) β (β―βπ) β 2)) |
106 | | elfzo0 13613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (πΌ β
(0..^((β―βπ)
β 1)) β (πΌ
β β0 β§ ((β―βπ) β 1) β β β§ πΌ < ((β―βπ) β 1))) |
107 | | simp-4l 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((((πΌ β
β0 β§ (β―βπ) β β0) β§ Β¬
πΌ = ((β―βπ) β 2)) β§ 2 <
(β―βπ)) β§
πΌ <
((β―βπ) β
1)) β πΌ β
β0) |
108 | | nn0z 12524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((β―βπ)
β β0 β (β―βπ) β β€) |
109 | | 2z 12535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ 2 β
β€ |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((β―βπ)
β β0 β 2 β β€) |
111 | 108, 110 | zsubcld 12612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((β―βπ)
β β0 β ((β―βπ) β 2) β
β€) |
112 | 111 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((β―βπ)
β β0 β§ 2 < (β―βπ)) β ((β―βπ) β 2) β
β€) |
113 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((β―βπ)
β β0 β 2 β β) |
114 | 113, 102 | posdifd 11742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((β―βπ)
β β0 β (2 < (β―βπ) β 0 < ((β―βπ) β 2))) |
115 | 114 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((β―βπ)
β β0 β§ 2 < (β―βπ)) β 0 < ((β―βπ) β 2)) |
116 | | elnnz 12509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((β―βπ)
β 2) β β β (((β―βπ) β 2) β β€ β§ 0 <
((β―βπ) β
2))) |
117 | 112, 115,
116 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((β―βπ)
β β0 β§ 2 < (β―βπ)) β ((β―βπ) β 2) β
β) |
118 | 117 | ad5ant24 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((((πΌ β
β0 β§ (β―βπ) β β0) β§ Β¬
πΌ = ((β―βπ) β 2)) β§ 2 <
(β―βπ)) β§
πΌ <
((β―βπ) β
1)) β ((β―βπ) β 2) β
β) |
119 | | nn0z 12524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (πΌ β β0
β πΌ β
β€) |
120 | | peano2zm 12546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
((β―βπ)
β β€ β ((β―βπ) β 1) β
β€) |
121 | 108, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
((β―βπ)
β β0 β ((β―βπ) β 1) β
β€) |
122 | | zltlem1 12556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((πΌ β β€ β§
((β―βπ) β
1) β β€) β (πΌ < ((β―βπ) β 1) β πΌ β€ (((β―βπ) β 1) β 1))) |
123 | 119, 121,
122 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β (πΌ < ((β―βπ) β 1) β πΌ β€ (((β―βπ) β 1) β 1))) |
124 | 17 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β (β―βπ) β β) |
125 | | 1cnd 11150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β 1 β β) |
126 | 124, 125,
125 | subsub4d 11543 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β (((β―βπ) β 1) β 1) =
((β―βπ) β
(1 + 1))) |
127 | | 1p1e2 12278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (1 + 1) =
2 |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β (1 + 1) = 2) |
129 | 128 | oveq2d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β ((β―βπ) β (1 + 1)) = ((β―βπ) β 2)) |
130 | 126, 129 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β (((β―βπ) β 1) β 1) =
((β―βπ) β
2)) |
131 | 130 | breq2d 5117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β (πΌ β€ (((β―βπ) β 1) β 1) β πΌ β€ ((β―βπ) β 2))) |
132 | 123, 131 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β (πΌ < ((β―βπ) β 1) β πΌ β€ ((β―βπ) β 2))) |
133 | | necom 2997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
(((β―βπ)
β 2) β πΌ β
πΌ β
((β―βπ) β
2)) |
134 | | df-ne 2944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (πΌ β ((β―βπ) β 2) β Β¬ πΌ = ((β―βπ) β 2)) |
135 | 133, 134 | bitr2i 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (Β¬
πΌ = ((β―βπ) β 2) β
((β―βπ) β
2) β πΌ) |
136 | | nn0re 12422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (πΌ β β0
β πΌ β
β) |
137 | 136 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((πΌ β β0
β§ (β―βπ)
β β0) β§ πΌ β€ ((β―βπ) β 2)) β πΌ β β) |
138 | 102, 113 | resubcld 11583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’
((β―βπ)
β β0 β ((β―βπ) β 2) β
β) |
139 | 138 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((πΌ β β0
β§ (β―βπ)
β β0) β§ πΌ β€ ((β―βπ) β 2)) β ((β―βπ) β 2) β
β) |
140 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((πΌ β β0
β§ (β―βπ)
β β0) β§ πΌ β€ ((β―βπ) β 2)) β πΌ β€ ((β―βπ) β 2)) |
141 | | leltne 11244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((πΌ β β β§
((β―βπ) β
2) β β β§ πΌ
β€ ((β―βπ)
β 2)) β (πΌ <
((β―βπ) β
2) β ((β―βπ) β 2) β πΌ)) |
142 | 141 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((πΌ β β β§
((β―βπ) β
2) β β β§ πΌ
β€ ((β―βπ)
β 2)) β (((β―βπ) β 2) β πΌ β πΌ < ((β―βπ) β 2))) |
143 | 137, 139,
140, 142 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (((πΌ β β0
β§ (β―βπ)
β β0) β§ πΌ β€ ((β―βπ) β 2)) β (((β―βπ) β 2) β πΌ β πΌ < ((β―βπ) β 2))) |
144 | 143 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (((πΌ β β0
β§ (β―βπ)
β β0) β§ πΌ β€ ((β―βπ) β 2)) β (((β―βπ) β 2) β πΌ β πΌ < ((β―βπ) β 2))) |
145 | 135, 144 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (((πΌ β β0
β§ (β―βπ)
β β0) β§ πΌ β€ ((β―βπ) β 2)) β (Β¬ πΌ = ((β―βπ) β 2) β πΌ < ((β―βπ) β 2))) |
146 | 145 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β (πΌ β€ ((β―βπ) β 2) β (Β¬ πΌ = ((β―βπ) β 2) β πΌ < ((β―βπ) β 2)))) |
147 | 132, 146 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β (πΌ < ((β―βπ) β 1) β (Β¬ πΌ = ((β―βπ) β 2) β πΌ < ((β―βπ) β 2)))) |
148 | 147 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((πΌ β β0
β§ (β―βπ)
β β0) β (Β¬ πΌ = ((β―βπ) β 2) β (πΌ < ((β―βπ) β 1) β πΌ < ((β―βπ) β 2)))) |
149 | 148 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((πΌ β β0
β§ (β―βπ)
β β0) β§ Β¬ πΌ = ((β―βπ) β 2)) β (πΌ < ((β―βπ) β 1) β πΌ < ((β―βπ) β 2))) |
150 | 149 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((((πΌ β β0
β§ (β―βπ)
β β0) β§ Β¬ πΌ = ((β―βπ) β 2)) β§ 2 <
(β―βπ)) β
(πΌ <
((β―βπ) β
1) β πΌ <
((β―βπ) β
2))) |
151 | 150 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((((πΌ β
β0 β§ (β―βπ) β β0) β§ Β¬
πΌ = ((β―βπ) β 2)) β§ 2 <
(β―βπ)) β§
πΌ <
((β―βπ) β
1)) β πΌ <
((β―βπ) β
2)) |
152 | 107, 118,
151 | 3jca 1128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((πΌ β
β0 β§ (β―βπ) β β0) β§ Β¬
πΌ = ((β―βπ) β 2)) β§ 2 <
(β―βπ)) β§
πΌ <
((β―βπ) β
1)) β (πΌ β
β0 β§ ((β―βπ) β 2) β β β§ πΌ < ((β―βπ) β 2))) |
153 | 152 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((πΌ β β0
β§ (β―βπ)
β β0) β§ Β¬ πΌ = ((β―βπ) β 2)) β§ 2 <
(β―βπ)) β
(πΌ <
((β―βπ) β
1) β (πΌ β
β0 β§ ((β―βπ) β 2) β β β§ πΌ < ((β―βπ) β 2)))) |
154 | 153 | exp41 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (πΌ β β0
β ((β―βπ)
β β0 β (Β¬ πΌ = ((β―βπ) β 2) β (2 <
(β―βπ) β
(πΌ <
((β―βπ) β
1) β (πΌ β
β0 β§ ((β―βπ) β 2) β β β§ πΌ < ((β―βπ) β
2))))))) |
155 | 154 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (πΌ β β0
β (πΌ <
((β―βπ) β
1) β (Β¬ πΌ =
((β―βπ) β
2) β (2 < (β―βπ) β ((β―βπ) β β0 β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2))))))) |
156 | 155 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΌ β β0
β§ πΌ <
((β―βπ) β
1)) β (Β¬ πΌ =
((β―βπ) β
2) β (2 < (β―βπ) β ((β―βπ) β β0 β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2)))))) |
157 | 156 | 3adant2 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πΌ β β0
β§ ((β―βπ)
β 1) β β β§ πΌ < ((β―βπ) β 1)) β (Β¬ πΌ = ((β―βπ) β 2) β (2 <
(β―βπ) β
((β―βπ) β
β0 β (πΌ β β0 β§
((β―βπ) β
2) β β β§ πΌ
< ((β―βπ)
β 2)))))) |
158 | 106, 157 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πΌ β
(0..^((β―βπ)
β 1)) β (Β¬ πΌ
= ((β―βπ)
β 2) β (2 < (β―βπ) β ((β―βπ) β β0 β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2)))))) |
159 | 158 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΌ β
(0..^((β―βπ)
β 1)) β§ Β¬ πΌ =
((β―βπ) β
2)) β (2 < (β―βπ) β ((β―βπ) β β0 β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2))))) |
160 | 159 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ)
β β0 β (2 < (β―βπ) β ((πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2)) β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2))))) |
161 | 160 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β (2 < (β―βπ) β ((πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2)) β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2))))) |
162 | 105, 161 | sylbird 259 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β ((β―βπ) β 2 β ((πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2)) β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2))))) |
163 | 99, 162 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β (Β¬ (β―βπ) = 2 β ((πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2)) β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2))))) |
164 | 163 | com23 86 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β ((πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2)) β (Β¬
(β―βπ) = 2
β (πΌ β
β0 β§ ((β―βπ) β 2) β β β§ πΌ < ((β―βπ) β
2))))) |
165 | 164 | imp 407 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β§ (πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2))) β (Β¬
(β―βπ) = 2
β (πΌ β
β0 β§ ((β―βπ) β 2) β β β§ πΌ < ((β―βπ) β 2)))) |
166 | 165 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
(β―βπ) = 2
β ((((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β§ (πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2))) β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2)))) |
167 | 98, 166 | pm2.61i 182 |
. . . . . . . . . . . . . . . . . 18
β’
((((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β§ (πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2))) β (πΌ β β0
β§ ((β―βπ)
β 2) β β β§ πΌ < ((β―βπ) β 2))) |
168 | | elfzo0 13613 |
. . . . . . . . . . . . . . . . . 18
β’ (πΌ β
(0..^((β―βπ)
β 2)) β (πΌ
β β0 β§ ((β―βπ) β 2) β β β§ πΌ < ((β―βπ) β 2))) |
169 | 167, 168 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’
((((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β§ (πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2))) β πΌ β
(0..^((β―βπ)
β 2))) |
170 | 80, 169 | jca 512 |
. . . . . . . . . . . . . . . 16
β’
((((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β§ (πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2))) β
((β―βπ) β
β0 β§ πΌ
β (0..^((β―βπ) β 2)))) |
171 | 170 | exp31 420 |
. . . . . . . . . . . . . . 15
β’
((β―βπ)
β β0 β (2 β€ (β―βπ) β ((πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2)) β
((β―βπ) β
β0 β§ πΌ
β (0..^((β―βπ) β 2)))))) |
172 | 2, 171 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β Word π β (2 β€ (β―βπ) β ((πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2)) β
((β―βπ) β
β0 β§ πΌ
β (0..^((β―βπ) β 2)))))) |
173 | 172 | imp 407 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2)) β
((β―βπ) β
β0 β§ πΌ
β (0..^((β―βπ) β 2))))) |
174 | 173 | 3adant1 1130 |
. . . . . . . . . . . 12
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β ((πΌ β (0..^((β―βπ) β 1)) β§ Β¬ πΌ = ((β―βπ) β 2)) β
((β―βπ) β
β0 β§ πΌ
β (0..^((β―βπ) β 2))))) |
175 | 174 | expd 416 |
. . . . . . . . . . 11
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (πΌ β (0..^((β―βπ) β 1)) β (Β¬
πΌ = ((β―βπ) β 2) β
((β―βπ) β
β0 β§ πΌ
β (0..^((β―βπ) β 2)))))) |
176 | 175 | com12 32 |
. . . . . . . . . 10
β’ (πΌ β
(0..^((β―βπ)
β 1)) β ((πΈ:dom
πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (Β¬ πΌ = ((β―βπ) β 2) β
((β―βπ) β
β0 β§ πΌ
β (0..^((β―βπ) β 2)))))) |
177 | 176 | adantl 482 |
. . . . . . . . 9
β’
(((lastSβπ) =
(πβ0) β§ πΌ β
(0..^((β―βπ)
β 1))) β ((πΈ:dom
πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (Β¬ πΌ = ((β―βπ) β 2) β
((β―βπ) β
β0 β§ πΌ
β (0..^((β―βπ) β 2)))))) |
178 | 177 | impcom 408 |
. . . . . . . 8
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β (Β¬
πΌ = ((β―βπ) β 2) β
((β―βπ) β
β0 β§ πΌ
β (0..^((β―βπ) β 2))))) |
179 | 178 | adantr 481 |
. . . . . . 7
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ) β (Β¬ πΌ = ((β―βπ) β 2) β ((β―βπ) β β0
β§ πΌ β
(0..^((β―βπ)
β 2))))) |
180 | 179 | impcom 408 |
. . . . . 6
β’ ((Β¬
πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β ((β―βπ) β β0 β§ πΌ β
(0..^((β―βπ)
β 2)))) |
181 | 3 | clwlkclwwlklem2fv1 28939 |
. . . . . 6
β’
(((β―βπ)
β β0 β§ πΌ β (0..^((β―βπ) β 2))) β (πΉβπΌ) = (β‘πΈβ{(πβπΌ), (πβ(πΌ + 1))})) |
182 | 180, 181 | syl 17 |
. . . . 5
β’ ((Β¬
πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β (πΉβπΌ) = (β‘πΈβ{(πβπΌ), (πβ(πΌ + 1))})) |
183 | 182 | fveq2d 6846 |
. . . 4
β’ ((Β¬
πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β (πΈβ(πΉβπΌ)) = (πΈβ(β‘πΈβ{(πβπΌ), (πβ(πΌ + 1))}))) |
184 | | simprr 771 |
. . . . 5
β’ ((Β¬
πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ) |
185 | | f1ocnvfv2 7223 |
. . . . 5
β’ ((πΈ:dom πΈβ1-1-ontoβran
πΈ β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ) β (πΈβ(β‘πΈβ{(πβπΌ), (πβ(πΌ + 1))})) = {(πβπΌ), (πβ(πΌ + 1))}) |
186 | 14, 184, 185 | syl2an2 684 |
. . . 4
β’ ((Β¬
πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β (πΈβ(β‘πΈβ{(πβπΌ), (πβ(πΌ + 1))})) = {(πβπΌ), (πβ(πΌ + 1))}) |
187 | 183, 186 | eqtrd 2776 |
. . 3
β’ ((Β¬
πΌ = ((β―βπ) β 2) β§ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ)) β (πΈβ(πΉβπΌ)) = {(πβπΌ), (πβ(πΌ + 1))}) |
188 | 79, 187 | pm2.61ian 810 |
. 2
β’ ((((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1)))) β§ {(πβπΌ), (πβ(πΌ + 1))} β ran πΈ) β (πΈβ(πΉβπΌ)) = {(πβπΌ), (πβ(πΌ + 1))}) |
189 | 188 | exp31 420 |
1
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1))) β ({(πβπΌ), (πβ(πΌ + 1))} β ran πΈ β (πΈβ(πΉβπΌ)) = {(πβπΌ), (πβ(πΌ + 1))}))) |