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	$⊢ φ \to X < Y$
	itggt0cn.2	$⊢ φ \to (x \in (X, Y) ⟼ B) \in 𝐿^{1}$
	itggt0cn.3	$⊢ (φ \land x \in (X, Y)) \to B \in ℝ^{+}$
	itggt0cn.cn	$⊢ φ \to (x \in (X, Y) ⟼ B) : (X, Y) \underset{cn}{⟶} ℂ$
Assertion	itggt0cn	$⊢ φ \to 0 < \int_{(X, Y)} B d x$

Proof

Step	Hyp	Ref	Expression
1		itggt0cn.1	$⊢ φ \to X < Y$
2		itggt0cn.2	$⊢ φ \to (x \in (X, Y) ⟼ B) \in 𝐿^{1}$
3		itggt0cn.3	$⊢ (φ \land x \in (X, Y)) \to B \in ℝ^{+}$
4		itggt0cn.cn	$⊢ φ \to (x \in (X, Y) ⟼ B) : (X, Y) \underset{cn}{⟶} ℂ$
5	3	rpred	$⊢ (φ \land x \in (X, Y)) \to B \in ℝ$
6	3	rpge0d	$⊢ (φ \land x \in (X, Y)) \to 0 \leq B$
7		elrege0	$⊢ B \in [0, +∞) \leftrightarrow (B \in ℝ \land 0 \leq B)$
8	5 6 7	sylanbrc	$⊢ (φ \land x \in (X, Y)) \to B \in [0, +∞)$
9		0e0icopnf	$⊢ 0 \in [0, +∞)$
10	9	a1i	$⊢ (φ \land \neg x \in (X, Y)) \to 0 \in [0, +∞)$
11	8 10	ifclda	$⊢ φ \to if (x \in (X, Y), B, 0) \in [0, +∞)$
12	11	adantr	$⊢ (φ \land x \in ℝ) \to if (x \in (X, Y), B, 0) \in [0, +∞)$
13	12	fmpttd	$⊢ φ \to (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) : ℝ ⟶ [0, +∞)$
14	3	rpgt0d	$⊢ (φ \land x \in (X, Y)) \to 0 < B$
15		elioore	$⊢ x \in (X, Y) \to x \in ℝ$
16	15	adantl	$⊢ (φ \land x \in (X, Y)) \to x \in ℝ$
17		iftrue	$⊢ x \in (X, Y) \to if (x \in (X, Y), B, 0) = B$
18	17	adantl	$⊢ (φ \land x \in (X, Y)) \to if (x \in (X, Y), B, 0) = B$
19	18 3	eqeltrd	$⊢ (φ \land x \in (X, Y)) \to if (x \in (X, Y), B, 0) \in ℝ^{+}$
20		eqid	$⊢ (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) = (x \in ℝ ⟼ if (x \in (X, Y), B, 0))$
21	20	fvmpt2	$⊢ (x \in ℝ \land if (x \in (X, Y), B, 0) \in ℝ^{+}) \to (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (x) = if (x \in (X, Y), B, 0)$
22	16 19 21	syl2anc	$⊢ (φ \land x \in (X, Y)) \to (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (x) = if (x \in (X, Y), B, 0)$
23	22 18	eqtrd	$⊢ (φ \land x \in (X, Y)) \to (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (x) = B$
24	14 23	breqtrrd	$⊢ (φ \land x \in (X, Y)) \to 0 < (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (x)$
25	24	ralrimiva	$⊢ φ \to \forall x \in (X, Y) 0 < (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (x)$
26		nfcv	$⊢ \underline{Ⅎ} x 0$
27		nfcv	$⊢ \underline{Ⅎ} x <$
28		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (y)$
29	26 27 28	nfbr	$⊢ Ⅎ x 0 < (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (y)$
30		nfv	$⊢ Ⅎ y 0 < (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (x)$
31		fveq2	$⊢ y = x \to (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (y) = (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (x)$
32	31	breq2d	$⊢ y = x \to (0 < (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (y) \leftrightarrow 0 < (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (x))$
33	29 30 32	cbvralw	$⊢ \forall y \in (X, Y) 0 < (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (y) \leftrightarrow \forall x \in (X, Y) 0 < (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (x)$
34	25 33	sylibr	$⊢ φ \to \forall y \in (X, Y) 0 < (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (y)$
35	34	r19.21bi	$⊢ (φ \land y \in (X, Y)) \to 0 < (x \in ℝ ⟼ if (x \in (X, Y), B, 0)) (y)$
36		ioossre	$⊢ (X, Y) \subseteq ℝ$
37		resmpt	$⊢ (X, Y) \subseteq ℝ \to {(x \in ℝ ⟼ if (x \in (X, Y), B, 0)) ↾}_{(X, Y)} = (x \in (X, Y) ⟼ if (x \in (X, Y), B, 0))$
38	36 37	ax-mp	$⊢ {(x \in ℝ ⟼ if (x \in (X, Y), B, 0)) ↾}_{(X, Y)} = (x \in (X, Y) ⟼ if (x \in (X, Y), B, 0))$
39	17	mpteq2ia	$⊢ (x \in (X, Y) ⟼ if (x \in (X, Y), B, 0)) = (x \in (X, Y) ⟼ B)$
40	38 39	eqtri	$⊢ {(x \in ℝ ⟼ if (x \in (X, Y), B, 0)) ↾}_{(X, Y)} = (x \in (X, Y) ⟼ B)$
41	40 4	eqeltrid	$⊢ φ \to ({(x \in ℝ ⟼ if (x \in (X, Y), B, 0)) ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ$
42	1 13 35 41	itg2gt0cn	$⊢ φ \to 0 < \int^{2} ((x \in ℝ ⟼ if (x \in (X, Y), B, 0)))$
43	5 2 6	itgposval	$⊢ φ \to \int_{(X, Y)} B d x = \int^{2} ((x \in ℝ ⟼ if (x \in (X, Y), B, 0)))$
44	42 43	breqtrrd	$⊢ φ \to 0 < \int_{(X, Y)} B d x$

Metamath Proof Explorer

Theorem itggt0cn

Proof