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\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	stle0i	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)\le 0\leftrightarrow S\left(A\right)=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		sto1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		stge0	$$⊢S\in \mathrm{States}\to \left(A\in {\mathbf{C}}_{\mathscr{H}}\to 0\le S\left(A\right)\right)$$
3	1 2	mpi	$$⊢S\in \mathrm{States}\to 0\le S\left(A\right)$$
4	3	anim2i	$$⊢\left(S\left(A\right)\le 0\wedge S\in \mathrm{States}\right)\to \left(S\left(A\right)\le 0\wedge 0\le S\left(A\right)\right)$$
5	4	expcom	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)\le 0\to \left(S\left(A\right)\le 0\wedge 0\le S\left(A\right)\right)\right)$$
6		stcl	$$⊢S\in \mathrm{States}\to \left(A\in {\mathbf{C}}_{\mathscr{H}}\to S\left(A\right)\in ℝ\right)$$
7	1 6	mpi	$$⊢S\in \mathrm{States}\to S\left(A\right)\in ℝ$$
8		0re	$$⊢0\in ℝ$$
9		letri3	$$⊢\left(S\left(A\right)\in ℝ\wedge 0\in ℝ\right)\to \left(S\left(A\right)=0\leftrightarrow \left(S\left(A\right)\le 0\wedge 0\le S\left(A\right)\right)\right)$$
10	7 8 9	sylancl	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)=0\leftrightarrow \left(S\left(A\right)\le 0\wedge 0\le S\left(A\right)\right)\right)$$
11	5 10	sylibrd	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)\le 0\to S\left(A\right)=0\right)$$
12		0le0	$$⊢0\le 0$$
13		breq1	$$⊢S\left(A\right)=0\to \left(S\left(A\right)\le 0\leftrightarrow 0\le 0\right)$$
14	12 13	mpbiri	$$⊢S\left(A\right)=0\to S\left(A\right)\le 0$$
15	11 14	impbid1	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)\le 0\leftrightarrow S\left(A\right)=0\right)$$