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