Metamath Proof Explorer

Theorem primrootscoprf

Description: Coprime powers of primitive roots are primitive roots, as a function. (Contributed by metakunt, 26-Apr-2025)

Ref Expression
Hypotheses primrootscoprf.1 ⊢ F = m ∈ R PrimRoots K ⟼ E ⋅ R m
primrootscoprf.2 ⊢ φ → R ∈ CMnd
primrootscoprf.3 ⊢ φ → K ∈ ℕ
primrootscoprf.4 ⊢ φ → E ∈ ℕ
primrootscoprf.5 ⊢ φ → E gcd K = 1
Assertion primrootscoprf ⊢ φ → F : R PrimRoots K ⟶ R PrimRoots K

Proof

Step Hyp Ref Expression
1 primrootscoprf.1 ⊢ F = m ∈ R PrimRoots K ⟼ E ⋅ R m
2 primrootscoprf.2 ⊢ φ → R ∈ CMnd
3 primrootscoprf.3 ⊢ φ → K ∈ ℕ
4 primrootscoprf.4 ⊢ φ → E ∈ ℕ
5 primrootscoprf.5 ⊢ φ → E gcd K = 1
6 2 adantr ⊢ φ ∧ m ∈ R PrimRoots K → R ∈ CMnd
7 3 adantr ⊢ φ ∧ m ∈ R PrimRoots K → K ∈ ℕ
8 4 adantr ⊢ φ ∧ m ∈ R PrimRoots K → E ∈ ℕ
9 5 adantr ⊢ φ ∧ m ∈ R PrimRoots K → E gcd K = 1
10 simpr ⊢ φ ∧ m ∈ R PrimRoots K → m ∈ R PrimRoots K
11 eqid ⊢ y ∈ Base R | ∃ x ∈ Base R x + R y = 0 R = y ∈ Base R | ∃ x ∈ Base R x + R y = 0 R
12 6 7 8 9 10 11 primrootscoprmpow ⊢ φ ∧ m ∈ R PrimRoots K → E ⋅ R m ∈ R PrimRoots K
13 12 1 fmptd ⊢ φ → F : R PrimRoots K ⟶ R PrimRoots K