:: by Artur Korni{\l}owicz and Robert Milewski

::

:: Received November 6, 2000

:: Copyright (c) 2000-2017 Association of Mizar Users

1 = (2 * 0) + 1

;

then Lm1: 1 div 2 = 0

by NAT_D:def 1;

2 = (2 * 1) + 0

;

then Lm2: 2 div 2 = 1

by NAT_D: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

ex K being set st

( K c= B & x c= union K ) ) holds

union A c= union B

proof end;

registration
end;

Lm5: now :: thesis: for m being Real st 2 <= m holds

(2 * m) - 2 >= 0

(2 * m) - 2 >= 0

let m be Real; :: thesis: ( 2 <= m implies (2 * m) - 2 >= 0 )

assume 2 <= m ; :: thesis: (2 * m) - 2 >= 0

then 2 * m >= 2 * 2 by XREAL_1:66;

then (2 * m) - 2 >= 4 - 2 by XREAL_1:9;

hence (2 * m) - 2 >= 0 ; :: thesis: verum

end;
assume 2 <= m ; :: thesis: (2 * m) - 2 >= 0

then 2 * m >= 2 * 2 by XREAL_1:66;

then (2 * m) - 2 >= 4 - 2 by XREAL_1:9;

hence (2 * m) - 2 >= 0 ; :: thesis: verum

Lm6: now :: thesis: for m being Real st 1 <= m holds

(2 * m) - 1 >= 0

(2 * m) - 1 >= 0

let m be Real; :: thesis: ( 1 <= m implies (2 * m) - 1 >= 0 )

assume 1 <= m ; :: thesis: (2 * m) - 1 >= 0

then 2 * m >= 2 * 1 by XREAL_1:66;

then (2 * m) - 1 >= 2 - 1 by XREAL_1:9;

hence (2 * m) - 1 >= 0 ; :: thesis: verum

end;
assume 1 <= m ; :: thesis: (2 * m) - 1 >= 0

then 2 * m >= 2 * 1 by XREAL_1:66;

then (2 * m) - 1 >= 2 - 1 by XREAL_1:9;

hence (2 * m) - 1 >= 0 ; :: thesis: verum

Lm7: for m being Nat st 2 <= m holds

(2 * m) - 2 = (2 * m) -' 2

by Lm5, XREAL_0:def 2;

Lm8: for m being Nat st 1 <= m holds

(2 * m) - 1 = (2 * m) -' 1

by Lm6, XREAL_0:def 2;

Lm9: now :: thesis: for m being Nat st m >= 1 holds

((2 * m) -' 2) + 1 = (2 * m) -' 1

((2 * m) -' 2) + 1 = (2 * m) -' 1

let m be Nat; :: thesis: ( m >= 1 implies ((2 * m) -' 2) + 1 = (2 * m) -' 1 )

assume A1: m >= 1 ; :: thesis: ((2 * m) -' 2) + 1 = (2 * m) -' 1

then 2 * m >= 2 * 1 by XREAL_1:64;

then (2 * m) - 1 >= 2 - 1 by XREAL_1:9;

then A2: (2 * m) -' 1 >= 1 by A1, Lm8;

thus ((2 * m) -' 2) + 1 = (((2 * m) -' 1) -' 1) + 1 by NAT_D:45

.= (2 * m) -' 1 by A2, XREAL_1:235 ; :: thesis: verum

end;
assume A1: m >= 1 ; :: thesis: ((2 * m) -' 2) + 1 = (2 * m) -' 1

then 2 * m >= 2 * 1 by XREAL_1:64;

then (2 * m) - 1 >= 2 - 1 by XREAL_1:9;

then A2: (2 * m) -' 1 >= 1 by A1, Lm8;

thus ((2 * m) -' 2) + 1 = (((2 * m) -' 1) -' 1) + 1 by NAT_D:45

.= (2 * m) -' 1 by A2, XREAL_1:235 ; :: thesis: verum

Lm10: for i, m being Nat

for x being Real 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 i, m being Nat st m < (2 |^ i) + 3 holds

(2 * m) -' 2 < (2 |^ (i + 1)) + 3

proof end;

Lm14: now :: thesis: for m being Nat st 2 <= m holds

(((2 * m) -' 2) + 1) - 2 = (2 * m) - 3

(((2 * m) -' 2) + 1) - 2 = (2 * m) - 3

let m be Nat; :: thesis: ( 2 <= m implies (((2 * m) -' 2) + 1) - 2 = (2 * m) - 3 )

assume 2 <= m ; :: thesis: (((2 * m) -' 2) + 1) - 2 = (2 * m) - 3

hence (((2 * m) -' 2) + 1) - 2 = (((2 * m) - 2) + 1) - 2 by Lm7

.= (2 * m) - 3 ;

:: thesis: verum

end;
assume 2 <= m ; :: thesis: (((2 * m) -' 2) + 1) - 2 = (2 * m) - 3

hence (((2 * m) -' 2) + 1) - 2 = (((2 * m) - 2) + 1) - 2 by Lm7

.= (2 * m) - 3 ;

:: thesis: verum

theorem Th3: :: JORDAN1D:3

for a, b, i, m 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

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 Th4: :: JORDAN1D:4

for a, b, i, n 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

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 i, m 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 Th5: :: JORDAN1D:5

for i, m, 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)))

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:6

for i, m, 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 ) }

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 Th7: :: JORDAN1D:7

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))) )

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:8

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) )

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 Th9: :: JORDAN1D:9

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))) )

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:10

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) )

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 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)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )

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: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)) & E-max C in right_cell ((Cage (C,n)),i) )

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 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)) & S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )

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: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)) & S-min C in right_cell ((Cage (C,n)),i) )

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 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)) & S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )

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: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)) & S-max C in right_cell ((Cage (C,n)),i) )

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 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)) & W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )

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: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)) & W-min C in right_cell ((Cage (C,n)),i) )

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 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)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )

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: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)) & W-max C in right_cell ((Cage (C,n)),i) )

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 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 (Gauge (C,n)) & N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )

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: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 (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )

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: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 (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) )

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 Th24: :: JORDAN1D:24

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) )

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:25

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) )

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:26

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)) )

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 Th27: :: 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)) & S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )

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:28

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) )

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:29

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)) )

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 Th30: :: 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)) & W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )

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:31

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) )

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:32

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)) )

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;