Metamath Proof Explorer

Theorem aks6d1c1p8

Description: If a number E is introspective to F , then so are its powers. (Contributed by metakunt, 30-Apr-2025)

Ref Expression
Hypotheses aks6d1c1.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
aks6d1c1.2 
|- S = ( Poly1 ` K )
aks6d1c1.3 
|- B = ( Base ` S )
aks6d1c1.4 
|- X = ( var1 ` K )
aks6d1c1.5 
|- W = ( mulGrp ` S )
aks6d1c1.6 
|- V = ( mulGrp ` K )
aks6d1c1.7 
|- .^ = ( .g ` V )
aks6d1c1.8 
|- C = ( algSc ` S )
aks6d1c1.9 
|- D = ( .g ` W )
aks6d1c1.10 
|- P = ( chr ` K )
aks6d1c1.11 
|- O = ( eval1 ` K )
aks6d1c1.12 
|- .+ = ( +g ` S )
aks6d1c1.13 
|- ( ph -> K e. Field )
aks6d1c1.14 
|- ( ph -> P e. Prime )
aks6d1c1.15 
|- ( ph -> R e. NN )
aks6d1c1.16 
|- ( ph -> N e. NN )
aks6d1c1.17 
|- ( ph -> P || N )
aks6d1c1.18 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c1p8.1 
|- ( ph -> E .~ F )
aks6d1c1p8.2 
|- ( ph -> L e. NN0 )
aks6d1c1p8.3 
|- ( ph -> ( E gcd R ) = 1 )
Assertion aks6d1c1p8 
|- ( ph -> ( E ^ L ) .~ F )

Proof

Step Hyp Ref Expression
1 aks6d1c1.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
2 aks6d1c1.2 
 |-  S = ( Poly1 ` K )
3 aks6d1c1.3 
 |-  B = ( Base ` S )
4 aks6d1c1.4 
 |-  X = ( var1 ` K )
5 aks6d1c1.5 
 |-  W = ( mulGrp ` S )
6 aks6d1c1.6 
 |-  V = ( mulGrp ` K )
7 aks6d1c1.7 
 |-  .^ = ( .g ` V )
8 aks6d1c1.8 
 |-  C = ( algSc ` S )
9 aks6d1c1.9 
 |-  D = ( .g ` W )
10 aks6d1c1.10 
 |-  P = ( chr ` K )
11 aks6d1c1.11 
 |-  O = ( eval1 ` K )
12 aks6d1c1.12 
 |-  .+ = ( +g ` S )
13 aks6d1c1.13 
 |-  ( ph -> K e. Field )
14 aks6d1c1.14 
 |-  ( ph -> P e. Prime )
15 aks6d1c1.15 
 |-  ( ph -> R e. NN )
16 aks6d1c1.16 
 |-  ( ph -> N e. NN )
17 aks6d1c1.17 
 |-  ( ph -> P || N )
18 aks6d1c1.18 
 |-  ( ph -> ( N gcd R ) = 1 )
19 aks6d1c1p8.1 
 |-  ( ph -> E .~ F )
20 aks6d1c1p8.2 
 |-  ( ph -> L e. NN0 )
21 aks6d1c1p8.3 
 |-  ( ph -> ( E gcd R ) = 1 )
22 oveq2 
 |-  ( h = 0 -> ( E ^ h ) = ( E ^ 0 ) )
23 22 breq1d 
 |-  ( h = 0 -> ( ( E ^ h ) .~ F <-> ( E ^ 0 ) .~ F ) )
24 oveq2 
 |-  ( h = i -> ( E ^ h ) = ( E ^ i ) )
25 24 breq1d 
 |-  ( h = i -> ( ( E ^ h ) .~ F <-> ( E ^ i ) .~ F ) )
26 oveq2 
 |-  ( h = ( i + 1 ) -> ( E ^ h ) = ( E ^ ( i + 1 ) ) )
27 26 breq1d 
 |-  ( h = ( i + 1 ) -> ( ( E ^ h ) .~ F <-> ( E ^ ( i + 1 ) ) .~ F ) )
28 oveq2 
 |-  ( h = L -> ( E ^ h ) = ( E ^ L ) )
29 28 breq1d 
 |-  ( h = L -> ( ( E ^ h ) .~ F <-> ( E ^ L ) .~ F ) )
30 1 19 aks6d1c1p1rcl 
 |-  ( ph -> ( E e. NN /\ F e. B ) )
31 30 simpld 
 |-  ( ph -> E e. NN )
32 31 nncnd 
 |-  ( ph -> E e. CC )
33 32 exp0d 
 |-  ( ph -> ( E ^ 0 ) = 1 )
34 eqid 
 |-  ( Base ` K ) = ( Base ` K )
35 13 fldcrngd 
 |-  ( ph -> K e. CRing )
36 35 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> K e. CRing )
37 6 crngmgp 
 |-  ( K e. CRing -> V e. CMnd )
38 35 37 syl 
 |-  ( ph -> V e. CMnd )
39 15 nnnn0d 
 |-  ( ph -> R e. NN0 )
40 38 39 7 isprimroot 
 |-  ( ph -> ( y e. ( V PrimRoots R ) <-> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l .^ y ) = ( 0g ` V ) -> R || l ) ) ) )
41 40 biimpd 
 |-  ( ph -> ( y e. ( V PrimRoots R ) -> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l .^ y ) = ( 0g ` V ) -> R || l ) ) ) )
42 41 imp 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l .^ y ) = ( 0g ` V ) -> R || l ) ) )
43 42 simp1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` V ) )
44 6 34 mgpbas 
 |-  ( Base ` K ) = ( Base ` V )
45 43 44 eleqtrrdi 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` K ) )
46 30 simprd 
 |-  ( ph -> F e. B )
47 46 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> F e. B )
48 11 2 34 3 36 45 47 fveval1fvcl 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` y ) e. ( Base ` K ) )
49 48 44 eleqtrdi 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` y ) e. ( Base ` V ) )
50 eqid 
 |-  ( Base ` V ) = ( Base ` V )
51 50 7 mulg1 
 |-  ( ( ( O ` F ) ` y ) e. ( Base ` V ) -> ( 1 .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` y ) )
52 49 51 syl 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( 1 .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` y ) )
53 50 7 mulg1 
 |-  ( y e. ( Base ` V ) -> ( 1 .^ y ) = y )
54 43 53 syl 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( 1 .^ y ) = y )
55 54 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y = ( 1 .^ y ) )
56 55 fveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` y ) = ( ( O ` F ) ` ( 1 .^ y ) ) )
57 52 56 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( 1 .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( 1 .^ y ) ) )
58 57 ralrimiva 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( 1 .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( 1 .^ y ) ) )
59 1nn 
 |-  1 e. NN
60 59 a1i 
 |-  ( ph -> 1 e. NN )
61 1 46 60 aks6d1c1p1 
 |-  ( ph -> ( 1 .~ F <-> A. y e. ( V PrimRoots R ) ( 1 .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( 1 .^ y ) ) ) )
62 58 61 mpbird 
 |-  ( ph -> 1 .~ F )
63 33 62 eqbrtrd 
 |-  ( ph -> ( E ^ 0 ) .~ F )
64 32 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> E e. CC )
65 1nn0 
 |-  1 e. NN0
66 65 a1i 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> 1 e. NN0 )
67 simplr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> i e. NN0 )
68 64 66 67 expaddd 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> ( E ^ ( i + 1 ) ) = ( ( E ^ i ) x. ( E ^ 1 ) ) )
69 64 exp1d 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> ( E ^ 1 ) = E )
70 69 oveq2d 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> ( ( E ^ i ) x. ( E ^ 1 ) ) = ( ( E ^ i ) x. E ) )
71 68 70 eqtrd 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> ( E ^ ( i + 1 ) ) = ( ( E ^ i ) x. E ) )
72 13 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> K e. Field )
73 14 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> P e. Prime )
74 15 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> R e. NN )
75 21 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> ( E gcd R ) = 1 )
76 17 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> P || N )
77 simpr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> ( E ^ i ) .~ F )
78 19 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> E .~ F )
79 1 2 3 4 5 6 7 8 10 11 12 72 73 74 75 76 77 78 aks6d1c1p5 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> ( ( E ^ i ) x. E ) .~ F )
80 71 79 eqbrtrd 
 |-  ( ( ( ph /\ i e. NN0 ) /\ ( E ^ i ) .~ F ) -> ( E ^ ( i + 1 ) ) .~ F )
81 23 25 27 29 63 80 nn0indd 
 |-  ( ( ph /\ L e. NN0 ) -> ( E ^ L ) .~ F )
82 20 81 mpdan 
 |-  ( ph -> ( E ^ L ) .~ F )