Metamath Proof Explorer

Theorem odlem2

Description: Any positive annihilator of a group element is an upper bound on the (positive) order of the element. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Stefan O'Rear, 5-Sep-2015) (Proof shortened by AV, 5-Oct-2020)

Ref Expression
Hypotheses odcl.1 
|- X = ( Base ` G )
odcl.2 
|- O = ( od ` G )
odid.3 
|- .x. = ( .g ` G )
odid.4 
|- .0. = ( 0g ` G )
Assertion odlem2 
|- ( ( A e. X /\ N e. NN /\ ( N .x. A ) = .0. ) -> ( O ` A ) e. ( 1 ... N ) )

Proof

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