let f be constant standard special_circular_sequence; :: thesis: ex i being Nat st
( i in dom f & (f /. i) `1 <> (f /. 1) `1 )
assume A1: for i being Nat st i in dom f holds
(f /. i) `1 = (f /. 1) `1 ; :: thesis: contradiction
A2: len f > 1 by Lm2;
then A3: len f >= 1 + 1 by NAT_1:13;
then A4: 1 + 1 in dom f by FINSEQ_3:25;
A5: now :: thesis: not (f /. 2) `2 = (f /. 1) `2
assume A6: (f /. 2) `2 = (f /. 1) `2 ; :: thesis: contradiction
(f /. 2) `1 = (f /. 1) `1 by A1, A4;
then f /. 2 = |[((f /. 1) `1),((f /. 1) `2)]| by A6, EUCLID:53
.= f /. 1 by EUCLID:53 ;
hence contradiction by A4, Th29, FINSEQ_5:6; :: thesis: verum
end;
( len f = 2 implies f /. 2 = f /. 1 ) by FINSEQ_6:def 1;
then A7: 2 < len f by A3, A5, XXREAL_0:1;
per cases ( (f /. 2) `2 < (f /. 1) `2 or (f /. 2) `2 > (f /. 1) `2 ) by A5, XXREAL_0:1;
suppose A8: (f /. 2) `2 < (f /. 1) `2 ; :: thesis: contradiction
defpred S1[ Nat] means ( 2 <= $1 & $1 < len f implies ( (f /. $1) `2 <= (f /. 2) `2 & (f /. ($1 + 1)) `2 < (f /. $1) `2 ) );
A9: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume that
A10: ( 2 <= j & j < len f implies ( (f /. j) `2 <= (f /. 2) `2 & (f /. (j + 1)) `2 < (f /. j) `2 ) ) and
A11: 2 <= j + 1 and
A12: j + 1 < len f ; :: thesis: ( (f /. (j + 1)) `2 <= (f /. 2) `2 & (f /. ((j + 1) + 1)) `2 < (f /. (j + 1)) `2 )
1 + 1 <= j + 1 by A11;
then A13: 1 <= j by XREAL_1:6;
thus (f /. (j + 1)) `2 <= (f /. 2) `2 :: thesis: (f /. ((j + 1) + 1)) `2 < (f /. (j + 1)) `2
proof
per cases ( 2 = j + 1 or 2 < j + 1 ) by A11, XXREAL_0:1;
suppose 2 = j + 1 ; :: thesis: (f /. (j + 1)) `2 <= (f /. 2) `2
hence (f /. (j + 1)) `2 <= (f /. 2) `2 ; :: thesis: verum
end;
suppose 2 < j + 1 ; :: thesis: (f /. (j + 1)) `2 <= (f /. 2) `2
hence (f /. (j + 1)) `2 <= (f /. 2) `2 by A10, A12, NAT_1:13, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A14: (j + 1) + 1 <= len f by A12, NAT_1:13;
A15: now :: thesis: (f /. (j + 1)) `2 < (f /. j) `2
per cases ( 1 + 1 = j + 1 or 2 < j + 1 ) by A11, XXREAL_0:1;
suppose 1 + 1 = j + 1 ; :: thesis: (f /. (j + 1)) `2 < (f /. j) `2
hence (f /. (j + 1)) `2 < (f /. j) `2 by A8; :: thesis: verum
end;
suppose 2 < j + 1 ; :: thesis: (f /. (j + 1)) `2 < (f /. j) `2
hence (f /. (j + 1)) `2 < (f /. j) `2 by A10, A12, NAT_1:13; :: thesis: verum
end;
end;
end;
A16: 1 <= j + 1 by NAT_1:11;
then A17: j + 1 in dom f by A12, FINSEQ_3:25;
then A18: (f /. (j + 1)) `1 = (f /. 1) `1 by A1;
j < len f by A12, NAT_1:13;
then A19: j in dom f by A13, FINSEQ_3:25;
then A20: (f /. j) `1 = (f /. 1) `1 by A1;
1 <= (j + 1) + 1 by NAT_1:11;
then A21: (j + 1) + 1 in dom f by A14, FINSEQ_3:25;
then A22: (f /. ((j + 1) + 1)) `1 = (f /. 1) `1 by A1;
assume A23: (f /. ((j + 1) + 1)) `2 >= (f /. (j + 1)) `2 ; :: thesis: contradiction
per cases ( (f /. ((j + 1) + 1)) `2 > (f /. (j + 1)) `2 or (f /. ((j + 1) + 1)) `2 = (f /. (j + 1)) `2 ) by A23, XXREAL_0:1;
suppose A24: (f /. ((j + 1) + 1)) `2 > (f /. (j + 1)) `2 ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( (f /. j) `2 <= (f /. ((j + 1) + 1)) `2 or (f /. j) `2 >= (f /. ((j + 1) + 1)) `2 ) ;
suppose (f /. j) `2 <= (f /. ((j + 1) + 1)) `2 ; :: thesis: contradiction
then f /. j in LSeg ((f /. (j + 1)),(f /. ((j + 1) + 1))) by A15, A20, A18, A22, Th7;
then A25: f /. j in LSeg (f,(j + 1)) by A14, A16, TOPREAL1:def 3;
(j + 1) + 1 = j + (1 + 1) ;
then A26: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A14, A13, TOPREAL1:def 6;
f /. j in LSeg (f,j) by A12, A13, TOPREAL1:21;
then f /. j in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A25, XBOOLE_0:def 4;
then f /. j = f /. (j + 1) by A26, TARSKI:def 1;
hence contradiction by A19, A17, Th29; :: thesis: verum
end;
suppose (f /. j) `2 >= (f /. ((j + 1) + 1)) `2 ; :: thesis: contradiction
then f /. ((j + 1) + 1) in LSeg ((f /. j),(f /. (j + 1))) by A20, A18, A22, A24, Th7;
then A27: f /. ((j + 1) + 1) in LSeg (f,j) by A12, A13, TOPREAL1:def 3;
(j + 1) + 1 = j + (1 + 1) ;
then A28: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A14, A13, TOPREAL1:def 6;
f /. ((j + 1) + 1) in LSeg (f,(j + 1)) by A14, A16, TOPREAL1:21;
then f /. ((j + 1) + 1) in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A27, XBOOLE_0:def 4;
then f /. ((j + 1) + 1) = f /. (j + 1) by A28, TARSKI:def 1;
hence contradiction by A17, A21, Th29; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A29: (f /. ((j + 1) + 1)) `2 = (f /. (j + 1)) `2 ; :: thesis: contradiction
(f /. ((j + 1) + 1)) `1 = (f /. 1) `1 by A1, A21
.= (f /. (j + 1)) `1 by A1, A17 ;
then f /. ((j + 1) + 1) = |[((f /. (j + 1)) `1),((f /. (j + 1)) `2)]| by A29, EUCLID:53
.= f /. (j + 1) by EUCLID:53 ;
hence contradiction by A17, A21, Th29; :: thesis: verum
end;
end;
end;
A30: ((len f) -' 1) + 1 = len f by A2, XREAL_1:235;
then A31: ( 2 <= (len f) -' 1 & (len f) -' 1 < len f ) by A7, NAT_1:13;
A32: S1[ 0 ] ;
A33: for j being Nat holds S1[j] from NAT_1:sch 2(A32, A9);
then A34: (f /. ((len f) -' 1)) `2 <= (f /. 2) `2 by A31;
(f /. (len f)) `2 < (f /. ((len f) -' 1)) `2 by A33, A30, A31;
then (f /. (len f)) `2 < (f /. 2) `2 by A34, XXREAL_0:2;
hence contradiction by A8, FINSEQ_6:def 1; :: thesis: verum
end;
suppose A35: (f /. 2) `2 > (f /. 1) `2 ; :: thesis: contradiction
defpred S1[ Nat] means ( 2 <= $1 & $1 < len f implies ( (f /. $1) `2 >= (f /. 2) `2 & (f /. ($1 + 1)) `2 > (f /. $1) `2 ) );
A36: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume that
A37: ( 2 <= j & j < len f implies ( (f /. j) `2 >= (f /. 2) `2 & (f /. (j + 1)) `2 > (f /. j) `2 ) ) and
A38: 2 <= j + 1 and
A39: j + 1 < len f ; :: thesis: ( (f /. (j + 1)) `2 >= (f /. 2) `2 & (f /. ((j + 1) + 1)) `2 > (f /. (j + 1)) `2 )
1 + 1 <= j + 1 by A38;
then A40: 1 <= j by XREAL_1:6;
thus (f /. (j + 1)) `2 >= (f /. 2) `2 :: thesis: (f /. ((j + 1) + 1)) `2 > (f /. (j + 1)) `2
proof
per cases ( 2 = j + 1 or 2 < j + 1 ) by A38, XXREAL_0:1;
suppose 2 = j + 1 ; :: thesis: (f /. (j + 1)) `2 >= (f /. 2) `2
hence (f /. (j + 1)) `2 >= (f /. 2) `2 ; :: thesis: verum
end;
suppose 2 < j + 1 ; :: thesis: (f /. (j + 1)) `2 >= (f /. 2) `2
hence (f /. (j + 1)) `2 >= (f /. 2) `2 by A37, A39, NAT_1:13, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A41: (j + 1) + 1 <= len f by A39, NAT_1:13;
A42: now :: thesis: (f /. (j + 1)) `2 > (f /. j) `2
per cases ( 1 + 1 = j + 1 or 2 < j + 1 ) by A38, XXREAL_0:1;
suppose 1 + 1 = j + 1 ; :: thesis: (f /. (j + 1)) `2 > (f /. j) `2
hence (f /. (j + 1)) `2 > (f /. j) `2 by A35; :: thesis: verum
end;
suppose 2 < j + 1 ; :: thesis: (f /. (j + 1)) `2 > (f /. j) `2
hence (f /. (j + 1)) `2 > (f /. j) `2 by A37, A39, NAT_1:13; :: thesis: verum
end;
end;
end;
A43: 1 <= j + 1 by NAT_1:11;
then A44: j + 1 in dom f by A39, FINSEQ_3:25;
then A45: (f /. (j + 1)) `1 = (f /. 1) `1 by A1;
j < len f by A39, NAT_1:13;
then A46: j in dom f by A40, FINSEQ_3:25;
then A47: (f /. j) `1 = (f /. 1) `1 by A1;
1 <= (j + 1) + 1 by NAT_1:11;
then A48: (j + 1) + 1 in dom f by A41, FINSEQ_3:25;
then A49: (f /. ((j + 1) + 1)) `1 = (f /. 1) `1 by A1;
assume A50: (f /. ((j + 1) + 1)) `2 <= (f /. (j + 1)) `2 ; :: thesis: contradiction
per cases ( (f /. ((j + 1) + 1)) `2 < (f /. (j + 1)) `2 or (f /. ((j + 1) + 1)) `2 = (f /. (j + 1)) `2 ) by A50, XXREAL_0:1;
suppose A51: (f /. ((j + 1) + 1)) `2 < (f /. (j + 1)) `2 ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( (f /. j) `2 >= (f /. ((j + 1) + 1)) `2 or (f /. j) `2 <= (f /. ((j + 1) + 1)) `2 ) ;
suppose (f /. j) `2 >= (f /. ((j + 1) + 1)) `2 ; :: thesis: contradiction
then f /. j in LSeg ((f /. (j + 1)),(f /. ((j + 1) + 1))) by A42, A47, A45, A49, Th7;
then A52: f /. j in LSeg (f,(j + 1)) by A41, A43, TOPREAL1:def 3;
(j + 1) + 1 = j + (1 + 1) ;
then A53: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A41, A40, TOPREAL1:def 6;
f /. j in LSeg (f,j) by A39, A40, TOPREAL1:21;
then f /. j in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A52, XBOOLE_0:def 4;
then f /. j = f /. (j + 1) by A53, TARSKI:def 1;
hence contradiction by A46, A44, Th29; :: thesis: verum
end;
suppose (f /. j) `2 <= (f /. ((j + 1) + 1)) `2 ; :: thesis: contradiction
then f /. ((j + 1) + 1) in LSeg ((f /. j),(f /. (j + 1))) by A47, A45, A49, A51, Th7;
then A54: f /. ((j + 1) + 1) in LSeg (f,j) by A39, A40, TOPREAL1:def 3;
(j + 1) + 1 = j + (1 + 1) ;
then A55: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A41, A40, TOPREAL1:def 6;
f /. ((j + 1) + 1) in LSeg (f,(j + 1)) by A41, A43, TOPREAL1:21;
then f /. ((j + 1) + 1) in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A54, XBOOLE_0:def 4;
then f /. ((j + 1) + 1) = f /. (j + 1) by A55, TARSKI:def 1;
hence contradiction by A44, A48, Th29; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A56: (f /. ((j + 1) + 1)) `2 = (f /. (j + 1)) `2 ; :: thesis: contradiction
(f /. ((j + 1) + 1)) `1 = (f /. 1) `1 by A1, A48
.= (f /. (j + 1)) `1 by A1, A44 ;
then f /. ((j + 1) + 1) = |[((f /. (j + 1)) `1),((f /. (j + 1)) `2)]| by A56, EUCLID:53
.= f /. (j + 1) by EUCLID:53 ;
hence contradiction by A44, A48, Th29; :: thesis: verum
end;
end;
end;
A57: ((len f) -' 1) + 1 = len f by A2, XREAL_1:235;
then A58: ( 2 <= (len f) -' 1 & (len f) -' 1 < len f ) by A7, NAT_1:13;
A59: S1[ 0 ] ;
A60: for j being Nat holds S1[j] from NAT_1:sch 2(A59, A36);
then A61: (f /. ((len f) -' 1)) `2 >= (f /. 2) `2 by A58;
(f /. (len f)) `2 > (f /. ((len f) -' 1)) `2 by A60, A57, A58;
then (f /. (len f)) `2 > (f /. 2) `2 by A61, XXREAL_0:2;
hence contradiction by A35, FINSEQ_6:def 1; :: thesis: verum
end;
end;