Cfrgtkky

I was studying "A Formal Proof of Sylow’s Theorem" by FLORIAN KAMMÜLLER and LAWRENCE C. PAULSON.

But I did not find a way to get $p^{alpha} mid o left( H right)$ from $p^{alpha + Bbbk } mid n o left( H right)$.

enter image description here

I have tried writing it on paper and I have tried various methods such as elimination, substitution and others.

Please help me to find a solution.

note:
I'm sorry because I'm a newcomer to this site, so I still don't understand how to use it. I'm also not good at speaking English. if I'm wrong, please forgive me.

I wrote down part of "A Formal Proof of Sylow’s Theorem" that I have worked on.

Hope it can help to find out what the problem is I can't find a solution.

========================================================================================================================================

Since $H$ is a subgroup of a group $G$ then by Langrange's theorem $eta o left( H right) = o left( G right)$ for some $eta$ is number of distinct right cosets of $H$ in $G$.

Since $eta$ is number of distinct right cosets of $H$ in $G$ then $card left( dfrac{G}{H} right) = eta$.

Since $eta o left( H right) = o left( G right)$ and $card left( dfrac{G}{H} right) = eta$ then $card left( dfrac{G}{H} right) o left( H right) = o left( G right)$.

Since $card left( dfrac{G}{H} right) o left( H right) = o left( G right)$ and $card left( dfrac{G}{H} right) = card left( left[ M_{1} right] right) $ then $card left( left[ M_{1} right] right) o left( H right) = o left( G right)$.

Since $card left( left[ M_{1} right] right) o left( H right) = o left( G right)$ and $o left( G right) = p^{alpha} m$ then $card left( left[ M_{1} right] right) o left( H right) = p^{alpha} m$ or $card left( left[ M_{1} right] right) card left( H right) = p^{alpha} m$.

Since $p^{r + 1} nmid card left( left[ M_{1} right] right) $ for the maximum natural number $r$ and $card left( left[ M_{1} right] right) = n$ then $p^{r + 1} nmid n$ or $p^{r} mid n$.

Let $Bbbk$ for the maximum natural number with $Bbbk leq r$ then $p^{Bbbk} mid n$.

Since $Bbbk$ for the maximum natural number, $r$ for the maximum natural number, and $Bbbk leq r$ then $r - Bbbk$ some integer with $r - Bbbk geq 0$.

Write $r - Bbbk = rho$ for some integer $rho$ with $rho geq 0$.

Since $r - Bbbk = rho$ then $r = Bbbk + rho$.

Now
begin{eqnarray*}
p^{r} &=& p^{Bbbk + rho}
\
&=& p^{Bbbk} p^{rho}
end{eqnarray*}
Since $p$ some integer with $p > 1$ and $rho geq 0$ then $p^{rho}$ some integer with $p^{rho} geq 1$ or $p^{rho} > 0$.

Write $p^{rho} = lambda$ for some integer $lambda$ with $lambda > 0$ then $p^{r} = p^{Bbbk} lambda$ hence $p^{Bbbk} mid p^{r}$.

Since $m = p^{r} w$ for some integer $w$ then $p^{alpha} m = p^{alpha} p^{r} w$ or $p^{alpha} m = p^{alpha + r} w$.

Since $p^{alpha + r}$ some integer, $p^{alpha} m$ some integer with $p^{alpha} m > 0$ and $p^{alpha} m = p^{alpha + r} w$ for some integer $w$ then $p^{alpha + r} mid p^{alpha} m$.

Since $p^{alpha + r} mid p^{alpha} m$, $card left( left[ M_{1} right] right) o left( H right) = p^{alpha} m$, and $card left( left[ M_{1} right[ right) = n$ then $p^{alpha + r} mid n o left( H right) $.

Since $p^{alpha + r} mid n o left( H right) $ then $n o left( H right) = p^{alpha + r} w$ for some integer $w$.

Now
begin{eqnarray*}
n o left( H right) &=& p^{alpha + r} w
\
&=& p^{alpha + Bbbk + rho} w
\
&=& p^{alpha + Bbbk } p^{rho} w
end{eqnarray*}
Since $p^{rho}$ some integer with $p^{rho} > 0$ and $w$ some integer then $p^{rho} w$ some integer.

Write $p^{rho} w = tau$ for some integer $tau$ then $n o left( H right) = p^{alpha + Bbbk } tau$ hence $p^{alpha + Bbbk } mid n o left( H right)$.

Since $p^{Bbbk} mid n$ then $p^{Bbbk}$ some integer non zero, $n$ some integer and $n = p^{Bbbk} upsilon$ for some integer $upsilon$.