Metamath Proof Explorer

Theorem mulgnn

Description: Group multiple (exponentiation) operation at a positive integer. (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgnn.b ⊢ B = Base G
mulgnn.p ⊢ + ˙ = + G
mulgnn.t ⊢ · ˙ = ⋅ G
mulgnn.s ⊢ S = seq 1 + ˙ ℕ × X
Assertion mulgnn ⊢ N ∈ ℕ ∧ X ∈ B → N · ˙ X = S ⁡ N

Proof

Step Hyp Ref Expression
1 mulgnn.b ⊢ B = Base G
2 mulgnn.p ⊢ + ˙ = + G
3 mulgnn.t ⊢ · ˙ = ⋅ G
4 mulgnn.s ⊢ S = seq 1 + ˙ ℕ × X
5 nnz ⊢ N ∈ ℕ → N ∈ ℤ
6 eqid ⊢ 0 G = 0 G
7 eqid ⊢ inv g ⁡ G = inv g ⁡ G
8 1 2 6 7 3 4 mulgval ⊢ N ∈ ℤ ∧ X ∈ B → N · ˙ X = if N = 0 0 G if 0 < N S ⁡ N inv g ⁡ G ⁡ S ⁡ − N
9 5 8 sylan ⊢ N ∈ ℕ ∧ X ∈ B → N · ˙ X = if N = 0 0 G if 0 < N S ⁡ N inv g ⁡ G ⁡ S ⁡ − N
10 nnne0 ⊢ N ∈ ℕ → N ≠ 0
11 10 neneqd ⊢ N ∈ ℕ → ¬ N = 0
12 11 iffalsed ⊢ N ∈ ℕ → if N = 0 0 G if 0 < N S ⁡ N inv g ⁡ G ⁡ S ⁡ − N = if 0 < N S ⁡ N inv g ⁡ G ⁡ S ⁡ − N
13 nngt0 ⊢ N ∈ ℕ → 0 < N
14 13 iftrued ⊢ N ∈ ℕ → if 0 < N S ⁡ N inv g ⁡ G ⁡ S ⁡ − N = S ⁡ N
15 12 14 eqtrd ⊢ N ∈ ℕ → if N = 0 0 G if 0 < N S ⁡ N inv g ⁡ G ⁡ S ⁡ − N = S ⁡ N
16 15 adantr ⊢ N ∈ ℕ ∧ X ∈ B → if N = 0 0 G if 0 < N S ⁡ N inv g ⁡ G ⁡ S ⁡ − N = S ⁡ N
17 9 16 eqtrd ⊢ N ∈ ℕ ∧ X ∈ B → N · ˙ X = S ⁡ N