itg2monolem1

Description: Lemma for itg2mono . We show that for any constant t less than one, t x. S.1 H is less than S , and so S.1 H <_ S , which is one half of the equality in itg2mono . Consider the sequence A ( n ) = { x | t x. H <_ F ( n ) } . This is an increasing sequence of measurable sets whose union is RR , and so ` H |`A ( n ) has an integral which equals S.1 H in the limit, by itg1climres . Then by taking the limit in ` ( t x. H ) |`A ( n ) <_ F ( n ) , we get t x. S.1 H <_ S as desired. (Contributed by Mario Carneiro, 16-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	itg2mono.1	$⊢ G = (x \in ℝ ⟼ sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <))$
	itg2mono.2	$⊢ (φ \land n \in ℕ) \to F (n) \in MblFn$
	itg2mono.3	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞)$
	itg2mono.4	$⊢ (φ \land n \in ℕ) \to F (n) \leq_{f} F (n + 1)$
	itg2mono.5	$⊢ (φ \land x \in ℝ) \to \exists y \in ℝ \forall n \in ℕ F (n) (x) \leq y$
	itg2mono.6	$⊢ S = sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <)$
	itg2mono.7	$⊢ φ \to T \in (0, 1)$
	itg2mono.8	$⊢ φ \to H \in dom \int^{1}$
	itg2mono.9	$⊢ φ \to H \leq_{f} G$
	itg2mono.10	$⊢ φ \to S \in ℝ$
	itg2mono.11	$⊢ A = (n \in ℕ ⟼ \{x \in ℝ \| T H (x) \leq F (n) (x)\})$
Assertion	itg2monolem1	$⊢ φ \to T \int^{1} (H) \leq S$

Proof

Step	Hyp	Ref	Expression
1		itg2mono.1	$⊢ G = (x \in ℝ ⟼ sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <))$
2		itg2mono.2	$⊢ (φ \land n \in ℕ) \to F (n) \in MblFn$
3		itg2mono.3	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞)$
4		itg2mono.4	$⊢ (φ \land n \in ℕ) \to F (n) \leq_{f} F (n + 1)$
5		itg2mono.5	$⊢ (φ \land x \in ℝ) \to \exists y \in ℝ \forall n \in ℕ F (n) (x) \leq y$
6		itg2mono.6	$⊢ S = sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <)$
7		itg2mono.7	$⊢ φ \to T \in (0, 1)$
8		itg2mono.8	$⊢ φ \to H \in dom \int^{1}$
9		itg2mono.9	$⊢ φ \to H \leq_{f} G$
10		itg2mono.10	$⊢ φ \to S \in ℝ$
11		itg2mono.11	$⊢ A = (n \in ℕ ⟼ \{x \in ℝ \| T H (x) \leq F (n) (x)\})$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13		1zzd	$⊢ φ \to 1 \in ℤ$
14		simpr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to x \in ℝ$
15		readdcl	$⊢ (x \in ℝ \land y \in ℝ) \to x + y \in ℝ$
16	15	adantl	$⊢ ((φ \land n \in ℕ) \land (x \in ℝ \land y \in ℝ)) \to x + y \in ℝ$
17		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
18		fss	$⊢ (F (n) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F (n) : ℝ ⟶ ℝ$
19	3 17 18	sylancl	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ ℝ$
20		0xr	$⊢ 0 \in ℝ^{*}$
21		1xr	$⊢ 1 \in ℝ^{*}$
22		elioo2	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (T \in (0, 1) \leftrightarrow (T \in ℝ \land 0 < T \land T < 1))$
23	20 21 22	mp2an	$⊢ T \in (0, 1) \leftrightarrow (T \in ℝ \land 0 < T \land T < 1)$
24	7 23	sylib	$⊢ φ \to (T \in ℝ \land 0 < T \land T < 1)$
25	24	simp1d	$⊢ φ \to T \in ℝ$
26	25	renegcld	$⊢ φ \to - T \in ℝ$
27	8 26	i1fmulc	$⊢ φ \to (ℝ \times \{- T\}) \times_{f} H \in dom \int^{1}$
28	27	adantr	$⊢ (φ \land n \in ℕ) \to (ℝ \times \{- T\}) \times_{f} H \in dom \int^{1}$
29		i1ff	$⊢ (ℝ \times \{- T\}) \times_{f} H \in dom \int^{1} \to ((ℝ \times \{- T\}) \times_{f} H) : ℝ ⟶ ℝ$
30	28 29	syl	$⊢ (φ \land n \in ℕ) \to ((ℝ \times \{- T\}) \times_{f} H) : ℝ ⟶ ℝ$
31		reex	$⊢ ℝ \in V$
32	31	a1i	$⊢ (φ \land n \in ℕ) \to ℝ \in V$
33		inidm	$⊢ ℝ \cap ℝ = ℝ$
34	16 19 30 32 32 33	off	$⊢ (φ \land n \in ℕ) \to (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) : ℝ ⟶ ℝ$
35	34	adantr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) : ℝ ⟶ ℝ$
36	35	ffnd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) Fn ℝ$
37		elpreima	$⊢ (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) Fn ℝ \to (x \in {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \leftrightarrow (x \in ℝ \land (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) \in (−∞, 0)))$
38	36 37	syl	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (x \in {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \leftrightarrow (x \in ℝ \land (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) \in (−∞, 0)))$
39	14 38	mpbirand	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (x \in {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \leftrightarrow (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) \in (−∞, 0))$
40		elioomnf	$⊢ 0 \in ℝ^{*} \to ((F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) \in (−∞, 0) \leftrightarrow ((F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) \in ℝ \land (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) < 0))$
41	20 40	ax-mp	$⊢ (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) \in (−∞, 0) \leftrightarrow ((F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) \in ℝ \land (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) < 0)$
42	34	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) \in ℝ$
43	42	biantrurd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to ((F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) < 0 \leftrightarrow ((F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) \in ℝ \land (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) < 0))$
44	41 43	bitr4id	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to ((F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) \in (−∞, 0) \leftrightarrow (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) < 0)$
45	3	ffnd	$⊢ (φ \land n \in ℕ) \to F (n) Fn ℝ$
46	30	ffnd	$⊢ (φ \land n \in ℕ) \to ((ℝ \times \{- T\}) \times_{f} H) Fn ℝ$
47		eqidd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (n) (x) = F (n) (x)$
48	26	adantr	$⊢ (φ \land n \in ℕ) \to - T \in ℝ$
49		i1ff	$⊢ H \in dom \int^{1} \to H : ℝ ⟶ ℝ$
50	8 49	syl	$⊢ φ \to H : ℝ ⟶ ℝ$
51	50	ffnd	$⊢ φ \to H Fn ℝ$
52	51	adantr	$⊢ (φ \land n \in ℕ) \to H Fn ℝ$
53		eqidd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to H (x) = H (x)$
54	32 48 52 53	ofc1	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to ((ℝ \times \{- T\}) \times_{f} H) (x) = (- T) H (x)$
55	25	recnd	$⊢ φ \to T \in ℂ$
56	55	ad2antrr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to T \in ℂ$
57	50	ffvelrnda	$⊢ (φ \land x \in ℝ) \to H (x) \in ℝ$
58	57	adantlr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to H (x) \in ℝ$
59	58	recnd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to H (x) \in ℂ$
60	56 59	mulneg1d	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (- T) H (x) = - T H (x)$
61	54 60	eqtrd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to ((ℝ \times \{- T\}) \times_{f} H) (x) = - T H (x)$
62	45 46 32 32 33 47 61	ofval	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) = F (n) (x) + (- T H (x))$
63	19	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (n) (x) \in ℝ$
64	63	recnd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (n) (x) \in ℂ$
65	25	adantr	$⊢ (φ \land x \in ℝ) \to T \in ℝ$
66	65 57	remulcld	$⊢ (φ \land x \in ℝ) \to T H (x) \in ℝ$
67	66	adantlr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to T H (x) \in ℝ$
68	67	recnd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to T H (x) \in ℂ$
69	64 68	negsubd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (n) (x) + (- T H (x)) = F (n) (x) - T H (x)$
70	62 69	eqtrd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) = F (n) (x) - T H (x)$
71	70	breq1d	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to ((F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) < 0 \leftrightarrow F (n) (x) - T H (x) < 0)$
72		0red	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to 0 \in ℝ$
73	63 67 72	ltsubaddd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (F (n) (x) - T H (x) < 0 \leftrightarrow F (n) (x) < 0 + T H (x))$
74	68	addid2d	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to 0 + T H (x) = T H (x)$
75	74	breq2d	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (F (n) (x) < 0 + T H (x) \leftrightarrow F (n) (x) < T H (x))$
76	71 73 75	3bitrd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to ((F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) (x) < 0 \leftrightarrow F (n) (x) < T H (x))$
77	39 44 76	3bitrd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (x \in {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \leftrightarrow F (n) (x) < T H (x))$
78	77	notbid	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (\neg x \in {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \leftrightarrow \neg F (n) (x) < T H (x))$
79		eldif	$⊢ x \in (ℝ ∖ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)]) \leftrightarrow (x \in ℝ \land \neg x \in {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)])$
80	79	baib	$⊢ x \in ℝ \to (x \in (ℝ ∖ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)]) \leftrightarrow \neg x \in {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)])$
81	80	adantl	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (x \in (ℝ ∖ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)]) \leftrightarrow \neg x \in {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)])$
82	67 63	lenltd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (T H (x) \leq F (n) (x) \leftrightarrow \neg F (n) (x) < T H (x))$
83	78 81 82	3bitr4d	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (x \in (ℝ ∖ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)]) \leftrightarrow T H (x) \leq F (n) (x))$
84	83	rabbi2dva	$⊢ (φ \land n \in ℕ) \to ℝ \cap (ℝ ∖ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)]) = \{x \in ℝ \| T H (x) \leq F (n) (x)\}$
85		rembl	$⊢ ℝ \in dom vol$
86		i1fmbf	$⊢ (ℝ \times \{- T\}) \times_{f} H \in dom \int^{1} \to (ℝ \times \{- T\}) \times_{f} H \in MblFn$
87	28 86	syl	$⊢ (φ \land n \in ℕ) \to (ℝ \times \{- T\}) \times_{f} H \in MblFn$
88	2 87	mbfadd	$⊢ (φ \land n \in ℕ) \to F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H) \in MblFn$
89		mbfima	$⊢ (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H) \in MblFn \land (F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H)) : ℝ ⟶ ℝ) \to {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \in dom vol$
90	88 34 89	syl2anc	$⊢ (φ \land n \in ℕ) \to {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \in dom vol$
91		cmmbl	$⊢ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \in dom vol \to ℝ ∖ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \in dom vol$
92	90 91	syl	$⊢ (φ \land n \in ℕ) \to ℝ ∖ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \in dom vol$
93		inmbl	$⊢ (ℝ \in dom vol \land ℝ ∖ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)] \in dom vol) \to ℝ \cap (ℝ ∖ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)]) \in dom vol$
94	85 92 93	sylancr	$⊢ (φ \land n \in ℕ) \to ℝ \cap (ℝ ∖ {(F (n) +_{f} ((ℝ \times \{- T\}) \times_{f} H))}^{-1} [(−∞, 0)]) \in dom vol$
95	84 94	eqeltrrd	$⊢ (φ \land n \in ℕ) \to \{x \in ℝ \| T H (x) \leq F (n) (x)\} \in dom vol$
96	95 11	fmptd	$⊢ φ \to A : ℕ ⟶ dom vol$
97	4	ralrimiva	$⊢ φ \to \forall n \in ℕ F (n) \leq_{f} F (n + 1)$
98		fveq2	$⊢ n = j \to F (n) = F (j)$
99		fvoveq1	$⊢ n = j \to F (n + 1) = F (j + 1)$
100	98 99	breq12d	$⊢ n = j \to (F (n) \leq_{f} F (n + 1) \leftrightarrow F (j) \leq_{f} F (j + 1))$
101	100	cbvralvw	$⊢ \forall n \in ℕ F (n) \leq_{f} F (n + 1) \leftrightarrow \forall j \in ℕ F (j) \leq_{f} F (j + 1)$
102	97 101	sylib	$⊢ φ \to \forall j \in ℕ F (j) \leq_{f} F (j + 1)$
103	102	r19.21bi	$⊢ (φ \land j \in ℕ) \to F (j) \leq_{f} F (j + 1)$
104	3	ralrimiva	$⊢ φ \to \forall n \in ℕ F (n) : ℝ ⟶ [0, +∞)$
105	98	feq1d	$⊢ n = j \to (F (n) : ℝ ⟶ [0, +∞) \leftrightarrow F (j) : ℝ ⟶ [0, +∞))$
106	105	cbvralvw	$⊢ \forall n \in ℕ F (n) : ℝ ⟶ [0, +∞) \leftrightarrow \forall j \in ℕ F (j) : ℝ ⟶ [0, +∞)$
107	104 106	sylib	$⊢ φ \to \forall j \in ℕ F (j) : ℝ ⟶ [0, +∞)$
108	107	r19.21bi	$⊢ (φ \land j \in ℕ) \to F (j) : ℝ ⟶ [0, +∞)$
109	108	ffnd	$⊢ (φ \land j \in ℕ) \to F (j) Fn ℝ$
110		peano2nn	$⊢ j \in ℕ \to j + 1 \in ℕ$
111		fveq2	$⊢ n = j + 1 \to F (n) = F (j + 1)$
112	111	feq1d	$⊢ n = j + 1 \to (F (n) : ℝ ⟶ [0, +∞) \leftrightarrow F (j + 1) : ℝ ⟶ [0, +∞))$
113	112	rspccva	$⊢ (\forall n \in ℕ F (n) : ℝ ⟶ [0, +∞) \land j + 1 \in ℕ) \to F (j + 1) : ℝ ⟶ [0, +∞)$
114	104 110 113	syl2an	$⊢ (φ \land j \in ℕ) \to F (j + 1) : ℝ ⟶ [0, +∞)$
115	114	ffnd	$⊢ (φ \land j \in ℕ) \to F (j + 1) Fn ℝ$
116	31	a1i	$⊢ (φ \land j \in ℕ) \to ℝ \in V$
117		eqidd	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to F (j) (x) = F (j) (x)$
118		eqidd	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to F (j + 1) (x) = F (j + 1) (x)$
119	109 115 116 116 33 117 118	ofrfval	$⊢ (φ \land j \in ℕ) \to (F (j) \leq_{f} F (j + 1) \leftrightarrow \forall x \in ℝ F (j) (x) \leq F (j + 1) (x))$
120	103 119	mpbid	$⊢ (φ \land j \in ℕ) \to \forall x \in ℝ F (j) (x) \leq F (j + 1) (x)$
121	120	r19.21bi	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to F (j) (x) \leq F (j + 1) (x)$
122	25	ad2antrr	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to T \in ℝ$
123	50	adantr	$⊢ (φ \land j \in ℕ) \to H : ℝ ⟶ ℝ$
124	123	ffvelrnda	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to H (x) \in ℝ$
125	122 124	remulcld	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to T H (x) \in ℝ$
126		fss	$⊢ (F (j) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F (j) : ℝ ⟶ ℝ$
127	108 17 126	sylancl	$⊢ (φ \land j \in ℕ) \to F (j) : ℝ ⟶ ℝ$
128	127	ffvelrnda	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to F (j) (x) \in ℝ$
129		fss	$⊢ (F (j + 1) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F (j + 1) : ℝ ⟶ ℝ$
130	114 17 129	sylancl	$⊢ (φ \land j \in ℕ) \to F (j + 1) : ℝ ⟶ ℝ$
131	130	ffvelrnda	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to F (j + 1) (x) \in ℝ$
132		letr	$⊢ (T H (x) \in ℝ \land F (j) (x) \in ℝ \land F (j + 1) (x) \in ℝ) \to ((T H (x) \leq F (j) (x) \land F (j) (x) \leq F (j + 1) (x)) \to T H (x) \leq F (j + 1) (x))$
133	125 128 131 132	syl3anc	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to ((T H (x) \leq F (j) (x) \land F (j) (x) \leq F (j + 1) (x)) \to T H (x) \leq F (j + 1) (x))$
134	121 133	mpan2d	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to (T H (x) \leq F (j) (x) \to T H (x) \leq F (j + 1) (x))$
135	134	ss2rabdv	$⊢ (φ \land j \in ℕ) \to \{x \in ℝ \| T H (x) \leq F (j) (x)\} \subseteq \{x \in ℝ \| T H (x) \leq F (j + 1) (x)\}$
136	98	fveq1d	$⊢ n = j \to F (n) (x) = F (j) (x)$
137	136	breq2d	$⊢ n = j \to (T H (x) \leq F (n) (x) \leftrightarrow T H (x) \leq F (j) (x))$
138	137	rabbidv	$⊢ n = j \to \{x \in ℝ \| T H (x) \leq F (n) (x)\} = \{x \in ℝ \| T H (x) \leq F (j) (x)\}$
139	31	rabex	$⊢ \{x \in ℝ \| T H (x) \leq F (j) (x)\} \in V$
140	138 11 139	fvmpt	$⊢ j \in ℕ \to A (j) = \{x \in ℝ \| T H (x) \leq F (j) (x)\}$
141	140	adantl	$⊢ (φ \land j \in ℕ) \to A (j) = \{x \in ℝ \| T H (x) \leq F (j) (x)\}$
142	110	adantl	$⊢ (φ \land j \in ℕ) \to j + 1 \in ℕ$
143	111	fveq1d	$⊢ n = j + 1 \to F (n) (x) = F (j + 1) (x)$
144	143	breq2d	$⊢ n = j + 1 \to (T H (x) \leq F (n) (x) \leftrightarrow T H (x) \leq F (j + 1) (x))$
145	144	rabbidv	$⊢ n = j + 1 \to \{x \in ℝ \| T H (x) \leq F (n) (x)\} = \{x \in ℝ \| T H (x) \leq F (j + 1) (x)\}$
146	31	rabex	$⊢ \{x \in ℝ \| T H (x) \leq F (j + 1) (x)\} \in V$
147	145 11 146	fvmpt	$⊢ j + 1 \in ℕ \to A (j + 1) = \{x \in ℝ \| T H (x) \leq F (j + 1) (x)\}$
148	142 147	syl	$⊢ (φ \land j \in ℕ) \to A (j + 1) = \{x \in ℝ \| T H (x) \leq F (j + 1) (x)\}$
149	135 141 148	3sstr4d	$⊢ (φ \land j \in ℕ) \to A (j) \subseteq A (j + 1)$
150	66	adantrr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to T H (x) \in ℝ$
151	57	adantrr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to H (x) \in ℝ$
152	63	an32s	$⊢ ((φ \land x \in ℝ) \land n \in ℕ) \to F (n) (x) \in ℝ$
153	152	fmpttd	$⊢ (φ \land x \in ℝ) \to (n \in ℕ ⟼ F (n) (x)) : ℕ ⟶ ℝ$
154	153	frnd	$⊢ (φ \land x \in ℝ) \to ran (n \in ℕ ⟼ F (n) (x)) \subseteq ℝ$
155		1nn	$⊢ 1 \in ℕ$
156		eqid	$⊢ (n \in ℕ ⟼ F (n) (x)) = (n \in ℕ ⟼ F (n) (x))$
157	156 152	dmmptd	$⊢ (φ \land x \in ℝ) \to dom (n \in ℕ ⟼ F (n) (x)) = ℕ$
158	155 157	eleqtrrid	$⊢ (φ \land x \in ℝ) \to 1 \in dom (n \in ℕ ⟼ F (n) (x))$
159	158	ne0d	$⊢ (φ \land x \in ℝ) \to dom (n \in ℕ ⟼ F (n) (x)) \neq \emptyset$
160		dm0rn0	$⊢ dom (n \in ℕ ⟼ F (n) (x)) = \emptyset \leftrightarrow ran (n \in ℕ ⟼ F (n) (x)) = \emptyset$
161	160	necon3bii	$⊢ dom (n \in ℕ ⟼ F (n) (x)) \neq \emptyset \leftrightarrow ran (n \in ℕ ⟼ F (n) (x)) \neq \emptyset$
162	159 161	sylib	$⊢ (φ \land x \in ℝ) \to ran (n \in ℕ ⟼ F (n) (x)) \neq \emptyset$
163	153	ffnd	$⊢ (φ \land x \in ℝ) \to (n \in ℕ ⟼ F (n) (x)) Fn ℕ$
164		breq1	$⊢ z = (n \in ℕ ⟼ F (n) (x)) (m) \to (z \leq y \leftrightarrow (n \in ℕ ⟼ F (n) (x)) (m) \leq y)$
165	164	ralrn	$⊢ (n \in ℕ ⟼ F (n) (x)) Fn ℕ \to (\forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y \leftrightarrow \forall m \in ℕ (n \in ℕ ⟼ F (n) (x)) (m) \leq y)$
166	163 165	syl	$⊢ (φ \land x \in ℝ) \to (\forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y \leftrightarrow \forall m \in ℕ (n \in ℕ ⟼ F (n) (x)) (m) \leq y)$
167		fveq2	$⊢ n = m \to F (n) = F (m)$
168	167	fveq1d	$⊢ n = m \to F (n) (x) = F (m) (x)$
169		fvex	$⊢ F (m) (x) \in V$
170	168 156 169	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ F (n) (x)) (m) = F (m) (x)$
171	170	breq1d	$⊢ m \in ℕ \to ((n \in ℕ ⟼ F (n) (x)) (m) \leq y \leftrightarrow F (m) (x) \leq y)$
172	171	ralbiia	$⊢ \forall m \in ℕ (n \in ℕ ⟼ F (n) (x)) (m) \leq y \leftrightarrow \forall m \in ℕ F (m) (x) \leq y$
173	168	breq1d	$⊢ n = m \to (F (n) (x) \leq y \leftrightarrow F (m) (x) \leq y)$
174	173	cbvralvw	$⊢ \forall n \in ℕ F (n) (x) \leq y \leftrightarrow \forall m \in ℕ F (m) (x) \leq y$
175	172 174	bitr4i	$⊢ \forall m \in ℕ (n \in ℕ ⟼ F (n) (x)) (m) \leq y \leftrightarrow \forall n \in ℕ F (n) (x) \leq y$
176	166 175	bitrdi	$⊢ (φ \land x \in ℝ) \to (\forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y \leftrightarrow \forall n \in ℕ F (n) (x) \leq y)$
177	176	rexbidv	$⊢ (φ \land x \in ℝ) \to (\exists y \in ℝ \forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y \leftrightarrow \exists y \in ℝ \forall n \in ℕ F (n) (x) \leq y)$
178	5 177	mpbird	$⊢ (φ \land x \in ℝ) \to \exists y \in ℝ \forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y$
179	154 162 178	suprcld	$⊢ (φ \land x \in ℝ) \to sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \in ℝ$
180	179	adantrr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \in ℝ$
181	24	simp3d	$⊢ φ \to T < 1$
182	181	adantr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to T < 1$
183	25	adantr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to T \in ℝ$
184		1red	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to 1 \in ℝ$
185		simprr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to 0 < H (x)$
186		ltmul1	$⊢ (T \in ℝ \land 1 \in ℝ \land (H (x) \in ℝ \land 0 < H (x))) \to (T < 1 \leftrightarrow T H (x) < 1 H (x))$
187	183 184 151 185 186	syl112anc	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to (T < 1 \leftrightarrow T H (x) < 1 H (x))$
188	182 187	mpbid	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to T H (x) < 1 H (x)$
189	151	recnd	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to H (x) \in ℂ$
190	189	mulid2d	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to 1 H (x) = H (x)$
191	188 190	breqtrd	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to T H (x) < H (x)$
192	179 1	fmptd	$⊢ φ \to G : ℝ ⟶ ℝ$
193	192	ffnd	$⊢ φ \to G Fn ℝ$
194	31	a1i	$⊢ φ \to ℝ \in V$
195		eqidd	$⊢ (φ \land y \in ℝ) \to H (y) = H (y)$
196		fveq2	$⊢ x = y \to F (n) (x) = F (n) (y)$
197	196	mpteq2dv	$⊢ x = y \to (n \in ℕ ⟼ F (n) (x)) = (n \in ℕ ⟼ F (n) (y))$
198	197	rneqd	$⊢ x = y \to ran (n \in ℕ ⟼ F (n) (x)) = ran (n \in ℕ ⟼ F (n) (y))$
199	198	supeq1d	$⊢ x = y \to sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) = sup (ran (n \in ℕ ⟼ F (n) (y)) ℝ <)$
200		ltso	$⊢ < Or ℝ$
201	200	supex	$⊢ sup (ran (n \in ℕ ⟼ F (n) (y)) ℝ <) \in V$
202	199 1 201	fvmpt	$⊢ y \in ℝ \to G (y) = sup (ran (n \in ℕ ⟼ F (n) (y)) ℝ <)$
203	202	adantl	$⊢ (φ \land y \in ℝ) \to G (y) = sup (ran (n \in ℕ ⟼ F (n) (y)) ℝ <)$
204	51 193 194 194 33 195 203	ofrfval	$⊢ φ \to (H \leq_{f} G \leftrightarrow \forall y \in ℝ H (y) \leq sup (ran (n \in ℕ ⟼ F (n) (y)) ℝ <))$
205	9 204	mpbid	$⊢ φ \to \forall y \in ℝ H (y) \leq sup (ran (n \in ℕ ⟼ F (n) (y)) ℝ <)$
206		fveq2	$⊢ x = y \to H (x) = H (y)$
207	206 199	breq12d	$⊢ x = y \to (H (x) \leq sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \leftrightarrow H (y) \leq sup (ran (n \in ℕ ⟼ F (n) (y)) ℝ <))$
208	207	cbvralvw	$⊢ \forall x \in ℝ H (x) \leq sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \leftrightarrow \forall y \in ℝ H (y) \leq sup (ran (n \in ℕ ⟼ F (n) (y)) ℝ <)$
209	205 208	sylibr	$⊢ φ \to \forall x \in ℝ H (x) \leq sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <)$
210	209	r19.21bi	$⊢ (φ \land x \in ℝ) \to H (x) \leq sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <)$
211	210	adantrr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to H (x) \leq sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <)$
212	150 151 180 191 211	ltletrd	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to T H (x) < sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <)$
213	154	adantrr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to ran (n \in ℕ ⟼ F (n) (x)) \subseteq ℝ$
214	162	adantrr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to ran (n \in ℕ ⟼ F (n) (x)) \neq \emptyset$
215	178	adantrr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to \exists y \in ℝ \forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y$
216		suprlub	$⊢ ((ran (n \in ℕ ⟼ F (n) (x)) \subseteq ℝ \land ran (n \in ℕ ⟼ F (n) (x)) \neq \emptyset \land \exists y \in ℝ \forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y) \land T H (x) \in ℝ) \to (T H (x) < sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \leftrightarrow \exists w \in ran (n \in ℕ ⟼ F (n) (x)) T H (x) < w)$
217	213 214 215 150 216	syl31anc	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to (T H (x) < sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \leftrightarrow \exists w \in ran (n \in ℕ ⟼ F (n) (x)) T H (x) < w)$
218	212 217	mpbid	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to \exists w \in ran (n \in ℕ ⟼ F (n) (x)) T H (x) < w$
219	163	adantrr	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to (n \in ℕ ⟼ F (n) (x)) Fn ℕ$
220		breq2	$⊢ w = (n \in ℕ ⟼ F (n) (x)) (j) \to (T H (x) < w \leftrightarrow T H (x) < (n \in ℕ ⟼ F (n) (x)) (j))$
221	220	rexrn	$⊢ (n \in ℕ ⟼ F (n) (x)) Fn ℕ \to (\exists w \in ran (n \in ℕ ⟼ F (n) (x)) T H (x) < w \leftrightarrow \exists j \in ℕ T H (x) < (n \in ℕ ⟼ F (n) (x)) (j))$
222	219 221	syl	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to (\exists w \in ran (n \in ℕ ⟼ F (n) (x)) T H (x) < w \leftrightarrow \exists j \in ℕ T H (x) < (n \in ℕ ⟼ F (n) (x)) (j))$
223		fvex	$⊢ F (j) (x) \in V$
224	136 156 223	fvmpt	$⊢ j \in ℕ \to (n \in ℕ ⟼ F (n) (x)) (j) = F (j) (x)$
225	224	breq2d	$⊢ j \in ℕ \to (T H (x) < (n \in ℕ ⟼ F (n) (x)) (j) \leftrightarrow T H (x) < F (j) (x))$
226	225	rexbiia	$⊢ \exists j \in ℕ T H (x) < (n \in ℕ ⟼ F (n) (x)) (j) \leftrightarrow \exists j \in ℕ T H (x) < F (j) (x)$
227	222 226	bitrdi	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to (\exists w \in ran (n \in ℕ ⟼ F (n) (x)) T H (x) < w \leftrightarrow \exists j \in ℕ T H (x) < F (j) (x))$
228	218 227	mpbid	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to \exists j \in ℕ T H (x) < F (j) (x)$
229	183 151	remulcld	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to T H (x) \in ℝ$
230	108	adantlr	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to F (j) : ℝ ⟶ [0, +∞)$
231		simplr	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to x \in ℝ$
232	230 231	ffvelrnd	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to F (j) (x) \in [0, +∞)$
233		elrege0	$⊢ F (j) (x) \in [0, +∞) \leftrightarrow (F (j) (x) \in ℝ \land 0 \leq F (j) (x))$
234	232 233	sylib	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to (F (j) (x) \in ℝ \land 0 \leq F (j) (x))$
235	234	simpld	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to F (j) (x) \in ℝ$
236	235	adantlrr	$⊢ ((φ \land (x \in ℝ \land 0 < H (x))) \land j \in ℕ) \to F (j) (x) \in ℝ$
237		ltle	$⊢ (T H (x) \in ℝ \land F (j) (x) \in ℝ) \to (T H (x) < F (j) (x) \to T H (x) \leq F (j) (x))$
238	229 236 237	syl2an2r	$⊢ ((φ \land (x \in ℝ \land 0 < H (x))) \land j \in ℕ) \to (T H (x) < F (j) (x) \to T H (x) \leq F (j) (x))$
239	238	reximdva	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to (\exists j \in ℕ T H (x) < F (j) (x) \to \exists j \in ℕ T H (x) \leq F (j) (x))$
240	228 239	mpd	$⊢ (φ \land (x \in ℝ \land 0 < H (x))) \to \exists j \in ℕ T H (x) \leq F (j) (x)$
241	240	anassrs	$⊢ ((φ \land x \in ℝ) \land 0 < H (x)) \to \exists j \in ℕ T H (x) \leq F (j) (x)$
242	155	ne0ii	$⊢ ℕ \neq \emptyset$
243	66	adantrr	$⊢ (φ \land (x \in ℝ \land H (x) \leq 0)) \to T H (x) \in ℝ$
244	243	adantr	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to T H (x) \in ℝ$
245		0red	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to 0 \in ℝ$
246	234	adantlrr	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to (F (j) (x) \in ℝ \land 0 \leq F (j) (x))$
247	246	simpld	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to F (j) (x) \in ℝ$
248		simplrr	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to H (x) \leq 0$
249	57	adantrr	$⊢ (φ \land (x \in ℝ \land H (x) \leq 0)) \to H (x) \in ℝ$
250	249	adantr	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to H (x) \in ℝ$
251	25	ad2antrr	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to T \in ℝ$
252	24	simp2d	$⊢ φ \to 0 < T$
253	252	ad2antrr	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to 0 < T$
254		lemul2	$⊢ (H (x) \in ℝ \land 0 \in ℝ \land (T \in ℝ \land 0 < T)) \to (H (x) \leq 0 \leftrightarrow T H (x) \leq T \cdot 0)$
255	250 245 251 253 254	syl112anc	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to (H (x) \leq 0 \leftrightarrow T H (x) \leq T \cdot 0)$
256	248 255	mpbid	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to T H (x) \leq T \cdot 0$
257	251	recnd	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to T \in ℂ$
258	257	mul01d	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to T \cdot 0 = 0$
259	256 258	breqtrd	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to T H (x) \leq 0$
260	246	simprd	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to 0 \leq F (j) (x)$
261	244 245 247 259 260	letrd	$⊢ ((φ \land (x \in ℝ \land H (x) \leq 0)) \land j \in ℕ) \to T H (x) \leq F (j) (x)$
262	261	ralrimiva	$⊢ (φ \land (x \in ℝ \land H (x) \leq 0)) \to \forall j \in ℕ T H (x) \leq F (j) (x)$
263		r19.2z	$⊢ (ℕ \neq \emptyset \land \forall j \in ℕ T H (x) \leq F (j) (x)) \to \exists j \in ℕ T H (x) \leq F (j) (x)$
264	242 262 263	sylancr	$⊢ (φ \land (x \in ℝ \land H (x) \leq 0)) \to \exists j \in ℕ T H (x) \leq F (j) (x)$
265	264	anassrs	$⊢ ((φ \land x \in ℝ) \land H (x) \leq 0) \to \exists j \in ℕ T H (x) \leq F (j) (x)$
266		0red	$⊢ (φ \land x \in ℝ) \to 0 \in ℝ$
267	241 265 266 57	ltlecasei	$⊢ (φ \land x \in ℝ) \to \exists j \in ℕ T H (x) \leq F (j) (x)$
268	267	ralrimiva	$⊢ φ \to \forall x \in ℝ \exists j \in ℕ T H (x) \leq F (j) (x)$
269		rabid2	$⊢ ℝ = \{x \in ℝ \| \exists j \in ℕ T H (x) \leq F (j) (x)\} \leftrightarrow \forall x \in ℝ \exists j \in ℕ T H (x) \leq F (j) (x)$
270	268 269	sylibr	$⊢ φ \to ℝ = \{x \in ℝ \| \exists j \in ℕ T H (x) \leq F (j) (x)\}$
271		iunrab	$⊢ ⋃_{j \in ℕ} \{x \in ℝ \| T H (x) \leq F (j) (x)\} = \{x \in ℝ \| \exists j \in ℕ T H (x) \leq F (j) (x)\}$
272	270 271	eqtr4di	$⊢ φ \to ℝ = ⋃_{j \in ℕ} \{x \in ℝ \| T H (x) \leq F (j) (x)\}$
273	141	iuneq2dv	$⊢ φ \to ⋃_{j \in ℕ} A (j) = ⋃_{j \in ℕ} \{x \in ℝ \| T H (x) \leq F (j) (x)\}$
274	96	ffnd	$⊢ φ \to A Fn ℕ$
275		fniunfv	$⊢ A Fn ℕ \to ⋃_{j \in ℕ} A (j) = ⋃ ran A$
276	274 275	syl	$⊢ φ \to ⋃_{j \in ℕ} A (j) = ⋃ ran A$
277	272 273 276	3eqtr2rd	$⊢ φ \to ⋃ ran A = ℝ$
278		eqid	$⊢ (x \in ℝ ⟼ if (x \in A (j), H (x), 0)) = (x \in ℝ ⟼ if (x \in A (j), H (x), 0))$
279	96 149 277 8 278	itg1climres	$⊢ φ \to (j \in ℕ ⟼ \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) ⇝ \int^{1} (H)$
280		nnex	$⊢ ℕ \in V$
281	280	mptex	$⊢ (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) \in V$
282	281	a1i	$⊢ φ \to (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) \in V$
283		fveq2	$⊢ j = k \to A (j) = A (k)$
284	283	eleq2d	$⊢ j = k \to (x \in A (j) \leftrightarrow x \in A (k))$
285	284	ifbid	$⊢ j = k \to if (x \in A (j), H (x), 0) = if (x \in A (k), H (x), 0)$
286	285	mpteq2dv	$⊢ j = k \to (x \in ℝ ⟼ if (x \in A (j), H (x), 0)) = (x \in ℝ ⟼ if (x \in A (k), H (x), 0))$
287	286	fveq2d	$⊢ j = k \to \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0))) = \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0)))$
288		eqid	$⊢ (j \in ℕ ⟼ \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) = (j \in ℕ ⟼ \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0))))$
289		fvex	$⊢ \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0))) \in V$
290	287 288 289	fvmpt	$⊢ k \in ℕ \to (j \in ℕ ⟼ \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) = \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0)))$
291	290	adantl	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) = \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0)))$
292	96	ffvelrnda	$⊢ (φ \land k \in ℕ) \to A (k) \in dom vol$
293		eqid	$⊢ (x \in ℝ ⟼ if (x \in A (k), H (x), 0)) = (x \in ℝ ⟼ if (x \in A (k), H (x), 0))$
294	293	i1fres	$⊢ (H \in dom \int^{1} \land A (k) \in dom vol) \to (x \in ℝ ⟼ if (x \in A (k), H (x), 0)) \in dom \int^{1}$
295	8 292 294	syl2an2r	$⊢ (φ \land k \in ℕ) \to (x \in ℝ ⟼ if (x \in A (k), H (x), 0)) \in dom \int^{1}$
296		itg1cl	$⊢ (x \in ℝ ⟼ if (x \in A (k), H (x), 0)) \in dom \int^{1} \to \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0))) \in ℝ$
297	295 296	syl	$⊢ (φ \land k \in ℕ) \to \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0))) \in ℝ$
298	291 297	eqeltrd	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) \in ℝ$
299	298	recnd	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) \in ℂ$
300	287	oveq2d	$⊢ j = k \to T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0))) = T \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0)))$
301		eqid	$⊢ (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) = (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0))))$
302		ovex	$⊢ T \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0))) \in V$
303	300 301 302	fvmpt	$⊢ k \in ℕ \to (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) = T \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0)))$
304	290	oveq2d	$⊢ k \in ℕ \to T (j \in ℕ ⟼ \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) = T \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0)))$
305	303 304	eqtr4d	$⊢ k \in ℕ \to (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) = T (j \in ℕ ⟼ \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k)$
306	305	adantl	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) = T (j \in ℕ ⟼ \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k)$
307	12 13 279 55 282 299 306	climmulc2	$⊢ φ \to (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) ⇝ T \int^{1} (H)$
308		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
309		fss	$⊢ (F (n) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F (n) : ℝ ⟶ [0, +∞]$
310	3 308 309	sylancl	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞]$
311	10	adantr	$⊢ (φ \land n \in ℕ) \to S \in ℝ$
312		itg2cl	$⊢ F (n) : ℝ ⟶ [0, +∞] \to \int^{2} (F (n)) \in ℝ^{*}$
313	310 312	syl	$⊢ (φ \land n \in ℕ) \to \int^{2} (F (n)) \in ℝ^{*}$
314	313	fmpttd	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) : ℕ ⟶ ℝ^{*}$
315	314	frnd	$⊢ φ \to ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{*}$
316		fvex	$⊢ \int^{2} (F (n)) \in V$
317	316	elabrex	$⊢ n \in ℕ \to \int^{2} (F (n)) \in \{x \| \exists n \in ℕ x = \int^{2} (F (n))\}$
318	317	adantl	$⊢ (φ \land n \in ℕ) \to \int^{2} (F (n)) \in \{x \| \exists n \in ℕ x = \int^{2} (F (n))\}$
319		eqid	$⊢ (n \in ℕ ⟼ \int^{2} (F (n))) = (n \in ℕ ⟼ \int^{2} (F (n)))$
320	319	rnmpt	$⊢ ran (n \in ℕ ⟼ \int^{2} (F (n))) = \{x \| \exists n \in ℕ x = \int^{2} (F (n))\}$
321	318 320	eleqtrrdi	$⊢ (φ \land n \in ℕ) \to \int^{2} (F (n)) \in ran (n \in ℕ ⟼ \int^{2} (F (n)))$
322		supxrub	$⊢ (ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{} \land \int^{2} (F (n)) \in ran (n \in ℕ ⟼ \int^{2} (F (n)))) \to \int^{2} (F (n)) \leq sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{} <)$
323	315 321 322	syl2an2r	$⊢ (φ \land n \in ℕ) \to \int^{2} (F (n)) \leq sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <)$
324	323 6	breqtrrdi	$⊢ (φ \land n \in ℕ) \to \int^{2} (F (n)) \leq S$
325		itg2lecl	$⊢ (F (n) : ℝ ⟶ [0, +∞] \land S \in ℝ \land \int^{2} (F (n)) \leq S) \to \int^{2} (F (n)) \in ℝ$
326	310 311 324 325	syl3anc	$⊢ (φ \land n \in ℕ) \to \int^{2} (F (n)) \in ℝ$
327	326	fmpttd	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) : ℕ ⟶ ℝ$
328	310	ralrimiva	$⊢ φ \to \forall n \in ℕ F (n) : ℝ ⟶ [0, +∞]$
329		fveq2	$⊢ n = k \to F (n) = F (k)$
330	329	feq1d	$⊢ n = k \to (F (n) : ℝ ⟶ [0, +∞] \leftrightarrow F (k) : ℝ ⟶ [0, +∞])$
331	330	cbvralvw	$⊢ \forall n \in ℕ F (n) : ℝ ⟶ [0, +∞] \leftrightarrow \forall k \in ℕ F (k) : ℝ ⟶ [0, +∞]$
332	328 331	sylib	$⊢ φ \to \forall k \in ℕ F (k) : ℝ ⟶ [0, +∞]$
333		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
334		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
335	334	feq1d	$⊢ k = n + 1 \to (F (k) : ℝ ⟶ [0, +∞] \leftrightarrow F (n + 1) : ℝ ⟶ [0, +∞])$
336	335	rspccva	$⊢ (\forall k \in ℕ F (k) : ℝ ⟶ [0, +∞] \land n + 1 \in ℕ) \to F (n + 1) : ℝ ⟶ [0, +∞]$
337	332 333 336	syl2an	$⊢ (φ \land n \in ℕ) \to F (n + 1) : ℝ ⟶ [0, +∞]$
338		itg2le	$⊢ (F (n) : ℝ ⟶ [0, +∞] \land F (n + 1) : ℝ ⟶ [0, +∞] \land F (n) \leq_{f} F (n + 1)) \to \int^{2} (F (n)) \leq \int^{2} (F (n + 1))$
339	310 337 4 338	syl3anc	$⊢ (φ \land n \in ℕ) \to \int^{2} (F (n)) \leq \int^{2} (F (n + 1))$
340	339	ralrimiva	$⊢ φ \to \forall n \in ℕ \int^{2} (F (n)) \leq \int^{2} (F (n + 1))$
341		2fveq3	$⊢ n = k \to \int^{2} (F (n)) = \int^{2} (F (k))$
342		fvex	$⊢ \int^{2} (F (k)) \in V$
343	341 319 342	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ \int^{2} (F (n))) (k) = \int^{2} (F (k))$
344		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
345		2fveq3	$⊢ n = k + 1 \to \int^{2} (F (n)) = \int^{2} (F (k + 1))$
346		fvex	$⊢ \int^{2} (F (k + 1)) \in V$
347	345 319 346	fvmpt	$⊢ k + 1 \in ℕ \to (n \in ℕ ⟼ \int^{2} (F (n))) (k + 1) = \int^{2} (F (k + 1))$
348	344 347	syl	$⊢ k \in ℕ \to (n \in ℕ ⟼ \int^{2} (F (n))) (k + 1) = \int^{2} (F (k + 1))$
349	343 348	breq12d	$⊢ k \in ℕ \to ((n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq (n \in ℕ ⟼ \int^{2} (F (n))) (k + 1) \leftrightarrow \int^{2} (F (k)) \leq \int^{2} (F (k + 1)))$
350	349	ralbiia	$⊢ \forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq (n \in ℕ ⟼ \int^{2} (F (n))) (k + 1) \leftrightarrow \forall k \in ℕ \int^{2} (F (k)) \leq \int^{2} (F (k + 1))$
351		fvoveq1	$⊢ n = k \to F (n + 1) = F (k + 1)$
352	351	fveq2d	$⊢ n = k \to \int^{2} (F (n + 1)) = \int^{2} (F (k + 1))$
353	341 352	breq12d	$⊢ n = k \to (\int^{2} (F (n)) \leq \int^{2} (F (n + 1)) \leftrightarrow \int^{2} (F (k)) \leq \int^{2} (F (k + 1)))$
354	353	cbvralvw	$⊢ \forall n \in ℕ \int^{2} (F (n)) \leq \int^{2} (F (n + 1)) \leftrightarrow \forall k \in ℕ \int^{2} (F (k)) \leq \int^{2} (F (k + 1))$
355	350 354	bitr4i	$⊢ \forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq (n \in ℕ ⟼ \int^{2} (F (n))) (k + 1) \leftrightarrow \forall n \in ℕ \int^{2} (F (n)) \leq \int^{2} (F (n + 1))$
356	340 355	sylibr	$⊢ φ \to \forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq (n \in ℕ ⟼ \int^{2} (F (n))) (k + 1)$
357	356	r19.21bi	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq (n \in ℕ ⟼ \int^{2} (F (n))) (k + 1)$
358	324	ralrimiva	$⊢ φ \to \forall n \in ℕ \int^{2} (F (n)) \leq S$
359	343	breq1d	$⊢ k \in ℕ \to ((n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq x \leftrightarrow \int^{2} (F (k)) \leq x)$
360	359	ralbiia	$⊢ \forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq x \leftrightarrow \forall k \in ℕ \int^{2} (F (k)) \leq x$
361	341	breq1d	$⊢ n = k \to (\int^{2} (F (n)) \leq x \leftrightarrow \int^{2} (F (k)) \leq x)$
362	361	cbvralvw	$⊢ \forall n \in ℕ \int^{2} (F (n)) \leq x \leftrightarrow \forall k \in ℕ \int^{2} (F (k)) \leq x$
363	360 362	bitr4i	$⊢ \forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq x \leftrightarrow \forall n \in ℕ \int^{2} (F (n)) \leq x$
364		breq2	$⊢ x = S \to (\int^{2} (F (n)) \leq x \leftrightarrow \int^{2} (F (n)) \leq S)$
365	364	ralbidv	$⊢ x = S \to (\forall n \in ℕ \int^{2} (F (n)) \leq x \leftrightarrow \forall n \in ℕ \int^{2} (F (n)) \leq S)$
366	363 365	syl5bb	$⊢ x = S \to (\forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq x \leftrightarrow \forall n \in ℕ \int^{2} (F (n)) \leq S)$
367	366	rspcev	$⊢ (S \in ℝ \land \forall n \in ℕ \int^{2} (F (n)) \leq S) \to \exists x \in ℝ \forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq x$
368	10 358 367	syl2anc	$⊢ φ \to \exists x \in ℝ \forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq x$
369	12 13 327 357 368	climsup	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) ⇝ sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ <)$
370	327	frnd	$⊢ φ \to ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ$
371	319 313	dmmptd	$⊢ φ \to dom (n \in ℕ ⟼ \int^{2} (F (n))) = ℕ$
372	242	a1i	$⊢ φ \to ℕ \neq \emptyset$
373	371 372	eqnetrd	$⊢ φ \to dom (n \in ℕ ⟼ \int^{2} (F (n))) \neq \emptyset$
374		dm0rn0	$⊢ dom (n \in ℕ ⟼ \int^{2} (F (n))) = \emptyset \leftrightarrow ran (n \in ℕ ⟼ \int^{2} (F (n))) = \emptyset$
375	374	necon3bii	$⊢ dom (n \in ℕ ⟼ \int^{2} (F (n))) \neq \emptyset \leftrightarrow ran (n \in ℕ ⟼ \int^{2} (F (n))) \neq \emptyset$
376	373 375	sylib	$⊢ φ \to ran (n \in ℕ ⟼ \int^{2} (F (n))) \neq \emptyset$
377	316 319	fnmpti	$⊢ (n \in ℕ ⟼ \int^{2} (F (n))) Fn ℕ$
378		breq1	$⊢ z = (n \in ℕ ⟼ \int^{2} (F (n))) (k) \to (z \leq x \leftrightarrow (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq x)$
379	378	ralrn	$⊢ (n \in ℕ ⟼ \int^{2} (F (n))) Fn ℕ \to (\forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq x \leftrightarrow \forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq x)$
380	377 379	mp1i	$⊢ φ \to (\forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq x \leftrightarrow \forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq x)$
381	380	rexbidv	$⊢ φ \to (\exists x \in ℝ \forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq x \leftrightarrow \exists x \in ℝ \forall k \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (k) \leq x)$
382	368 381	mpbird	$⊢ φ \to \exists x \in ℝ \forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq x$
383		supxrre	$⊢ (ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ \land ran (n \in ℕ ⟼ \int^{2} (F (n))) \neq \emptyset \land \exists x \in ℝ \forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq x) \to sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <) = sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ <)$
384	370 376 382 383	syl3anc	$⊢ φ \to sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <) = sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ <)$
385	6 384	syl5req	$⊢ φ \to sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ <) = S$
386	369 385	breqtrd	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) ⇝ S$
387	25	adantr	$⊢ (φ \land j \in ℕ) \to T \in ℝ$
388	96	ffvelrnda	$⊢ (φ \land j \in ℕ) \to A (j) \in dom vol$
389	278	i1fres	$⊢ (H \in dom \int^{1} \land A (j) \in dom vol) \to (x \in ℝ ⟼ if (x \in A (j), H (x), 0)) \in dom \int^{1}$
390	8 388 389	syl2an2r	$⊢ (φ \land j \in ℕ) \to (x \in ℝ ⟼ if (x \in A (j), H (x), 0)) \in dom \int^{1}$
391		itg1cl	$⊢ (x \in ℝ ⟼ if (x \in A (j), H (x), 0)) \in dom \int^{1} \to \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0))) \in ℝ$
392	390 391	syl	$⊢ (φ \land j \in ℕ) \to \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0))) \in ℝ$
393	387 392	remulcld	$⊢ (φ \land j \in ℕ) \to T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0))) \in ℝ$
394	393	fmpttd	$⊢ φ \to (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) : ℕ ⟶ ℝ$
395	394	ffvelrnda	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) \in ℝ$
396	327	ffvelrnda	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ \int^{2} (F (n))) (k) \in ℝ$
397	329	feq1d	$⊢ n = k \to (F (n) : ℝ ⟶ [0, +∞) \leftrightarrow F (k) : ℝ ⟶ [0, +∞))$
398	397	cbvralvw	$⊢ \forall n \in ℕ F (n) : ℝ ⟶ [0, +∞) \leftrightarrow \forall k \in ℕ F (k) : ℝ ⟶ [0, +∞)$
399	104 398	sylib	$⊢ φ \to \forall k \in ℕ F (k) : ℝ ⟶ [0, +∞)$
400	399	r19.21bi	$⊢ (φ \land k \in ℕ) \to F (k) : ℝ ⟶ [0, +∞)$
401		fss	$⊢ (F (k) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F (k) : ℝ ⟶ [0, +∞]$
402	400 308 401	sylancl	$⊢ (φ \land k \in ℕ) \to F (k) : ℝ ⟶ [0, +∞]$
403	31	a1i	$⊢ (φ \land k \in ℕ) \to ℝ \in V$
404	25	adantr	$⊢ (φ \land k \in ℕ) \to T \in ℝ$
405	404	adantr	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to T \in ℝ$
406		fvex	$⊢ H (x) \in V$
407		c0ex	$⊢ 0 \in V$
408	406 407	ifex	$⊢ if (x \in A (k), H (x), 0) \in V$
409	408	a1i	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to if (x \in A (k), H (x), 0) \in V$
410		fconstmpt	$⊢ ℝ \times \{T\} = (x \in ℝ ⟼ T)$
411	410	a1i	$⊢ (φ \land k \in ℕ) \to ℝ \times \{T\} = (x \in ℝ ⟼ T)$
412		eqidd	$⊢ (φ \land k \in ℕ) \to (x \in ℝ ⟼ if (x \in A (k), H (x), 0)) = (x \in ℝ ⟼ if (x \in A (k), H (x), 0))$
413	403 405 409 411 412	offval2	$⊢ (φ \land k \in ℕ) \to (ℝ \times \{T\}) \times_{f} (x \in ℝ ⟼ if (x \in A (k), H (x), 0)) = (x \in ℝ ⟼ T if (x \in A (k), H (x), 0))$
414		ovif2	$⊢ T if (x \in A (k), H (x), 0) = if (x \in A (k), T H (x), T \cdot 0)$
415	55	adantr	$⊢ (φ \land k \in ℕ) \to T \in ℂ$
416	415	mul01d	$⊢ (φ \land k \in ℕ) \to T \cdot 0 = 0$
417	416	ifeq2d	$⊢ (φ \land k \in ℕ) \to if (x \in A (k), T H (x), T \cdot 0) = if (x \in A (k), T H (x), 0)$
418	414 417	syl5eq	$⊢ (φ \land k \in ℕ) \to T if (x \in A (k), H (x), 0) = if (x \in A (k), T H (x), 0)$
419	418	mpteq2dv	$⊢ (φ \land k \in ℕ) \to (x \in ℝ ⟼ T if (x \in A (k), H (x), 0)) = (x \in ℝ ⟼ if (x \in A (k), T H (x), 0))$
420	413 419	eqtrd	$⊢ (φ \land k \in ℕ) \to (ℝ \times \{T\}) \times_{f} (x \in ℝ ⟼ if (x \in A (k), H (x), 0)) = (x \in ℝ ⟼ if (x \in A (k), T H (x), 0))$
421	295 404	i1fmulc	$⊢ (φ \land k \in ℕ) \to (ℝ \times \{T\}) \times_{f} (x \in ℝ ⟼ if (x \in A (k), H (x), 0)) \in dom \int^{1}$
422	420 421	eqeltrrd	$⊢ (φ \land k \in ℕ) \to (x \in ℝ ⟼ if (x \in A (k), T H (x), 0)) \in dom \int^{1}$
423		iftrue	$⊢ x \in A (k) \to if (x \in A (k), T H (x), 0) = T H (x)$
424	423	adantl	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x \in A (k)) \to if (x \in A (k), T H (x), 0) = T H (x)$
425	329	fveq1d	$⊢ n = k \to F (n) (x) = F (k) (x)$
426	425	breq2d	$⊢ n = k \to (T H (x) \leq F (n) (x) \leftrightarrow T H (x) \leq F (k) (x))$
427	426	rabbidv	$⊢ n = k \to \{x \in ℝ \| T H (x) \leq F (n) (x)\} = \{x \in ℝ \| T H (x) \leq F (k) (x)\}$
428	31	rabex	$⊢ \{x \in ℝ \| T H (x) \leq F (k) (x)\} \in V$
429	427 11 428	fvmpt	$⊢ k \in ℕ \to A (k) = \{x \in ℝ \| T H (x) \leq F (k) (x)\}$
430	429	ad2antlr	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to A (k) = \{x \in ℝ \| T H (x) \leq F (k) (x)\}$
431	430	eleq2d	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to (x \in A (k) \leftrightarrow x \in \{x \in ℝ \| T H (x) \leq F (k) (x)\})$
432	431	biimpa	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x \in A (k)) \to x \in \{x \in ℝ \| T H (x) \leq F (k) (x)\}$
433		rabid	$⊢ x \in \{x \in ℝ \| T H (x) \leq F (k) (x)\} \leftrightarrow (x \in ℝ \land T H (x) \leq F (k) (x))$
434	433	simprbi	$⊢ x \in \{x \in ℝ \| T H (x) \leq F (k) (x)\} \to T H (x) \leq F (k) (x)$
435	432 434	syl	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x \in A (k)) \to T H (x) \leq F (k) (x)$
436	424 435	eqbrtrd	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x \in A (k)) \to if (x \in A (k), T H (x), 0) \leq F (k) (x)$
437		iffalse	$⊢ \neg x \in A (k) \to if (x \in A (k), T H (x), 0) = 0$
438	437	adantl	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land \neg x \in A (k)) \to if (x \in A (k), T H (x), 0) = 0$
439	400	ffvelrnda	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to F (k) (x) \in [0, +∞)$
440		elrege0	$⊢ F (k) (x) \in [0, +∞) \leftrightarrow (F (k) (x) \in ℝ \land 0 \leq F (k) (x))$
441	440	simprbi	$⊢ F (k) (x) \in [0, +∞) \to 0 \leq F (k) (x)$
442	439 441	syl	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to 0 \leq F (k) (x)$
443	442	adantr	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land \neg x \in A (k)) \to 0 \leq F (k) (x)$
444	438 443	eqbrtrd	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land \neg x \in A (k)) \to if (x \in A (k), T H (x), 0) \leq F (k) (x)$
445	436 444	pm2.61dan	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to if (x \in A (k), T H (x), 0) \leq F (k) (x)$
446	445	ralrimiva	$⊢ (φ \land k \in ℕ) \to \forall x \in ℝ if (x \in A (k), T H (x), 0) \leq F (k) (x)$
447		ovex	$⊢ T H (x) \in V$
448	447 407	ifex	$⊢ if (x \in A (k), T H (x), 0) \in V$
449	448	a1i	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to if (x \in A (k), T H (x), 0) \in V$
450		fvexd	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to F (k) (x) \in V$
451		eqidd	$⊢ (φ \land k \in ℕ) \to (x \in ℝ ⟼ if (x \in A (k), T H (x), 0)) = (x \in ℝ ⟼ if (x \in A (k), T H (x), 0))$
452	400	feqmptd	$⊢ (φ \land k \in ℕ) \to F (k) = (x \in ℝ ⟼ F (k) (x))$
453	403 449 450 451 452	ofrfval2	$⊢ (φ \land k \in ℕ) \to ((x \in ℝ ⟼ if (x \in A (k), T H (x), 0)) \leq_{f} F (k) \leftrightarrow \forall x \in ℝ if (x \in A (k), T H (x), 0) \leq F (k) (x))$
454	446 453	mpbird	$⊢ (φ \land k \in ℕ) \to (x \in ℝ ⟼ if (x \in A (k), T H (x), 0)) \leq_{f} F (k)$
455		itg2ub	$⊢ (F (k) : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in A (k), T H (x), 0)) \in dom \int^{1} \land (x \in ℝ ⟼ if (x \in A (k), T H (x), 0)) \leq_{f} F (k)) \to \int^{1} ((x \in ℝ ⟼ if (x \in A (k), T H (x), 0))) \leq \int^{2} (F (k))$
456	402 422 454 455	syl3anc	$⊢ (φ \land k \in ℕ) \to \int^{1} ((x \in ℝ ⟼ if (x \in A (k), T H (x), 0))) \leq \int^{2} (F (k))$
457	303	adantl	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) = T \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0)))$
458	295 404	itg1mulc	$⊢ (φ \land k \in ℕ) \to \int^{1} ((ℝ \times \{T\}) \times_{f} (x \in ℝ ⟼ if (x \in A (k), H (x), 0))) = T \int^{1} ((x \in ℝ ⟼ if (x \in A (k), H (x), 0)))$
459	420	fveq2d	$⊢ (φ \land k \in ℕ) \to \int^{1} ((ℝ \times \{T\}) \times_{f} (x \in ℝ ⟼ if (x \in A (k), H (x), 0))) = \int^{1} ((x \in ℝ ⟼ if (x \in A (k), T H (x), 0)))$
460	457 458 459	3eqtr2d	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) = \int^{1} ((x \in ℝ ⟼ if (x \in A (k), T H (x), 0)))$
461	343	adantl	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ \int^{2} (F (n))) (k) = \int^{2} (F (k))$
462	456 460 461	3brtr4d	$⊢ (φ \land k \in ℕ) \to (j \in ℕ ⟼ T \int^{1} ((x \in ℝ ⟼ if (x \in A (j), H (x), 0)))) (k) \leq (n \in ℕ ⟼ \int^{2} (F (n))) (k)$
463	12 13 307 386 395 396 462	climle	$⊢ φ \to T \int^{1} (H) \leq S$

Metamath Proof Explorer

Theorem itg2monolem1

Proof