Metamath Proof Explorer


Theorem elfzoext

Description: Membership of an integer in an extended open range of integers, extension added to the right. (Contributed by AV, 30-Apr-2020) (Proof shortened by AV, 23-Sep-2025)

Ref Expression
Assertion elfzoext
|- ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. ( M ..^ ( N + I ) ) )

Proof

Step Hyp Ref Expression
1 elfzoextl
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. ( M ..^ ( I + N ) ) )
2 elfzoel2
 |-  ( Z e. ( M ..^ N ) -> N e. ZZ )
3 2 zcnd
 |-  ( Z e. ( M ..^ N ) -> N e. CC )
4 3 adantr
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> N e. CC )
5 nn0cn
 |-  ( I e. NN0 -> I e. CC )
6 5 adantl
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> I e. CC )
7 4 6 addcomd
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( N + I ) = ( I + N ) )
8 7 oveq2d
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( M ..^ ( N + I ) ) = ( M ..^ ( I + N ) ) )
9 1 8 eleqtrrd
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. ( M ..^ ( N + I ) ) )