Theorem uzin

Description: Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013)

	Ref	Expression
Assertion	uzin	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge if\left(M\le N,N,M\right)}$$

Proof

Step	Hyp	Ref	Expression
1		uztric	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(N\in {\mathbb{Z}}_{\ge M}\vee M\in {\mathbb{Z}}_{\ge N}\right)$$
2		uzss	$$⊢N\in {\mathbb{Z}}_{\ge M}\to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}$$
3		sseqin2	$$⊢{\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}\leftrightarrow {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge N}$$
4	2 3	sylib	$$⊢N\in {\mathbb{Z}}_{\ge M}\to {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge N}$$
5		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\le N$$
6		iftrue	$$⊢M\le N\to if\left(M\le N,N,M\right)=N$$
7	5 6	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to if\left(M\le N,N,M\right)=N$$
8	7	fveq2d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to {\mathbb{Z}}_{\ge if\left(M\le N,N,M\right)}={\mathbb{Z}}_{\ge N}$$
9	4 8	eqtr4d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge if\left(M\le N,N,M\right)}$$
10		uzss	$$⊢M\in {\mathbb{Z}}_{\ge N}\to {\mathbb{Z}}_{\ge M}\subseteq {\mathbb{Z}}_{\ge N}$$
11		df-ss	$$⊢{\mathbb{Z}}_{\ge M}\subseteq {\mathbb{Z}}_{\ge N}\leftrightarrow {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge M}$$
12	10 11	sylib	$$⊢M\in {\mathbb{Z}}_{\ge N}\to {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge M}$$
13		eluzle	$$⊢M\in {\mathbb{Z}}_{\ge N}\to N\le M$$
14		eluzel2	$$⊢M\in {\mathbb{Z}}_{\ge N}\to N\in \mathbb{Z}$$
15		eluzelz	$$⊢M\in {\mathbb{Z}}_{\ge N}\to M\in \mathbb{Z}$$
16		zre	$$⊢N\in \mathbb{Z}\to N\in ℝ$$
17		zre	$$⊢M\in \mathbb{Z}\to M\in ℝ$$
18		letri3	$$⊢\left(N\in ℝ\wedge M\in ℝ\right)\to \left(N=M\leftrightarrow \left(N\le M\wedge M\le N\right)\right)$$
19	16 17 18	syl2an	$$⊢\left(N\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left(N=M\leftrightarrow \left(N\le M\wedge M\le N\right)\right)$$
20	14 15 19	syl2anc	$$⊢M\in {\mathbb{Z}}_{\ge N}\to \left(N=M\leftrightarrow \left(N\le M\wedge M\le N\right)\right)$$
21	13 20	mpbirand	$$⊢M\in {\mathbb{Z}}_{\ge N}\to \left(N=M\leftrightarrow M\le N\right)$$
22	21	biimprcd	$$⊢M\le N\to \left(M\in {\mathbb{Z}}_{\ge N}\to N=M\right)$$
23	6	eqeq1d	$$⊢M\le N\to \left(if\left(M\le N,N,M\right)=M\leftrightarrow N=M\right)$$
24	22 23	sylibrd	$$⊢M\le N\to \left(M\in {\mathbb{Z}}_{\ge N}\to if\left(M\le N,N,M\right)=M\right)$$
25	24	com12	$$⊢M\in {\mathbb{Z}}_{\ge N}\to \left(M\le N\to if\left(M\le N,N,M\right)=M\right)$$
26		iffalse	$$⊢\neg M\le N\to if\left(M\le N,N,M\right)=M$$
27	25 26	pm2.61d1	$$⊢M\in {\mathbb{Z}}_{\ge N}\to if\left(M\le N,N,M\right)=M$$
28	27	fveq2d	$$⊢M\in {\mathbb{Z}}_{\ge N}\to {\mathbb{Z}}_{\ge if\left(M\le N,N,M\right)}={\mathbb{Z}}_{\ge M}$$
29	12 28	eqtr4d	$$⊢M\in {\mathbb{Z}}_{\ge N}\to {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge if\left(M\le N,N,M\right)}$$
30	9 29	jaoi	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\vee M\in {\mathbb{Z}}_{\ge N}\right)\to {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge if\left(M\le N,N,M\right)}$$
31	1 30	syl	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge if\left(M\le N,N,M\right)}$$