Metamath Proof Explorer

Theorem primrootlekpowne0

Description: There is no smaller power of a primitive root that sends it to the neutral element. (Contributed by metakunt, 15-May-2025)

Ref Expression
Hypotheses primrootlekpowne0.1 
|- ( ph -> R e. CMnd )
primrootlekpowne0.2 
|- ( ph -> K e. NN )
primrootlekpowne0.3 
|- ( ph -> M e. ( R PrimRoots K ) )
primrootlekpowne0.4 
|- ( ph -> N e. ( 1 ... ( K - 1 ) ) )
Assertion primrootlekpowne0 
|- ( ph -> ( N ( .g ` R ) M ) =/= ( 0g ` R ) )

Proof

Step Hyp Ref Expression
1 primrootlekpowne0.1 
 |-  ( ph -> R e. CMnd )
2 primrootlekpowne0.2 
 |-  ( ph -> K e. NN )
3 primrootlekpowne0.3 
 |-  ( ph -> M e. ( R PrimRoots K ) )
4 primrootlekpowne0.4 
 |-  ( ph -> N e. ( 1 ... ( K - 1 ) ) )
5 oveq1 
 |-  ( l = N -> ( l ( .g ` R ) M ) = ( N ( .g ` R ) M ) )
6 5 eqeq1d 
 |-  ( l = N -> ( ( l ( .g ` R ) M ) = ( 0g ` R ) <-> ( N ( .g ` R ) M ) = ( 0g ` R ) ) )
7 breq2 
 |-  ( l = N -> ( K || l <-> K || N ) )
8 6 7 imbi12d 
 |-  ( l = N -> ( ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) <-> ( ( N ( .g ` R ) M ) = ( 0g ` R ) -> K || N ) ) )
9 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
10 eqid 
 |-  ( .g ` R ) = ( .g ` R )
11 1 9 10 isprimroot 
 |-  ( ph -> ( M e. ( R PrimRoots K ) <-> ( M e. ( Base ` R ) /\ ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) )
12 11 biimpd 
 |-  ( ph -> ( M e. ( R PrimRoots K ) -> ( M e. ( Base ` R ) /\ ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) )
13 3 12 mpd 
 |-  ( ph -> ( M e. ( Base ` R ) /\ ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) )
14 13 simp3d 
 |-  ( ph -> A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) )
15 14 adantr 
 |-  ( ( ph /\ ( N ( .g ` R ) M ) = ( 0g ` R ) ) -> A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) )
16 elfznn 
 |-  ( N e. ( 1 ... ( K - 1 ) ) -> N e. NN )
17 4 16 syl 
 |-  ( ph -> N e. NN )
18 17 nnnn0d 
 |-  ( ph -> N e. NN0 )
19 18 adantr 
 |-  ( ( ph /\ ( N ( .g ` R ) M ) = ( 0g ` R ) ) -> N e. NN0 )
20 8 15 19 rspcdva 
 |-  ( ( ph /\ ( N ( .g ` R ) M ) = ( 0g ` R ) ) -> ( ( N ( .g ` R ) M ) = ( 0g ` R ) -> K || N ) )
21 20 syldbl2 
 |-  ( ( ph /\ ( N ( .g ` R ) M ) = ( 0g ` R ) ) -> K || N )
22 17 nnred 
 |-  ( ph -> N e. RR )
23 2 nnred 
 |-  ( ph -> K e. RR )
24 1red 
 |-  ( ph -> 1 e. RR )
25 23 24 resubcld 
 |-  ( ph -> ( K - 1 ) e. RR )
26 elfzle2 
 |-  ( N e. ( 1 ... ( K - 1 ) ) -> N <_ ( K - 1 ) )
27 4 26 syl 
 |-  ( ph -> N <_ ( K - 1 ) )
28 23 ltm1d 
 |-  ( ph -> ( K - 1 ) < K )
29 22 25 23 27 28 lelttrd 
 |-  ( ph -> N < K )
30 22 23 ltnled 
 |-  ( ph -> ( N < K <-> -. K <_ N ) )
31 29 30 mpbid 
 |-  ( ph -> -. K <_ N )
32 9 nn0zd 
 |-  ( ph -> K e. ZZ )
33 dvdsle 
 |-  ( ( K e. ZZ /\ N e. NN ) -> ( K || N -> K <_ N ) )
34 32 17 33 syl2anc 
 |-  ( ph -> ( K || N -> K <_ N ) )
35 34 con3d 
 |-  ( ph -> ( -. K <_ N -> -. K || N ) )
36 31 35 mpd 
 |-  ( ph -> -. K || N )
37 36 adantr 
 |-  ( ( ph /\ ( N ( .g ` R ) M ) = ( 0g ` R ) ) -> -. K || N )
38 21 37 pm2.21dd 
 |-  ( ( ph /\ ( N ( .g ` R ) M ) = ( 0g ` R ) ) -> ( N ( .g ` R ) M ) =/= ( 0g ` R ) )
39 simpr 
 |-  ( ( ph /\ ( N ( .g ` R ) M ) =/= ( 0g ` R ) ) -> ( N ( .g ` R ) M ) =/= ( 0g ` R ) )
40 38 39 pm2.61dane 
 |-  ( ph -> ( N ( .g ` R ) M ) =/= ( 0g ` R ) )