Metamath Proof Explorer

Theorem wrdlenge2n0

Description: A word with length at least 2 is not empty. (Contributed by AV, 18-Jun-2018) (Proof shortened by AV, 14-Oct-2018)

Ref Expression
Assertion wrdlenge2n0 
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> W =/= (/) )

Proof

Step Hyp Ref Expression
1 1red 
 |-  ( W e. Word V -> 1 e. RR )
2 2re 
 |-  2 e. RR
3 2 a1i 
 |-  ( W e. Word V -> 2 e. RR )
4 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
5 4 nn0red 
 |-  ( W e. Word V -> ( # ` W ) e. RR )
6 1 3 5 3jca 
 |-  ( W e. Word V -> ( 1 e. RR /\ 2 e. RR /\ ( # ` W ) e. RR ) )
7 6 adantr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( 1 e. RR /\ 2 e. RR /\ ( # ` W ) e. RR ) )
8 simpr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 <_ ( # ` W ) )
9 1lt2 
 |-  1 < 2
10 8 9 jctil 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( 1 < 2 /\ 2 <_ ( # ` W ) ) )
11 ltleletr 
 |-  ( ( 1 e. RR /\ 2 e. RR /\ ( # ` W ) e. RR ) -> ( ( 1 < 2 /\ 2 <_ ( # ` W ) ) -> 1 <_ ( # ` W ) ) )
12 7 10 11 sylc 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 1 <_ ( # ` W ) )
13 wrdlenge1n0 
 |-  ( W e. Word V -> ( W =/= (/) <-> 1 <_ ( # ` W ) ) )
14 13 adantr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( W =/= (/) <-> 1 <_ ( # ` W ) ) )
15 12 14 mpbird 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> W =/= (/) )