Theorem oddvds

Description: The only multiples of A that are equal to the identity are the multiples of the order of A . (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 23-Sep-2015)

	Ref	Expression
Hypotheses	odcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
	odid.3	⊢ · = ( .g ‘ 𝐺 )
	odid.4	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	oddvds	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		odcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
3		odid.3	⊢ · = ( .g ‘ 𝐺 )
4		odid.4	⊢ 0 = ( 0g ‘ 𝐺 )
5		simpr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
6		simpl3	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℤ )
7		dvdsval3	⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = 0 ) )
8	5 6 7	syl2anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = 0 ) )
9		simpl2	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ 𝑋 )
10	1 4 3	mulg0	⊢ ( 𝐴 ∈ 𝑋 → ( 0 · 𝐴 ) = 0 )
11	9 10	syl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 0 · 𝐴 ) = 0 )
12		oveq1	⊢ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = 0 → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 0 · 𝐴 ) )
13	12	eqeq1d	⊢ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = 0 → ( ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 ↔ ( 0 · 𝐴 ) = 0 ) )
14	11 13	syl5ibrcom	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = 0 → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 ) )
15	6	zred	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℝ )
16	5	nnrpd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ )
17		modlt	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) < ( 𝑂 ‘ 𝐴 ) )
18	15 16 17	syl2anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) < ( 𝑂 ‘ 𝐴 ) )
19	6 5	zmodcld	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 )
20	19	nn0red	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℝ )
21	5	nnred	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
22	20 21	ltnled	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) < ( 𝑂 ‘ 𝐴 ) ↔ ¬ ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) )
23	18 22	mpbid	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ¬ ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) )
24	1 2 3 4	odlem2	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ ∧ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) )
25		elfzle2	⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) → ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) )
26	24 25	syl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ ∧ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) )
27	26	3com23	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 ∧ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) )
28	27	3expia	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) )
29	28	con3d	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 ) → ( ¬ ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) → ¬ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ ) )
30	29	impancom	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ¬ ( 𝑂 ‘ 𝐴 ) ≤ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) → ( ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 → ¬ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ ) )
31	9 23 30	syl2anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 → ¬ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ ) )
32		elnn0	⊢ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 ↔ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ ∨ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = 0 ) )
33	19 32	sylib	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ ∨ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = 0 ) )
34	33	ord	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ¬ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = 0 ) )
35	31 34	syld	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = 0 ) )
36	14 35	impbid	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = 0 ↔ ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 ) )
37	1 2 3 4	odmod	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )
38	37	eqeq1d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 0 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
39	8 36 38	3bitrd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
40		simpr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) = 0 )
41	40	breq1d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ 0 ∥ 𝑁 ) )
42		simpl3	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → 𝑁 ∈ ℤ )
43		0dvds	⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )
44	42 43	syl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )
45		simpl2	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → 𝐴 ∈ 𝑋 )
46	45 10	syl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 0 · 𝐴 ) = 0 )
47		oveq1	⊢ ( 𝑁 = 0 → ( 𝑁 · 𝐴 ) = ( 0 · 𝐴 ) )
48	47	eqeq1d	⊢ ( 𝑁 = 0 → ( ( 𝑁 · 𝐴 ) = 0 ↔ ( 0 · 𝐴 ) = 0 ) )
49	46 48	syl5ibrcom	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑁 = 0 → ( 𝑁 · 𝐴 ) = 0 ) )
50	1 2 3 4	odnncl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
51	50	nnne0d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( 𝑂 ‘ 𝐴 ) ≠ 0 )
52	51	expr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ( ( 𝑁 · 𝐴 ) = 0 → ( 𝑂 ‘ 𝐴 ) ≠ 0 ) )
53	52	impancom	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( 𝑁 ≠ 0 → ( 𝑂 ‘ 𝐴 ) ≠ 0 ) )
54	53	necon4d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 → 𝑁 = 0 ) )
55	54	impancom	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ( 𝑁 · 𝐴 ) = 0 → 𝑁 = 0 ) )
56	49 55	impbid	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑁 = 0 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
57	41 44 56	3bitrd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
58	1 2	odcl	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
59	58	3ad2ant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
60		elnn0	⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
61	59 60	sylib	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
62	39 57 61	mpjaodan	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )