Metamath Proof Explorer


Theorem uzinico2

Description: An upper interval of integers is the intersection of a larger upper interval of integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis uzinico2.1
|- ( ph -> N e. ( ZZ>= ` M ) )
Assertion uzinico2
|- ( ph -> ( ZZ>= ` N ) = ( ( ZZ>= ` M ) i^i ( N [,) +oo ) ) )

Proof

Step Hyp Ref Expression
1 uzinico2.1
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 inass
 |-  ( ( ( ZZ>= ` M ) i^i ZZ ) i^i ( N [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( ZZ i^i ( N [,) +oo ) ) )
3 2 a1i
 |-  ( ph -> ( ( ( ZZ>= ` M ) i^i ZZ ) i^i ( N [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( ZZ i^i ( N [,) +oo ) ) ) )
4 incom
 |-  ( ( ZZ>= ` M ) i^i ( ZZ i^i ( N [,) +oo ) ) ) = ( ( ZZ i^i ( N [,) +oo ) ) i^i ( ZZ>= ` M ) )
5 4 a1i
 |-  ( ph -> ( ( ZZ>= ` M ) i^i ( ZZ i^i ( N [,) +oo ) ) ) = ( ( ZZ i^i ( N [,) +oo ) ) i^i ( ZZ>= ` M ) ) )
6 uzssz
 |-  ( ZZ>= ` M ) C_ ZZ
7 6 a1i
 |-  ( ph -> ( ZZ>= ` M ) C_ ZZ )
8 7 1 sseldd
 |-  ( ph -> N e. ZZ )
9 eqid
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
10 8 9 uzinico
 |-  ( ph -> ( ZZ>= ` N ) = ( ZZ i^i ( N [,) +oo ) ) )
11 10 eqcomd
 |-  ( ph -> ( ZZ i^i ( N [,) +oo ) ) = ( ZZ>= ` N ) )
12 11 ineq1d
 |-  ( ph -> ( ( ZZ i^i ( N [,) +oo ) ) i^i ( ZZ>= ` M ) ) = ( ( ZZ>= ` N ) i^i ( ZZ>= ` M ) ) )
13 1 uzssd
 |-  ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
14 df-ss
 |-  ( ( ZZ>= ` N ) C_ ( ZZ>= ` M ) <-> ( ( ZZ>= ` N ) i^i ( ZZ>= ` M ) ) = ( ZZ>= ` N ) )
15 13 14 sylib
 |-  ( ph -> ( ( ZZ>= ` N ) i^i ( ZZ>= ` M ) ) = ( ZZ>= ` N ) )
16 5 12 15 3eqtrd
 |-  ( ph -> ( ( ZZ>= ` M ) i^i ( ZZ i^i ( N [,) +oo ) ) ) = ( ZZ>= ` N ) )
17 uzssz
 |-  ( ZZ>= ` N ) C_ ZZ
18 df-ss
 |-  ( ( ZZ>= ` N ) C_ ZZ <-> ( ( ZZ>= ` N ) i^i ZZ ) = ( ZZ>= ` N ) )
19 17 18 mpbi
 |-  ( ( ZZ>= ` N ) i^i ZZ ) = ( ZZ>= ` N )
20 19 a1i
 |-  ( ph -> ( ( ZZ>= ` N ) i^i ZZ ) = ( ZZ>= ` N ) )
21 20 eqcomd
 |-  ( ph -> ( ZZ>= ` N ) = ( ( ZZ>= ` N ) i^i ZZ ) )
22 3 16 21 3eqtrrd
 |-  ( ph -> ( ( ZZ>= ` N ) i^i ZZ ) = ( ( ( ZZ>= ` M ) i^i ZZ ) i^i ( N [,) +oo ) ) )
23 df-ss
 |-  ( ( ZZ>= ` M ) C_ ZZ <-> ( ( ZZ>= ` M ) i^i ZZ ) = ( ZZ>= ` M ) )
24 6 23 mpbi
 |-  ( ( ZZ>= ` M ) i^i ZZ ) = ( ZZ>= ` M )
25 24 ineq1i
 |-  ( ( ( ZZ>= ` M ) i^i ZZ ) i^i ( N [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( N [,) +oo ) )
26 25 a1i
 |-  ( ph -> ( ( ( ZZ>= ` M ) i^i ZZ ) i^i ( N [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( N [,) +oo ) ) )
27 22 20 26 3eqtr3d
 |-  ( ph -> ( ZZ>= ` N ) = ( ( ZZ>= ` M ) i^i ( N [,) +oo ) ) )