Metamath Proof Explorer

Theorem odnncl

Description: If a nonzero multiple of an element is zero, the element has positive order. (Contributed by Stefan O'Rear, 5-Sep-2015) (Revised by Mario Carneiro, 22-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odid.3 ⊢ · = ( .g ‘ 𝐺 )
4 odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
5 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → 𝐴 ∈ 𝑋 )
6 simprl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → 𝑁 ≠ 0 )
7 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → 𝑁 ∈ ℤ )
8 7 zcnd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → 𝑁 ∈ ℂ )
9 abs00 ⊢ ( 𝑁 ∈ ℂ → ( ( abs ‘ 𝑁 ) = 0 ↔ 𝑁 = 0 ) )
10 9 necon3bbid ⊢ ( 𝑁 ∈ ℂ → ( ¬ ( abs ‘ 𝑁 ) = 0 ↔ 𝑁 ≠ 0 ) )
11 8 10 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( ¬ ( abs ‘ 𝑁 ) = 0 ↔ 𝑁 ≠ 0 ) )
12 6 11 mpbird ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ¬ ( abs ‘ 𝑁 ) = 0 )
13 nn0abscl ⊢ ( 𝑁 ∈ ℤ → ( abs ‘ 𝑁 ) ∈ ℕ0 )
14 7 13 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( abs ‘ 𝑁 ) ∈ ℕ0 )
15 elnn0 ⊢ ( ( abs ‘ 𝑁 ) ∈ ℕ0 ↔ ( ( abs ‘ 𝑁 ) ∈ ℕ ∨ ( abs ‘ 𝑁 ) = 0 ) )
16 14 15 sylib ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( ( abs ‘ 𝑁 ) ∈ ℕ ∨ ( abs ‘ 𝑁 ) = 0 ) )
17 16 ord ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( ¬ ( abs ‘ 𝑁 ) ∈ ℕ → ( abs ‘ 𝑁 ) = 0 ) )
18 12 17 mt3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( abs ‘ 𝑁 ) ∈ ℕ )
19 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( 𝑁 · 𝐴 ) = 0 )
20 oveq1 ⊢ ( ( abs ‘ 𝑁 ) = 𝑁 → ( ( abs ‘ 𝑁 ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )
21 20 eqeq1d ⊢ ( ( abs ‘ 𝑁 ) = 𝑁 → ( ( ( abs ‘ 𝑁 ) · 𝐴 ) = 0 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
22 19 21 syl5ibrcom ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( ( abs ‘ 𝑁 ) = 𝑁 → ( ( abs ‘ 𝑁 ) · 𝐴 ) = 0 ) )
23 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → 𝐺 ∈ Grp )
24 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
25 1 3 24 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( - 𝑁 · 𝐴 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝐴 ) ) )
26 23 7 5 25 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( - 𝑁 · 𝐴 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝐴 ) ) )
27 19 fveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝐴 ) ) = ( ( invg ‘ 𝐺 ) ‘ 0 ) )
28 4 24 grpinvid ⊢ ( 𝐺 ∈ Grp → ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 )
29 23 28 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 )
30 26 27 29 3eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( - 𝑁 · 𝐴 ) = 0 )
31 oveq1 ⊢ ( ( abs ‘ 𝑁 ) = - 𝑁 → ( ( abs ‘ 𝑁 ) · 𝐴 ) = ( - 𝑁 · 𝐴 ) )
32 31 eqeq1d ⊢ ( ( abs ‘ 𝑁 ) = - 𝑁 → ( ( ( abs ‘ 𝑁 ) · 𝐴 ) = 0 ↔ ( - 𝑁 · 𝐴 ) = 0 ) )
33 30 32 syl5ibrcom ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( ( abs ‘ 𝑁 ) = - 𝑁 → ( ( abs ‘ 𝑁 ) · 𝐴 ) = 0 ) )
34 7 zred ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → 𝑁 ∈ ℝ )
35 34 absord ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( ( abs ‘ 𝑁 ) = 𝑁 ∨ ( abs ‘ 𝑁 ) = - 𝑁 ) )
36 22 33 35 mpjaod ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( ( abs ‘ 𝑁 ) · 𝐴 ) = 0 )
37 1 2 3 4 odlem2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( abs ‘ 𝑁 ) ∈ ℕ ∧ ( ( abs ‘ 𝑁 ) · 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... ( abs ‘ 𝑁 ) ) )
38 5 18 36 37 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... ( abs ‘ 𝑁 ) ) )
39 elfznn ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... ( abs ‘ 𝑁 ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
40 38 39 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≠ 0 ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )