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 𝐴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 ) )