Step | Hyp | Ref
| Expression |
1 | | ccatlen 14470 |
. . . . . . 7
β’ ((π΄ β Word π β§ π΅ β Word π) β (β―β(π΄ ++ π΅)) = ((β―βπ΄) + (β―βπ΅))) |
2 | 1 | oveq1d 7377 |
. . . . . 6
β’ ((π΄ β Word π β§ π΅ β Word π) β ((β―β(π΄ ++ π΅)) β 1) = (((β―βπ΄) + (β―βπ΅)) β 1)) |
3 | 2 | 3adant3 1133 |
. . . . 5
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β ((β―β(π΄ ++ π΅)) β 1) = (((β―βπ΄) + (β―βπ΅)) β 1)) |
4 | | lencl 14428 |
. . . . . . . . . 10
β’ (π΄ β Word π β (β―βπ΄) β
β0) |
5 | 4 | nn0zd 12532 |
. . . . . . . . 9
β’ (π΄ β Word π β (β―βπ΄) β β€) |
6 | | lennncl 14429 |
. . . . . . . . 9
β’ ((π΅ β Word π β§ π΅ β β
) β (β―βπ΅) β
β) |
7 | | simpl 484 |
. . . . . . . . . 10
β’
(((β―βπ΄)
β β€ β§ (β―βπ΅) β β) β
(β―βπ΄) β
β€) |
8 | | nnz 12527 |
. . . . . . . . . . 11
β’
((β―βπ΅)
β β β (β―βπ΅) β β€) |
9 | | zaddcl 12550 |
. . . . . . . . . . 11
β’
(((β―βπ΄)
β β€ β§ (β―βπ΅) β β€) β
((β―βπ΄) +
(β―βπ΅)) β
β€) |
10 | 8, 9 | sylan2 594 |
. . . . . . . . . 10
β’
(((β―βπ΄)
β β€ β§ (β―βπ΅) β β) β
((β―βπ΄) +
(β―βπ΅)) β
β€) |
11 | | zre 12510 |
. . . . . . . . . . 11
β’
((β―βπ΄)
β β€ β (β―βπ΄) β β) |
12 | | nnrp 12933 |
. . . . . . . . . . 11
β’
((β―βπ΅)
β β β (β―βπ΅) β
β+) |
13 | | ltaddrp 12959 |
. . . . . . . . . . 11
β’
(((β―βπ΄)
β β β§ (β―βπ΅) β β+) β
(β―βπ΄) <
((β―βπ΄) +
(β―βπ΅))) |
14 | 11, 12, 13 | syl2an 597 |
. . . . . . . . . 10
β’
(((β―βπ΄)
β β€ β§ (β―βπ΅) β β) β
(β―βπ΄) <
((β―βπ΄) +
(β―βπ΅))) |
15 | 7, 10, 14 | 3jca 1129 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β€ β§ (β―βπ΅) β β) β
((β―βπ΄) β
β€ β§ ((β―βπ΄) + (β―βπ΅)) β β€ β§ (β―βπ΄) < ((β―βπ΄) + (β―βπ΅)))) |
16 | 5, 6, 15 | syl2an 597 |
. . . . . . . 8
β’ ((π΄ β Word π β§ (π΅ β Word π β§ π΅ β β
)) β ((β―βπ΄) β β€ β§
((β―βπ΄) +
(β―βπ΅)) β
β€ β§ (β―βπ΄) < ((β―βπ΄) + (β―βπ΅)))) |
17 | 16 | 3impb 1116 |
. . . . . . 7
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β ((β―βπ΄) β β€ β§
((β―βπ΄) +
(β―βπ΅)) β
β€ β§ (β―βπ΄) < ((β―βπ΄) + (β―βπ΅)))) |
18 | | fzolb 13585 |
. . . . . . 7
β’
((β―βπ΄)
β ((β―βπ΄)..^((β―βπ΄) + (β―βπ΅))) β ((β―βπ΄) β β€ β§ ((β―βπ΄) + (β―βπ΅)) β β€ β§
(β―βπ΄) <
((β―βπ΄) +
(β―βπ΅)))) |
19 | 17, 18 | sylibr 233 |
. . . . . 6
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β (β―βπ΄) β ((β―βπ΄)..^((β―βπ΄) + (β―βπ΅)))) |
20 | | fzoend 13670 |
. . . . . 6
β’
((β―βπ΄)
β ((β―βπ΄)..^((β―βπ΄) + (β―βπ΅))) β (((β―βπ΄) + (β―βπ΅)) β 1) β
((β―βπ΄)..^((β―βπ΄) + (β―βπ΅)))) |
21 | 19, 20 | syl 17 |
. . . . 5
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β (((β―βπ΄) + (β―βπ΅)) β 1) β
((β―βπ΄)..^((β―βπ΄) + (β―βπ΅)))) |
22 | 3, 21 | eqeltrd 2838 |
. . . 4
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β ((β―β(π΄ ++ π΅)) β 1) β ((β―βπ΄)..^((β―βπ΄) + (β―βπ΅)))) |
23 | | ccatval2 14473 |
. . . 4
β’ ((π΄ β Word π β§ π΅ β Word π β§ ((β―β(π΄ ++ π΅)) β 1) β ((β―βπ΄)..^((β―βπ΄) + (β―βπ΅)))) β ((π΄ ++ π΅)β((β―β(π΄ ++ π΅)) β 1)) = (π΅β(((β―β(π΄ ++ π΅)) β 1) β (β―βπ΄)))) |
24 | 22, 23 | syld3an3 1410 |
. . 3
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β ((π΄ ++ π΅)β((β―β(π΄ ++ π΅)) β 1)) = (π΅β(((β―β(π΄ ++ π΅)) β 1) β (β―βπ΄)))) |
25 | 2 | oveq1d 7377 |
. . . . . 6
β’ ((π΄ β Word π β§ π΅ β Word π) β (((β―β(π΄ ++ π΅)) β 1) β (β―βπ΄)) = ((((β―βπ΄) + (β―βπ΅)) β 1) β
(β―βπ΄))) |
26 | 4 | nn0cnd 12482 |
. . . . . . 7
β’ (π΄ β Word π β (β―βπ΄) β β) |
27 | | lencl 14428 |
. . . . . . . 8
β’ (π΅ β Word π β (β―βπ΅) β
β0) |
28 | 27 | nn0cnd 12482 |
. . . . . . 7
β’ (π΅ β Word π β (β―βπ΅) β β) |
29 | | addcl 11140 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ (β―βπ΅) β β) β
((β―βπ΄) +
(β―βπ΅)) β
β) |
30 | | 1cnd 11157 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ (β―βπ΅) β β) β 1 β
β) |
31 | | simpl 484 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ (β―βπ΅) β β) β
(β―βπ΄) β
β) |
32 | 29, 30, 31 | sub32d 11551 |
. . . . . . . 8
β’
(((β―βπ΄)
β β β§ (β―βπ΅) β β) β
((((β―βπ΄) +
(β―βπ΅)) β
1) β (β―βπ΄)) = ((((β―βπ΄) + (β―βπ΅)) β (β―βπ΄)) β 1)) |
33 | | pncan2 11415 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ (β―βπ΅) β β) β
(((β―βπ΄) +
(β―βπ΅)) β
(β―βπ΄)) =
(β―βπ΅)) |
34 | 33 | oveq1d 7377 |
. . . . . . . 8
β’
(((β―βπ΄)
β β β§ (β―βπ΅) β β) β
((((β―βπ΄) +
(β―βπ΅)) β
(β―βπ΄)) β
1) = ((β―βπ΅)
β 1)) |
35 | 32, 34 | eqtrd 2777 |
. . . . . . 7
β’
(((β―βπ΄)
β β β§ (β―βπ΅) β β) β
((((β―βπ΄) +
(β―βπ΅)) β
1) β (β―βπ΄)) = ((β―βπ΅) β 1)) |
36 | 26, 28, 35 | syl2an 597 |
. . . . . 6
β’ ((π΄ β Word π β§ π΅ β Word π) β ((((β―βπ΄) + (β―βπ΅)) β 1) β (β―βπ΄)) = ((β―βπ΅) β 1)) |
37 | 25, 36 | eqtrd 2777 |
. . . . 5
β’ ((π΄ β Word π β§ π΅ β Word π) β (((β―β(π΄ ++ π΅)) β 1) β (β―βπ΄)) = ((β―βπ΅) β 1)) |
38 | 37 | 3adant3 1133 |
. . . 4
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β
(((β―β(π΄ ++
π΅)) β 1) β
(β―βπ΄)) =
((β―βπ΅) β
1)) |
39 | 38 | fveq2d 6851 |
. . 3
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β (π΅β(((β―β(π΄ ++ π΅)) β 1) β (β―βπ΄))) = (π΅β((β―βπ΅) β 1))) |
40 | 24, 39 | eqtrd 2777 |
. 2
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β ((π΄ ++ π΅)β((β―β(π΄ ++ π΅)) β 1)) = (π΅β((β―βπ΅) β 1))) |
41 | | ovex 7395 |
. . 3
β’ (π΄ ++ π΅) β V |
42 | | lsw 14459 |
. . 3
β’ ((π΄ ++ π΅) β V β (lastSβ(π΄ ++ π΅)) = ((π΄ ++ π΅)β((β―β(π΄ ++ π΅)) β 1))) |
43 | 41, 42 | mp1i 13 |
. 2
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β (lastSβ(π΄ ++ π΅)) = ((π΄ ++ π΅)β((β―β(π΄ ++ π΅)) β 1))) |
44 | | lsw 14459 |
. . 3
β’ (π΅ β Word π β (lastSβπ΅) = (π΅β((β―βπ΅) β 1))) |
45 | 44 | 3ad2ant2 1135 |
. 2
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β (lastSβπ΅) = (π΅β((β―βπ΅) β 1))) |
46 | 40, 43, 45 | 3eqtr4d 2787 |
1
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β
) β (lastSβ(π΄ ++ π΅)) = (lastSβπ΅)) |