Step 
Hyp 
Ref 
Expression 
1 

0z 
⊢ 0 ∈ ℤ 
2 

expval 
⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℤ ) → ( 𝐴 ↑ 0 ) = if ( 0 = 0 , 1 , if ( 0 < 0 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 0 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘  0 ) ) ) ) ) 
3 
1 2

mpan2 
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = if ( 0 = 0 , 1 , if ( 0 < 0 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 0 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘  0 ) ) ) ) ) 
4 

eqid 
⊢ 0 = 0 
5 
4

iftruei 
⊢ if ( 0 = 0 , 1 , if ( 0 < 0 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 0 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘  0 ) ) ) ) = 1 
6 
3 5

eqtrdi 
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 ) 