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

Theorem sylow1 17333
 Description: Sylow's first theorem. If is a prime power that divides the cardinality of , then has a supgroup with size . This is part of Metamath 100 proof #72. (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 2471 . . 3
8 eqid 2471 . . 3
9 oveq2 6316 . . . . . . 7
109cbvmptv 4488 . . . . . 6
11 oveq1 6315 . . . . . . 7
1211mpteq2dv 4483 . . . . . 6
1310, 12syl5eq 2517 . . . . 5
1413rneqd 5068 . . . 4
15 mpteq1 4476 . . . . 5
1615rneqd 5068 . . . 4
1714, 16cbvmpt2v 6390 . . 3
18 preq12 4044 . . . . . 6
1918sseq1d 3445 . . . . 5
20 oveq2 6316 . . . . . . 7
21 id 22 . . . . . . 7
2220, 21eqeqan12d 2487 . . . . . 6
2322rexbidv 2892 . . . . 5
2419, 23anbi12d 725 . . . 4
2524cbvopabv 4465 . . 3
261, 2, 3, 4, 5, 6, 7, 8, 17, 25sylow1lem3 17330 . 2