let G be finite commutative Group; :: thesis: for p being Prime
for m being Nat
for a being Element of G st card G = p |^ m & a <> 1_ G holds
ex n being Nat st ord a = p |^ (n + 1)
let p be Prime; :: thesis: for m being Nat
for a being Element of G st card G = p |^ m & a <> 1_ G holds
ex n being Nat st ord a = p |^ (n + 1)
let m be Nat; :: thesis: for a being Element of G st card G = p |^ m & a <> 1_ G holds
ex n being Nat st ord a = p |^ (n + 1)
let a be Element of G; :: thesis: ( card G = p |^ m & a <> 1_ G implies ex n being Nat st ord a = p |^ (n + 1) )
assume A1: ( card G = p |^ m & a <> 1_ G ) ; :: thesis: ex n being Nat st ord a = p |^ (n + 1)
reconsider Gra = gr {a} as strict normal Subgroup of G by GROUP_3:116;
consider n1 being Nat such that
A8: ( card Gra = p |^ n1 & n1 <= m ) by GROUPP_1:2, A1, GROUP_2:148;
ord a = p |^ n1 by A8, GR_CY_1:7;
then n1 <> 0 by A1, GROUP_1:43, NEWTON:4;
then 1 <= n1 by NAT_1:14;
then n1 - 1 in NAT by INT_1:3, XREAL_1:48;
then reconsider n = n1 - 1 as Nat ;
take n ; :: thesis: ord a = p |^ (n + 1)
thus ord a = p |^ (n + 1) by A8, GR_CY_1:7; :: thesis: verum