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