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 5 25 26	mulgnn0cld	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ∈ 𝑋 )
55	1 27 4	mndlid	⊢ ( ( 𝐺 ∈ Mnd ∧ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ∈ 𝑋 ) → ( 0 ( +g ‘ 𝐺 ) ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
56	5 54 55	syl2anc	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 0 ( +g ‘ 𝐺 ) ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
57	45 53 56	3eqtr3rd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )