This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem odcl

Description: The order of a group element is always a nonnegative integer. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses odcl.1 ⊢ X = Base G
odcl.2 ⊢ O = od ⁡ G
Assertion odcl ⊢ A ∈ X → O ⁡ A ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ X = Base G
2 odcl.2 ⊢ O = od ⁡ G
3 eqid ⊢ ⋅ G = ⋅ G
4 eqid ⊢ 0 G = 0 G
5 eqid ⊢ y ∈ ℕ | y ⋅ G A = 0 G = y ∈ ℕ | y ⋅ G A = 0 G
6 1 3 4 2 5 odlem1 ⊢ A ∈ X → O ⁡ A = 0 ∧ y ∈ ℕ | y ⋅ G A = 0 G = ∅ ∨ O ⁡ A ∈ y ∈ ℕ | y ⋅ G A = 0 G
7 simpl ⊢ O ⁡ A = 0 ∧ y ∈ ℕ | y ⋅ G A = 0 G = ∅ → O ⁡ A = 0
8 elrabi ⊢ O ⁡ A ∈ y ∈ ℕ | y ⋅ G A = 0 G → O ⁡ A ∈ ℕ
9 7 8 orim12i ⊢ O ⁡ A = 0 ∧ y ∈ ℕ | y ⋅ G A = 0 G = ∅ ∨ O ⁡ A ∈ y ∈ ℕ | y ⋅ G A = 0 G → O ⁡ A = 0 ∨ O ⁡ A ∈ ℕ
10 6 9 syl ⊢ A ∈ X → O ⁡ A = 0 ∨ O ⁡ A ∈ ℕ
11 10 orcomd ⊢ A ∈ X → O ⁡ A ∈ ℕ ∨ O ⁡ A = 0
12 elnn0 ⊢ O ⁡ A ∈ ℕ 0 ↔ O ⁡ A ∈ ℕ ∨ O ⁡ A = 0
13 11 12 sylibr ⊢ A ∈ X → O ⁡ A ∈ ℕ 0