# Metamath Proof Explorer

## Theorem difgtsumgt

Description: If the difference of a real number and a nonnegative integer is greater than another real number, the sum of the real number and the nonnegative integer is also greater than the other real number. (Contributed by AV, 13-Aug-2021)

Ref Expression
Assertion difgtsumgt ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to \left({C}<{A}-{B}\to {C}<{A}+{B}\right)$

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
2 nn0cn ${⊢}{B}\in {ℕ}_{0}\to {B}\in ℂ$
3 1 2 anim12i ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\right)\to \left({A}\in ℂ\wedge {B}\in ℂ\right)$
4 3 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to \left({A}\in ℂ\wedge {B}\in ℂ\right)$
5 negsub ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+\left(-{B}\right)={A}-{B}$
6 4 5 syl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to {A}+\left(-{B}\right)={A}-{B}$
7 6 eqcomd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to {A}-{B}={A}+\left(-{B}\right)$
8 7 breq2d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to \left({C}<{A}-{B}↔{C}<{A}+\left(-{B}\right)\right)$
9 simp3 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to {C}\in ℝ$
10 simp1 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to {A}\in ℝ$
11 nn0re ${⊢}{B}\in {ℕ}_{0}\to {B}\in ℝ$
12 11 renegcld ${⊢}{B}\in {ℕ}_{0}\to -{B}\in ℝ$
13 12 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to -{B}\in ℝ$
14 10 13 readdcld ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to {A}+\left(-{B}\right)\in ℝ$
15 11 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to {B}\in ℝ$
16 10 15 readdcld ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to {A}+{B}\in ℝ$
17 9 14 16 3jca ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to \left({C}\in ℝ\wedge {A}+\left(-{B}\right)\in ℝ\wedge {A}+{B}\in ℝ\right)$
18 nn0negleid ${⊢}{B}\in {ℕ}_{0}\to -{B}\le {B}$
19 18 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to -{B}\le {B}$
20 13 15 10 19 leadd2dd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to {A}+\left(-{B}\right)\le {A}+{B}$
21 17 20 lelttrdi ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to \left({C}<{A}+\left(-{B}\right)\to {C}<{A}+{B}\right)$
22 8 21 sylbid ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge {C}\in ℝ\right)\to \left({C}<{A}-{B}\to {C}<{A}+{B}\right)$