let n be Nat; :: thesis: ( not Necklace n, ComplRelStr (Necklace n) are_isomorphic or n = 0 or n = 1 or n = 4 )
assume A1: Necklace n, ComplRelStr (Necklace n) are_isomorphic ; :: thesis: ( n = 0 or n = 1 or n = 4 )
set S = Necklace n;
set T = ComplRelStr (Necklace n);
card n = n ;
then A2: card [:n,n:] = n * n by CARD_2:46;
assume A3: ( not n = 0 & not n = 1 & not n = 4 ) ; :: thesis: contradiction
( n <= 4 implies not not n = 0 & ... & not n = 4 ) ;
then ( n = 2 or n = 3 or n > 4 ) by A3;
then A4: card the InternalRel of (Necklace n) = 2 * (n - 1) by Th26;
A5: ((n * n) - (2 * (n - 1))) - n <> 2 * (n - 1)
proof
A6: delta (1,(- 5),4) = ((- 5) ^2) - ((4 * 1) * 4) by QUIN_1:def 1
.= 9 ;
assume not ((n * n) - (2 * (n - 1))) - n <> 2 * (n - 1) ; :: thesis: contradiction
then ((1 * (n ^2)) + ((- 5) * n)) + 4 = 0 ;
then ( n = ((- (- 5)) - (sqrt (delta (1,(- 5),4)))) / (2 * 1) or n = ((- (- 5)) + (sqrt (delta (1,(- 5),4)))) / (2 * 1) ) by A6, QUIN_1:15;
then ( n = (5 - (sqrt (3 ^2))) / 2 or n = (5 + (sqrt (3 ^2))) / 2 ) by A6;
then A7: ( n = (5 - 3) / 2 or n = (5 + 3) / 2 ) by SQUARE_1:22;
per cases ( n = 1 or n = 4 ) by A7;
end;
end;
A8: id the carrier of (Necklace n) misses the InternalRel of (Necklace n)
proof
assume not id the carrier of (Necklace n) misses the InternalRel of (Necklace n) ; :: thesis: contradiction
then consider x being object such that
A9: x in id the carrier of (Necklace n) and
A10: x in the InternalRel of (Necklace n) by XBOOLE_0:3;
consider i being Element of NAT such that
i + 1 < n and
A11: ( x = [i,(i + 1)] or x = [(i + 1),i] ) by A10, Th18;
consider x1, x2 being object such that
A12: x = [x1,x2] by A9, RELAT_1:def 1;
A13: x1 = x2 by A9, A12, RELAT_1:def 10;
per cases ( [x1,x2] = [i,(i + 1)] or [x1,x2] = [(i + 1),i] ) by A12, A11;
suppose [x1,x2] = [i,(i + 1)] ; :: thesis: contradiction
then ( x1 = i & x2 = i + 1 ) by XTUPLE_0:1;
hence contradiction by A13; :: thesis: verum
end;
suppose [x1,x2] = [(i + 1),i] ; :: thesis: contradiction
then ( x1 = i + 1 & x2 = i ) by XTUPLE_0:1;
hence contradiction by A13; :: thesis: verum
end;
end;
end;
the carrier of (Necklace n) = n by Th19;
then A14: card ( the InternalRel of (Necklace n) `) = (n * n) - (2 * (n - 1)) by A4, A2, CARD_2:44;
( the carrier of (Necklace n) = n & n = card n ) by Th19;
then A15: card (id the carrier of (Necklace n)) = n by Th4;
card the InternalRel of (ComplRelStr (Necklace n)) = card (( the InternalRel of (Necklace n) `) \ (id the carrier of (Necklace n))) by Def8
.= ((n * n) - (2 * (n - 1))) - n by A14, A15, A8, CARD_2:44, XBOOLE_1:86 ;
hence contradiction by A1, A4, A5, Th16; :: thesis: verum