# Metamath Proof Explorer

## Theorem itg20

Description: The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg20 ${⊢}{\int }^{2}\left(ℝ×\left\{0\right\}\right)=0$

### Proof

Step Hyp Ref Expression
1 i1f0 ${⊢}ℝ×\left\{0\right\}\in \mathrm{dom}{\int }^{1}$
2 reex ${⊢}ℝ\in \mathrm{V}$
3 2 a1i ${⊢}\top \to ℝ\in \mathrm{V}$
4 i1ff ${⊢}ℝ×\left\{0\right\}\in \mathrm{dom}{\int }^{1}\to \left(ℝ×\left\{0\right\}\right):ℝ⟶ℝ$
5 1 4 mp1i ${⊢}\top \to \left(ℝ×\left\{0\right\}\right):ℝ⟶ℝ$
6 leid ${⊢}{x}\in ℝ\to {x}\le {x}$
7 6 adantl ${⊢}\left(\top \wedge {x}\in ℝ\right)\to {x}\le {x}$
8 3 5 7 caofref ${⊢}\top \to \left(ℝ×\left\{0\right\}\right){\le }_{f}\left(ℝ×\left\{0\right\}\right)$
9 ax-resscn ${⊢}ℝ\subseteq ℂ$
10 9 a1i ${⊢}\top \to ℝ\subseteq ℂ$
11 5 ffnd ${⊢}\top \to \left(ℝ×\left\{0\right\}\right)Fnℝ$
12 10 11 0pledm ${⊢}\top \to \left({0}_{𝑝}{\le }_{f}\left(ℝ×\left\{0\right\}\right)↔\left(ℝ×\left\{0\right\}\right){\le }_{f}\left(ℝ×\left\{0\right\}\right)\right)$
13 8 12 mpbird ${⊢}\top \to {0}_{𝑝}{\le }_{f}\left(ℝ×\left\{0\right\}\right)$
14 13 mptru ${⊢}{0}_{𝑝}{\le }_{f}\left(ℝ×\left\{0\right\}\right)$
15 itg2itg1 ${⊢}\left(ℝ×\left\{0\right\}\in \mathrm{dom}{\int }^{1}\wedge {0}_{𝑝}{\le }_{f}\left(ℝ×\left\{0\right\}\right)\right)\to {\int }^{2}\left(ℝ×\left\{0\right\}\right)={\int }^{1}\left(ℝ×\left\{0\right\}\right)$
16 1 14 15 mp2an ${⊢}{\int }^{2}\left(ℝ×\left\{0\right\}\right)={\int }^{1}\left(ℝ×\left\{0\right\}\right)$
17 itg10 ${⊢}{\int }^{1}\left(ℝ×\left\{0\right\}\right)=0$
18 16 17 eqtri ${⊢}{\int }^{2}\left(ℝ×\left\{0\right\}\right)=0$