Metamath Proof Explorer


Theorem stge0

Description: The value of a state is nonnegative. (Contributed by NM, 24-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion stge0
|- ( S e. States -> ( A e. CH -> 0 <_ ( S ` A ) ) )

Proof

Step Hyp Ref Expression
1 sticl
 |-  ( S e. States -> ( A e. CH -> ( S ` A ) e. ( 0 [,] 1 ) ) )
2 elicc01
 |-  ( ( S ` A ) e. ( 0 [,] 1 ) <-> ( ( S ` A ) e. RR /\ 0 <_ ( S ` A ) /\ ( S ` A ) <_ 1 ) )
3 2 simp2bi
 |-  ( ( S ` A ) e. ( 0 [,] 1 ) -> 0 <_ ( S ` A ) )
4 1 3 syl6
 |-  ( S e. States -> ( A e. CH -> 0 <_ ( S ` A ) ) )