Metamath Proof Explorer

Theorem ablsimpgfindlem2

Description: Lemma for ablsimpgfind . An element of an abelian finite simple group which squares to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses ablsimpgfindlem1.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
ablsimpgfindlem1.2
ablsimpgfindlem1.3
ablsimpgfindlem1.4 ${⊢}{O}=\mathrm{od}\left({G}\right)$
ablsimpgfindlem1.5 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
ablsimpgfindlem1.6 ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$
Assertion ablsimpgfindlem2

Proof

Step Hyp Ref Expression
1 ablsimpgfindlem1.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 ablsimpgfindlem1.2
3 ablsimpgfindlem1.3
4 ablsimpgfindlem1.4 ${⊢}{O}=\mathrm{od}\left({G}\right)$
5 ablsimpgfindlem1.5 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
6 ablsimpgfindlem1.6 ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$
7 simpr
8 6 simpggrpd ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
9 8 adantr ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {G}\in \mathrm{Grp}$
10 simpr ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}\in {B}$
11 2z ${⊢}2\in ℤ$
12 11 a1i ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to 2\in ℤ$
13 9 10 12 3jca ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \left({G}\in \mathrm{Grp}\wedge {x}\in {B}\wedge 2\in ℤ\right)$
18 2ne0 ${⊢}2\ne 0$
21 0dvds ${⊢}2\in ℤ\to \left(0\parallel 2↔2=0\right)$
22 11 21 ax-mp ${⊢}0\parallel 2↔2=0$
24 nbrne2 ${⊢}\left({O}\left({x}\right)\parallel 2\wedge ¬0\parallel 2\right)\to {O}\left({x}\right)\ne 0$