Metamath Proof Explorer


Theorem itggt0cn

Description: itggt0 holds for continuous functions in the absence of ax-cc . (Contributed by Brendan Leahy, 16-Nov-2017)

Ref Expression
Hypotheses itggt0cn.1 φ X < Y
itggt0cn.2 φ x X Y B 𝐿 1
itggt0cn.3 φ x X Y B +
itggt0cn.cn φ x X Y B : X Y cn
Assertion itggt0cn φ 0 < X Y B dx

Proof

Step Hyp Ref Expression
1 itggt0cn.1 φ X < Y
2 itggt0cn.2 φ x X Y B 𝐿 1
3 itggt0cn.3 φ x X Y B +
4 itggt0cn.cn φ x X Y B : X Y cn
5 3 rpred φ x X Y B
6 3 rpge0d φ x X Y 0 B
7 elrege0 B 0 +∞ B 0 B
8 5 6 7 sylanbrc φ x X Y B 0 +∞
9 0e0icopnf 0 0 +∞
10 9 a1i φ ¬ x X Y 0 0 +∞
11 8 10 ifclda φ if x X Y B 0 0 +∞
12 11 adantr φ x if x X Y B 0 0 +∞
13 12 fmpttd φ x if x X Y B 0 : 0 +∞
14 3 rpgt0d φ x X Y 0 < B
15 elioore x X Y x
16 15 adantl φ x X Y x
17 iftrue x X Y if x X Y B 0 = B
18 17 adantl φ x X Y if x X Y B 0 = B
19 18 3 eqeltrd φ x X Y if x X Y B 0 +
20 eqid x if x X Y B 0 = x if x X Y B 0
21 20 fvmpt2 x if x X Y B 0 + x if x X Y B 0 x = if x X Y B 0
22 16 19 21 syl2anc φ x X Y x if x X Y B 0 x = if x X Y B 0
23 22 18 eqtrd φ x X Y x if x X Y B 0 x = B
24 14 23 breqtrrd φ x X Y 0 < x if x X Y B 0 x
25 24 ralrimiva φ x X Y 0 < x if x X Y B 0 x
26 nfcv _ x 0
27 nfcv _ x <
28 nffvmpt1 _ x x if x X Y B 0 y
29 26 27 28 nfbr x 0 < x if x X Y B 0 y
30 nfv y 0 < x if x X Y B 0 x
31 fveq2 y = x x if x X Y B 0 y = x if x X Y B 0 x
32 31 breq2d y = x 0 < x if x X Y B 0 y 0 < x if x X Y B 0 x
33 29 30 32 cbvralw y X Y 0 < x if x X Y B 0 y x X Y 0 < x if x X Y B 0 x
34 25 33 sylibr φ y X Y 0 < x if x X Y B 0 y
35 34 r19.21bi φ y X Y 0 < x if x X Y B 0 y
36 ioossre X Y
37 resmpt X Y x if x X Y B 0 X Y = x X Y if x X Y B 0
38 36 37 ax-mp x if x X Y B 0 X Y = x X Y if x X Y B 0
39 17 mpteq2ia x X Y if x X Y B 0 = x X Y B
40 38 39 eqtri x if x X Y B 0 X Y = x X Y B
41 40 4 eqeltrid φ x if x X Y B 0 X Y : X Y cn
42 1 13 35 41 itg2gt0cn φ 0 < 2 x if x X Y B 0
43 5 2 6 itgposval φ X Y B dx = 2 x if x X Y B 0
44 42 43 breqtrrd φ 0 < X Y B dx