:: JORDAN1D semantic presentation

1 = (2 * 0) + 1
;

then Lm1: 1 div 2 = 0
by NAT_1:def 1;

2 = (2 * 1) + 0
;

then Lm2: 2 div 2 = 1
by NAT_1:def 1;

Lm3: for x, A, B, C, D being set holds
( x in ((A \/ B) \/ C) \/ D iff ( x in A or x in B or x in C or x in D ) )

proof end;

Lm4: for A, B, C, D being set holds union {A,B,C,D} = ((A \/ B) \/ C) \/ D

proof end;

theorem Th1: :: JORDAN1D:1

for A, B being set st ( for x being set st x in A holds
ex K being set st
( K c= B & x c= union K ) ) holds
union A c= union B

proof end;

registration

let m be even Integer;
cluster m + 2 -> even ;
coherence

proof end;

end;

registration

let m be odd Integer;
cluster m + 2 -> odd ;
coherence

proof end;

end;

registration

let m be non empty Nat;
cluster 2 |^ m -> even ;
coherence

proof end;

end;

registration

let n be even Nat;
let m be non empty Nat;
cluster n |^ m -> even ;
coherence

proof end;

end;

theorem Th2: :: JORDAN1D:2

for i being Nat
for r being real number st r <> 0 holds
(1 / r) * (r |^ (i + 1)) = r |^ i

proof end;

theorem Th3: :: JORDAN1D:3

for r, s being real number st r / s is not Integer holds
- [\(r / s)/] = [\((- r) / s)/] + 1

proof end;

theorem Th4: :: JORDAN1D:4

for r, s being real number st r / s is Integer holds
- [\(r / s)/] = [\((- r) / s)/]

proof end;

theorem :: JORDAN1D:5

for n, k being Nat st n > 0 & k mod n <> 0 holds
- (k div n) = ((- k) div n) + 1

proof end;

theorem :: JORDAN1D:6

for n, k being Nat st n > 0 & k mod n = 0 holds
- (k div n) = (- k) div n

proof end;

Lm5: now

let m be real number ; :: thesis:
assume 2 <= m ; :: thesis:
then 2 * m >= 2 * 2 by XREAL_1:68;
then (2 * m) - 2 >= 4 - 2 by XREAL_1:11;
hence (2 * m) - 2 >= 0 ; :: thesis:

end;

Lm6: now

let m be real number ; :: thesis:
assume 1 <= m ; :: thesis:
then 2 * m >= 2 * 1 by XREAL_1:68;
then (2 * m) - 1 >= 2 - 1 by XREAL_1:11;
hence (2 * m) - 1 >= 0 ; :: thesis:

end;

Lm7: now

let m be Nat; :: thesis:
assume 2 <= m ; :: thesis:
then (2 * m) - 2 >= 0 by Lm5;
hence (2 * m) - 2 = (2 * m) -' 2 by BINARITH:def 3; :: thesis:

end;

Lm8: now

let m be Nat; :: thesis:
assume 1 <= m ; :: thesis:
then (2 * m) - 1 >= 0 by Lm6;
hence (2 * m) - 1 = (2 * m) -' 1 by BINARITH:def 3; :: thesis:

end;

Lm9: now

let m be Nat; :: thesis:
assume A1: m >= 1 ; :: thesis:
then 2 * m >= 2 * 1 by XREAL_1:66;
then (2 * m) - 1 >= 2 - 1 by XREAL_1:11;
then A2: (2 * m) -' 1 >= 1 by A1, Lm8;
thus ((2 * m) -' 2) + 1 = (((2 * m) -' 1) -' 1) + 1 by JORDAN3:8
.= (2 * m) -' 1 by A2, BINARITH:53 ; :: thesis:

end;

Lm10: for m, i being Nat
for x being real number st 2 <= m holds
(x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)

proof end;

Lm11: for m being Nat st 2 <= m holds
1 <= (2 * m) -' 2

proof end;

Lm12: for m being Nat st 1 <= m holds
1 <= (2 * m) -' 1

proof end;

Lm13: for m, i being Nat st m < (2 |^ i) + 3 holds
(2 * m) -' 2 < (2 |^ (i + 1)) + 3

proof end;

Lm14: now

let m be Nat; :: thesis:
assume 2 <= m ; :: thesis:
hence (((2 * m) -' 2) + 1) - 2 = (((2 * m) - 2) + 1) - 2 by Lm7
.= (2 * m) - 3 ;
:: thesis:

end;

theorem Th7: :: JORDAN1D:7

for m, i, a, b being Nat
for D being non empty Subset of (TOP-REAL 2) st 2 <= m & m < len (Gauge D,i) & 1 <= a & a <= len (Gauge D,i) & 1 <= b & b <= len (Gauge D,(i + 1)) holds
((Gauge D,i) * m,a) `1 = ((Gauge D,(i + 1)) * ((2 * m) -' 2),b) `1

proof end;

theorem Th8: :: JORDAN1D:8

for n, i, a, b being Nat
for D being non empty Subset of (TOP-REAL 2) st 2 <= n & n < len (Gauge D,i) & 1 <= a & a <= len (Gauge D,i) & 1 <= b & b <= len (Gauge D,(i + 1)) holds
((Gauge D,i) * a,n) `2 = ((Gauge D,(i + 1)) * b,((2 * n) -' 2)) `2

proof end;

Lm15: for m, i being Nat
for D being non empty Subset of (TOP-REAL 2) st m + 1 < len (Gauge D,i) holds
(2 * m) -' 1 < len (Gauge D,(i + 1))

proof end;

theorem Th9: :: JORDAN1D:9

for m, i, n being Nat
for D being compact non horizontal non vertical Subset of (TOP-REAL 2) st 2 <= m & m + 1 < len (Gauge D,i) & 2 <= n & n + 1 < len (Gauge D,i) holds
cell (Gauge D,i),m,n = (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1))

proof end;

theorem :: JORDAN1D:10

for m, i, n being Nat
for D being compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Nat st 2 <= m & m + 1 < len (Gauge D,i) & 2 <= n & n + 1 < len (Gauge D,i) holds
cell (Gauge D,i),m,n = union { (cell (Gauge D,(i + k)),a,b) where a, b is Nat : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) }

proof end;

theorem Th11: :: JORDAN1D:11

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & N-max C in right_cell (Cage C,n),i,(Gauge C,n) )

proof end;

theorem :: JORDAN1D:12

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & N-max C in right_cell (Cage C,n),i )

proof end;

theorem Th13: :: JORDAN1D:13

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & E-min C in right_cell (Cage C,n),i,(Gauge C,n) )

proof end;

theorem :: JORDAN1D:14

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & E-min C in right_cell (Cage C,n),i )

proof end;

theorem Th15: :: JORDAN1D:15

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & E-max C in right_cell (Cage C,n),i,(Gauge C,n) )

proof end;

theorem :: JORDAN1D:16

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & E-max C in right_cell (Cage C,n),i )

proof end;

theorem Th17: :: JORDAN1D:17

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & S-min C in right_cell (Cage C,n),i,(Gauge C,n) )

proof end;

theorem :: JORDAN1D:18

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & S-min C in right_cell (Cage C,n),i )

proof end;

theorem Th19: :: JORDAN1D:19

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & S-max C in right_cell (Cage C,n),i,(Gauge C,n) )

proof end;

theorem :: JORDAN1D:20

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & S-max C in right_cell (Cage C,n),i )

proof end;

theorem Th21: :: JORDAN1D:21

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & W-min C in right_cell (Cage C,n),i,(Gauge C,n) )

proof end;

theorem :: JORDAN1D:22

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & W-min C in right_cell (Cage C,n),i )

proof end;

theorem Th23: :: JORDAN1D:23

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & W-max C in right_cell (Cage C,n),i,(Gauge C,n) )

proof end;

theorem :: JORDAN1D:24

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage C,n) & W-max C in right_cell (Cage C,n),i )

proof end;

theorem Th25: :: JORDAN1D:25

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge C,n) & N-min (L~ (Cage C,n)) = (Gauge C,n) * i,(width (Gauge C,n)) )

proof end;

theorem :: JORDAN1D:26

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge C,n) & N-max (L~ (Cage C,n)) = (Gauge C,n) * i,(width (Gauge C,n)) )

proof end;

theorem :: JORDAN1D:27

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge C,n) & (Gauge C,n) * i,(width (Gauge C,n)) in rng (Cage C,n) )

proof end;

theorem Th28: :: JORDAN1D:28

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge C,n) & E-min (L~ (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),j )

proof end;

theorem :: JORDAN1D:29

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge C,n) & E-max (L~ (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),j )

proof end;

theorem :: JORDAN1D:30

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge C,n) & (Gauge C,n) * (len (Gauge C,n)),j in rng (Cage C,n) )

proof end;

theorem Th31: :: JORDAN1D:31

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge C,n) & S-min (L~ (Cage C,n)) = (Gauge C,n) * i,1 )

proof end;

theorem :: JORDAN1D:32

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge C,n) & S-max (L~ (Cage C,n)) = (Gauge C,n) * i,1 )

proof end;

theorem :: JORDAN1D:33

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge C,n) & (Gauge C,n) * i,1 in rng (Cage C,n) )

proof end;

theorem Th34: :: JORDAN1D:34

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge C,n) & W-min (L~ (Cage C,n)) = (Gauge C,n) * 1,j )

proof end;

theorem :: JORDAN1D:35

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge C,n) & W-max (L~ (Cage C,n)) = (Gauge C,n) * 1,j )

proof end;

theorem :: JORDAN1D:36

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge C,n) & (Gauge C,n) * 1,j in rng (Cage C,n) )

proof end;