Metamath Proof Explorer

Theorem odmodnn0

Description: Reduce the argument of a group multiple by modding out the order of the element. (Contributed by Mario Carneiro, 23-Sep-2015)

Ref Expression
Hypotheses odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odid.3 ⊢ · = ( .g ‘ 𝐺 )
odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion odmodnn0 ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odid.3 ⊢ · = ( .g ‘ 𝐺 )
4 odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
5 simpl1 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝐺 ∈ Mnd )
6 nnnn0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
7 6 adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
8 simpl3 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℕ0 )
9 8 nn0red ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℝ )
10 nnrp ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ )
11 10 adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ )
12 9 11 rerpdivcld ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ∈ ℝ )
13 8 nn0ge0d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 0 ≤ 𝑁 )
14 nnre ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
15 14 adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
16 nngt0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → 0 < ( 𝑂 ‘ 𝐴 ) )
17 16 adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 0 < ( 𝑂 ‘ 𝐴 ) )
18 divge0 ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ ( ( 𝑂 ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( 𝑂 ‘ 𝐴 ) ) ) → 0 ≤ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) )
19 9 13 15 17 18 syl22anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 0 ≤ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) )
20 flge0nn0 ⊢ ( ( ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) → ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℕ0 )
21 12 19 20 syl2anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℕ0 )
22 7 21 nn0mulcld ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ∈ ℕ0 )
23 8 nn0zd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℤ )
24 zmodcl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 )
25 23 24 sylancom ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 )
26 simpl2 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ 𝑋 )
27 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
28 1 3 27 mulgnn0dir ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ∈ ℕ0 ∧ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) + ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) · 𝐴 ) = ( ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) ( +g ‘ 𝐺 ) ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) )
29 5 22 25 26 28 syl13anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) + ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) · 𝐴 ) = ( ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) ( +g ‘ 𝐺 ) ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) )
30 15 recnd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℂ )
31 21 nn0cnd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℂ )
32 30 31 mulcomd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) )
33 32 oveq1d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) = ( ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
34 1 3 mulgnn0ass ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℕ0 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ) )
35 5 21 7 26 34 syl13anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ) )
36 1 2 3 4 odid ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
37 26 36 syl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
38 37 oveq2d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · 0 ) )
39 1 3 4 mulgnn0z ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · 0 ) = 0 )
40 5 21 39 syl2anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · 0 ) = 0 )
41 38 40 eqtrd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ) = 0 )
42 35 41 eqtrd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) · ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 )
43 33 42 eqtrd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) = 0 )
44 43 oveq1d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) · 𝐴 ) ( +g ‘ 𝐺 ) ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) = ( 0 ( +g ‘ 𝐺 ) ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) )
45 29 44 eqtrd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) + ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) · 𝐴 ) = ( 0 ( +g ‘ 𝐺 ) ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) )
46 modval ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 − ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ) )
47 9 11 46 syl2anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 − ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ) )
48 47 oveq2d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) + ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) = ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) + ( 𝑁 − ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ) ) )
49 22 nn0cnd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ∈ ℂ )
50 8 nn0cnd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℂ )
51 49 50 pncan3d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) + ( 𝑁 − ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) ) ) = 𝑁 )
52 48 51 eqtrd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) + ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) = 𝑁 )
53 52 oveq1d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( ( 𝑂 ‘ 𝐴 ) · ( ⌊ ‘ ( 𝑁 / ( 𝑂 ‘ 𝐴 ) ) ) ) + ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )
54 1 3 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ∈ 𝑋 )
55 5 25 26 54 syl3anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ∈ 𝑋 )
56 1 27 4 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ∈ 𝑋 ) → ( 0 ( +g ‘ 𝐺 ) ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
57 5 55 56 syl2anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 0 ( +g ‘ 𝐺 ) ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
58 45 53 57 3eqtr3rd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )