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

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