Step |
Hyp |
Ref |
Expression |
1 |
|
elfzoextl |
⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ∈ ( 𝑀 ..^ ( 𝐼 + 𝑁 ) ) ) |
2 |
|
elfzoel2 |
⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ ) |
3 |
2
|
zcnd |
⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℂ ) |
4 |
3
|
adantr |
⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℂ ) |
5 |
|
nn0cn |
⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℂ ) |
6 |
5
|
adantl |
⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℂ ) |
7 |
4 6
|
addcomd |
⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑁 + 𝐼 ) = ( 𝐼 + 𝑁 ) ) |
8 |
7
|
oveq2d |
⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) = ( 𝑀 ..^ ( 𝐼 + 𝑁 ) ) ) |
9 |
1 8
|
eleqtrrd |
⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ∈ ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) ) |