ftc1anclem4

		Ref	Expression
	Assertion	ftc1anclem4	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|G (t) - F (t)\|)) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	$⊢ (G : ℝ ⟶ ℝ \land t \in ℝ) \to G (t) \in ℝ$
2	1	recnd	$⊢ (G : ℝ ⟶ ℝ \land t \in ℝ) \to G (t) \in ℂ$
3		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
4	3	ffvelrnda	$⊢ (F \in dom \int^{1} \land t \in ℝ) \to F (t) \in ℝ$
5	4	recnd	$⊢ (F \in dom \int^{1} \land t \in ℝ) \to F (t) \in ℂ$
6		subcl	$⊢ (G (t) \in ℂ \land F (t) \in ℂ) \to G (t) - F (t) \in ℂ$
7	2 5 6	syl2anr	$⊢ ((F \in dom \int^{1} \land t \in ℝ) \land (G : ℝ ⟶ ℝ \land t \in ℝ)) \to G (t) - F (t) \in ℂ$
8	7	anandirs	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to G (t) - F (t) \in ℂ$
9	8	abscld	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|G (t) - F (t)\| \in ℝ$
10	9	rexrd	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|G (t) - F (t)\| \in ℝ^{*}$
11	8	absge0d	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to 0 \leq \|G (t) - F (t)\|$
12		elxrge0	$⊢ \|G (t) - F (t)\| \in [0, +∞] \leftrightarrow (\|G (t) - F (t)\| \in ℝ^{*} \land 0 \leq \|G (t) - F (t)\|)$
13	10 11 12	sylanbrc	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|G (t) - F (t)\| \in [0, +∞]$
14	13	fmpttd	$⊢ (F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t) - F (t)\|) : ℝ ⟶ [0, +∞]$
15	14	3adant2	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t) - F (t)\|) : ℝ ⟶ [0, +∞]$
16		reex	$⊢ ℝ \in V$
17	16	a1i	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to ℝ \in V$
18		fvexd	$⊢ ((F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|G (t)\| \in V$
19		fvexd	$⊢ ((F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|F (t)\| \in V$
20		eqidd	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t)\|) = (t \in ℝ ⟼ \|G (t)\|)$
21		eqidd	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|F (t)\|) = (t \in ℝ ⟼ \|F (t)\|)$
22	17 18 19 20 21	offval2	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t)\|) +_{f} (t \in ℝ ⟼ \|F (t)\|) = (t \in ℝ ⟼ \|G (t)\| + \|F (t)\|)$
23	22	fveq2d	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|G (t)\|) +_{f} (t \in ℝ ⟼ \|F (t)\|)) = \int^{2} ((t \in ℝ ⟼ \|G (t)\| + \|F (t)\|))$
24		id	$⊢ G : ℝ ⟶ ℝ \to G : ℝ ⟶ ℝ$
25	24	feqmptd	$⊢ G : ℝ ⟶ ℝ \to G = (t \in ℝ ⟼ G (t))$
26		absf	$⊢ abs : ℂ ⟶ ℝ$
27	26	a1i	$⊢ G : ℝ ⟶ ℝ \to abs : ℂ ⟶ ℝ$
28	27	feqmptd	$⊢ G : ℝ ⟶ ℝ \to abs = (x \in ℂ ⟼ \|x\|)$
29		fveq2	$⊢ x = G (t) \to \|x\| = \|G (t)\|$
30	2 25 28 29	fmptco	$⊢ G : ℝ ⟶ ℝ \to abs \circ G = (t \in ℝ ⟼ \|G (t)\|)$
31	30	adantl	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to abs \circ G = (t \in ℝ ⟼ \|G (t)\|)$
32		iblmbf	$⊢ G \in 𝐿^{1} \to G \in MblFn$
33		ftc1anclem1	$⊢ (G : ℝ ⟶ ℝ \land G \in MblFn) \to abs \circ G \in MblFn$
34	32 33	sylan2	$⊢ (G : ℝ ⟶ ℝ \land G \in 𝐿^{1}) \to abs \circ G \in MblFn$
35	34	ancoms	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to abs \circ G \in MblFn$
36	31 35	eqeltrrd	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t)\|) \in MblFn$
37	36	3adant1	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t)\|) \in MblFn$
38	2	abscld	$⊢ (G : ℝ ⟶ ℝ \land t \in ℝ) \to \|G (t)\| \in ℝ$
39	2	absge0d	$⊢ (G : ℝ ⟶ ℝ \land t \in ℝ) \to 0 \leq \|G (t)\|$
40		elrege0	$⊢ \|G (t)\| \in [0, +∞) \leftrightarrow (\|G (t)\| \in ℝ \land 0 \leq \|G (t)\|)$
41	38 39 40	sylanbrc	$⊢ (G : ℝ ⟶ ℝ \land t \in ℝ) \to \|G (t)\| \in [0, +∞)$
42	41	fmpttd	$⊢ G : ℝ ⟶ ℝ \to (t \in ℝ ⟼ \|G (t)\|) : ℝ ⟶ [0, +∞)$
43	42	3ad2ant3	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t)\|) : ℝ ⟶ [0, +∞)$
44		iftrue	$⊢ t \in ℝ \to if (t \in ℝ, \|G (t)\|, 0) = \|G (t)\|$
45	44	mpteq2ia	$⊢ (t \in ℝ ⟼ if (t \in ℝ, \|G (t)\|, 0)) = (t \in ℝ ⟼ \|G (t)\|)$
46	45	fveq2i	$⊢ \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|G (t)\|, 0))) = \int^{2} ((t \in ℝ ⟼ \|G (t)\|))$
47	1	adantll	$⊢ ((G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to G (t) \in ℝ$
48		simpr	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to G : ℝ ⟶ ℝ$
49	48	feqmptd	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to G = (t \in ℝ ⟼ G (t))$
50		simpl	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to G \in 𝐿^{1}$
51	49 50	eqeltrrd	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ G (t)) \in 𝐿^{1}$
52	47 51 36	iblabsnc	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t)\|) \in 𝐿^{1}$
53	38	adantll	$⊢ ((G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|G (t)\| \in ℝ$
54	39	adantll	$⊢ ((G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to 0 \leq \|G (t)\|$
55	53 54	iblpos	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to ((t \in ℝ ⟼ \|G (t)\|) \in 𝐿^{1} \leftrightarrow ((t \in ℝ ⟼ \|G (t)\|) \in MblFn \land \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|G (t)\|, 0))) \in ℝ))$
56	52 55	mpbid	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to ((t \in ℝ ⟼ \|G (t)\|) \in MblFn \land \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|G (t)\|, 0))) \in ℝ)$
57	56	simprd	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|G (t)\|, 0))) \in ℝ$
58	46 57	eqeltrrid	$⊢ (G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|G (t)\|)) \in ℝ$
59	58	3adant1	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|G (t)\|)) \in ℝ$
60	5	abscld	$⊢ (F \in dom \int^{1} \land t \in ℝ) \to \|F (t)\| \in ℝ$
61	5	absge0d	$⊢ (F \in dom \int^{1} \land t \in ℝ) \to 0 \leq \|F (t)\|$
62		elrege0	$⊢ \|F (t)\| \in [0, +∞) \leftrightarrow (\|F (t)\| \in ℝ \land 0 \leq \|F (t)\|)$
63	60 61 62	sylanbrc	$⊢ (F \in dom \int^{1} \land t \in ℝ) \to \|F (t)\| \in [0, +∞)$
64	63	fmpttd	$⊢ F \in dom \int^{1} \to (t \in ℝ ⟼ \|F (t)\|) : ℝ ⟶ [0, +∞)$
65	64	3ad2ant1	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|F (t)\|) : ℝ ⟶ [0, +∞)$
66		iftrue	$⊢ t \in ℝ \to if (t \in ℝ, \|F (t)\|, 0) = \|F (t)\|$
67	66	mpteq2ia	$⊢ (t \in ℝ ⟼ if (t \in ℝ, \|F (t)\|, 0)) = (t \in ℝ ⟼ \|F (t)\|)$
68	67	fveq2i	$⊢ \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|F (t)\|, 0))) = \int^{2} ((t \in ℝ ⟼ \|F (t)\|))$
69	3	feqmptd	$⊢ F \in dom \int^{1} \to F = (t \in ℝ ⟼ F (t))$
70		i1fibl	$⊢ F \in dom \int^{1} \to F \in 𝐿^{1}$
71	69 70	eqeltrrd	$⊢ F \in dom \int^{1} \to (t \in ℝ ⟼ F (t)) \in 𝐿^{1}$
72	26	a1i	$⊢ F \in dom \int^{1} \to abs : ℂ ⟶ ℝ$
73	72	feqmptd	$⊢ F \in dom \int^{1} \to abs = (x \in ℂ ⟼ \|x\|)$
74		fveq2	$⊢ x = F (t) \to \|x\| = \|F (t)\|$
75	5 69 73 74	fmptco	$⊢ F \in dom \int^{1} \to abs \circ F = (t \in ℝ ⟼ \|F (t)\|)$
76		i1fmbf	$⊢ F \in dom \int^{1} \to F \in MblFn$
77		ftc1anclem1	$⊢ (F : ℝ ⟶ ℝ \land F \in MblFn) \to abs \circ F \in MblFn$
78	3 76 77	syl2anc	$⊢ F \in dom \int^{1} \to abs \circ F \in MblFn$
79	75 78	eqeltrrd	$⊢ F \in dom \int^{1} \to (t \in ℝ ⟼ \|F (t)\|) \in MblFn$
80	4 71 79	iblabsnc	$⊢ F \in dom \int^{1} \to (t \in ℝ ⟼ \|F (t)\|) \in 𝐿^{1}$
81	60 61	iblpos	$⊢ F \in dom \int^{1} \to ((t \in ℝ ⟼ \|F (t)\|) \in 𝐿^{1} \leftrightarrow ((t \in ℝ ⟼ \|F (t)\|) \in MblFn \land \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|F (t)\|, 0))) \in ℝ))$
82	80 81	mpbid	$⊢ F \in dom \int^{1} \to ((t \in ℝ ⟼ \|F (t)\|) \in MblFn \land \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|F (t)\|, 0))) \in ℝ)$
83	82	simprd	$⊢ F \in dom \int^{1} \to \int^{2} ((t \in ℝ ⟼ if (t \in ℝ, \|F (t)\|, 0))) \in ℝ$
84	68 83	eqeltrrid	$⊢ F \in dom \int^{1} \to \int^{2} ((t \in ℝ ⟼ \|F (t)\|)) \in ℝ$
85	84	3ad2ant1	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|F (t)\|)) \in ℝ$
86	37 43 59 65 85	itg2addnc	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|G (t)\|) +_{f} (t \in ℝ ⟼ \|F (t)\|)) = \int^{2} ((t \in ℝ ⟼ \|G (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|F (t)\|))$
87	23 86	eqtr3d	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|G (t)\| + \|F (t)\|)) = \int^{2} ((t \in ℝ ⟼ \|G (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|F (t)\|))$
88	59 85	readdcld	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|G (t)\|)) + \int^{2} ((t \in ℝ ⟼ \|F (t)\|)) \in ℝ$
89	87 88	eqeltrd	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|G (t)\| + \|F (t)\|)) \in ℝ$
90		readdcl	$⊢ (\|G (t)\| \in ℝ \land \|F (t)\| \in ℝ) \to \|G (t)\| + \|F (t)\| \in ℝ$
91	38 60 90	syl2anr	$⊢ ((F \in dom \int^{1} \land t \in ℝ) \land (G : ℝ ⟶ ℝ \land t \in ℝ)) \to \|G (t)\| + \|F (t)\| \in ℝ$
92	91	anandirs	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|G (t)\| + \|F (t)\| \in ℝ$
93	92	rexrd	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|G (t)\| + \|F (t)\| \in ℝ^{*}$
94	38	adantll	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|G (t)\| \in ℝ$
95	60	adantlr	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|F (t)\| \in ℝ$
96	39	adantll	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to 0 \leq \|G (t)\|$
97	61	adantlr	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to 0 \leq \|F (t)\|$
98	94 95 96 97	addge0d	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to 0 \leq \|G (t)\| + \|F (t)\|$
99		elxrge0	$⊢ \|G (t)\| + \|F (t)\| \in [0, +∞] \leftrightarrow (\|G (t)\| + \|F (t)\| \in ℝ^{*} \land 0 \leq \|G (t)\| + \|F (t)\|)$
100	93 98 99	sylanbrc	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|G (t)\| + \|F (t)\| \in [0, +∞]$
101	100	fmpttd	$⊢ (F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t)\| + \|F (t)\|) : ℝ ⟶ [0, +∞]$
102	101	3adant2	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t)\| + \|F (t)\|) : ℝ ⟶ [0, +∞]$
103		abs2dif2	$⊢ (G (t) \in ℂ \land F (t) \in ℂ) \to \|G (t) - F (t)\| \leq \|G (t)\| + \|F (t)\|$
104	2 5 103	syl2anr	$⊢ ((F \in dom \int^{1} \land t \in ℝ) \land (G : ℝ ⟶ ℝ \land t \in ℝ)) \to \|G (t) - F (t)\| \leq \|G (t)\| + \|F (t)\|$
105	104	anandirs	$⊢ ((F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \land t \in ℝ) \to \|G (t) - F (t)\| \leq \|G (t)\| + \|F (t)\|$
106	105	ralrimiva	$⊢ (F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \to \forall t \in ℝ \|G (t) - F (t)\| \leq \|G (t)\| + \|F (t)\|$
107	16	a1i	$⊢ (F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \to ℝ \in V$
108		eqidd	$⊢ (F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t) - F (t)\|) = (t \in ℝ ⟼ \|G (t) - F (t)\|)$
109		eqidd	$⊢ (F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t)\| + \|F (t)\|) = (t \in ℝ ⟼ \|G (t)\| + \|F (t)\|)$
110	107 9 92 108 109	ofrfval2	$⊢ (F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \to ((t \in ℝ ⟼ \|G (t) - F (t)\|) \leq_{f} (t \in ℝ ⟼ \|G (t)\| + \|F (t)\|) \leftrightarrow \forall t \in ℝ \|G (t) - F (t)\| \leq \|G (t)\| + \|F (t)\|)$
111	106 110	mpbird	$⊢ (F \in dom \int^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t) - F (t)\|) \leq_{f} (t \in ℝ ⟼ \|G (t)\| + \|F (t)\|)$
112	111	3adant2	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to (t \in ℝ ⟼ \|G (t) - F (t)\|) \leq_{f} (t \in ℝ ⟼ \|G (t)\| + \|F (t)\|)$
113		itg2le	$⊢ ((t \in ℝ ⟼ \|G (t) - F (t)\|) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ \|G (t)\| + \|F (t)\|) : ℝ ⟶ [0, +∞] \land (t \in ℝ ⟼ \|G (t) - F (t)\|) \leq_{f} (t \in ℝ ⟼ \|G (t)\| + \|F (t)\|)) \to \int^{2} ((t \in ℝ ⟼ \|G (t) - F (t)\|)) \leq \int^{2} ((t \in ℝ ⟼ \|G (t)\| + \|F (t)\|))$
114	15 102 112 113	syl3anc	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|G (t) - F (t)\|)) \leq \int^{2} ((t \in ℝ ⟼ \|G (t)\| + \|F (t)\|))$
115		itg2lecl	$⊢ ((t \in ℝ ⟼ \|G (t) - F (t)\|) : ℝ ⟶ [0, +∞] \land \int^{2} ((t \in ℝ ⟼ \|G (t)\| + \|F (t)\|)) \in ℝ \land \int^{2} ((t \in ℝ ⟼ \|G (t) - F (t)\|)) \leq \int^{2} ((t \in ℝ ⟼ \|G (t)\| + \|F (t)\|))) \to \int^{2} ((t \in ℝ ⟼ \|G (t) - F (t)\|)) \in ℝ$
116	15 89 114 115	syl3anc	$⊢ (F \in dom \int^{1} \land G \in 𝐿^{1} \land G : ℝ ⟶ ℝ) \to \int^{2} ((t \in ℝ ⟼ \|G (t) - F (t)\|)) \in ℝ$

Metamath Proof Explorer

Theorem ftc1anclem4

Proof