This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ringm1expp1

Description: Ring exponentiation of minus one: Adding one to the exponent is the same as taking the additive inverse. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses ringm1expp1.1 
|- .1. = ( 1r ` R )
ringm1expp1.2 
|- N = ( invg ` R )
ringm1expp1.3 
|- .^ = ( .g ` ( mulGrp ` R ) )
ringm1expp1.4 
|- ( ph -> R e. Ring )
ringm1expp1.5 
|- ( ph -> K e. NN0 )
Assertion ringm1expp1 
|- ( ph -> ( ( K + 1 ) .^ ( N ` .1. ) ) = ( N ` ( K .^ ( N ` .1. ) ) ) )

Proof

Step Hyp Ref Expression
1 ringm1expp1.1 
 |-  .1. = ( 1r ` R )
2 ringm1expp1.2 
 |-  N = ( invg ` R )
3 ringm1expp1.3 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
4 ringm1expp1.4 
 |-  ( ph -> R e. Ring )
5 ringm1expp1.5 
 |-  ( ph -> K e. NN0 )
6 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
7 6 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
8 4 7 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 4 ringgrpd 
 |-  ( ph -> R e. Grp )
11 9 1 4 ringidcld 
 |-  ( ph -> .1. e. ( Base ` R ) )
12 9 2 10 11 grpinvcld 
 |-  ( ph -> ( N ` .1. ) e. ( Base ` R ) )
13 6 9 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
14 eqid 
 |-  ( .r ` R ) = ( .r ` R )
15 6 14 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
16 13 3 15 mulgnn0p1 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ K e. NN0 /\ ( N ` .1. ) e. ( Base ` R ) ) -> ( ( K + 1 ) .^ ( N ` .1. ) ) = ( ( K .^ ( N ` .1. ) ) ( .r ` R ) ( N ` .1. ) ) )
17 8 5 12 16 syl3anc 
 |-  ( ph -> ( ( K + 1 ) .^ ( N ` .1. ) ) = ( ( K .^ ( N ` .1. ) ) ( .r ` R ) ( N ` .1. ) ) )
18 13 3 8 5 12 mulgnn0cld 
 |-  ( ph -> ( K .^ ( N ` .1. ) ) e. ( Base ` R ) )
19 9 14 1 2 4 18 ringnegr 
 |-  ( ph -> ( ( K .^ ( N ` .1. ) ) ( .r ` R ) ( N ` .1. ) ) = ( N ` ( K .^ ( N ` .1. ) ) ) )
20 17 19 eqtrd 
 |-  ( ph -> ( ( K + 1 ) .^ ( N ` .1. ) ) = ( N ` ( K .^ ( N ` .1. ) ) ) )