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	⊢ ( 𝜑 → 𝑋 < 𝑌 )
	itggt0cn.2	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ 𝐿1 )
	itggt0cn.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐵 ∈ ℝ+ )
	itggt0cn.cn	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
Assertion	itggt0cn	⊢ ( 𝜑 → 0 < ∫ ( 𝑋 (,) 𝑌 ) 𝐵 d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		itggt0cn.1	⊢ ( 𝜑 → 𝑋 < 𝑌 )
2		itggt0cn.2	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ 𝐿1 )
3		itggt0cn.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐵 ∈ ℝ+ )
4		itggt0cn.cn	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
5	3	rpred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐵 ∈ ℝ )
6	3	rpge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 0 ≤ 𝐵 )
7		elrege0	⊢ ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
8	5 6 7	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐵 ∈ ( 0 [,) +∞ ) )
9		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
10	9	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 0 ∈ ( 0 [,) +∞ ) )
11	8 10	ifclda	⊢ ( 𝜑 → if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
13	12	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
14	3	rpgt0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 0 < 𝐵 )
15		elioore	⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → 𝑥 ∈ ℝ )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑥 ∈ ℝ )
17		iftrue	⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) = 𝐵 )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) = 𝐵 )
19	18 3	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ∈ ℝ+ )
20		eqid	⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) )
21	20	fvmpt2	⊢ ( ( 𝑥 ∈ ℝ ∧ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) )
22	16 19 21	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) )
23	22 18	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑥 ) = 𝐵 )
24	14 23	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑥 ) )
25	24	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑥 ) )
26		nfcv	⊢ Ⅎ 𝑥 0
27		nfcv	⊢ Ⅎ 𝑥 <
28		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑦 )
29	26 27 28	nfbr	⊢ Ⅎ 𝑥 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑦 )
30		nfv	⊢ Ⅎ 𝑦 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑥 )
31		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑥 ) )
32	31	breq2d	⊢ ( 𝑦 = 𝑥 → ( 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑦 ) ↔ 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑥 ) ) )
33	29 30 32	cbvralw	⊢ ( ∀ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑥 ) )
34	25 33	sylibr	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑦 ) )
35	34	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ‘ 𝑦 ) )
36		ioossre	⊢ ( 𝑋 (,) 𝑌 ) ⊆ ℝ
37		resmpt	⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ℝ → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) )
38	36 37	ax-mp	⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) )
39	17	mpteq2ia	⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 )
40	38 39	eqtri	⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 )
41	40 4	eqeltrid	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
42	1 13 35 41	itg2gt0cn	⊢ ( 𝜑 → 0 < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ) )
43	5 2 6	itgposval	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) 𝐵 d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) , 𝐵 , 0 ) ) ) )
44	42 43	breqtrrd	⊢ ( 𝜑 → 0 < ∫ ( 𝑋 (,) 𝑌 ) 𝐵 d 𝑥 )