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	$⊢ X = {Base}_{G}$
	odcl.2	$⊢ O = od (G)$
	odid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	odid.4	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	odmodnn0	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to (N \mod O (A)) \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$⊢ X = {Base}_{G}$
2		odcl.2	$⊢ O = od (G)$
3		odid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		odid.4	$⊢ \underset{˙}{0} = 0_{G}$
5		simpl1	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to G \in Mnd$
6		nnnn0	$⊢ O (A) \in ℕ \to O (A) \in ℕ_{0}$
7	6	adantl	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) \in ℕ_{0}$
8		simpl3	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to N \in ℕ_{0}$
9	8	nn0red	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to N \in ℝ$
10		nnrp	$⊢ O (A) \in ℕ \to O (A) \in ℝ^{+}$
11	10	adantl	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) \in ℝ^{+}$
12	9 11	rerpdivcld	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to \frac{N}{O (A)} \in ℝ$
13	8	nn0ge0d	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to 0 \leq N$
14		nnre	$⊢ O (A) \in ℕ \to O (A) \in ℝ$
15	14	adantl	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) \in ℝ$
16		nngt0	$⊢ O (A) \in ℕ \to 0 < O (A)$
17	16	adantl	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to 0 < O (A)$
18		divge0	$⊢ ((N \in ℝ \land 0 \leq N) \land (O (A) \in ℝ \land 0 < O (A))) \to 0 \leq \frac{N}{O (A)}$
19	9 13 15 17 18	syl22anc	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to 0 \leq \frac{N}{O (A)}$
20		flge0nn0	$⊢ (\frac{N}{O (A)} \in ℝ \land 0 \leq \frac{N}{O (A)}) \to ⌊\frac{N}{O (A)}⌋ \in ℕ_{0}$
21	12 19 20	syl2anc	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ \in ℕ_{0}$
22	7 21	nn0mulcld	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ \in ℕ_{0}$
23	8	nn0zd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to N \in ℤ$
24		zmodcl	$⊢ (N \in ℤ \land O (A) \in ℕ) \to N \mod O (A) \in ℕ_{0}$
25	23 24	sylancom	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to N \mod O (A) \in ℕ_{0}$
26		simpl2	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to A \in X$
27		eqid	$⊢ +_{G} = +_{G}$
28	1 3 27	mulgnn0dir	$⊢ (G \in Mnd \land (O (A) ⌊\frac{N}{O (A)}⌋ \in ℕ_{0} \land N \mod O (A) \in ℕ_{0} \land A \in X)) \to (O (A) ⌊\frac{N}{O (A)}⌋ + (N \mod O (A))) \underset{˙}{\cdot} A = (O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A) +_{G} ((N \mod O (A)) \underset{˙}{\cdot} A)$
29	5 22 25 26 28	syl13anc	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to (O (A) ⌊\frac{N}{O (A)}⌋ + (N \mod O (A))) \underset{˙}{\cdot} A = (O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A) +_{G} ((N \mod O (A)) \underset{˙}{\cdot} A)$
30	15	recnd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) \in ℂ$
31	21	nn0cnd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ \in ℂ$
32	30 31	mulcomd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ = ⌊\frac{N}{O (A)}⌋ O (A)$
33	32	oveq1d	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A = ⌊\frac{N}{O (A)}⌋ O (A) \underset{˙}{\cdot} A$
34	1 3	mulgnn0ass	$⊢ (G \in Mnd \land (⌊\frac{N}{O (A)}⌋ \in ℕ_{0} \land O (A) \in ℕ_{0} \land A \in X)) \to ⌊\frac{N}{O (A)}⌋ O (A) \underset{˙}{\cdot} A = ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} (O (A) \underset{˙}{\cdot} A)$
35	5 21 7 26 34	syl13anc	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ O (A) \underset{˙}{\cdot} A = ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} (O (A) \underset{˙}{\cdot} A)$
36	1 2 3 4	odid	$⊢ A \in X \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
37	26 36	syl	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
38	37	oveq2d	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} (O (A) \underset{˙}{\cdot} A) = ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} \underset{˙}{0}$
39	1 3 4	mulgnn0z	$⊢ (G \in Mnd \land ⌊\frac{N}{O (A)}⌋ \in ℕ_{0}) \to ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
40	5 21 39	syl2anc	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
41	38 40	eqtrd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} (O (A) \underset{˙}{\cdot} A) = \underset{˙}{0}$
42	35 41	eqtrd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to ⌊\frac{N}{O (A)}⌋ O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
43	33 42	eqtrd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A = \underset{˙}{0}$
44	43	oveq1d	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to (O (A) ⌊\frac{N}{O (A)}⌋ \underset{˙}{\cdot} A) +_{G} ((N \mod O (A)) \underset{˙}{\cdot} A) = \underset{˙}{0} +_{G} ((N \mod O (A)) \underset{˙}{\cdot} A)$
45	29 44	eqtrd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to (O (A) ⌊\frac{N}{O (A)}⌋ + (N \mod O (A))) \underset{˙}{\cdot} A = \underset{˙}{0} +_{G} ((N \mod O (A)) \underset{˙}{\cdot} A)$
46		modval	$⊢ (N \in ℝ \land O (A) \in ℝ^{+}) \to N \mod O (A) = N - O (A) ⌊\frac{N}{O (A)}⌋$
47	9 11 46	syl2anc	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to N \mod O (A) = N - O (A) ⌊\frac{N}{O (A)}⌋$
48	47	oveq2d	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ + (N \mod O (A)) = O (A) ⌊\frac{N}{O (A)}⌋ + N - O (A) ⌊\frac{N}{O (A)}⌋$
49	22	nn0cnd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ \in ℂ$
50	8	nn0cnd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to N \in ℂ$
51	49 50	pncan3d	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ + N - O (A) ⌊\frac{N}{O (A)}⌋ = N$
52	48 51	eqtrd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to O (A) ⌊\frac{N}{O (A)}⌋ + (N \mod O (A)) = N$
53	52	oveq1d	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to (O (A) ⌊\frac{N}{O (A)}⌋ + (N \mod O (A))) \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$
54	1 3	mulgnn0cl	$⊢ (G \in Mnd \land N \mod O (A) \in ℕ_{0} \land A \in X) \to (N \mod O (A)) \underset{˙}{\cdot} A \in X$
55	5 25 26 54	syl3anc	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to (N \mod O (A)) \underset{˙}{\cdot} A \in X$
56	1 27 4	mndlid	$⊢ (G \in Mnd \land (N \mod O (A)) \underset{˙}{\cdot} A \in X) \to \underset{˙}{0} +_{G} ((N \mod O (A)) \underset{˙}{\cdot} A) = (N \mod O (A)) \underset{˙}{\cdot} A$
57	5 55 56	syl2anc	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to \underset{˙}{0} +_{G} ((N \mod O (A)) \underset{˙}{\cdot} A) = (N \mod O (A)) \underset{˙}{\cdot} A$
58	45 53 57	3eqtr3rd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) \in ℕ) \to (N \mod O (A)) \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$

Metamath Proof Explorer

Theorem odmodnn0

Proof