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 )