Metamath Proof Explorer

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 ) )