Metamath Proof Explorer


Theorem gexlem2

Description: Any positive annihilator of all the group elements is an upper bound on the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016) (Proof shortened by AV, 26-Sep-2020)

Ref Expression
Hypotheses gexcl.1
|- X = ( Base ` G )
gexcl.2
|- E = ( gEx ` G )
gexid.3
|- .x. = ( .g ` G )
gexid.4
|- .0. = ( 0g ` G )
Assertion gexlem2
|- ( ( G e. V /\ N e. NN /\ A. x e. X ( N .x. x ) = .0. ) -> E e. ( 1 ... N ) )

Proof

Step Hyp Ref Expression
1 gexcl.1
 |-  X = ( Base ` G )
2 gexcl.2
 |-  E = ( gEx ` G )
3 gexid.3
 |-  .x. = ( .g ` G )
4 gexid.4
 |-  .0. = ( 0g ` G )
5 oveq1
 |-  ( y = N -> ( y .x. x ) = ( N .x. x ) )
6 5 eqeq1d
 |-  ( y = N -> ( ( y .x. x ) = .0. <-> ( N .x. x ) = .0. ) )
7 6 ralbidv
 |-  ( y = N -> ( A. x e. X ( y .x. x ) = .0. <-> A. x e. X ( N .x. x ) = .0. ) )
8 7 elrab
 |-  ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } <-> ( N e. NN /\ A. x e. X ( N .x. x ) = .0. ) )
9 eqid
 |-  { y e. NN | A. x e. X ( y .x. x ) = .0. } = { y e. NN | A. x e. X ( y .x. x ) = .0. }
10 1 3 4 2 9 gexval
 |-  ( G e. V -> E = if ( { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) , 0 , inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) ) )
11 ne0i
 |-  ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> { y e. NN | A. x e. X ( y .x. x ) = .0. } =/= (/) )
12 ifnefalse
 |-  ( { y e. NN | A. x e. X ( y .x. x ) = .0. } =/= (/) -> if ( { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) , 0 , inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) ) = inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) )
13 11 12 syl
 |-  ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> if ( { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) , 0 , inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) ) = inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) )
14 10 13 sylan9eq
 |-  ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> E = inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) )
15 ssrab2
 |-  { y e. NN | A. x e. X ( y .x. x ) = .0. } C_ NN
16 nnuz
 |-  NN = ( ZZ>= ` 1 )
17 15 16 sseqtri
 |-  { y e. NN | A. x e. X ( y .x. x ) = .0. } C_ ( ZZ>= ` 1 )
18 11 adantl
 |-  ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> { y e. NN | A. x e. X ( y .x. x ) = .0. } =/= (/) )
19 infssuzcl
 |-  ( ( { y e. NN | A. x e. X ( y .x. x ) = .0. } C_ ( ZZ>= ` 1 ) /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } =/= (/) ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. { y e. NN | A. x e. X ( y .x. x ) = .0. } )
20 17 18 19 sylancr
 |-  ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. { y e. NN | A. x e. X ( y .x. x ) = .0. } )
21 15 20 sselid
 |-  ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. NN )
22 infssuzle
 |-  ( ( { y e. NN | A. x e. X ( y .x. x ) = .0. } C_ ( ZZ>= ` 1 ) /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N )
23 17 22 mpan
 |-  ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N )
24 23 adantl
 |-  ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N )
25 elrabi
 |-  ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> N e. NN )
26 25 nnzd
 |-  ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> N e. ZZ )
27 fznn
 |-  ( N e. ZZ -> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. ( 1 ... N ) <-> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. NN /\ inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N ) ) )
28 26 27 syl
 |-  ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. ( 1 ... N ) <-> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. NN /\ inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N ) ) )
29 28 adantl
 |-  ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. ( 1 ... N ) <-> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. NN /\ inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N ) ) )
30 21 24 29 mpbir2and
 |-  ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. ( 1 ... N ) )
31 14 30 eqeltrd
 |-  ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> E e. ( 1 ... N ) )
32 8 31 sylan2br
 |-  ( ( G e. V /\ ( N e. NN /\ A. x e. X ( N .x. x ) = .0. ) ) -> E e. ( 1 ... N ) )
33 32 3impb
 |-  ( ( G e. V /\ N e. NN /\ A. x e. X ( N .x. x ) = .0. ) -> E e. ( 1 ... N ) )