Description: Addition of positive and nonnegative numbers is positive. (Contributed by Asger C. Ipsen, 12-May-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | leidd.1 | |- ( ph -> A e. RR ) |
|
ltnegd.2 | |- ( ph -> B e. RR ) |
||
addgtge0d.3 | |- ( ph -> 0 < A ) |
||
addgtge0d.4 | |- ( ph -> 0 <_ B ) |
||
Assertion | addgtge0d | |- ( ph -> 0 < ( A + B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leidd.1 | |- ( ph -> A e. RR ) |
|
2 | ltnegd.2 | |- ( ph -> B e. RR ) |
|
3 | addgtge0d.3 | |- ( ph -> 0 < A ) |
|
4 | addgtge0d.4 | |- ( ph -> 0 <_ B ) |
|
5 | addgtge0 | |- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 <_ B ) ) -> 0 < ( A + B ) ) |
|
6 | 1 2 3 4 5 | syl22anc | |- ( ph -> 0 < ( A + B ) ) |