Metamath Proof Explorer

Theorem s5len

Description: The length of a length 5 string. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s5len 
|- ( # ` <" A B C D E "> ) = 5

Proof

Step Hyp Ref Expression
1 df-s5 
 |-  <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
2 s4cli 
 |-  <" A B C D "> e. Word _V
3 s4len 
 |-  ( # ` <" A B C D "> ) = 4
4 4p1e5 
 |-  ( 4 + 1 ) = 5
5 1 2 3 4 cats1len 
 |-  ( # ` <" A B C D E "> ) = 5