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