:: URYSOHN2 semantic presentation

theorem Th1: :: URYSOHN2:1

for b₁ being Interval st b₁ <> {} holds
( ( ^^ b₁ <' b₁ ^^ implies vol b₁ = (b₁ ^^ ) - (^^ b₁) ) & ( b₁ ^^ = ^^ b₁ implies vol b₁ = 0. ) )

proof end;

theorem Th2: :: URYSOHN2:2

for b₁ being Subset of REAL
for b₂ being Real st b₂ <> 0 holds
(b₂ " ) * (b₂ * b₁) = b₁

proof end;

theorem Th3: :: URYSOHN2:3

for b₁ being Real st b₁ <> 0 holds
for b₂ being Subset of REAL st b₂ = REAL holds
b₁ * b₂ = b₂

proof end;

theorem Th4: :: URYSOHN2:4

for b₁ being Subset of REAL st b₁ <> {} holds
0 * b₁ = {0}

proof end;

theorem Th5: :: URYSOHN2:5

for b₁ being Real holds b₁ * {} = {}

proof end;

theorem Th6: :: URYSOHN2:6

for b₁, b₂ being R_eal holds
( not b₁ <=' b₂ or ( b₁ = -infty & b₂ = -infty ) or ( b₁ = -infty & b₂ in REAL ) or ( b₁ = -infty & b₂ = +infty ) or ( b₁ in REAL & b₂ in REAL ) or ( b₁ in REAL & b₂ = +infty ) or ( b₁ = +infty & b₂ = +infty ) )

proof end;

theorem Th7: :: URYSOHN2:7

for b₁ being R_eal holds [.b₁,b₁.] is Interval

proof end;

theorem Th8: :: URYSOHN2:8

for b₁ being Interval holds 0 * b₁ is Interval

proof end;

theorem Th9: :: URYSOHN2:9

for b₁ being Interval
for b₂ being Real st b₂ <> 0 & b₁ is open_interval holds
b₂ * b₁ is open_interval

proof end;

theorem Th10: :: URYSOHN2:10

for b₁ being Interval
for b₂ being Real st b₂ <> 0 & b₁ is closed_interval holds
b₂ * b₁ is closed_interval

proof end;

theorem Th11: :: URYSOHN2:11

for b₁ being Interval
for b₂ being Real st 0 < b₂ & b₁ is right_open_interval holds
b₂ * b₁ is right_open_interval

proof end;

theorem Th12: :: URYSOHN2:12

for b₁ being Interval
for b₂ being Real st b₂ < 0 & b₁ is right_open_interval holds
b₂ * b₁ is left_open_interval

proof end;

theorem Th13: :: URYSOHN2:13

for b₁ being Interval
for b₂ being Real st 0 < b₂ & b₁ is left_open_interval holds
b₂ * b₁ is left_open_interval

proof end;

theorem Th14: :: URYSOHN2:14

for b₁ being Interval
for b₂ being Real st b₂ < 0 & b₁ is left_open_interval holds
b₂ * b₁ is right_open_interval

proof end;

theorem Th15: :: URYSOHN2:15

for b₁ being Interval st b₁ <> {} holds
for b₂ being Real st 0 < b₂ holds
for b₃ being Interval st b₃ = b₂ * b₁ & b₁ = [.(^^ b₁),(b₁ ^^ ).] holds
( b₃ = [.(^^ b₃),(b₃ ^^ ).] & ( for b₄, b₅ being Real st b₄ = ^^ b₁ & b₅ = b₁ ^^ holds
( ^^ b₃ = b₂ * b₄ & b₃ ^^ = b₂ * b₅ ) ) )

proof end;

theorem Th16: :: URYSOHN2:16

for b₁ being Interval st b₁ <> {} holds
for b₂ being Real st 0 < b₂ holds
for b₃ being Interval st b₃ = b₂ * b₁ & b₁ = ].(^^ b₁),(b₁ ^^ ).] holds
( b₃ = ].(^^ b₃),(b₃ ^^ ).] & ( for b₄, b₅ being Real st b₄ = ^^ b₁ & b₅ = b₁ ^^ holds
( ^^ b₃ = b₂ * b₄ & b₃ ^^ = b₂ * b₅ ) ) )

proof end;

theorem Th17: :: URYSOHN2:17

for b₁ being Interval st b₁ <> {} holds
for b₂ being Real st 0 < b₂ holds
for b₃ being Interval st b₃ = b₂ * b₁ & b₁ = ].(^^ b₁),(b₁ ^^ ).[ holds
( b₃ = ].(^^ b₃),(b₃ ^^ ).[ & ( for b₄, b₅ being Real st b₄ = ^^ b₁ & b₅ = b₁ ^^ holds
( ^^ b₃ = b₂ * b₄ & b₃ ^^ = b₂ * b₅ ) ) )

proof end;

theorem Th18: :: URYSOHN2:18

for b₁ being Interval st b₁ <> {} holds
for b₂ being Real st 0 < b₂ holds
for b₃ being Interval st b₃ = b₂ * b₁ & b₁ = [.(^^ b₁),(b₁ ^^ ).[ holds
( b₃ = [.(^^ b₃),(b₃ ^^ ).[ & ( for b₄, b₅ being Real st b₄ = ^^ b₁ & b₅ = b₁ ^^ holds
( ^^ b₃ = b₂ * b₄ & b₃ ^^ = b₂ * b₅ ) ) )

proof end;

theorem Th19: :: URYSOHN2:19

for b₁ being Interval
for b₂ being Real holds b₂ * b₁ is Interval

proof end;

registration

let c₁ be Interval;
let c₂ be Real;
cluster a₂ * a₁ -> interval ;
correctness by Th19;

end;

theorem Th20: :: URYSOHN2:20

for b₁ being Interval
for b₂ being Real st 0 <= b₂ holds
for b₃ being Real st b₃ = vol b₁ holds
b₂ * b₃ = vol (b₂ * b₁)

proof end;

theorem Th21: :: URYSOHN2:21

canceled;

theorem Th22: :: URYSOHN2:22

canceled;

theorem Th23: :: URYSOHN2:23

for b₁ being Real st 0 < b₁ holds
ex b₂ being Nat st 1 < (2 |^ b₂) * b₁

proof end;

theorem Th24: :: URYSOHN2:24

for b₁, b₂ being Real st 0 <= b₁ & 1 < b₂ - b₁ holds
ex b₃ being Nat st
( b₁ < b₃ & b₃ < b₂ )

proof end;

theorem Th25: :: URYSOHN2:25

canceled;

theorem Th26: :: URYSOHN2:26

canceled;

theorem Th27: :: URYSOHN2:27

for b₁ being Nat holds dyadic b₁ c= DYADIC

proof end;

theorem Th28: :: URYSOHN2:28

for b₁, b₂ being Real st b₁ < b₂ & 0 <= b₁ & b₂ <= 1 holds
ex b₃ being Real st
( b₃ in DYADIC & b₁ < b₃ & b₃ < b₂ )

proof end;

theorem Th29: :: URYSOHN2:29

for b₁, b₂ being Real st b₁ < b₂ holds
ex b₃ being Real st
( b₃ in DOM & b₁ < b₃ & b₃ < b₂ )

proof end;

theorem Th30: :: URYSOHN2:30

for b₁ being non empty Subset of ExtREAL
for b₂, b₃ being R_eal st b₁ c= [.b₂,b₃.] holds
( b₂ <=' inf b₁ & sup b₁ <=' b₃ )

proof end;

theorem Th31: :: URYSOHN2:31

( 0 in DYADIC & 1 in DYADIC )

proof end;

theorem Th32: :: URYSOHN2:32

for b₁, b₂ being R_eal st b₁ = 0 & b₂ = 1 holds
DYADIC c= [.b₁,b₂.]

proof end;

theorem Th33: :: URYSOHN2:33

for b₁, b₂ being Nat st b₁ <= b₂ holds
dyadic b₁ c= dyadic b₂

proof end;

theorem Th34: :: URYSOHN2:34

for b₁, b₂, b₃, b₄ being Real st b₁ < b₃ & b₃ < b₂ & b₁ < b₄ & b₄ < b₂ holds
abs (b₄ - b₃) < b₂ - b₁

proof end;

theorem Th35: :: URYSOHN2:35

for b₁ being Real st 0 < b₁ holds
for b₂ being Real st 0 < b₂ & b₂ <= 1 holds
ex b₃, b₄ being Real st
( b₃ in DYADIC \/ R>1 & b₄ in DYADIC \/ R>1 & 0 < b₃ & b₃ < b₂ & b₂ < b₄ & b₄ - b₃ < b₁ )

proof end;