Metamath Proof Explorer

Theorem gexcl

Description: The exponent of a group is a nonnegative integer. (Contributed by Mario Carneiro, 23-Apr-2016)

Ref Expression
Hypotheses gexcl.1 ⊢ X = Base G
gexcl.2 ⊢ E = gEx ⁡ G
Assertion gexcl ⊢ G ∈ V → E ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 gexcl.1 ⊢ X = Base G
2 gexcl.2 ⊢ E = gEx ⁡ G
3 eqid ⊢ ⋅ G = ⋅ G
4 eqid ⊢ 0 G = 0 G
5 eqid ⊢ y ∈ ℕ | ∀ x ∈ X y ⋅ G x = 0 G = y ∈ ℕ | ∀ x ∈ X y ⋅ G x = 0 G
6 1 3 4 2 5 gexlem1 ⊢ G ∈ V → E = 0 ∧ y ∈ ℕ | ∀ x ∈ X y ⋅ G x = 0 G = ∅ ∨ E ∈ y ∈ ℕ | ∀ x ∈ X y ⋅ G x = 0 G
7 simpl ⊢ E = 0 ∧ y ∈ ℕ | ∀ x ∈ X y ⋅ G x = 0 G = ∅ → E = 0
8 elrabi ⊢ E ∈ y ∈ ℕ | ∀ x ∈ X y ⋅ G x = 0 G → E ∈ ℕ
9 7 8 orim12i ⊢ E = 0 ∧ y ∈ ℕ | ∀ x ∈ X y ⋅ G x = 0 G = ∅ ∨ E ∈ y ∈ ℕ | ∀ x ∈ X y ⋅ G x = 0 G → E = 0 ∨ E ∈ ℕ
10 6 9 syl ⊢ G ∈ V → E = 0 ∨ E ∈ ℕ
11 10 orcomd ⊢ G ∈ V → E ∈ ℕ ∨ E = 0
12 elnn0 ⊢ E ∈ ℕ 0 ↔ E ∈ ℕ ∨ E = 0
13 11 12 sylibr ⊢ G ∈ V → E ∈ ℕ 0