Metamath Proof Explorer


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 C
Assertion stle0i S States S A 0 S A = 0

Proof

Step Hyp Ref Expression
1 sto1.1 A C
2 stge0 S States A C 0 S A
3 1 2 mpi S States 0 S A
4 3 anim2i S A 0 S States S A 0 0 S A
5 4 expcom S States S A 0 S A 0 0 S A
6 stcl S States A C S A
7 1 6 mpi S States S A
8 0re 0
9 letri3 S A 0 S A = 0 S A 0 0 S A
10 7 8 9 sylancl S States S A = 0 S A 0 0 S A
11 5 10 sylibrd S 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 States S A 0 S A = 0