This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℝ ) → ( 𝐶 < ( 𝐴 − 𝐵 ) → 𝐶 < ( 𝐴 + 𝐵 ) ) )

Proof

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