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 ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → C < A − B → C < A + B

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 nn0cn ⊢ B ∈ ℕ 0 → B ∈ ℂ
3 1 2 anim12i ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 → A ∈ ℂ ∧ B ∈ ℂ
4 3 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → A ∈ ℂ ∧ B ∈ ℂ
5 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
6 4 5 syl ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → A + − B = A − B
7 6 eqcomd ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → A − B = A + − B
8 7 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → C < A − B ↔ C < A + − B
9 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → C ∈ ℝ
10 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → A ∈ ℝ
11 nn0re ⊢ B ∈ ℕ 0 → B ∈ ℝ
12 11 renegcld ⊢ B ∈ ℕ 0 → − B ∈ ℝ
13 12 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → − B ∈ ℝ
14 10 13 readdcld ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → A + − B ∈ ℝ
15 11 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → B ∈ ℝ
16 10 15 readdcld ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → A + B ∈ ℝ
17 9 14 16 3jca ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → C ∈ ℝ ∧ A + − B ∈ ℝ ∧ A + B ∈ ℝ
18 nn0negleid ⊢ B ∈ ℕ 0 → − B ≤ B
19 18 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → − B ≤ B
20 13 15 10 19 leadd2dd ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → A + − B ≤ A + B
21 17 20 lelttrdi ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → C < A + − B → C < A + B
22 8 21 sylbid ⊢ A ∈ ℝ ∧ B ∈ ℕ 0 ∧ C ∈ ℝ → C < A − B → C < A + B