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

Metamath Proof Explorer

Theorem gexnnod

Description: Every group element has finite order if the exponent is finite. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexod.1 
|- X = ( Base ` G )
gexod.2 
|- E = ( gEx ` G )
gexod.3 
|- O = ( od ` G )
Assertion gexnnod 
|- ( ( G e. Grp /\ E e. NN /\ A e. X ) -> ( O ` A ) e. NN )

Proof

Step Hyp Ref Expression
1 gexod.1 
 |-  X = ( Base ` G )
2 gexod.2 
 |-  E = ( gEx ` G )
3 gexod.3 
 |-  O = ( od ` G )
4 nnne0 
 |-  ( E e. NN -> E =/= 0 )
5 4 3ad2ant2 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> E =/= 0 )
6 nnz 
 |-  ( E e. NN -> E e. ZZ )
7 6 3ad2ant2 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> E e. ZZ )
8 0dvds 
 |-  ( E e. ZZ -> ( 0 || E <-> E = 0 ) )
9 7 8 syl 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> ( 0 || E <-> E = 0 ) )
10 9 necon3bbid 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> ( -. 0 || E <-> E =/= 0 ) )
11 5 10 mpbird 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> -. 0 || E )
12 1 2 3 gexod 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` A ) || E )
13 12 3adant2 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> ( O ` A ) || E )
14 breq1 
 |-  ( ( O ` A ) = 0 -> ( ( O ` A ) || E <-> 0 || E ) )
15 13 14 syl5ibcom 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> ( ( O ` A ) = 0 -> 0 || E ) )
16 11 15 mtod 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> -. ( O ` A ) = 0 )
17 1 3 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
18 17 3ad2ant3 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> ( O ` A ) e. NN0 )
19 elnn0 
 |-  ( ( O ` A ) e. NN0 <-> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
20 18 19 sylib 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
21 20 ord 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> ( -. ( O ` A ) e. NN -> ( O ` A ) = 0 ) )
22 16 21 mt3d 
 |-  ( ( G e. Grp /\ E e. NN /\ A e. X ) -> ( O ` A ) e. NN )