Metamath Proof Explorer


Theorem sltaddpos1d

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

Ref Expression
Hypotheses sltaddpos.1 φ A No
sltaddpos.2 φ B No
Assertion sltaddpos1d φ 0 s < s A B < s B + s A

Proof

Step Hyp Ref Expression
1 sltaddpos.1 φ A No
2 sltaddpos.2 φ B No
3 0sno 0 s No
4 3 a1i φ 0 s No
5 4 1 2 sltadd2d φ 0 s < s A B + s 0 s < s B + s A
6 2 addsridd φ B + s 0 s = B
7 6 breq1d φ B + s 0 s < s B + s A B < s B + s A
8 5 7 bitrd φ 0 s < s A B < s B + s A