Metamath Proof Explorer


Theorem uniioombllem2a

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses uniioombl.1 φ F : 2
uniioombl.2 φ Disj x . F x
uniioombl.3 S = seq 1 + abs F
uniioombl.a A = ran . F
uniioombl.e φ vol * E
uniioombl.c φ C +
uniioombl.g φ G : 2
uniioombl.s φ E ran . G
uniioombl.t T = seq 1 + abs G
uniioombl.v φ sup ran T * < vol * E + C
Assertion uniioombllem2a φ J z . F z . G J ran .

Proof

Step Hyp Ref Expression
1 uniioombl.1 φ F : 2
2 uniioombl.2 φ Disj x . F x
3 uniioombl.3 S = seq 1 + abs F
4 uniioombl.a A = ran . F
5 uniioombl.e φ vol * E
6 uniioombl.c φ C +
7 uniioombl.g φ G : 2
8 uniioombl.s φ E ran . G
9 uniioombl.t T = seq 1 + abs G
10 uniioombl.v φ sup ran T * < vol * E + C
11 1 adantr φ J F : 2
12 11 ffvelrnda φ J z F z 2
13 12 elin2d φ J z F z 2
14 1st2nd2 F z 2 F z = 1 st F z 2 nd F z
15 13 14 syl φ J z F z = 1 st F z 2 nd F z
16 15 fveq2d φ J z . F z = . 1 st F z 2 nd F z
17 df-ov 1 st F z 2 nd F z = . 1 st F z 2 nd F z
18 16 17 eqtr4di φ J z . F z = 1 st F z 2 nd F z
19 7 ffvelrnda φ J G J 2
20 19 elin2d φ J G J 2
21 1st2nd2 G J 2 G J = 1 st G J 2 nd G J
22 20 21 syl φ J G J = 1 st G J 2 nd G J
23 22 fveq2d φ J . G J = . 1 st G J 2 nd G J
24 df-ov 1 st G J 2 nd G J = . 1 st G J 2 nd G J
25 23 24 eqtr4di φ J . G J = 1 st G J 2 nd G J
26 25 adantr φ J z . G J = 1 st G J 2 nd G J
27 18 26 ineq12d φ J z . F z . G J = 1 st F z 2 nd F z 1 st G J 2 nd G J
28 ovolfcl F : 2 z 1 st F z 2 nd F z 1 st F z 2 nd F z
29 11 28 sylan φ J z 1 st F z 2 nd F z 1 st F z 2 nd F z
30 29 simp1d φ J z 1 st F z
31 30 rexrd φ J z 1 st F z *
32 29 simp2d φ J z 2 nd F z
33 32 rexrd φ J z 2 nd F z *
34 ovolfcl G : 2 J 1 st G J 2 nd G J 1 st G J 2 nd G J
35 7 34 sylan φ J 1 st G J 2 nd G J 1 st G J 2 nd G J
36 35 simp1d φ J 1 st G J
37 36 rexrd φ J 1 st G J *
38 37 adantr φ J z 1 st G J *
39 35 simp2d φ J 2 nd G J
40 39 rexrd φ J 2 nd G J *
41 40 adantr φ J z 2 nd G J *
42 iooin 1 st F z * 2 nd F z * 1 st G J * 2 nd G J * 1 st F z 2 nd F z 1 st G J 2 nd G J = if 1 st F z 1 st G J 1 st G J 1 st F z if 2 nd F z 2 nd G J 2 nd F z 2 nd G J
43 31 33 38 41 42 syl22anc φ J z 1 st F z 2 nd F z 1 st G J 2 nd G J = if 1 st F z 1 st G J 1 st G J 1 st F z if 2 nd F z 2 nd G J 2 nd F z 2 nd G J
44 27 43 eqtrd φ J z . F z . G J = if 1 st F z 1 st G J 1 st G J 1 st F z if 2 nd F z 2 nd G J 2 nd F z 2 nd G J
45 ioorebas if 1 st F z 1 st G J 1 st G J 1 st F z if 2 nd F z 2 nd G J 2 nd F z 2 nd G J ran .
46 44 45 eqeltrdi φ J z . F z . G J ran .