Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylow1 Structured version   Unicode version

Theorem sylow1 15229
 Description: Sylow's first theorem. If is a prime power that divides the cardinality of , then has a supgroup with size . (Contributed by Mario Carneiro, 16-Jan-2015.)
Hypotheses
Ref Expression
sylow1.x
sylow1.g
sylow1.f
sylow1.p
sylow1.n
sylow1.d
Assertion
Ref Expression
sylow1 SubGrp
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem sylow1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sylow1.x . . 3
2 sylow1.g . . 3
3 sylow1.f . . 3
4 sylow1.p . . 3
5 sylow1.n . . 3
6 sylow1.d . . 3
7 eqid 2435 . . 3
8 eqid 2435 . . 3
9 oveq2 6081 . . . . . . 7
109cbvmptv 4292 . . . . . 6
11 oveq1 6080 . . . . . . 7
1211mpteq2dv 4288 . . . . . 6
1310, 12syl5eq 2479 . . . . 5
1413rneqd 5089 . . . 4
15 mpteq1 4281 . . . . 5
1615rneqd 5089 . . . 4
1714, 16cbvmpt2v 6144 . . 3
18 preq12 3877 . . . . . 6
1918sseq1d 3367 . . . . 5
20 oveq2 6081 . . . . . . 7
21 id 20 . . . . . . 7
2220, 21eqeqan12d 2450 . . . . . 6
2322rexbidv 2718 . . . . 5
2419, 23anbi12d 692 . . . 4
2524cbvopabv 4269 . . 3
261, 2, 3, 4, 5, 6, 7, 8, 17, 25sylow1lem3 15226 . 2