Metamath Proof Explorer

Theorem rprmdvdspow

Description: If a prime element divides a ring "power", it divides the term. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmdvdspow.b 
|- B = ( Base ` R )
rprmdvdspow.p 
|- P = ( RPrime ` R )
rprmdvdspow.d 
|- .|| = ( ||r ` R )
rprmdvdspow.m 
|- M = ( mulGrp ` R )
rprmdvdspow.o 
|- .^ = ( .g ` M )
rprmdvdspow.r 
|- ( ph -> R e. CRing )
rprmdvdspow.x 
|- ( ph -> X e. B )
rprmdvdspow.q 
|- ( ph -> Q e. P )
rprmdvdspow.n 
|- ( ph -> N e. NN0 )
rprmdvdspow.1 
|- ( ph -> Q .|| ( N .^ X ) )
Assertion rprmdvdspow 
|- ( ph -> Q .|| X )

Proof

Step Hyp Ref Expression
1 rprmdvdspow.b 
 |-  B = ( Base ` R )
2 rprmdvdspow.p 
 |-  P = ( RPrime ` R )
3 rprmdvdspow.d 
 |-  .|| = ( ||r ` R )
4 rprmdvdspow.m 
 |-  M = ( mulGrp ` R )
5 rprmdvdspow.o 
 |-  .^ = ( .g ` M )
6 rprmdvdspow.r 
 |-  ( ph -> R e. CRing )
7 rprmdvdspow.x 
 |-  ( ph -> X e. B )
8 rprmdvdspow.q 
 |-  ( ph -> Q e. P )
9 rprmdvdspow.n 
 |-  ( ph -> N e. NN0 )
10 rprmdvdspow.1 
 |-  ( ph -> Q .|| ( N .^ X ) )
11 oveq1 
 |-  ( i = 0 -> ( i .^ X ) = ( 0 .^ X ) )
12 11 breq2d 
 |-  ( i = 0 -> ( Q .|| ( i .^ X ) <-> Q .|| ( 0 .^ X ) ) )
13 12 imbi1d 
 |-  ( i = 0 -> ( ( Q .|| ( i .^ X ) -> Q .|| X ) <-> ( Q .|| ( 0 .^ X ) -> Q .|| X ) ) )
14 oveq1 
 |-  ( i = n -> ( i .^ X ) = ( n .^ X ) )
15 14 breq2d 
 |-  ( i = n -> ( Q .|| ( i .^ X ) <-> Q .|| ( n .^ X ) ) )
16 15 imbi1d 
 |-  ( i = n -> ( ( Q .|| ( i .^ X ) -> Q .|| X ) <-> ( Q .|| ( n .^ X ) -> Q .|| X ) ) )
17 oveq1 
 |-  ( i = ( n + 1 ) -> ( i .^ X ) = ( ( n + 1 ) .^ X ) )
18 17 breq2d 
 |-  ( i = ( n + 1 ) -> ( Q .|| ( i .^ X ) <-> Q .|| ( ( n + 1 ) .^ X ) ) )
19 18 imbi1d 
 |-  ( i = ( n + 1 ) -> ( ( Q .|| ( i .^ X ) -> Q .|| X ) <-> ( Q .|| ( ( n + 1 ) .^ X ) -> Q .|| X ) ) )
20 oveq1 
 |-  ( i = N -> ( i .^ X ) = ( N .^ X ) )
21 20 breq2d 
 |-  ( i = N -> ( Q .|| ( i .^ X ) <-> Q .|| ( N .^ X ) ) )
22 21 imbi1d 
 |-  ( i = N -> ( ( Q .|| ( i .^ X ) -> Q .|| X ) <-> ( Q .|| ( N .^ X ) -> Q .|| X ) ) )
23 4 1 mgpbas 
 |-  B = ( Base ` M )
24 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
25 4 24 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
26 23 25 5 mulg0 
 |-  ( X e. B -> ( 0 .^ X ) = ( 1r ` R ) )
27 7 26 syl 
 |-  ( ph -> ( 0 .^ X ) = ( 1r ` R ) )
28 27 breq2d 
 |-  ( ph -> ( Q .|| ( 0 .^ X ) <-> Q .|| ( 1r ` R ) ) )
29 28 biimpa 
 |-  ( ( ph /\ Q .|| ( 0 .^ X ) ) -> Q .|| ( 1r ` R ) )
30 24 3 2 6 8 rprmndvdsr1 
 |-  ( ph -> -. Q .|| ( 1r ` R ) )
31 30 adantr 
 |-  ( ( ph /\ Q .|| ( 0 .^ X ) ) -> -. Q .|| ( 1r ` R ) )
32 29 31 pm2.21dd 
 |-  ( ( ph /\ Q .|| ( 0 .^ X ) ) -> Q .|| X )
33 32 ex 
 |-  ( ph -> ( Q .|| ( 0 .^ X ) -> Q .|| X ) )
34 simpllr 
 |-  ( ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) /\ Q .|| ( n .^ X ) ) -> ( Q .|| ( n .^ X ) -> Q .|| X ) )
35 34 syldbl2 
 |-  ( ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) /\ Q .|| ( n .^ X ) ) -> Q .|| X )
36 simpr 
 |-  ( ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) /\ Q .|| X ) -> Q .|| X )
37 eqid 
 |-  ( .r ` R ) = ( .r ` R )
38 6 ad3antrrr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) -> R e. CRing )
39 8 ad3antrrr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) -> Q e. P )
40 6 crngringd 
 |-  ( ph -> R e. Ring )
41 4 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
42 40 41 syl 
 |-  ( ph -> M e. Mnd )
43 42 ad3antrrr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) -> M e. Mnd )
44 simpllr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) -> n e. NN0 )
45 7 ad3antrrr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) -> X e. B )
46 23 5 43 44 45 mulgnn0cld 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) -> ( n .^ X ) e. B )
47 42 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> M e. Mnd )
48 simpr 
 |-  ( ( ph /\ n e. NN0 ) -> n e. NN0 )
49 7 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> X e. B )
50 4 37 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
51 23 5 50 mulgnn0p1 
 |-  ( ( M e. Mnd /\ n e. NN0 /\ X e. B ) -> ( ( n + 1 ) .^ X ) = ( ( n .^ X ) ( .r ` R ) X ) )
52 47 48 49 51 syl3anc 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n + 1 ) .^ X ) = ( ( n .^ X ) ( .r ` R ) X ) )
53 52 breq2d 
 |-  ( ( ph /\ n e. NN0 ) -> ( Q .|| ( ( n + 1 ) .^ X ) <-> Q .|| ( ( n .^ X ) ( .r ` R ) X ) ) )
54 53 biimpa 
 |-  ( ( ( ph /\ n e. NN0 ) /\ Q .|| ( ( n + 1 ) .^ X ) ) -> Q .|| ( ( n .^ X ) ( .r ` R ) X ) )
55 54 adantlr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) -> Q .|| ( ( n .^ X ) ( .r ` R ) X ) )
56 1 2 3 37 38 39 46 45 55 rprmdvds 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) -> ( Q .|| ( n .^ X ) \/ Q .|| X ) )
57 35 36 56 mpjaodan 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) /\ Q .|| ( ( n + 1 ) .^ X ) ) -> Q .|| X )
58 57 ex 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( Q .|| ( n .^ X ) -> Q .|| X ) ) -> ( Q .|| ( ( n + 1 ) .^ X ) -> Q .|| X ) )
59 13 16 19 22 33 58 nn0indd 
 |-  ( ( ph /\ N e. NN0 ) -> ( Q .|| ( N .^ X ) -> Q .|| X ) )
60 9 59 mpdan 
 |-  ( ph -> ( Q .|| ( N .^ X ) -> Q .|| X ) )
61 10 60 mpd 
 |-  ( ph -> Q .|| X )