Theorem stge1i

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

	Ref	Expression
Hypothesis	sto1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	stge1i	$$⊢S\in \mathrm{States}\to \left(1\le S\left(A\right)\leftrightarrow S\left(A\right)=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		sto1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		stle1	$$⊢S\in \mathrm{States}\to \left(A\in {\mathbf{C}}_{\mathscr{H}}\to S\left(A\right)\le 1\right)$$
3	1 2	mpi	$$⊢S\in \mathrm{States}\to S\left(A\right)\le 1$$
4	3	anim1i	$$⊢\left(S\in \mathrm{States}\wedge 1\le S\left(A\right)\right)\to \left(S\left(A\right)\le 1\wedge 1\le S\left(A\right)\right)$$
5	4	ex	$$⊢S\in \mathrm{States}\to \left(1\le S\left(A\right)\to \left(S\left(A\right)\le 1\wedge 1\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		1re	$$⊢1\in ℝ$$
9		letri3	$$⊢\left(S\left(A\right)\in ℝ\wedge 1\in ℝ\right)\to \left(S\left(A\right)=1\leftrightarrow \left(S\left(A\right)\le 1\wedge 1\le S\left(A\right)\right)\right)$$
10	7 8 9	sylancl	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)=1\leftrightarrow \left(S\left(A\right)\le 1\wedge 1\le S\left(A\right)\right)\right)$$
11	5 10	sylibrd	$$⊢S\in \mathrm{States}\to \left(1\le S\left(A\right)\to S\left(A\right)=1\right)$$
12		1le1	$$⊢1\le 1$$
13		breq2	$$⊢S\left(A\right)=1\to \left(1\le S\left(A\right)\leftrightarrow 1\le 1\right)$$
14	12 13	mpbiri	$$⊢S\left(A\right)=1\to 1\le S\left(A\right)$$
15	11 14	impbid1	$$⊢S\in \mathrm{States}\to \left(1\le S\left(A\right)\leftrightarrow S\left(A\right)=1\right)$$