let n be non zero Nat; :: thesis: for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for k being Nat st k <> 0 & k < n holds
x |^ k <> 1_ (Dihedral_group n)
let g1 be Element of (INT.Group n); :: thesis: ( g1 = 1 implies for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for k being Nat st k <> 0 & k < n holds
x |^ k <> 1_ (Dihedral_group n) )
assume A0: g1 = 1 ; :: thesis: for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for k being Nat st k <> 0 & k < n holds
x |^ k <> 1_ (Dihedral_group n)
let x be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> implies for k being Nat st k <> 0 & k < n holds
x |^ k <> 1_ (Dihedral_group n) )
assume A1: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: for k being Nat st k <> 0 & k < n holds
x |^ k <> 1_ (Dihedral_group n)
let k be Nat; :: thesis: ( k <> 0 & k < n implies x |^ k <> 1_ (Dihedral_group n) )
assume A2: k <> 0 ; :: thesis: ( not k < n or x |^ k <> 1_ (Dihedral_group n) )
assume A3: k < n ; :: thesis: x |^ k <> 1_ (Dihedral_group n)
defpred S₁[ Nat] means ex g being Element of (INT.Group n) st
( g = $1 mod n & g = g1 |^ $1 );
A4: S₁[ 0 ]

proof

take 1_ (INT.Group n) ; :: thesis: ( 1_ (INT.Group n) = 0 mod n & 1_ (INT.Group n) = g1 |^ 0 )
thus 1_ (INT.Group n) = 0 by GR_CY_1:14
.= 0 mod n by NAT_D:26 ; :: thesis: 1_ (INT.Group n) = g1 |^ 0
thus 1_ (INT.Group n) = g1 |^ 0 by GROUP_1:25; :: thesis: verum

end;

A5: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume B1: S₁[j] ; :: thesis: S₁[j + 1]

per cases ( (j + 1) mod n = 0 or (j + 1) mod n <> 0 ) ;

suppose B2: (j + 1) mod n = 0 ; :: thesis: S₁[j + 1]

ex g being Element of (INT.Group n) st
( g = (j + 1) mod n & g = g1 |^ (j + 1) )

proof

take g = 1_ (INT.Group n); :: thesis: ( g = (j + 1) mod n & g = g1 |^ (j + 1) )
thus g = 0 by GR_CY_1:14
.= (j + 1) mod n by B2 ; :: thesis: g = g1 |^ (j + 1)
ex t being Nat st
( j + 1 = (n * t) + 0 & 0 < n ) by B2, NAT_D:def 2;
then consider t being Nat such that
B2a: j + 1 = n * t ;
thus g1 |^ (j + 1) = g1 |^ (n * t) by B2a
.= (g1 |^ t) |^ n by GROUP_1:35
.= (g1 |^ t) |^ (card (INT.Group n))
.= g by GR_CY_1:9 ; :: thesis: verum

end;

hence S₁[j + 1] ; :: thesis: verum

end;

suppose B3: (j + 1) mod n <> 0 ; :: thesis: S₁[j + 1]

ex g being Element of (INT.Group n) st
( g = (j + 1) mod n & g = g1 |^ (j + 1) )

proof

consider g0 being Element of (INT.Group n) such that
B4: ( g0 = j mod n & g0 = g1 |^ j ) by B1;
take g = g0 * g1; :: thesis: ( g = (j + 1) mod n & g = g1 |^ (j + 1) )
n <> 1

proof

assume B5: n = 1 ; :: thesis: contradiction
j + 1 = (1 * (j + 1)) + 0 ;
then (j + 1) mod 1 = 0 by NAT_D:def 2;
hence contradiction by B3, B5; :: thesis: verum

end;

then n > 1 by NAT_1:53;
then B6: ( 1 in Segm n & j mod n in Segm n ) by NAT_1:44, NAT_D:1;
thus g = (addint n) . (g0,g1) by Th75
.= (addint n) . ((j mod n),1) by A0, B4
.= ((j mod n) + 1) mod n by B6, GR_CY_1:def 4
.= (j + 1) mod n by NAT_D:22 ; :: thesis: g = g1 |^ (j + 1)
thus g = (g1 |^ j) * g1 by B4
.= g1 |^ (j + 1) by GROUP_1:34 ; :: thesis: verum

end;

hence S₁[j + 1] ; :: thesis: verum

end;

end;

end;

A6: for j being Nat holds S₁[j] from NAT_1:sch 2(A4, A5);
consider gk being Element of (INT.Group n) such that
A7: ( gk = k mod n & gk = g1 |^ k ) by A6;
k mod n = k by A3, NAT_D:24;
then gk <> 0 by A2, A7;
then gk <> 1_ (INT.Group n) by GR_CY_1:14;
then A8: g1 |^ k <> 1_ (INT.Group n) by A7;
x |^ k = <*(g1 |^ k),(1_ (INT.Group 2))*> by A1, Th25;
then x |^ k <> <*(1_ (INT.Group n)),(1_ (INT.Group 2))*> by A8, FINSEQ_1:77;
hence x |^ k <> 1_ (Dihedral_group n) by Th17; :: thesis: verum