itgle - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > itgle		Structured version Visualization version GIF version

Theorem itgle 25831

Description: Monotonicity of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.)

**Hypotheses**
Ref	Expression
itgle.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹)
itgle.2	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹)
itgle.3	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
itgle.4	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
itgle.5	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶)

**Assertion**
Ref	Expression
itgle	⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ≤ ∫𝐴𝐶 d𝑥)

Distinct variable groups: 𝑥,𝐴 𝜑,𝑥 Allowed substitution hints: 𝐵(𝑥) 𝐶(𝑥)

**Proof of Theorem itgle**
Step	Hyp	Ref	Expression
1		itgle.1	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹)
2		itgle.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
3	2	iblrelem 25812	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ)))
4	1, 3	mpbid 231	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ))
5	4	simp2d 1140	. . 3 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ)
6		itgle.2	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹)
7		itgle.4	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
8	7	iblrelem 25812	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0))) ∈ ℝ)))
9	6, 8	mpbid 231	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0))) ∈ ℝ))
10	9	simp3d 1141	. . 3 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0))) ∈ ℝ)
11	9	simp2d 1140	. . 3 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ)
12	4	simp3d 1141	. . 3 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ)
13	2	ad2ant2r 745	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)) → 𝐵 ∈ ℝ)
14	13	rexrd 11316	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)) → 𝐵 ∈ ℝ^*)
15		simprr 771	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ 𝐵)
16		elxrge0 13493	. . . . . . 7 ⊢ (𝐵 ∈ (0[,]+∞) ↔ (𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵))
17	14, 15, 16	sylanbrc 581	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)) → 𝐵 ∈ (0[,]+∞))
18		0e0iccpnf 13495	. . . . . . 7 ⊢ 0 ∈ (0[,]+∞)
19	18	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ∈ (0[,]+∞))
20	17, 19	ifclda 4569	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,]+∞))
21	20	fmpttd 7132	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)):ℝ⟶(0[,]+∞))
22	7	ad2ant2r 745	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)) → 𝐶 ∈ ℝ)
23	22	rexrd 11316	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)) → 𝐶 ∈ ℝ^*)
24		simprr 771	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)) → 0 ≤ 𝐶)
25		elxrge0 13493	. . . . . . 7 ⊢ (𝐶 ∈ (0[,]+∞) ↔ (𝐶 ∈ ℝ^* ∧ 0 ≤ 𝐶))
26	23, 24, 25	sylanbrc 581	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)) → 𝐶 ∈ (0[,]+∞))
27	18	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)) → 0 ∈ (0[,]+∞))
28	26, 27	ifclda 4569	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,]+∞))
29	28	fmpttd 7132	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)):ℝ⟶(0[,]+∞))
30		0re 11268	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
31		max1 13223	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
32	30, 7, 31	sylancr 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
33		ifcl 4579	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
34	7, 30, 33	sylancl 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
35		itgle.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶)
36		max2 13225	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0))
37	30, 7, 36	sylancr 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0))
38	2, 7, 34, 35, 37	letrd 11423	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ if(0 ≤ 𝐶, 𝐶, 0))
39		maxle 13229	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ if(0 ≤ 𝐶, 𝐶, 0) ↔ (0 ≤ if(0 ≤ 𝐶, 𝐶, 0) ∧ 𝐵 ≤ if(0 ≤ 𝐶, 𝐶, 0))))
40	30, 2, 34, 39	mp3an2i 1463	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) ≤ if(0 ≤ 𝐶, 𝐶, 0) ↔ (0 ≤ if(0 ≤ 𝐶, 𝐶, 0) ∧ 𝐵 ≤ if(0 ≤ 𝐶, 𝐶, 0))))
41	32, 38, 40	mpbir2and 711	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ≤ if(0 ≤ 𝐶, 𝐶, 0))
42		iftrue 4540	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) = if(0 ≤ 𝐵, 𝐵, 0))
43	42	adantl 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) = if(0 ≤ 𝐵, 𝐵, 0))
44		iftrue 4540	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) = if(0 ≤ 𝐶, 𝐶, 0))
45	44	adantl 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) = if(0 ≤ 𝐶, 𝐶, 0))
46	41, 43, 45	3brtr4d 5186	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ≤ if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0))
47	46	ex 411	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ≤ if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0)))
48		0le0 12370	. . . . . . . . . 10 ⊢ 0 ≤ 0
49	48	a1i 11	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → 0 ≤ 0)
50		iffalse 4543	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) = 0)
51		iffalse 4543	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) = 0)
52	49, 50, 51	3brtr4d 5186	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ≤ if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0))
53	47, 52	pm2.61d1 180	. . . . . . 7 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ≤ if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0))
54		ifan 4587	. . . . . . 7 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0)
55		ifan 4587	. . . . . . 7 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0)
56	53, 54, 55	3brtr4g 5188	. . . . . 6 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ≤ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
57	56	ralrimivw 3143	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ≤ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
58		reex 11251	. . . . . . 7 ⊢ ℝ ∈ V
59	58	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ∈ V)
60		eqidd 2730	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)))
61		eqidd 2730	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))
62	59, 20, 28, 60, 61	ofrfval2 7714	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ≤ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))
63	57, 62	mpbird 256	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))
64		itg2le 25761	. . . 4 ⊢ (((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))))
65	21, 29, 63, 64	syl3anc 1368	. . 3 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))))
66	7	renegcld 11693	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐶 ∈ ℝ)
67	66	ad2ant2r 745	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶)) → -𝐶 ∈ ℝ)
68	67	rexrd 11316	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶)) → -𝐶 ∈ ℝ^*)
69		simprr 771	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶)) → 0 ≤ -𝐶)
70		elxrge0 13493	. . . . . . 7 ⊢ (-𝐶 ∈ (0[,]+∞) ↔ (-𝐶 ∈ ℝ^* ∧ 0 ≤ -𝐶))
71	68, 69, 70	sylanbrc 581	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶)) → -𝐶 ∈ (0[,]+∞))
72	18	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶)) → 0 ∈ (0[,]+∞))
73	71, 72	ifclda 4569	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0) ∈ (0[,]+∞))
74	73	fmpttd 7132	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0)):ℝ⟶(0[,]+∞))
75	2	renegcld 11693	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ)
76	75	ad2ant2r 745	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵)) → -𝐵 ∈ ℝ)
77	76	rexrd 11316	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵)) → -𝐵 ∈ ℝ^*)
78		simprr 771	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵)) → 0 ≤ -𝐵)
79		elxrge0 13493	. . . . . . 7 ⊢ (-𝐵 ∈ (0[,]+∞) ↔ (-𝐵 ∈ ℝ^* ∧ 0 ≤ -𝐵))
80	77, 78, 79	sylanbrc 581	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵)) → -𝐵 ∈ (0[,]+∞))
81	18	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵)) → 0 ∈ (0[,]+∞))
82	80, 81	ifclda 4569	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0) ∈ (0[,]+∞))
83	82	fmpttd 7132	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)):ℝ⟶(0[,]+∞))
84		max1 13223	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ -𝐵 ∈ ℝ) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0))
85	30, 75, 84	sylancr 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0))
86		ifcl 4579	. . . . . . . . . . . . 13 ⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
87	75, 30, 86	sylancl 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
88	2, 7	lenegd 11845	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 𝐶 ↔ -𝐶 ≤ -𝐵))
89	35, 88	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐶 ≤ -𝐵)
90		max2 13225	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ -𝐵 ∈ ℝ) → -𝐵 ≤ if(0 ≤ -𝐵, -𝐵, 0))
91	30, 75, 90	sylancr 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ≤ if(0 ≤ -𝐵, -𝐵, 0))
92	66, 75, 87, 89, 91	letrd 11423	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐶 ≤ if(0 ≤ -𝐵, -𝐵, 0))
93		maxle 13229	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ -𝐶 ∈ ℝ ∧ if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) → (if(0 ≤ -𝐶, -𝐶, 0) ≤ if(0 ≤ -𝐵, -𝐵, 0) ↔ (0 ≤ if(0 ≤ -𝐵, -𝐵, 0) ∧ -𝐶 ≤ if(0 ≤ -𝐵, -𝐵, 0))))
94	30, 66, 87, 93	mp3an2i 1463	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐶, -𝐶, 0) ≤ if(0 ≤ -𝐵, -𝐵, 0) ↔ (0 ≤ if(0 ≤ -𝐵, -𝐵, 0) ∧ -𝐶 ≤ if(0 ≤ -𝐵, -𝐵, 0))))
95	85, 92, 94	mpbir2and 711	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐶, -𝐶, 0) ≤ if(0 ≤ -𝐵, -𝐵, 0))
96		iftrue 4540	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -𝐶, -𝐶, 0), 0) = if(0 ≤ -𝐶, -𝐶, 0))
97	96	adantl 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ -𝐶, -𝐶, 0), 0) = if(0 ≤ -𝐶, -𝐶, 0))
98		iftrue 4540	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0) = if(0 ≤ -𝐵, -𝐵, 0))
99	98	adantl 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0) = if(0 ≤ -𝐵, -𝐵, 0))
100	95, 97, 99	3brtr4d 5186	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ -𝐶, -𝐶, 0), 0) ≤ if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0))
101	100	ex 411	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -𝐶, -𝐶, 0), 0) ≤ if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0)))
102		iffalse 4543	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -𝐶, -𝐶, 0), 0) = 0)
103		iffalse 4543	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0) = 0)
104	49, 102, 103	3brtr4d 5186	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -𝐶, -𝐶, 0), 0) ≤ if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0))
105	101, 104	pm2.61d1 180	. . . . . . 7 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ -𝐶, -𝐶, 0), 0) ≤ if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0))
106		ifan 4587	. . . . . . 7 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ -𝐶, -𝐶, 0), 0)
107		ifan 4587	. . . . . . 7 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0)
108	105, 106, 107	3brtr4g 5188	. . . . . 6 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0) ≤ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))
109	108	ralrimivw 3143	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0) ≤ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))
110		eqidd 2730	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0)))
111		eqidd 2730	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)))
112	59, 73, 82, 110, 111	ofrfval2 7714	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0) ≤ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)))
113	109, 112	mpbird 256	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)))
114		itg2le 25761	. . . 4 ⊢ (((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))))
115	74, 83, 113, 114	syl3anc 1368	. . 3 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))))
116	5, 10, 11, 12, 65, 115	le2subd 11886	. 2 ⊢ (𝜑 → ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) − (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)))) ≤ ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) − (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0)))))
117	2, 1	itgrevallem1 25816	. 2 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) − (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)))))
118	7, 6	itgrevallem1 25816	. 2 ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) − (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐶), -𝐶, 0)))))
119	116, 117, 118	3brtr4d 5186	1 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ≤ ∫𝐴𝐶 d𝑥)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2100 ∀wral 3054 Vcvv 3472 ifcif 4534 class class class wbr 5154 ↦ cmpt 5237 ⟶wf 6553 ‘cfv 6557 (class class class)co 7428 ∘_r cofr 7692 ℝcr 11159 0cc0 11160 +∞cpnf 11297 ℝ^*cxr 11299 ≤ cle 11301 − cmin 11496 -cneg 11497 [,]cicc 13386 MblFncmbf 25635 ∫₂citg2 25637 𝐿¹cibl 25638 ∫citg 25639

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2102 ax-9 2110 ax-10 2133 ax-11 2150 ax-12 2170 ax-ext 2700 ax-rep 5291 ax-sep 5305 ax-nul 5312 ax-pow 5371 ax-pr 5435 ax-un 7749 ax-inf2 9686 ax-cnex 11216 ax-resscn 11217 ax-1cn 11218 ax-icn 11219 ax-addcl 11220 ax-addrcl 11221 ax-mulcl 11222 ax-mulrcl 11223 ax-mulcom 11224 ax-addass 11225 ax-mulass 11226 ax-distr 11227 ax-i2m1 11228 ax-1ne0 11229 ax-1rid 11230 ax-rnegex 11231 ax-rrecex 11232 ax-cnre 11233 ax-pre-lttri 11234 ax-pre-lttrn 11235 ax-pre-ltadd 11236 ax-pre-mulgt0 11237 ax-pre-sup 11238 ax-addf 11239

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2062 df-mo 2532 df-eu 2561 df-clab 2707 df-cleq 2721 df-clel 2806 df-nfc 2881 df-ne 2934 df-nel 3040 df-ral 3055 df-rex 3064 df-rmo 3373 df-reu 3374 df-rab 3429 df-v 3474 df-sbc 3788 df-csb 3904 df-dif 3961 df-un 3963 df-in 3965 df-ss 3975 df-pss 3978 df-nul 4334 df-if 4535 df-pw 4610 df-sn 4635 df-pr 4637 df-op 4641 df-uni 4917 df-int 4958 df-iun 5006 df-disj 5122 df-br 5155 df-opab 5217 df-mpt 5238 df-tr 5272 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5639 df-se 5640 df-we 5641 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6316 df-ord 6382 df-on 6383 df-lim 6384 df-suc 6385 df-iota 6509 df-fun 6559 df-fn 6560 df-f 6561 df-f1 6562 df-fo 6563 df-f1o 6564 df-fv 6565 df-isom 6566 df-riota 7384 df-ov 7431 df-oprab 7432 df-mpo 7433 df-of 7693 df-ofr 7694 df-om 7883 df-1st 8009 df-2nd 8010 df-frecs 8301 df-wrecs 8332 df-recs 8406 df-rdg 8445 df-1o 8501 df-2o 8502 df-er 8739 df-map 8862 df-pm 8863 df-en 8980 df-dom 8981 df-sdom 8982 df-fin 8983 df-sup 9487 df-inf 9488 df-oi 9555 df-dju 9946 df-card 9984 df-pnf 11302 df-mnf 11303 df-xr 11304 df-ltxr 11305 df-le 11306 df-sub 11498 df-neg 11499 df-div 11924 df-nn 12270 df-2 12332 df-3 12333 df-4 12334 df-n0 12530 df-z 12616 df-uz 12880 df-q 12990 df-rp 13034 df-xadd 13152 df-ioo 13387 df-ico 13389 df-icc 13390 df-fz 13544 df-fzo 13687 df-fl 13818 df-mod 13896 df-seq 14028 df-exp 14088 df-hash 14355 df-cj 15118 df-re 15119 df-im 15120 df-sqrt 15254 df-abs 15255 df-clim 15504 df-sum 15705 df-xmet 21349 df-met 21350 df-ovol 25485 df-vol 25486 df-mbf 25640 df-itg1 25641 df-itg2 25642 df-ibl 25643 df-itg 25644 df-0p 25691

This theorem is referenced by: itgge0 25832 itgless 25838 itgabs 25856 itgulm 26435 itgabsnc 37476 intlewftc 41846 wallispilem1 45800 fourierdlem47 45888 fourierdlem87 45928 etransclem23 45992

W3C validator