let Gc be finite strict cyclic Group; :: thesis: ( ex k being Element of NAT st card Gc = 2 * k implies ex g1 being Element of Gc st

( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds

g1 = g2 ) ) )

set n = card Gc;

given k being Element of NAT such that A1: card Gc = 2 * k ; :: thesis: ex g1 being Element of Gc st

( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds

g1 = g2 ) )

consider g being Element of Gc such that

A2: Gc = gr {g} by GR_CY_1:def 7;

A3: ord g = card Gc by A2, GR_CY_1:7;

take g |^ k ; :: thesis: ( ord (g |^ k) = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds

g |^ k = g2 ) )

A4: (g |^ k) |^ 2 = g |^ (card Gc) by A1, GROUP_1:35

.= 1_ Gc by GR_CY_1:9 ;

A5: k <> 0 by A1;

A6: for p being Nat st (g |^ k) |^ p = 1_ Gc & p <> 0 holds

2 <= p

hence ord (g |^ k) = 2 by A4, A6, GROUP_1:def 11; :: thesis: for g2 being Element of Gc st ord g2 = 2 holds

g |^ k = g2

let g2 be Element of Gc; :: thesis: ( ord g2 = 2 implies g |^ k = g2 )

consider k1 being Element of NAT such that

A10: g2 = g |^ k1 by A2, Th6;

assume that

A11: ord g2 = 2 and

A12: g |^ k <> g2 ; :: thesis: contradiction

( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds

g1 = g2 ) ) )

set n = card Gc;

given k being Element of NAT such that A1: card Gc = 2 * k ; :: thesis: ex g1 being Element of Gc st

( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds

g1 = g2 ) )

consider g being Element of Gc such that

A2: Gc = gr {g} by GR_CY_1:def 7;

A3: ord g = card Gc by A2, GR_CY_1:7;

take g |^ k ; :: thesis: ( ord (g |^ k) = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds

g |^ k = g2 ) )

A4: (g |^ k) |^ 2 = g |^ (card Gc) by A1, GROUP_1:35

.= 1_ Gc by GR_CY_1:9 ;

A5: k <> 0 by A1;

A6: for p being Nat st (g |^ k) |^ p = 1_ Gc & p <> 0 holds

2 <= p

proof

not g |^ k is being_of_order_0
by GR_CY_1:6;
let p be Nat; :: thesis: ( (g |^ k) |^ p = 1_ Gc & p <> 0 implies 2 <= p )

assume that

A7: (g |^ k) |^ p = 1_ Gc and

A8: ( p <> 0 & 2 > p ) ; :: thesis: contradiction

A9: ( not g is being_of_order_0 & 1_ Gc = g |^ (k * p) ) by A7, GROUP_1:35, GR_CY_1:6;

( card Gc > k * p & k * p <> 0 ) by A1, A5, A8, XCMPLX_1:6, XREAL_1:68;

hence contradiction by A3, A9, GROUP_1:def 11; :: thesis: verum

end;assume that

A7: (g |^ k) |^ p = 1_ Gc and

A8: ( p <> 0 & 2 > p ) ; :: thesis: contradiction

A9: ( not g is being_of_order_0 & 1_ Gc = g |^ (k * p) ) by A7, GROUP_1:35, GR_CY_1:6;

( card Gc > k * p & k * p <> 0 ) by A1, A5, A8, XCMPLX_1:6, XREAL_1:68;

hence contradiction by A3, A9, GROUP_1:def 11; :: thesis: verum

hence ord (g |^ k) = 2 by A4, A6, GROUP_1:def 11; :: thesis: for g2 being Element of Gc st ord g2 = 2 holds

g |^ k = g2

let g2 be Element of Gc; :: thesis: ( ord g2 = 2 implies g |^ k = g2 )

consider k1 being Element of NAT such that

A10: g2 = g |^ k1 by A2, Th6;

assume that

A11: ord g2 = 2 and

A12: g |^ k <> g2 ; :: thesis: contradiction

now :: thesis: contradiction

hence
contradiction
; :: thesis: verumA13:
not g is being_of_order_0
by GR_CY_1:6;

consider t, t1 being Nat such that

A14: k1 = (k * t) + t1 and

A15: t1 < k by A5, NAT_1:17;

A16: 2 * t1 < card Gc by A1, A15, XREAL_1:68;

t1 <> 0

1_ Gc = (g |^ k1) |^ 2 by A11, A10, GROUP_1:41

.= g |^ (((k * t) + t1) * 2) by A14, GROUP_1:35

.= g |^ (((card Gc) * t) + (t1 * 2)) by A1

.= (g |^ ((card Gc) * t)) * (g |^ (t1 * 2)) by GROUP_1:33

.= ((g |^ (ord g)) |^ t) * (g |^ (t1 * 2)) by A3, GROUP_1:35

.= ((1_ Gc) |^ t) * (g |^ (t1 * 2)) by GROUP_1:41

.= (1_ Gc) * (g |^ (t1 * 2)) by GROUP_1:31

.= g |^ (2 * t1) by GROUP_1:def 4 ;

hence contradiction by A3, A18, A16, A13, GROUP_1:def 11; :: thesis: verum

end;consider t, t1 being Nat such that

A14: k1 = (k * t) + t1 and

A15: t1 < k by A5, NAT_1:17;

A16: 2 * t1 < card Gc by A1, A15, XREAL_1:68;

t1 <> 0

proof

then A18:
2 * t1 <> 0
;
assume
t1 = 0
; :: thesis: contradiction

then A17: g |^ k1 = g |^ (k * ((2 * (t div 2)) + (t mod 2))) by A14, NAT_D:2

.= g |^ (((k * 2) * (t div 2)) + (k * (t mod 2)))

.= (g |^ ((k * 2) * (t div 2))) * (g |^ (k * (t mod 2))) by GROUP_1:33

.= ((g |^ (k * 2)) |^ (t div 2)) * (g |^ (k * (t mod 2))) by GROUP_1:35

.= ((1_ Gc) |^ (t div 2)) * (g |^ (k * (t mod 2))) by A4, GROUP_1:35

.= (1_ Gc) * (g |^ (k * (t mod 2))) by GROUP_1:31

.= g |^ (k * (t mod 2)) by GROUP_1:def 4 ;

end;then A17: g |^ k1 = g |^ (k * ((2 * (t div 2)) + (t mod 2))) by A14, NAT_D:2

.= g |^ (((k * 2) * (t div 2)) + (k * (t mod 2)))

.= (g |^ ((k * 2) * (t div 2))) * (g |^ (k * (t mod 2))) by GROUP_1:33

.= ((g |^ (k * 2)) |^ (t div 2)) * (g |^ (k * (t mod 2))) by GROUP_1:35

.= ((1_ Gc) |^ (t div 2)) * (g |^ (k * (t mod 2))) by A4, GROUP_1:35

.= (1_ Gc) * (g |^ (k * (t mod 2))) by GROUP_1:31

.= g |^ (k * (t mod 2)) by GROUP_1:def 4 ;

1_ Gc = (g |^ k1) |^ 2 by A11, A10, GROUP_1:41

.= g |^ (((k * t) + t1) * 2) by A14, GROUP_1:35

.= g |^ (((card Gc) * t) + (t1 * 2)) by A1

.= (g |^ ((card Gc) * t)) * (g |^ (t1 * 2)) by GROUP_1:33

.= ((g |^ (ord g)) |^ t) * (g |^ (t1 * 2)) by A3, GROUP_1:35

.= ((1_ Gc) |^ t) * (g |^ (t1 * 2)) by GROUP_1:41

.= (1_ Gc) * (g |^ (t1 * 2)) by GROUP_1:31

.= g |^ (2 * t1) by GROUP_1:def 4 ;

hence contradiction by A3, A18, A16, A13, GROUP_1:def 11; :: thesis: verum