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 · ˙ = G
odid.4 0 ˙ = 0 G
Assertion odlem2 A X N N · ˙ A = 0 ˙ O A 1 N

Proof

Step Hyp Ref Expression
1 odcl.1 X = Base G
2 odcl.2 O = od G
3 odid.3 · ˙ = G
4 odid.4 0 ˙ = 0 G
5 oveq1 y = N y · ˙ A = N · ˙ A
6 5 eqeq1d y = N y · ˙ A = 0 ˙ N · ˙ A = 0 ˙
7 6 elrab N y | y · ˙ A = 0 ˙ N N · ˙ A = 0 ˙
8 eqid y | y · ˙ A = 0 ˙ = y | y · ˙ A = 0 ˙
9 1 3 4 2 8 odval A X O A = if y | y · ˙ A = 0 ˙ = 0 sup y | y · ˙ A = 0 ˙ <
10 n0i N y | y · ˙ A = 0 ˙ ¬ y | y · ˙ A = 0 ˙ =
11 10 iffalsed N y | y · ˙ A = 0 ˙ if y | y · ˙ A = 0 ˙ = 0 sup y | y · ˙ A = 0 ˙ < = sup y | y · ˙ A = 0 ˙ <
12 9 11 sylan9eq A X N y | y · ˙ A = 0 ˙ O A = sup y | y · ˙ A = 0 ˙ <
13 ssrab2 y | y · ˙ A = 0 ˙
14 nnuz = 1
15 13 14 sseqtri y | y · ˙ A = 0 ˙ 1
16 ne0i N y | y · ˙ A = 0 ˙ y | y · ˙ A = 0 ˙
17 16 adantl A X N y | y · ˙ A = 0 ˙ y | y · ˙ A = 0 ˙
18 infssuzcl y | y · ˙ A = 0 ˙ 1 y | y · ˙ A = 0 ˙ sup y | y · ˙ A = 0 ˙ < y | y · ˙ A = 0 ˙
19 15 17 18 sylancr A X N y | y · ˙ A = 0 ˙ sup y | y · ˙ A = 0 ˙ < y | y · ˙ A = 0 ˙
20 13 19 sselid A X N y | y · ˙ A = 0 ˙ sup y | y · ˙ A = 0 ˙ <
21 infssuzle y | y · ˙ A = 0 ˙ 1 N y | y · ˙ A = 0 ˙ sup y | y · ˙ A = 0 ˙ < N
22 15 21 mpan N y | y · ˙ A = 0 ˙ sup y | y · ˙ A = 0 ˙ < N
23 22 adantl A X N y | y · ˙ A = 0 ˙ sup y | y · ˙ A = 0 ˙ < N
24 elrabi N y | y · ˙ A = 0 ˙ N
25 24 nnzd N y | y · ˙ A = 0 ˙ N
26 fznn N sup y | y · ˙ A = 0 ˙ < 1 N sup y | y · ˙ A = 0 ˙ < sup y | y · ˙ A = 0 ˙ < N
27 25 26 syl N y | y · ˙ A = 0 ˙ sup y | y · ˙ A = 0 ˙ < 1 N sup y | y · ˙ A = 0 ˙ < sup y | y · ˙ A = 0 ˙ < N
28 27 adantl A X N y | y · ˙ A = 0 ˙ sup y | y · ˙ A = 0 ˙ < 1 N sup y | y · ˙ A = 0 ˙ < sup y | y · ˙ A = 0 ˙ < N
29 20 23 28 mpbir2and A X N y | y · ˙ A = 0 ˙ sup y | y · ˙ A = 0 ˙ < 1 N
30 12 29 eqeltrd A X N y | y · ˙ A = 0 ˙ O A 1 N
31 7 30 sylan2br A X N N · ˙ A = 0 ˙ O A 1 N
32 31 3impb A X N N · ˙ A = 0 ˙ O A 1 N