let f be non constant standard special_circular_sequence; :: thesis: ex i being Element of NAT st
( i in dom f & (f /. i) `1 <> (f /. 1) `1 )
assume A1: for i being Element of 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:27;
A5: now
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:57
.= f /. 1 by EUCLID:57 ;
hence contradiction by A4, Th31, 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[ Element of 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 Element of NAT st S1[j] holds
S1[j + 1]
proof
let j be Element of 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:8;
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
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:27;
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:27;
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:27;
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
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, Th8;
then A25: f /. j in LSeg f,(j + 1) by A14, A16, TOPREAL1:def 5;
(j + 1) + 1 = j + (1 + 1) ;
then A26: (LSeg f,j) /\ (LSeg f,(j + 1)) = {(f /. (j + 1))} by A14, A13, TOPREAL1:def 8;
f /. j in LSeg f,j by A12, A13, TOPREAL1:27;
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, Th31; :: 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, Th8;
then A27: f /. ((j + 1) + 1) in LSeg f,j by A12, A13, TOPREAL1:def 5;
(j + 1) + 1 = j + (1 + 1) ;
then A28: (LSeg f,j) /\ (LSeg f,(j + 1)) = {(f /. (j + 1))} by A14, A13, TOPREAL1:def 8;
f /. ((j + 1) + 1) in LSeg f,(j + 1) by A14, A16, TOPREAL1:27;
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, Th31; :: 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:57
.= f /. (j + 1) by EUCLID:57 ;
hence contradiction by A17, A21, Th31; :: thesis: verum
end;
end;
end;
A30: ((len f) -' 1) + 1 = len f by A2, XREAL_1:237;
then A31: ( 2 <= (len f) -' 1 & (len f) -' 1 < len f ) by A7, NAT_1:13;
A32: S1[ 0 ] ;
A33: for j being Element of NAT holds S1[j] from NAT_1:sch 1(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[ Element of 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 Element of NAT st S1[j] holds
S1[j + 1]
proof
let j be Element of 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:8;
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
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:27;
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:27;
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:27;
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
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, Th8;
then A52: f /. j in LSeg f,(j + 1) by A41, A43, TOPREAL1:def 5;
(j + 1) + 1 = j + (1 + 1) ;
then A53: (LSeg f,j) /\ (LSeg f,(j + 1)) = {(f /. (j + 1))} by A41, A40, TOPREAL1:def 8;
f /. j in LSeg f,j by A39, A40, TOPREAL1:27;
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, Th31; :: 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, Th8;
then A54: f /. ((j + 1) + 1) in LSeg f,j by A39, A40, TOPREAL1:def 5;
(j + 1) + 1 = j + (1 + 1) ;
then A55: (LSeg f,j) /\ (LSeg f,(j + 1)) = {(f /. (j + 1))} by A41, A40, TOPREAL1:def 8;
f /. ((j + 1) + 1) in LSeg f,(j + 1) by A41, A43, TOPREAL1:27;
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, Th31; :: 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:57
.= f /. (j + 1) by EUCLID:57 ;
hence contradiction by A44, A48, Th31; :: thesis: verum
end;
end;
end;
A57: ((len f) -' 1) + 1 = len f by A2, XREAL_1:237;
then A58: ( 2 <= (len f) -' 1 & (len f) -' 1 < len f ) by A7, NAT_1:13;
A59: S1[ 0 ] ;
A60: for j being Element of NAT holds S1[j] from NAT_1:sch 1(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;