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	$$⊢\phi \to N\in \mathbb{Z}$$
	zltlesub.a	$$⊢\phi \to A\in ℝ$$
	zltlesub.nlea	$$⊢\phi \to N\le A$$
	zltlesub.b	$$⊢\phi \to B\in ℝ$$
	zltlesub.blt1	$$⊢\phi \to B<1$$
	zltlesub.asb	$$⊢\phi \to A-B\in \mathbb{Z}$$
Assertion	zltlesub	$$⊢\phi \to N\le A-B$$

Proof

Step	Hyp	Ref	Expression
1		zltlesub.n	$$⊢\phi \to N\in \mathbb{Z}$$
2		zltlesub.a	$$⊢\phi \to A\in ℝ$$
3		zltlesub.nlea	$$⊢\phi \to N\le A$$
4		zltlesub.b	$$⊢\phi \to B\in ℝ$$
5		zltlesub.blt1	$$⊢\phi \to B<1$$
6		zltlesub.asb	$$⊢\phi \to A-B\in \mathbb{Z}$$
7	1	zred	$$⊢\phi \to N\in ℝ$$
8	6	zred	$$⊢\phi \to A-B\in ℝ$$
9	8 4	readdcld	$$⊢\phi \to A-B+B\in ℝ$$
10		peano2re	$$⊢A-B\in ℝ\to A-B+1\in ℝ$$
11	8 10	syl	$$⊢\phi \to A-B+1\in ℝ$$
12	2	recnd	$$⊢\phi \to A\in ℂ$$
13	4	recnd	$$⊢\phi \to B\in ℂ$$
14	12 13	npcand	$$⊢\phi \to A-B+B=A$$
15	3 14	breqtrrd	$$⊢\phi \to N\le A-B+B$$
16		1red	$$⊢\phi \to 1\in ℝ$$
17	4 16 8 5	ltadd2dd	$$⊢\phi \to A-B+B<A-B+1$$
18	7 9 11 15 17	lelttrd	$$⊢\phi \to N<A-B+1$$
19		zleltp1	$$⊢\left(N\in \mathbb{Z}\wedge A-B\in \mathbb{Z}\right)\to \left(N\le A-B\leftrightarrow N<A-B+1\right)$$
20	1 6 19	syl2anc	$$⊢\phi \to \left(N\le A-B\leftrightarrow N<A-B+1\right)$$
21	18 20	mpbird	$$⊢\phi \to N\le A-B$$