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 ) ) )