Theorem stle0i

Description: If a state is less than or equal to 0, it is 0. (Contributed by NM, 11-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sto1.1	|- A e. CH
Assertion	stle0i	|- ( S e. States -> ( ( S ` A ) <_ 0 <-> ( S ` A ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		sto1.1	|- A e. CH
2		stge0	|- ( S e. States -> ( A e. CH -> 0 <_ ( S ` A ) ) )
3	1 2	mpi	|- ( S e. States -> 0 <_ ( S ` A ) )
4	3	anim2i	|- ( ( ( S ` A ) <_ 0 /\ S e. States ) -> ( ( S ` A ) <_ 0 /\ 0 <_ ( S ` A ) ) )
5	4	expcom	|- ( S e. States -> ( ( S ` A ) <_ 0 -> ( ( S ` A ) <_ 0 /\ 0 <_ ( S ` A ) ) ) )
6		stcl	|- ( S e. States -> ( A e. CH -> ( S ` A ) e. RR ) )
7	1 6	mpi	|- ( S e. States -> ( S ` A ) e. RR )
8		0re	|- 0 e. RR
9		letri3	|- ( ( ( S ` A ) e. RR /\ 0 e. RR ) -> ( ( S ` A ) = 0 <-> ( ( S ` A ) <_ 0 /\ 0 <_ ( S ` A ) ) ) )
10	7 8 9	sylancl	|- ( S e. States -> ( ( S ` A ) = 0 <-> ( ( S ` A ) <_ 0 /\ 0 <_ ( S ` A ) ) ) )
11	5 10	sylibrd	|- ( S e. States -> ( ( S ` A ) <_ 0 -> ( S ` A ) = 0 ) )
12		0le0	|- 0 <_ 0
13		breq1	|- ( ( S ` A ) = 0 -> ( ( S ` A ) <_ 0 <-> 0 <_ 0 ) )
14	12 13	mpbiri	|- ( ( S ` A ) = 0 -> ( S ` A ) <_ 0 )
15	11 14	impbid1	|- ( S e. States -> ( ( S ` A ) <_ 0 <-> ( S ` A ) = 0 ) )