:: JORDAN1D semantic presentation

1 = (2 * 0) + 1
;

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

2 = (2 * 1) + 0
;

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

Lemma3: for b1, b2, b3, b4, b5 being set holds
( b1 in ((b2 \/ b3) \/ b4) \/ b5 iff ( b1 in b2 or b1 in b3 or b1 in b4 or b1 in b5 ) )
proof end;

Lemma4: for b1, b2, b3, b4 being set holds union {b1,b2,b3,b4} = ((b1 \/ b2) \/ b3) \/ b4
proof end;

theorem Th1: :: JORDAN1D:1
for b1, b2 being set st ( for b3 being set st b3 in b1 holds
ex b4 being set st
( b4 c= b2 & b3 c= union b4 ) ) holds
union b1 c= union b2
proof end;

registration
let c1 be even Integer;
cluster a1 + 2 -> even ;
coherence
c1 + 2 is even
proof end;
end;

registration
let c1 be odd Integer;
cluster a1 + 2 -> odd ;
coherence
not c1 + 2 is even
proof end;
end;

registration
let c1 be non empty Nat;
cluster 2 |^ a1 -> even ;
coherence
2 |^ c1 is even
proof end;
end;

registration
let c1 be even Nat;
let c2 be non empty Nat;
cluster a1 |^ a2 -> even ;
coherence
c1 |^ c2 is even
proof end;
end;

theorem Th2: :: JORDAN1D:2
for b1 being Nat
for b2 being real number st b2 <> 0 holds
(1 / b2) * (b2 |^ (b1 + 1)) = b2 |^ b1
proof end;

theorem Th3: :: JORDAN1D:3
for b1, b2 being real number st b1 / b2 is not Integer holds
- [\(b1 / b2)/] = [\((- b1) / b2)/] + 1
proof end;

theorem Th4: :: JORDAN1D:4
for b1, b2 being real number st b1 / b2 is Integer holds
- [\(b1 / b2)/] = [\((- b1) / b2)/]
proof end;

theorem Th5: :: JORDAN1D:5
for b1, b2 being Nat st b1 > 0 & b2 mod b1 <> 0 holds
- (b2 div b1) = ((- b2) div b1) + 1
proof end;

theorem Th6: :: JORDAN1D:6
for b1, b2 being Nat st b1 > 0 & b2 mod b1 = 0 holds
- (b2 div b1) = (- b2) div b1
proof end;

E9: now
let c1 be real number ;
assume 2 <= c1 ;
then 2 * c1 >= 2 * 2 by XREAL_1:68;
then (2 * c1) - 2 >= 4 - 2 by XREAL_1:11;
hence (2 * c1) - 2 >= 0 ;
end;

E10: now
let c1 be real number ;
assume 1 <= c1 ;
then 2 * c1 >= 2 * 1 by XREAL_1:68;
then (2 * c1) - 1 >= 2 - 1 by XREAL_1:11;
hence (2 * c1) - 1 >= 0 ;
end;

E11: now
let c1 be Nat;
assume 2 <= c1 ;
then (2 * c1) - 2 >= 0 by Lemma9;
hence (2 * c1) - 2 = (2 * c1) -' 2 by BINARITH:def 3;
end;

E12: now
let c1 be Nat;
assume 1 <= c1 ;
then (2 * c1) - 1 >= 0 by Lemma10;
hence (2 * c1) - 1 = (2 * c1) -' 1 by BINARITH:def 3;
end;

E13: now
let c1 be Nat;
assume E14: c1 >= 1 ;
then 2 * c1 >= 2 * 1 by XREAL_1:66;
then (2 * c1) - 1 >= 2 - 1 by XREAL_1:11;
then E15: (2 * c1) -' 1 >= 1 by E14, Lemma12;
thus ((2 * c1) -' 2) + 1 = (((2 * c1) -' 1) -' 1) + 1 by JORDAN3:8
.= (2 * c1) -' 1 by E15, BINARITH:53 ;
end;

Lemma14: for b1, b2 being Nat
for b3 being real number st 2 <= b1 holds
(b3 / (2 |^ b2)) * (b1 - 2) = (b3 / (2 |^ (b2 + 1))) * (((2 * b1) -' 2) - 2)
proof end;

Lemma15: for b1 being Nat st 2 <= b1 holds
1 <= (2 * b1) -' 2
proof end;

Lemma16: for b1 being Nat st 1 <= b1 holds
1 <= (2 * b1) -' 1
proof end;

Lemma17: for b1, b2 being Nat st b1 < (2 |^ b2) + 3 holds
(2 * b1) -' 2 < (2 |^ (b2 + 1)) + 3
proof end;

E18: now
let c1 be Nat;
assume 2 <= c1 ;
hence (((2 * c1) -' 2) + 1) - 2 = (((2 * c1) - 2) + 1) - 2 by Lemma11
.= (2 * c1) - 3 ;

end;

theorem Th7: :: JORDAN1D:7
for b1, b2, b3, b4 being Nat
for b5 being non empty Subset of (TOP-REAL 2) st 2 <= b1 & b1 < len (Gauge b5,b2) & 1 <= b3 & b3 <= len (Gauge b5,b2) & 1 <= b4 & b4 <= len (Gauge b5,(b2 + 1)) holds
((Gauge b5,b2) * b1,b3) `1 = ((Gauge b5,(b2 + 1)) * ((2 * b1) -' 2),b4) `1
proof end;

theorem Th8: :: JORDAN1D:8
for b1, b2, b3, b4 being Nat
for b5 being non empty Subset of (TOP-REAL 2) st 2 <= b1 & b1 < len (Gauge b5,b2) & 1 <= b3 & b3 <= len (Gauge b5,b2) & 1 <= b4 & b4 <= len (Gauge b5,(b2 + 1)) holds
((Gauge b5,b2) * b3,b1) `2 = ((Gauge b5,(b2 + 1)) * b4,((2 * b1) -' 2)) `2
proof end;

Lemma21: for b1, b2 being Nat
for b3 being non empty Subset of (TOP-REAL 2) st b1 + 1 < len (Gauge b3,b2) holds
(2 * b1) -' 1 < len (Gauge b3,(b2 + 1))
proof end;

theorem Th9: :: JORDAN1D:9
for b1, b2, b3 being Nat
for b4 being compact non horizontal non vertical Subset of (TOP-REAL 2) st 2 <= b1 & b1 + 1 < len (Gauge b4,b2) & 2 <= b3 & b3 + 1 < len (Gauge b4,b2) holds
cell (Gauge b4,b2),b1,b3 = (((cell (Gauge b4,(b2 + 1)),((2 * b1) -' 2),((2 * b3) -' 2)) \/ (cell (Gauge b4,(b2 + 1)),((2 * b1) -' 1),((2 * b3) -' 2))) \/ (cell (Gauge b4,(b2 + 1)),((2 * b1) -' 2),((2 * b3) -' 1))) \/ (cell (Gauge b4,(b2 + 1)),((2 * b1) -' 1),((2 * b3) -' 1))
proof end;

theorem Th10: :: JORDAN1D:10
for b1, b2, b3 being Nat
for b4 being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b5 being Nat st 2 <= b1 & b1 + 1 < len (Gauge b4,b2) & 2 <= b3 & b3 + 1 < len (Gauge b4,b2) holds
cell (Gauge b4,b2),b1,b3 = union { (cell (Gauge b4,(b2 + b5)),b6,b7) where B is Nat, B is Nat : ( (((2 |^ b5) * b1) - (2 |^ (b5 + 1))) + 2 <= b6 & b6 <= (((2 |^ b5) * b1) - (2 |^ b5)) + 1 & (((2 |^ b5) * b3) - (2 |^ (b5 + 1))) + 2 <= b7 & b7 <= (((2 |^ b5) * b3) - (2 |^ b5)) + 1 ) }
proof end;

theorem Th11: :: JORDAN1D:11
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & N-max b2 in right_cell (Cage b2,b1),b3,(Gauge b2,b1) )
proof end;

theorem Th12: :: JORDAN1D:12
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & N-max b2 in right_cell (Cage b2,b1),b3 )
proof end;

theorem Th13: :: JORDAN1D:13
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & E-min b2 in right_cell (Cage b2,b1),b3,(Gauge b2,b1) )
proof end;

theorem Th14: :: JORDAN1D:14
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & E-min b2 in right_cell (Cage b2,b1),b3 )
proof end;

theorem Th15: :: JORDAN1D:15
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & E-max b2 in right_cell (Cage b2,b1),b3,(Gauge b2,b1) )
proof end;

theorem Th16: :: JORDAN1D:16
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & E-max b2 in right_cell (Cage b2,b1),b3 )
proof end;

theorem Th17: :: JORDAN1D:17
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & S-min b2 in right_cell (Cage b2,b1),b3,(Gauge b2,b1) )
proof end;

theorem Th18: :: JORDAN1D:18
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & S-min b2 in right_cell (Cage b2,b1),b3 )
proof end;

theorem Th19: :: JORDAN1D:19
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & S-max b2 in right_cell (Cage b2,b1),b3,(Gauge b2,b1) )
proof end;

theorem Th20: :: JORDAN1D:20
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & S-max b2 in right_cell (Cage b2,b1),b3 )
proof end;

theorem Th21: :: JORDAN1D:21
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & W-min b2 in right_cell (Cage b2,b1),b3,(Gauge b2,b1) )
proof end;

theorem Th22: :: JORDAN1D:22
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & W-min b2 in right_cell (Cage b2,b1),b3 )
proof end;

theorem Th23: :: JORDAN1D:23
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & W-max b2 in right_cell (Cage b2,b1),b3,(Gauge b2,b1) )
proof end;

theorem Th24: :: JORDAN1D:24
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 < len (Cage b2,b1) & W-max b2 in right_cell (Cage b2,b1),b3 )
proof end;

theorem Th25: :: JORDAN1D:25
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= len (Gauge b2,b1) & N-min (L~ (Cage b2,b1)) = (Gauge b2,b1) * b3,(width (Gauge b2,b1)) )
proof end;

theorem Th26: :: JORDAN1D:26
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= len (Gauge b2,b1) & N-max (L~ (Cage b2,b1)) = (Gauge b2,b1) * b3,(width (Gauge b2,b1)) )
proof end;

theorem Th27: :: JORDAN1D:27
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= len (Gauge b2,b1) & (Gauge b2,b1) * b3,(width (Gauge b2,b1)) in rng (Cage b2,b1) )
proof end;

theorem Th28: :: JORDAN1D:28
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= width (Gauge b2,b1) & E-min (L~ (Cage b2,b1)) = (Gauge b2,b1) * (len (Gauge b2,b1)),b3 )
proof end;

theorem Th29: :: JORDAN1D:29
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= width (Gauge b2,b1) & E-max (L~ (Cage b2,b1)) = (Gauge b2,b1) * (len (Gauge b2,b1)),b3 )
proof end;

theorem Th30: :: JORDAN1D:30
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * (len (Gauge b2,b1)),b3 in rng (Cage b2,b1) )
proof end;

theorem Th31: :: JORDAN1D:31
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= len (Gauge b2,b1) & S-min (L~ (Cage b2,b1)) = (Gauge b2,b1) * b3,1 )
proof end;

theorem Th32: :: JORDAN1D:32
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= len (Gauge b2,b1) & S-max (L~ (Cage b2,b1)) = (Gauge b2,b1) * b3,1 )
proof end;

theorem Th33: :: JORDAN1D:33
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= len (Gauge b2,b1) & (Gauge b2,b1) * b3,1 in rng (Cage b2,b1) )
proof end;

theorem Th34: :: JORDAN1D:34
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= width (Gauge b2,b1) & W-min (L~ (Cage b2,b1)) = (Gauge b2,b1) * 1,b3 )
proof end;

theorem Th35: :: JORDAN1D:35
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= width (Gauge b2,b1) & W-max (L~ (Cage b2,b1)) = (Gauge b2,b1) * 1,b3 )
proof end;

theorem Th36: :: JORDAN1D:36
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 <= width (Gauge b2,b1) & (Gauge b2,b1) * 1,b3 in rng (Cage b2,b1) )
proof end;