Theorem zltlesub

Description: If an integer N is less than or equal to a real, and we subtract a quantity less than 1 , then N is less than or equal to the result. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	zltlesub.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	zltlesub.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	zltlesub.nlea	⊢ ( 𝜑 → 𝑁 ≤ 𝐴 )
	zltlesub.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	zltlesub.blt1	⊢ ( 𝜑 → 𝐵 < 1 )
	zltlesub.asb	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℤ )
Assertion	zltlesub	⊢ ( 𝜑 → 𝑁 ≤ ( 𝐴 − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		zltlesub.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
2		zltlesub.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3		zltlesub.nlea	⊢ ( 𝜑 → 𝑁 ≤ 𝐴 )
4		zltlesub.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		zltlesub.blt1	⊢ ( 𝜑 → 𝐵 < 1 )
6		zltlesub.asb	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℤ )
7	1	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
8	6	zred	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℝ )
9	8 4	readdcld	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) + 𝐵 ) ∈ ℝ )
10		peano2re	⊢ ( ( 𝐴 − 𝐵 ) ∈ ℝ → ( ( 𝐴 − 𝐵 ) + 1 ) ∈ ℝ )
11	8 10	syl	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) + 1 ) ∈ ℝ )
12	2	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
13	4	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
14	12 13	npcand	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) + 𝐵 ) = 𝐴 )
15	3 14	breqtrrd	⊢ ( 𝜑 → 𝑁 ≤ ( ( 𝐴 − 𝐵 ) + 𝐵 ) )
16		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
17	4 16 8 5	ltadd2dd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) + 𝐵 ) < ( ( 𝐴 − 𝐵 ) + 1 ) )
18	7 9 11 15 17	lelttrd	⊢ ( 𝜑 → 𝑁 < ( ( 𝐴 − 𝐵 ) + 1 ) )
19		zleltp1	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) → ( 𝑁 ≤ ( 𝐴 − 𝐵 ) ↔ 𝑁 < ( ( 𝐴 − 𝐵 ) + 1 ) ) )
20	1 6 19	syl2anc	⊢ ( 𝜑 → ( 𝑁 ≤ ( 𝐴 − 𝐵 ) ↔ 𝑁 < ( ( 𝐴 − 𝐵 ) + 1 ) ) )
21	18 20	mpbird	⊢ ( 𝜑 → 𝑁 ≤ ( 𝐴 − 𝐵 ) )