Theorem itg2lea

Description: Approximate version of itg2le . If F <_ G for almost all x , then S.2 F <_ S.2 G . (Contributed by Mario Carneiro, 11-Aug-2014)

	Ref	Expression
Hypotheses	itg2lea.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
	itg2lea.2	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
	itg2lea.3	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	itg2lea.4	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
	itg2lea.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
Assertion	itg2lea	⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		itg2lea.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
2		itg2lea.2	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
3		itg2lea.3	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4		itg2lea.4	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
5		itg2lea.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
6	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝑓 ∈ dom ∫1 )
8	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝐴 ⊆ ℝ )
9	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( vol* ‘ 𝐴 ) = 0 )
10		i1ff	⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 : ℝ ⟶ ℝ )
11	10	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝑓 : ℝ ⟶ ℝ )
12		eldifi	⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → 𝑥 ∈ ℝ )
13		ffvelcdm	⊢ ( ( 𝑓 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
14	11 12 13	syl2an	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
15	14	rexrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ* )
16		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
17	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
18		ffvelcdm	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
19	17 12 18	syl2an	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
20	16 19	sselid	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
21		ffvelcdm	⊢ ( ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
22	6 12 21	syl2an	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
23	16 22	sselid	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ* )
24		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝑓 ∘r ≤ 𝐹 )
25	11	ffnd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝑓 Fn ℝ )
26	17	ffnd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝐹 Fn ℝ )
27		reex	⊢ ℝ ∈ V
28	27	a1i	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ℝ ∈ V )
29		inidm	⊢ ( ℝ ∩ ℝ ) = ℝ
30		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
31		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
32	25 26 28 28 29 30 31	ofrfval	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( 𝑓 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
33	24 32	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ∀ 𝑥 ∈ ℝ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
34	33	r19.21bi	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
35	12 34	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
36	5	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
37	15 20 23 35 36	xrletrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
38	6 7 8 9 37	itg2uba	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ∫1 ‘ 𝑓 ) ≤ ( ∫2 ‘ 𝐺 ) )
39	38	expr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ∫2 ‘ 𝐺 ) ) )
40	39	ralrimiva	⊢ ( 𝜑 → ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ∫2 ‘ 𝐺 ) ) )
41		itg2cl	⊢ ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐺 ) ∈ ℝ* )
42	2 41	syl	⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ∈ ℝ* )
43		itg2leub	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐺 ) ∈ ℝ* ) → ( ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ∫2 ‘ 𝐺 ) ) ) )
44	1 42 43	syl2anc	⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ∫2 ‘ 𝐺 ) ) ) )
45	40 44	mpbird	⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) )