oddvdsnn0

Description: The only multiples of A that are equal to the identity are the multiples of the order of A . (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	oddvdsnn0	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$

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		0nn0	$⊢ 0 \in ℕ_{0}$
6	1 2 3 4	mndodcong	$⊢ ((G \in Mnd \land A \in X) \land (N \in ℕ_{0} \land 0 \in ℕ_{0}) \land O (A) \in ℕ) \to (O (A) ∥ (N - 0) \leftrightarrow N \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A)$
7	6	3expia	$⊢ ((G \in Mnd \land A \in X) \land (N \in ℕ_{0} \land 0 \in ℕ_{0})) \to (O (A) \in ℕ \to (O (A) ∥ (N - 0) \leftrightarrow N \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A))$
8	5 7	mpanr2	$⊢ ((G \in Mnd \land A \in X) \land N \in ℕ_{0}) \to (O (A) \in ℕ \to (O (A) ∥ (N - 0) \leftrightarrow N \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A))$
9	8	3impa	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to (O (A) \in ℕ \to (O (A) ∥ (N - 0) \leftrightarrow N \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A))$
10		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
11	10	3ad2ant3	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to N \in ℂ$
12	11	subid1d	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to N - 0 = N$
13	12	breq2d	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to (O (A) ∥ (N - 0) \leftrightarrow O (A) ∥ N)$
14	1 4 3	mulg0	$⊢ A \in X \to 0 \underset{˙}{\cdot} A = \underset{˙}{0}$
15	14	3ad2ant2	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to 0 \underset{˙}{\cdot} A = \underset{˙}{0}$
16	15	eqeq2d	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to (N \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
17	13 16	bibi12d	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to ((O (A) ∥ (N - 0) \leftrightarrow N \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A) \leftrightarrow (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0}))$
18	9 17	sylibd	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to (O (A) \in ℕ \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0}))$
19		simpr	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) = 0) \to O (A) = 0$
20	19	breq1d	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) = 0) \to (O (A) ∥ N \leftrightarrow 0 ∥ N)$
21		simpl3	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) = 0) \to N \in ℕ_{0}$
22		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
23		0dvds	$⊢ N \in ℤ \to (0 ∥ N \leftrightarrow N = 0)$
24	21 22 23	3syl	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) = 0) \to (0 ∥ N \leftrightarrow N = 0)$
25	15	adantr	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) = 0) \to 0 \underset{˙}{\cdot} A = \underset{˙}{0}$
26		oveq1	$⊢ N = 0 \to N \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A$
27	26	eqeq1d	$⊢ N = 0 \to (N \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow 0 \underset{˙}{\cdot} A = \underset{˙}{0})$
28	25 27	syl5ibrcom	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) = 0) \to (N = 0 \to N \underset{˙}{\cdot} A = \underset{˙}{0})$
29	1 2 3 4	odlem2	$⊢ (A \in X \land N \in ℕ \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to O (A) \in (1 \dots N)$
30	29	3com23	$⊢ (A \in X \land N \underset{˙}{\cdot} A = \underset{˙}{0} \land N \in ℕ) \to O (A) \in (1 \dots N)$
31		elfznn	$⊢ O (A) \in (1 \dots N) \to O (A) \in ℕ$
32		nnne0	$⊢ O (A) \in ℕ \to O (A) \neq 0$
33	30 31 32	3syl	$⊢ (A \in X \land N \underset{˙}{\cdot} A = \underset{˙}{0} \land N \in ℕ) \to O (A) \neq 0$
34	33	3expia	$⊢ (A \in X \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to (N \in ℕ \to O (A) \neq 0)$
35	34	3ad2antl2	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to (N \in ℕ \to O (A) \neq 0)$
36	35	necon2bd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to (O (A) = 0 \to \neg N \in ℕ)$
37		simpl3	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to N \in ℕ_{0}$
38		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
39	37 38	sylib	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to (N \in ℕ \lor N = 0)$
40	39	ord	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to (\neg N \in ℕ \to N = 0)$
41	36 40	syld	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to (O (A) = 0 \to N = 0)$
42	41	impancom	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) = 0) \to (N \underset{˙}{\cdot} A = \underset{˙}{0} \to N = 0)$
43	28 42	impbid	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) = 0) \to (N = 0 \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
44	20 24 43	3bitrd	$⊢ ((G \in Mnd \land A \in X \land N \in ℕ_{0}) \land O (A) = 0) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
45	44	ex	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to (O (A) = 0 \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0}))$
46	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
47	46	3ad2ant2	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to O (A) \in ℕ_{0}$
48		elnn0	$⊢ O (A) \in ℕ_{0} \leftrightarrow (O (A) \in ℕ \lor O (A) = 0)$
49	47 48	sylib	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to (O (A) \in ℕ \lor O (A) = 0)$
50	18 45 49	mpjaod	$⊢ (G \in Mnd \land A \in X \land N \in ℕ_{0}) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$

Metamath Proof Explorer

Theorem oddvdsnn0

Proof