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	⊢ 𝐴 ∈ Cℋ
Assertion	stle0i	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) ≤ 0 ↔ ( 𝑆 ‘ 𝐴 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		sto1.1	⊢ 𝐴 ∈ Cℋ
2		stge0	⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → 0 ≤ ( 𝑆 ‘ 𝐴 ) ) )
3	1 2	mpi	⊢ ( 𝑆 ∈ States → 0 ≤ ( 𝑆 ‘ 𝐴 ) )
4	3	anim2i	⊢ ( ( ( 𝑆 ‘ 𝐴 ) ≤ 0 ∧ 𝑆 ∈ States ) → ( ( 𝑆 ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( 𝑆 ‘ 𝐴 ) ) )
5	4	expcom	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) ≤ 0 → ( ( 𝑆 ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( 𝑆 ‘ 𝐴 ) ) ) )
6		stcl	⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) ∈ ℝ ) )
7	1 6	mpi	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
8		0re	⊢ 0 ∈ ℝ
9		letri3	⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) = 0 ↔ ( ( 𝑆 ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( 𝑆 ‘ 𝐴 ) ) ) )
10	7 8 9	sylancl	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) = 0 ↔ ( ( 𝑆 ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( 𝑆 ‘ 𝐴 ) ) ) )
11	5 10	sylibrd	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) ≤ 0 → ( 𝑆 ‘ 𝐴 ) = 0 ) )
12		0le0	⊢ 0 ≤ 0
13		breq1	⊢ ( ( 𝑆 ‘ 𝐴 ) = 0 → ( ( 𝑆 ‘ 𝐴 ) ≤ 0 ↔ 0 ≤ 0 ) )
14	12 13	mpbiri	⊢ ( ( 𝑆 ‘ 𝐴 ) = 0 → ( 𝑆 ‘ 𝐴 ) ≤ 0 )
15	11 14	impbid1	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) ≤ 0 ↔ ( 𝑆 ‘ 𝐴 ) = 0 ) )