let Iac, Icb, I be non empty closed_interval Subset of REAL; for D1 being Division of Iac
for D2 being Division of Icb st upper_bound Iac <= lower_bound Icb & I = [.(lower_bound Iac),(upper_bound Icb).] holds
D1 (#) D2 is Division of I
let Dac be Division of Iac; for D2 being Division of Icb st upper_bound Iac <= lower_bound Icb & I = [.(lower_bound Iac),(upper_bound Icb).] holds
Dac (#) D2 is Division of I
let Dcb be Division of Icb; ( upper_bound Iac <= lower_bound Icb & I = [.(lower_bound Iac),(upper_bound Icb).] implies Dac (#) Dcb is Division of I )
assume that
A1:
upper_bound Iac <= lower_bound Icb
and
A2:
I = [.(lower_bound Iac),(upper_bound Icb).]
; Dac (#) Dcb is Division of I
lower_bound Iac <= upper_bound Iac
by BORSUK_4:28;
then A3:
lower_bound Iac <= lower_bound Icb
by A1, XXREAL_0:2;
lower_bound Icb <= upper_bound Icb
by BORSUK_4:28;
then A4:
lower_bound Iac <= upper_bound Icb
by A3, XXREAL_0:2;
then
( lower_bound I = lower_bound Iac & upper_bound I = upper_bound Icb )
by A2, JORDAN5A:19;
then A5:
Iac \/ Icb c= I
by A1, Th37;
A6:
rng Dac c= Iac
by INTEGRA1:def 2;
A7:
rng Dcb c= Icb
by INTEGRA1:def 2;
rng Dcb <> {}
;
then
1 in dom Dcb
by FINSEQ_3:32;
then A8:
1 in Seg (len Dcb)
by FINSEQ_1:def 3;
then
1 <= len Dcb
by FINSEQ_1:1;
then A9:
(len Dac) + 1 <= (len Dac) + (len Dcb)
by XREAL_1:7;
set Dacb = Dac (#) Dcb;
per cases
( Dcb . 1 <> upper_bound Iac or Dcb . 1 = upper_bound Iac )
;
suppose
Dcb . 1
<> upper_bound Iac
;
Dac (#) Dcb is Division of Ithen A10:
Dac (#) Dcb = Dac ^ Dcb
by A1, Def4;
rng (Dac (#) Dcb) = (rng Dac) \/ (rng Dcb)
by A10, FINSEQ_1:31;
then
rng (Dac (#) Dcb) c= Iac \/ Icb
by A6, A7, XBOOLE_1:13;
then A11:
rng (Dac (#) Dcb) c= I
by A5;
len (Dac (#) Dcb) = (len Dac) + (len Dcb)
by A10, FINSEQ_1:22;
then (Dac (#) Dcb) . (len (Dac (#) Dcb)) =
Dcb . (((len Dac) + (len Dcb)) - (len Dac))
by A9, A10, FINSEQ_1:23
.=
upper_bound Icb
by INTEGRA1:def 2
.=
upper_bound I
by A4, A2, JORDAN5A:19
;
hence
Dac (#) Dcb is
Division of
I
by A11, INTEGRA1:def 2;
verum end; suppose A12:
Dcb . 1
= upper_bound Iac
;
Dac (#) Dcb is Division of Ithen A13:
Dac (#) Dcb = Dac ^ (Dcb /^ 1)
by A1, Def4;
then A14:
rng (Dac (#) Dcb) c= (rng Dac) \/ (rng (Dcb /^ 1))
by FINSEQ_1:31;
rng (Dcb /^ 1) c= rng Dcb
by FINSEQ_5:33;
then A15:
(rng Dac) \/ (rng (Dcb /^ 1)) c= (rng Dac) \/ (rng Dcb)
by XBOOLE_1:13;
(rng Dac) \/ (rng Dcb) c= Iac \/ Icb
by A6, A7, XBOOLE_1:13;
then
rng (Dac (#) Dcb) c= Iac \/ Icb
by A14, A15;
then A16:
rng (Dac (#) Dcb) c= I
by A5;
A17:
len (Dac (#) Dcb) = (len Dac) + (len (Dcb /^ 1))
by A13, FINSEQ_1:22;
A18:
1
<= len Dcb
by A8, FINSEQ_1:1;
then A18bis:
len (Dcb /^ 1) = (len Dcb) - 1
by RFINSEQ:def 1;
per cases
( len Dcb = 1 or len Dcb <> 1 )
;
suppose
len Dcb <> 1
;
Dac (#) Dcb is Division of Ithen A20:
2
- 1
<= (len Dcb) - 1
by NAT_1:23, XREAL_1:9;
A21:
Seg (len (Dcb /^ 1)) = dom (Dcb /^ 1)
by FINSEQ_1:def 3;
A22:
len (Dcb /^ 1) = (len Dcb) - 1
by A18, RFINSEQ:def 1;
1
<= len (Dcb /^ 1)
by A18, RFINSEQ:def 1, A20;
then A23:
len (Dcb /^ 1) in dom (Dcb /^ 1)
by A21, FINSEQ_1:1;
Dcb /^ 1
<> {}
by A22, A20;
then
rng (Dcb /^ 1) <> {}
;
then
1
in dom (Dcb /^ 1)
by FINSEQ_3:32;
then
1
<= len (Dcb /^ 1)
by FINSEQ_3:25;
then
(
(len Dac) + 1
<= (len Dac) + (len (Dcb /^ 1)) &
(len Dac) + (len (Dcb /^ 1)) <= (len Dac) + (len (Dcb /^ 1)) )
by XREAL_1:7;
then (Dac (#) Dcb) . (len (Dac (#) Dcb)) =
(Dcb /^ 1) . (((len Dac) + (len (Dcb /^ 1))) - (len Dac))
by A17, A13, FINSEQ_1:23
.=
Dcb . ((len (Dcb /^ 1)) + 1)
by A18, RFINSEQ:def 1, A23
.=
upper_bound Icb
by A18bis, INTEGRA1:def 2
.=
upper_bound I
by A4, A2, JORDAN5A:19
;
hence
Dac (#) Dcb is
Division of
I
by A16, INTEGRA1:def 2;
verum end; end;