Description: Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 104.1 of Gleason p. 134. (Contributed by Mario Carneiro, 28May2016)
Ref  Expression  

Hypotheses  expcld.1   ( ph > A e. CC ) 

expcld.2   ( ph > N e. NN0 ) 

Assertion  expp1d   ( ph > ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) ) 
Step  Hyp  Ref  Expression 

1  expcld.1   ( ph > A e. CC ) 

2  expcld.2   ( ph > N e. NN0 ) 

3  expp1   ( ( A e. CC /\ N e. NN0 ) > ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) ) 

4  1 2 3  syl2anc   ( ph > ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) ) 