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 sseldi 
 |-  ( ( 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 ) )