Step | Hyp | Ref
| Expression |
1 | | s2len 14840 |
. . . . . . 7
β’
(β―ββ¨β01ββ©) = 2 |
2 | 1 | eqcomi 2742 |
. . . . . 6
β’ 2 =
(β―ββ¨β01ββ©) |
3 | 2 | fveq2i 6895 |
. . . . 5
β’
(β€β₯β2) =
(β€β₯β(β―ββ¨β01ββ©)) |
4 | 3 | imaeq2i 6058 |
. . . 4
β’ (β‘β― β
(β€β₯β2)) = (β‘β― β
(β€β₯β(β―ββ¨β01ββ©))) |
5 | 4 | ineq2i 4210 |
. . 3
β’ (Word
β0 β© (β‘β―
β (β€β₯β2))) = (Word β0 β©
(β‘β― β
(β€β₯β(β―ββ¨β01ββ©)))) |
6 | | eqid 2733 |
. . 3
β’ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))) = ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))) |
7 | 5, 6 | mpteq12i 5255 |
. 2
β’ (π€ β (Word
β0 β© (β‘β―
β (β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))) = (π€ β (Word β0 β©
(β‘β― β
(β€β₯β(β―ββ¨β01ββ©))))
β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))) |
8 | | elin 3965 |
. . . . . 6
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β (π€ β Word
β0 β§ π€
β (β‘β― β
(β€β₯β(β―ββ¨β01ββ©))))) |
9 | 8 | simplbi 499 |
. . . . 5
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β π€ β Word
β0) |
10 | | wrdf 14469 |
. . . . 5
β’ (π€ β Word β0
β π€:(0..^(β―βπ€))βΆβ0) |
11 | 9, 10 | syl 17 |
. . . 4
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β π€:(0..^(β―βπ€))βΆβ0) |
12 | 8 | simprbi 498 |
. . . . . . . . 9
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β π€ β (β‘β― β
(β€β₯β(β―ββ¨β01ββ©)))) |
13 | | hashf 14298 |
. . . . . . . . . 10
β’
β―:VβΆ(β0 βͺ {+β}) |
14 | | ffn 6718 |
. . . . . . . . . 10
β’
(β―:VβΆ(β0 βͺ {+β}) β β―
Fn V) |
15 | | elpreima 7060 |
. . . . . . . . . 10
β’ (β―
Fn V β (π€ β
(β‘β― β
(β€β₯β(β―ββ¨β01ββ©)))
β (π€ β V β§
(β―βπ€) β
(β€β₯β(β―ββ¨β01ββ©))))) |
16 | 13, 14, 15 | mp2b 10 |
. . . . . . . . 9
β’ (π€ β (β‘β― β
(β€β₯β(β―ββ¨β01ββ©)))
β (π€ β V β§
(β―βπ€) β
(β€β₯β(β―ββ¨β01ββ©)))) |
17 | 12, 16 | sylib 217 |
. . . . . . . 8
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β (π€ β V β§
(β―βπ€) β
(β€β₯β(β―ββ¨β01ββ©)))) |
18 | 17 | simprd 497 |
. . . . . . 7
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β (β―βπ€)
β
(β€β₯β(β―ββ¨β01ββ©))) |
19 | 18, 3 | eleqtrrdi 2845 |
. . . . . 6
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β (β―βπ€)
β (β€β₯β2)) |
20 | | uznn0sub 12861 |
. . . . . 6
β’
((β―βπ€)
β (β€β₯β2) β ((β―βπ€) β 2) β
β0) |
21 | 19, 20 | syl 17 |
. . . . 5
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β ((β―βπ€)
β 2) β β0) |
22 | | 1zzd 12593 |
. . . . . . 7
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β 1 β β€) |
23 | | 1p1e2 12337 |
. . . . . . . . 9
β’ (1 + 1) =
2 |
24 | 23 | fveq2i 6895 |
. . . . . . . 8
β’
(β€β₯β(1 + 1)) =
(β€β₯β2) |
25 | 19, 24 | eleqtrrdi 2845 |
. . . . . . 7
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β (β―βπ€)
β (β€β₯β(1 + 1))) |
26 | | peano2uzr 12887 |
. . . . . . 7
β’ ((1
β β€ β§ (β―βπ€) β (β€β₯β(1 +
1))) β (β―βπ€) β
(β€β₯β1)) |
27 | 22, 25, 26 | syl2anc 585 |
. . . . . 6
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β (β―βπ€)
β (β€β₯β1)) |
28 | | nnuz 12865 |
. . . . . 6
β’ β =
(β€β₯β1) |
29 | 27, 28 | eleqtrrdi 2845 |
. . . . 5
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β (β―βπ€)
β β) |
30 | 29 | nnred 12227 |
. . . . . 6
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β (β―βπ€)
β β) |
31 | | 2rp 12979 |
. . . . . . 7
β’ 2 β
β+ |
32 | 31 | a1i 11 |
. . . . . 6
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β 2 β β+) |
33 | 30, 32 | ltsubrpd 13048 |
. . . . 5
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β ((β―βπ€)
β 2) < (β―βπ€)) |
34 | | elfzo0 13673 |
. . . . 5
β’
(((β―βπ€)
β 2) β (0..^(β―βπ€)) β (((β―βπ€) β 2) β β0 β§
(β―βπ€) β
β β§ ((β―βπ€) β 2) < (β―βπ€))) |
35 | 21, 29, 33, 34 | syl3anbrc 1344 |
. . . 4
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β ((β―βπ€)
β 2) β (0..^(β―βπ€))) |
36 | 11, 35 | ffvelcdmd 7088 |
. . 3
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β (π€β((β―βπ€) β 2)) β
β0) |
37 | | fzo0end 13724 |
. . . . 5
β’
((β―βπ€)
β β β ((β―βπ€) β 1) β (0..^(β―βπ€))) |
38 | 29, 37 | syl 17 |
. . . 4
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β ((β―βπ€)
β 1) β (0..^(β―βπ€))) |
39 | 11, 38 | ffvelcdmd 7088 |
. . 3
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β (π€β((β―βπ€) β 1)) β
β0) |
40 | 36, 39 | nn0addcld 12536 |
. 2
β’ (π€ β (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©))))
β ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))) β
β0) |
41 | 7, 40 | fmpti 7112 |
1
β’ (π€ β (Word
β0 β© (β‘β―
β (β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))):(Word β0
β© (β‘β― β
(β€β₯β(β―ββ¨β01ββ©))))βΆβ0 |