Metamath Proof Explorer


Theorem sltsubposd

Description: Subtraction of a positive number decreases the sum. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Hypotheses sltsubpos.1 φ A No
sltsubpos.2 φ B No
Assertion sltsubposd φ 0 s < s A B - s A < s B

Proof

Step Hyp Ref Expression
1 sltsubpos.1 φ A No
2 sltsubpos.2 φ B No
3 0sno 0 s No
4 3 a1i φ 0 s No
5 4 1 2 sltsub2d φ 0 s < s A B - s A < s B - s 0 s
6 subsid1 B No B - s 0 s = B
7 2 6 syl φ B - s 0 s = B
8 7 breq2d φ B - s A < s B - s 0 s B - s A < s B
9 5 8 bitrd φ 0 s < s A B - s A < s B