let f be V8() standard special_circular_sequence; ex i being Nat st
( i in dom f & (f /. i) `2 <> (f /. 1) `2 )
assume A1:
for i being Nat st i in dom f holds
(f /. i) `2 = (f /. 1) `2
; 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;
( 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) `1 < (f /. 1) `1 or (f /. 2) `1 > (f /. 1) `1 )
by A5, XXREAL_0:1;
suppose A8:
(f /. 2) `1 < (f /. 1) `1
;
contradictiondefpred S1[
Nat]
means ( 2
<= $1 & $1
< len f implies (
(f /. $1) `1 <= (f /. 2) `1 &
(f /. ($1 + 1)) `1 < (f /. $1) `1 ) );
A9:
for
j being
Nat st
S1[
j] holds
S1[
j + 1]
proof
let j be
Nat;
( S1[j] implies S1[j + 1] )
assume that A10:
( 2
<= j &
j < len f implies (
(f /. j) `1 <= (f /. 2) `1 &
(f /. (j + 1)) `1 < (f /. j) `1 ) )
and A11:
2
<= j + 1
and A12:
j + 1
< len f
;
( (f /. (j + 1)) `1 <= (f /. 2) `1 & (f /. ((j + 1) + 1)) `1 < (f /. (j + 1)) `1 )
1
+ 1
<= j + 1
by A11;
then A13:
1
<= j
by XREAL_1:6;
thus
(f /. (j + 1)) `1 <= (f /. 2) `1
(f /. ((j + 1) + 1)) `1 < (f /. (j + 1)) `1
A14:
(j + 1) + 1
<= len f
by A12, NAT_1:13;
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)) `2 = (f /. 1) `2
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) `2 = (f /. 1) `2
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)) `2 = (f /. 1) `2
by A1;
assume A23:
(f /. ((j + 1) + 1)) `1 >= (f /. (j + 1)) `1
;
contradiction
per cases
( (f /. ((j + 1) + 1)) `1 > (f /. (j + 1)) `1 or (f /. ((j + 1) + 1)) `1 = (f /. (j + 1)) `1 )
by A23, XXREAL_0:1;
suppose A24:
(f /. ((j + 1) + 1)) `1 > (f /. (j + 1)) `1
;
contradictionnow contradictionper 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
;
contradictionthen
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 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;
verum end; suppose
(f /. j) `1 >= (f /. ((j + 1) + 1)) `1
;
contradictionthen
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 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;
verum end; end; end; hence
contradiction
;
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)) `1 <= (f /. 2) `1
by A31;
(f /. (len f)) `1 < (f /. ((len f) -' 1)) `1
by A33, A30, A31;
then
(f /. (len f)) `1 < (f /. 2) `1
by A34, XXREAL_0:2;
hence
contradiction
by A8, FINSEQ_6:def 1;
verum end; suppose A35:
(f /. 2) `1 > (f /. 1) `1
;
contradictiondefpred S1[
Nat]
means ( 2
<= $1 & $1
< len f implies (
(f /. $1) `1 >= (f /. 2) `1 &
(f /. ($1 + 1)) `1 > (f /. $1) `1 ) );
A36:
for
j being
Nat st
S1[
j] holds
S1[
j + 1]
proof
let j be
Nat;
( S1[j] implies S1[j + 1] )
assume that A37:
( 2
<= j &
j < len f implies (
(f /. j) `1 >= (f /. 2) `1 &
(f /. (j + 1)) `1 > (f /. j) `1 ) )
and A38:
2
<= j + 1
and A39:
j + 1
< len f
;
( (f /. (j + 1)) `1 >= (f /. 2) `1 & (f /. ((j + 1) + 1)) `1 > (f /. (j + 1)) `1 )
1
+ 1
<= j + 1
by A38;
then A40:
1
<= j
by XREAL_1:6;
thus
(f /. (j + 1)) `1 >= (f /. 2) `1
(f /. ((j + 1) + 1)) `1 > (f /. (j + 1)) `1
A41:
(j + 1) + 1
<= len f
by A39, NAT_1:13;
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)) `2 = (f /. 1) `2
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) `2 = (f /. 1) `2
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)) `2 = (f /. 1) `2
by A1;
assume A50:
(f /. ((j + 1) + 1)) `1 <= (f /. (j + 1)) `1
;
contradiction
per cases
( (f /. ((j + 1) + 1)) `1 < (f /. (j + 1)) `1 or (f /. ((j + 1) + 1)) `1 = (f /. (j + 1)) `1 )
by A50, XXREAL_0:1;
suppose A51:
(f /. ((j + 1) + 1)) `1 < (f /. (j + 1)) `1
;
contradictionnow contradictionper 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
;
contradictionthen
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 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;
verum end; suppose
(f /. j) `1 <= (f /. ((j + 1) + 1)) `1
;
contradictionthen
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 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;
verum end; end; end; hence
contradiction
;
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)) `1 >= (f /. 2) `1
by A58;
(f /. (len f)) `1 > (f /. ((len f) -' 1)) `1
by A60, A57, A58;
then
(f /. (len f)) `1 > (f /. 2) `1
by A61, XXREAL_0:2;
hence
contradiction
by A35, FINSEQ_6:def 1;
verum end; end;