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