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

Metamath Proof Explorer

Theorem gexcl3

Description: If the order of every group element is bounded by N , the group has finite exponent. (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 gexcl3 
|- ( ( G e. Grp /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> E 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 simpl 
 |-  ( ( G e. Grp /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> G e. Grp )
5 1 grpbn0 
 |-  ( G e. Grp -> X =/= (/) )
6 r19.2z 
 |-  ( ( X =/= (/) /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> E. x e. X ( O ` x ) e. ( 1 ... N ) )
7 5 6 sylan 
 |-  ( ( G e. Grp /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> E. x e. X ( O ` x ) e. ( 1 ... N ) )
8 elfzuz2 
 |-  ( ( O ` x ) e. ( 1 ... N ) -> N e. ( ZZ>= ` 1 ) )
9 nnuz 
 |-  NN = ( ZZ>= ` 1 )
10 8 9 eleqtrrdi 
 |-  ( ( O ` x ) e. ( 1 ... N ) -> N e. NN )
11 10 rexlimivw 
 |-  ( E. x e. X ( O ` x ) e. ( 1 ... N ) -> N e. NN )
12 7 11 syl 
 |-  ( ( G e. Grp /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> N e. NN )
13 12 nnnn0d 
 |-  ( ( G e. Grp /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> N e. NN0 )
14 13 faccld 
 |-  ( ( G e. Grp /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> ( ! ` N ) e. NN )
15 elfzuzb 
 |-  ( ( O ` x ) e. ( 1 ... N ) <-> ( ( O ` x ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( O ` x ) ) ) )
16 elnnuz 
 |-  ( ( O ` x ) e. NN <-> ( O ` x ) e. ( ZZ>= ` 1 ) )
17 dvdsfac 
 |-  ( ( ( O ` x ) e. NN /\ N e. ( ZZ>= ` ( O ` x ) ) ) -> ( O ` x ) || ( ! ` N ) )
18 16 17 sylanbr 
 |-  ( ( ( O ` x ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( O ` x ) ) ) -> ( O ` x ) || ( ! ` N ) )
19 15 18 sylbi 
 |-  ( ( O ` x ) e. ( 1 ... N ) -> ( O ` x ) || ( ! ` N ) )
20 19 adantl 
 |-  ( ( ( G e. Grp /\ x e. X ) /\ ( O ` x ) e. ( 1 ... N ) ) -> ( O ` x ) || ( ! ` N ) )
21 simpll 
 |-  ( ( ( G e. Grp /\ x e. X ) /\ ( O ` x ) e. ( 1 ... N ) ) -> G e. Grp )
22 simplr 
 |-  ( ( ( G e. Grp /\ x e. X ) /\ ( O ` x ) e. ( 1 ... N ) ) -> x e. X )
23 10 adantl 
 |-  ( ( ( G e. Grp /\ x e. X ) /\ ( O ` x ) e. ( 1 ... N ) ) -> N e. NN )
24 23 nnnn0d 
 |-  ( ( ( G e. Grp /\ x e. X ) /\ ( O ` x ) e. ( 1 ... N ) ) -> N e. NN0 )
25 24 faccld 
 |-  ( ( ( G e. Grp /\ x e. X ) /\ ( O ` x ) e. ( 1 ... N ) ) -> ( ! ` N ) e. NN )
26 25 nnzd 
 |-  ( ( ( G e. Grp /\ x e. X ) /\ ( O ` x ) e. ( 1 ... N ) ) -> ( ! ` N ) e. ZZ )
27 eqid 
 |-  ( .g ` G ) = ( .g ` G )
28 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
29 1 3 27 28 oddvds 
 |-  ( ( G e. Grp /\ x e. X /\ ( ! ` N ) e. ZZ ) -> ( ( O ` x ) || ( ! ` N ) <-> ( ( ! ` N ) ( .g ` G ) x ) = ( 0g ` G ) ) )
30 21 22 26 29 syl3anc 
 |-  ( ( ( G e. Grp /\ x e. X ) /\ ( O ` x ) e. ( 1 ... N ) ) -> ( ( O ` x ) || ( ! ` N ) <-> ( ( ! ` N ) ( .g ` G ) x ) = ( 0g ` G ) ) )
31 20 30 mpbid 
 |-  ( ( ( G e. Grp /\ x e. X ) /\ ( O ` x ) e. ( 1 ... N ) ) -> ( ( ! ` N ) ( .g ` G ) x ) = ( 0g ` G ) )
32 31 ex 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( O ` x ) e. ( 1 ... N ) -> ( ( ! ` N ) ( .g ` G ) x ) = ( 0g ` G ) ) )
33 32 ralimdva 
 |-  ( G e. Grp -> ( A. x e. X ( O ` x ) e. ( 1 ... N ) -> A. x e. X ( ( ! ` N ) ( .g ` G ) x ) = ( 0g ` G ) ) )
34 33 imp 
 |-  ( ( G e. Grp /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> A. x e. X ( ( ! ` N ) ( .g ` G ) x ) = ( 0g ` G ) )
35 1 2 27 28 gexlem2 
 |-  ( ( G e. Grp /\ ( ! ` N ) e. NN /\ A. x e. X ( ( ! ` N ) ( .g ` G ) x ) = ( 0g ` G ) ) -> E e. ( 1 ... ( ! ` N ) ) )
36 4 14 34 35 syl3anc 
 |-  ( ( G e. Grp /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> E e. ( 1 ... ( ! ` N ) ) )
37 elfznn 
 |-  ( E e. ( 1 ... ( ! ` N ) ) -> E e. NN )
38 36 37 syl 
 |-  ( ( G e. Grp /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> E e. NN )