itg2gt0

Description: If the function F is strictly positive on a set of positive measure, then the integral of the function is positive. (Contributed by Mario Carneiro, 30-Aug-2014)

	Ref	Expression
Hypotheses	itg2gt0.1	$⊢ φ \to A \in dom vol$
	itg2gt0.2	$⊢ φ \to 0 < vol (A)$
	itg2gt0.3	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	itg2gt0.4	$⊢ φ \to F \in MblFn$
	itg2gt0.5	$⊢ (φ \land x \in A) \to 0 < F (x)$
Assertion	itg2gt0	$⊢ φ \to 0 < \int^{2} (F)$

Proof

Step	Hyp	Ref	Expression
1		itg2gt0.1	$⊢ φ \to A \in dom vol$
2		itg2gt0.2	$⊢ φ \to 0 < vol (A)$
3		itg2gt0.3	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
4		itg2gt0.4	$⊢ φ \to F \in MblFn$
5		itg2gt0.5	$⊢ (φ \land x \in A) \to 0 < F (x)$
6		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
7		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
8	7	ffvelcdmi	$⊢ A \in dom vol \to vol (A) \in [0, +∞]$
9	6 8	sselid	$⊢ A \in dom vol \to vol (A) \in ℝ^{*}$
10	1 9	syl	$⊢ φ \to vol (A) \in ℝ^{*}$
11	10	adantr	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to vol (A) \in ℝ^{*}$
12	4	elexd	$⊢ φ \to F \in V$
13		cnvexg	$⊢ F \in V \to F^{-1} \in V$
14	12 13	syl	$⊢ φ \to F^{-1} \in V$
15		imaexg	$⊢ F^{-1} \in V \to F^{-1} [(\frac{1}{n}, +∞)] \in V$
16	14 15	syl	$⊢ φ \to F^{-1} [(\frac{1}{n}, +∞)] \in V$
17	16	adantr	$⊢ (φ \land n \in ℕ) \to F^{-1} [(\frac{1}{n}, +∞)] \in V$
18	17	fmpttd	$⊢ φ \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) : ℕ ⟶ V$
19	18	ffnd	$⊢ φ \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) Fn ℕ$
20		fniunfv	$⊢ (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) Fn ℕ \to ⋃_{k \in ℕ} (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) = ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])$
21	19 20	syl	$⊢ φ \to ⋃_{k \in ℕ} (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) = ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])$
22		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
23		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F : ℝ ⟶ ℝ$
24	3 22 23	sylancl	$⊢ φ \to F : ℝ ⟶ ℝ$
25		mbfima	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ) \to F^{-1} [(\frac{1}{n}, +∞)] \in dom vol$
26	4 24 25	syl2anc	$⊢ φ \to F^{-1} [(\frac{1}{n}, +∞)] \in dom vol$
27	26	adantr	$⊢ (φ \land n \in ℕ) \to F^{-1} [(\frac{1}{n}, +∞)] \in dom vol$
28	27	fmpttd	$⊢ φ \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) : ℕ ⟶ dom vol$
29	28	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \in dom vol$
30	29	ralrimiva	$⊢ φ \to \forall k \in ℕ (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \in dom vol$
31		iunmbl	$⊢ \forall k \in ℕ (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \in dom vol \to ⋃_{k \in ℕ} (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \in dom vol$
32	30 31	syl	$⊢ φ \to ⋃_{k \in ℕ} (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \in dom vol$
33	21 32	eqeltrrd	$⊢ φ \to ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \in dom vol$
34		mblss	$⊢ ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \in dom vol \to ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \subseteq ℝ$
35	33 34	syl	$⊢ φ \to ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \subseteq ℝ$
36		ovolcl	$⊢ ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \subseteq ℝ \to {vol}^{} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])) \in ℝ^{}$
37	35 36	syl	$⊢ φ \to {vol}^{} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])) \in ℝ^{}$
38	37	adantr	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to {vol}^{} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])) \in ℝ^{}$
39		0xr	$⊢ 0 \in ℝ^{*}$
40	39	a1i	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to 0 \in ℝ^{*}$
41		mblvol	$⊢ A \in dom vol \to vol (A) = {vol}^{*} (A)$
42	1 41	syl	$⊢ φ \to vol (A) = {vol}^{*} (A)$
43		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
44	1 43	syl	$⊢ φ \to A \subseteq ℝ$
45	44	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
46	3	ffvelcdmda	$⊢ (φ \land x \in ℝ) \to F (x) \in [0, +∞)$
47		elrege0	$⊢ F (x) \in [0, +∞) \leftrightarrow (F (x) \in ℝ \land 0 \leq F (x))$
48	46 47	sylib	$⊢ (φ \land x \in ℝ) \to (F (x) \in ℝ \land 0 \leq F (x))$
49	48	simpld	$⊢ (φ \land x \in ℝ) \to F (x) \in ℝ$
50	45 49	syldan	$⊢ (φ \land x \in A) \to F (x) \in ℝ$
51		nnrecl	$⊢ (F (x) \in ℝ \land 0 < F (x)) \to \exists k \in ℕ \frac{1}{k} < F (x)$
52	50 5 51	syl2anc	$⊢ (φ \land x \in A) \to \exists k \in ℕ \frac{1}{k} < F (x)$
53	3	ffnd	$⊢ φ \to F Fn ℝ$
54	53	ad2antrr	$⊢ ((φ \land x \in A) \land k \in ℕ) \to F Fn ℝ$
55		elpreima	$⊢ F Fn ℝ \to (x \in F^{-1} [(\frac{1}{k}, +∞)] \leftrightarrow (x \in ℝ \land F (x) \in (\frac{1}{k}, +∞)))$
56	54 55	syl	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (x \in F^{-1} [(\frac{1}{k}, +∞)] \leftrightarrow (x \in ℝ \land F (x) \in (\frac{1}{k}, +∞)))$
57	45	adantr	$⊢ ((φ \land x \in A) \land k \in ℕ) \to x \in ℝ$
58	57	biantrurd	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (F (x) \in (\frac{1}{k}, +∞) \leftrightarrow (x \in ℝ \land F (x) \in (\frac{1}{k}, +∞)))$
59		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
60	59	adantl	$⊢ (φ \land k \in ℕ) \to \frac{1}{k} \in ℝ$
61	60	rexrd	$⊢ (φ \land k \in ℕ) \to \frac{1}{k} \in ℝ^{*}$
62	61	adantlr	$⊢ ((φ \land x \in A) \land k \in ℕ) \to \frac{1}{k} \in ℝ^{*}$
63		elioopnf	$⊢ \frac{1}{k} \in ℝ^{*} \to (F (x) \in (\frac{1}{k}, +∞) \leftrightarrow (F (x) \in ℝ \land \frac{1}{k} < F (x)))$
64	62 63	syl	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (F (x) \in (\frac{1}{k}, +∞) \leftrightarrow (F (x) \in ℝ \land \frac{1}{k} < F (x)))$
65	56 58 64	3bitr2d	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (x \in F^{-1} [(\frac{1}{k}, +∞)] \leftrightarrow (F (x) \in ℝ \land \frac{1}{k} < F (x)))$
66		id	$⊢ k \in ℕ \to k \in ℕ$
67		imaexg	$⊢ F^{-1} \in V \to F^{-1} [(\frac{1}{k}, +∞)] \in V$
68	14 67	syl	$⊢ φ \to F^{-1} [(\frac{1}{k}, +∞)] \in V$
69	68	adantr	$⊢ (φ \land x \in A) \to F^{-1} [(\frac{1}{k}, +∞)] \in V$
70		oveq2	$⊢ n = k \to \frac{1}{n} = \frac{1}{k}$
71	70	oveq1d	$⊢ n = k \to (\frac{1}{n}, +∞) = (\frac{1}{k}, +∞)$
72	71	imaeq2d	$⊢ n = k \to F^{-1} [(\frac{1}{n}, +∞)] = F^{-1} [(\frac{1}{k}, +∞)]$
73		eqid	$⊢ (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) = (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])$
74	72 73	fvmptg	$⊢ (k \in ℕ \land F^{-1} [(\frac{1}{k}, +∞)] \in V) \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) = F^{-1} [(\frac{1}{k}, +∞)]$
75	66 69 74	syl2anr	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) = F^{-1} [(\frac{1}{k}, +∞)]$
76	75	eleq2d	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (x \in (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \leftrightarrow x \in F^{-1} [(\frac{1}{k}, +∞)])$
77	50	adantr	$⊢ ((φ \land x \in A) \land k \in ℕ) \to F (x) \in ℝ$
78	77	biantrurd	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (\frac{1}{k} < F (x) \leftrightarrow (F (x) \in ℝ \land \frac{1}{k} < F (x)))$
79	65 76 78	3bitr4rd	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (\frac{1}{k} < F (x) \leftrightarrow x \in (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k))$
80	79	rexbidva	$⊢ (φ \land x \in A) \to (\exists k \in ℕ \frac{1}{k} < F (x) \leftrightarrow \exists k \in ℕ x \in (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k))$
81	52 80	mpbid	$⊢ (φ \land x \in A) \to \exists k \in ℕ x \in (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k)$
82	81	ex	$⊢ φ \to (x \in A \to \exists k \in ℕ x \in (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k))$
83		eluni2	$⊢ x \in ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \leftrightarrow \exists z \in ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) x \in z$
84		eleq2	$⊢ z = (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \to (x \in z \leftrightarrow x \in (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k))$
85	84	rexrn	$⊢ (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) Fn ℕ \to (\exists z \in ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) x \in z \leftrightarrow \exists k \in ℕ x \in (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k))$
86	19 85	syl	$⊢ φ \to (\exists z \in ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) x \in z \leftrightarrow \exists k \in ℕ x \in (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k))$
87	83 86	bitrid	$⊢ φ \to (x \in ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \leftrightarrow \exists k \in ℕ x \in (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k))$
88	82 87	sylibrd	$⊢ φ \to (x \in A \to x \in ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]))$
89	88	ssrdv	$⊢ φ \to A \subseteq ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])$
90		ovolss	$⊢ (A \subseteq ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \land ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \subseteq ℝ) \to {vol}^{} (A) \leq {vol}^{} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]))$
91	89 35 90	syl2anc	$⊢ φ \to {vol}^{} (A) \leq {vol}^{} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]))$
92	42 91	eqbrtrd	$⊢ φ \to vol (A) \leq {vol}^{*} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]))$
93	92	adantr	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to vol (A) \leq {vol}^{*} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]))$
94		mblvol	$⊢ ⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \in dom vol \to vol (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])) = {vol}^{*} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]))$
95	33 94	syl	$⊢ φ \to vol (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])) = {vol}^{*} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]))$
96		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
97	96	adantl	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℕ$
98		nnrecre	$⊢ k + 1 \in ℕ \to \frac{1}{k + 1} \in ℝ$
99	97 98	syl	$⊢ (φ \land k \in ℕ) \to \frac{1}{k + 1} \in ℝ$
100	99	rexrd	$⊢ (φ \land k \in ℕ) \to \frac{1}{k + 1} \in ℝ^{*}$
101		nnre	$⊢ k \in ℕ \to k \in ℝ$
102	101	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℝ$
103	102	lep1d	$⊢ (φ \land k \in ℕ) \to k \leq k + 1$
104		nngt0	$⊢ k \in ℕ \to 0 < k$
105	104	adantl	$⊢ (φ \land k \in ℕ) \to 0 < k$
106	97	nnred	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℝ$
107	97	nngt0d	$⊢ (φ \land k \in ℕ) \to 0 < k + 1$
108		lerec	$⊢ ((k \in ℝ \land 0 < k) \land (k + 1 \in ℝ \land 0 < k + 1)) \to (k \leq k + 1 \leftrightarrow \frac{1}{k + 1} \leq \frac{1}{k})$
109	102 105 106 107 108	syl22anc	$⊢ (φ \land k \in ℕ) \to (k \leq k + 1 \leftrightarrow \frac{1}{k + 1} \leq \frac{1}{k})$
110	103 109	mpbid	$⊢ (φ \land k \in ℕ) \to \frac{1}{k + 1} \leq \frac{1}{k}$
111		iooss1	$⊢ (\frac{1}{k + 1} \in ℝ^{*} \land \frac{1}{k + 1} \leq \frac{1}{k}) \to (\frac{1}{k}, +∞) \subseteq (\frac{1}{k + 1}, +∞)$
112	100 110 111	syl2anc	$⊢ (φ \land k \in ℕ) \to (\frac{1}{k}, +∞) \subseteq (\frac{1}{k + 1}, +∞)$
113		imass2	$⊢ (\frac{1}{k}, +∞) \subseteq (\frac{1}{k + 1}, +∞) \to F^{-1} [(\frac{1}{k}, +∞)] \subseteq F^{-1} [(\frac{1}{k + 1}, +∞)]$
114	112 113	syl	$⊢ (φ \land k \in ℕ) \to F^{-1} [(\frac{1}{k}, +∞)] \subseteq F^{-1} [(\frac{1}{k + 1}, +∞)]$
115	66 68 74	syl2anr	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) = F^{-1} [(\frac{1}{k}, +∞)]$
116		imaexg	$⊢ F^{-1} \in V \to F^{-1} [(\frac{1}{k + 1}, +∞)] \in V$
117	14 116	syl	$⊢ φ \to F^{-1} [(\frac{1}{k + 1}, +∞)] \in V$
118		oveq2	$⊢ n = k + 1 \to \frac{1}{n} = \frac{1}{k + 1}$
119	118	oveq1d	$⊢ n = k + 1 \to (\frac{1}{n}, +∞) = (\frac{1}{k + 1}, +∞)$
120	119	imaeq2d	$⊢ n = k + 1 \to F^{-1} [(\frac{1}{n}, +∞)] = F^{-1} [(\frac{1}{k + 1}, +∞)]$
121	120 73	fvmptg	$⊢ (k + 1 \in ℕ \land F^{-1} [(\frac{1}{k + 1}, +∞)] \in V) \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k + 1) = F^{-1} [(\frac{1}{k + 1}, +∞)]$
122	96 117 121	syl2anr	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k + 1) = F^{-1} [(\frac{1}{k + 1}, +∞)]$
123	114 115 122	3sstr4d	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \subseteq (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k + 1)$
124	123	ralrimiva	$⊢ φ \to \forall k \in ℕ (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \subseteq (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k + 1)$
125		volsup	$⊢ ((n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) : ℕ ⟶ dom vol \land \forall k \in ℕ (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \subseteq (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k + 1)) \to vol (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])) = sup (vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] ℝ^{*} <)$
126	28 124 125	syl2anc	$⊢ φ \to vol (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])) = sup (vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] ℝ^{*} <)$
127	95 126	eqtr3d	$⊢ φ \to {vol}^{} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])) = sup (vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] ℝ^{} <)$
128	127	adantr	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to {vol}^{} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])) = sup (vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] ℝ^{} <)$
129	68	adantr	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to F^{-1} [(\frac{1}{k}, +∞)] \in V$
130	66 129 74	syl2anr	$⊢ ((φ \land \neg 0 < \int^{2} (F)) \land k \in ℕ) \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) = F^{-1} [(\frac{1}{k}, +∞)]$
131	130	fveq2d	$⊢ ((φ \land \neg 0 < \int^{2} (F)) \land k \in ℕ) \to vol ((n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k)) = vol (F^{-1} [(\frac{1}{k}, +∞)])$
132	39	a1i	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to 0 \in ℝ^{*}$
133		nnrecgt0	$⊢ k \in ℕ \to 0 < \frac{1}{k}$
134	133	adantl	$⊢ (φ \land k \in ℕ) \to 0 < \frac{1}{k}$
135		0re	$⊢ 0 \in ℝ$
136		ltle	$⊢ (0 \in ℝ \land \frac{1}{k} \in ℝ) \to (0 < \frac{1}{k} \to 0 \leq \frac{1}{k})$
137	135 60 136	sylancr	$⊢ (φ \land k \in ℕ) \to (0 < \frac{1}{k} \to 0 \leq \frac{1}{k})$
138	134 137	mpd	$⊢ (φ \land k \in ℕ) \to 0 \leq \frac{1}{k}$
139		elxrge0	$⊢ \frac{1}{k} \in [0, +∞] \leftrightarrow (\frac{1}{k} \in ℝ^{*} \land 0 \leq \frac{1}{k})$
140	61 138 139	sylanbrc	$⊢ (φ \land k \in ℕ) \to \frac{1}{k} \in [0, +∞]$
141		0e0iccpnf	$⊢ 0 \in [0, +∞]$
142		ifcl	$⊢ (\frac{1}{k} \in [0, +∞] \land 0 \in [0, +∞]) \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \in [0, +∞]$
143	140 141 142	sylancl	$⊢ (φ \land k \in ℕ) \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \in [0, +∞]$
144	143	adantr	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \in [0, +∞]$
145	144	fmpttd	$⊢ (φ \land k \in ℕ) \to (x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)) : ℝ ⟶ [0, +∞]$
146	145	adantrr	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to (x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)) : ℝ ⟶ [0, +∞]$
147		itg2cl	$⊢ (x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)) : ℝ ⟶ [0, +∞] \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \in ℝ^{*}$
148	146 147	syl	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \in ℝ^{*}$
149		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
150		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F : ℝ ⟶ [0, +∞]$
151	3 149 150	sylancl	$⊢ φ \to F : ℝ ⟶ [0, +∞]$
152		itg2cl	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) \in ℝ^{*}$
153	151 152	syl	$⊢ φ \to \int^{2} (F) \in ℝ^{*}$
154	153	adantr	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to \int^{2} (F) \in ℝ^{*}$
155		0nrp	$⊢ \neg 0 \in ℝ^{+}$
156		simpr	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))$
157	115 29	eqeltrrd	$⊢ (φ \land k \in ℕ) \to F^{-1} [(\frac{1}{k}, +∞)] \in dom vol$
158	157	adantrr	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to F^{-1} [(\frac{1}{k}, +∞)] \in dom vol$
159	158	adantr	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to F^{-1} [(\frac{1}{k}, +∞)] \in dom vol$
160	156 135	eqeltrrdi	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \in ℝ$
161	60 134	elrpd	$⊢ (φ \land k \in ℕ) \to \frac{1}{k} \in ℝ^{+}$
162	161	adantrr	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to \frac{1}{k} \in ℝ^{+}$
163	162	adantr	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to \frac{1}{k} \in ℝ^{+}$
164		itg2const2	$⊢ (F^{-1} [(\frac{1}{k}, +∞)] \in dom vol \land \frac{1}{k} \in ℝ^{+}) \to (vol (F^{-1} [(\frac{1}{k}, +∞)]) \in ℝ \leftrightarrow \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \in ℝ)$
165	159 163 164	syl2anc	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to (vol (F^{-1} [(\frac{1}{k}, +∞)]) \in ℝ \leftrightarrow \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \in ℝ)$
166	160 165	mpbird	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to vol (F^{-1} [(\frac{1}{k}, +∞)]) \in ℝ$
167		elrege0	$⊢ \frac{1}{k} \in [0, +∞) \leftrightarrow (\frac{1}{k} \in ℝ \land 0 \leq \frac{1}{k})$
168	60 138 167	sylanbrc	$⊢ (φ \land k \in ℕ) \to \frac{1}{k} \in [0, +∞)$
169	168	adantrr	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to \frac{1}{k} \in [0, +∞)$
170	169	adantr	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to \frac{1}{k} \in [0, +∞)$
171		itg2const	$⊢ (F^{-1} [(\frac{1}{k}, +∞)] \in dom vol \land vol (F^{-1} [(\frac{1}{k}, +∞)]) \in ℝ \land \frac{1}{k} \in [0, +∞)) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) = (\frac{1}{k}) vol (F^{-1} [(\frac{1}{k}, +∞)])$
172	159 166 170 171	syl3anc	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) = (\frac{1}{k}) vol (F^{-1} [(\frac{1}{k}, +∞)])$
173	156 172	eqtrd	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to 0 = (\frac{1}{k}) vol (F^{-1} [(\frac{1}{k}, +∞)])$
174		simplrr	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to 0 < vol (F^{-1} [(\frac{1}{k}, +∞)])$
175	166 174	elrpd	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to vol (F^{-1} [(\frac{1}{k}, +∞)]) \in ℝ^{+}$
176	163 175	rpmulcld	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to (\frac{1}{k}) vol (F^{-1} [(\frac{1}{k}, +∞)]) \in ℝ^{+}$
177	173 176	eqeltrd	$⊢ ((φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \land 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))) \to 0 \in ℝ^{+}$
178	177	ex	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to (0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \to 0 \in ℝ^{+})$
179	155 178	mtoi	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to \neg 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))$
180		itg2ge0	$⊢ (x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)) : ℝ ⟶ [0, +∞] \to 0 \leq \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))$
181	146 180	syl	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to 0 \leq \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))$
182		xrleloe	$⊢ (0 \in ℝ^{} \land \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \in ℝ^{}) \to (0 \leq \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \leftrightarrow (0 < \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \lor 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))))$
183	39 148 182	sylancr	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to (0 \leq \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \leftrightarrow (0 < \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \lor 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))))$
184	181 183	mpbid	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to (0 < \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \lor 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))))$
185	184	ord	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to (\neg 0 < \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \to 0 = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))))$
186	179 185	mt3d	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to 0 < \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)))$
187	151	adantr	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to F : ℝ ⟶ [0, +∞]$
188	60	adantr	$⊢ ((φ \land k \in ℕ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to \frac{1}{k} \in ℝ$
189	53	adantr	$⊢ (φ \land k \in ℕ) \to F Fn ℝ$
190	189 55	syl	$⊢ (φ \land k \in ℕ) \to (x \in F^{-1} [(\frac{1}{k}, +∞)] \leftrightarrow (x \in ℝ \land F (x) \in (\frac{1}{k}, +∞)))$
191	190	biimpa	$⊢ ((φ \land k \in ℕ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to (x \in ℝ \land F (x) \in (\frac{1}{k}, +∞))$
192	191	simpld	$⊢ ((φ \land k \in ℕ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to x \in ℝ$
193	49	adantlr	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to F (x) \in ℝ$
194	192 193	syldan	$⊢ ((φ \land k \in ℕ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to F (x) \in ℝ$
195	61	adantr	$⊢ ((φ \land k \in ℕ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to \frac{1}{k} \in ℝ^{*}$
196	191	simprd	$⊢ ((φ \land k \in ℕ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to F (x) \in (\frac{1}{k}, +∞)$
197		simpr	$⊢ (F (x) \in ℝ \land \frac{1}{k} < F (x)) \to \frac{1}{k} < F (x)$
198	63 197	biimtrdi	$⊢ \frac{1}{k} \in ℝ^{*} \to (F (x) \in (\frac{1}{k}, +∞) \to \frac{1}{k} < F (x))$
199	195 196 198	sylc	$⊢ ((φ \land k \in ℕ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to \frac{1}{k} < F (x)$
200	188 194 199	ltled	$⊢ ((φ \land k \in ℕ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to \frac{1}{k} \leq F (x)$
201	48	simprd	$⊢ (φ \land x \in ℝ) \to 0 \leq F (x)$
202	201	adantlr	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to 0 \leq F (x)$
203	192 202	syldan	$⊢ ((φ \land k \in ℕ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to 0 \leq F (x)$
204		breq1	$⊢ \frac{1}{k} = if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \to (\frac{1}{k} \leq F (x) \leftrightarrow if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x))$
205		breq1	$⊢ 0 = if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \to (0 \leq F (x) \leftrightarrow if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x))$
206	204 205	ifboth	$⊢ (\frac{1}{k} \leq F (x) \land 0 \leq F (x)) \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x)$
207	200 203 206	syl2anc	$⊢ ((φ \land k \in ℕ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x)$
208	207	adantlr	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x \in F^{-1} [(\frac{1}{k}, +∞)]) \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x)$
209		iffalse	$⊢ \neg x \in F^{-1} [(\frac{1}{k}, +∞)] \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) = 0$
210	209	adantl	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land \neg x \in F^{-1} [(\frac{1}{k}, +∞)]) \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) = 0$
211	202	adantr	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land \neg x \in F^{-1} [(\frac{1}{k}, +∞)]) \to 0 \leq F (x)$
212	210 211	eqbrtrd	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land \neg x \in F^{-1} [(\frac{1}{k}, +∞)]) \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x)$
213	208 212	pm2.61dan	$⊢ ((φ \land k \in ℕ) \land x \in ℝ) \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x)$
214	213	ralrimiva	$⊢ (φ \land k \in ℕ) \to \forall x \in ℝ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x)$
215	214	adantrr	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to \forall x \in ℝ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x)$
216		reex	$⊢ ℝ \in V$
217	216	a1i	$⊢ φ \to ℝ \in V$
218		ovex	$⊢ \frac{1}{k} \in V$
219		c0ex	$⊢ 0 \in V$
220	218 219	ifex	$⊢ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \in V$
221	220	a1i	$⊢ (φ \land x \in ℝ) \to if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \in V$
222		fvexd	$⊢ (φ \land x \in ℝ) \to F (x) \in V$
223		eqidd	$⊢ φ \to (x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)) = (x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))$
224	3	feqmptd	$⊢ φ \to F = (x \in ℝ ⟼ F (x))$
225	217 221 222 223 224	ofrfval2	$⊢ φ \to ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)) \leq_{f} F \leftrightarrow \forall x \in ℝ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x))$
226	225	biimpar	$⊢ (φ \land \forall x \in ℝ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0) \leq F (x)) \to (x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)) \leq_{f} F$
227	215 226	syldan	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to (x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)) \leq_{f} F$
228		itg2le	$⊢ ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)) : ℝ ⟶ [0, +∞] \land F : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0)) \leq_{f} F) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \leq \int^{2} (F)$
229	146 187 227 228	syl3anc	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(\frac{1}{k}, +∞)], \frac{1}{k}, 0))) \leq \int^{2} (F)$
230	132 148 154 186 229	xrltletrd	$⊢ (φ \land (k \in ℕ \land 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))) \to 0 < \int^{2} (F)$
231	230	expr	$⊢ (φ \land k \in ℕ) \to (0 < vol (F^{-1} [(\frac{1}{k}, +∞)]) \to 0 < \int^{2} (F))$
232	231	con3d	$⊢ (φ \land k \in ℕ) \to (\neg 0 < \int^{2} (F) \to \neg 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))$
233	7	ffvelcdmi	$⊢ F^{-1} [(\frac{1}{k}, +∞)] \in dom vol \to vol (F^{-1} [(\frac{1}{k}, +∞)]) \in [0, +∞]$
234	6 233	sselid	$⊢ F^{-1} [(\frac{1}{k}, +∞)] \in dom vol \to vol (F^{-1} [(\frac{1}{k}, +∞)]) \in ℝ^{*}$
235	157 234	syl	$⊢ (φ \land k \in ℕ) \to vol (F^{-1} [(\frac{1}{k}, +∞)]) \in ℝ^{*}$
236		xrlenlt	$⊢ (vol (F^{-1} [(\frac{1}{k}, +∞)]) \in ℝ^{} \land 0 \in ℝ^{}) \to (vol (F^{-1} [(\frac{1}{k}, +∞)]) \leq 0 \leftrightarrow \neg 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))$
237	235 39 236	sylancl	$⊢ (φ \land k \in ℕ) \to (vol (F^{-1} [(\frac{1}{k}, +∞)]) \leq 0 \leftrightarrow \neg 0 < vol (F^{-1} [(\frac{1}{k}, +∞)]))$
238	232 237	sylibrd	$⊢ (φ \land k \in ℕ) \to (\neg 0 < \int^{2} (F) \to vol (F^{-1} [(\frac{1}{k}, +∞)]) \leq 0)$
239	238	imp	$⊢ ((φ \land k \in ℕ) \land \neg 0 < \int^{2} (F)) \to vol (F^{-1} [(\frac{1}{k}, +∞)]) \leq 0$
240	239	an32s	$⊢ ((φ \land \neg 0 < \int^{2} (F)) \land k \in ℕ) \to vol (F^{-1} [(\frac{1}{k}, +∞)]) \leq 0$
241	131 240	eqbrtrd	$⊢ ((φ \land \neg 0 < \int^{2} (F)) \land k \in ℕ) \to vol ((n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k)) \leq 0$
242	241	ralrimiva	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to \forall k \in ℕ vol ((n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k)) \leq 0$
243		ffn	$⊢ (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) : ℕ ⟶ V \to (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) Fn ℕ$
244		fveq2	$⊢ z = (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \to vol (z) = vol ((n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k))$
245	244	breq1d	$⊢ z = (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k) \to (vol (z) \leq 0 \leftrightarrow vol ((n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k)) \leq 0)$
246	245	ralrn	$⊢ (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) Fn ℕ \to (\forall z \in ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) vol (z) \leq 0 \leftrightarrow \forall k \in ℕ vol ((n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k)) \leq 0)$
247	18 243 246	3syl	$⊢ φ \to (\forall z \in ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) vol (z) \leq 0 \leftrightarrow \forall k \in ℕ vol ((n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k)) \leq 0)$
248	247	adantr	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to (\forall z \in ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) vol (z) \leq 0 \leftrightarrow \forall k \in ℕ vol ((n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) (k)) \leq 0)$
249	242 248	mpbird	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to \forall z \in ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) vol (z) \leq 0$
250		ffn	$⊢ vol : dom vol ⟶ [0, +∞] \to vol Fn dom vol$
251	7 250	ax-mp	$⊢ vol Fn dom vol$
252	28	frnd	$⊢ φ \to ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \subseteq dom vol$
253	252	adantr	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \subseteq dom vol$
254		breq1	$⊢ x = vol (z) \to (x \leq 0 \leftrightarrow vol (z) \leq 0)$
255	254	ralima	$⊢ (vol Fn dom vol \land ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) \subseteq dom vol) \to (\forall x \in vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] x \leq 0 \leftrightarrow \forall z \in ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) vol (z) \leq 0)$
256	251 253 255	sylancr	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to (\forall x \in vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] x \leq 0 \leftrightarrow \forall z \in ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)]) vol (z) \leq 0)$
257	249 256	mpbird	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to \forall x \in vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] x \leq 0$
258		imassrn	$⊢ vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] \subseteq ran vol$
259		frn	$⊢ vol : dom vol ⟶ [0, +∞] \to ran vol \subseteq [0, +∞]$
260	7 259	ax-mp	$⊢ ran vol \subseteq [0, +∞]$
261	260 6	sstri	$⊢ ran vol \subseteq ℝ^{*}$
262	258 261	sstri	$⊢ vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] \subseteq ℝ^{*}$
263		supxrleub	$⊢ (vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] \subseteq ℝ^{} \land 0 \in ℝ^{}) \to (sup (vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] ℝ^{*} <) \leq 0 \leftrightarrow \forall x \in vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] x \leq 0)$
264	262 39 263	mp2an	$⊢ sup (vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] ℝ^{*} <) \leq 0 \leftrightarrow \forall x \in vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] x \leq 0$
265	257 264	sylibr	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to sup (vol [ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])] ℝ^{*} <) \leq 0$
266	128 265	eqbrtrd	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to {vol}^{*} (⋃ ran (n \in ℕ ⟼ F^{-1} [(\frac{1}{n}, +∞)])) \leq 0$
267	11 38 40 93 266	xrletrd	$⊢ (φ \land \neg 0 < \int^{2} (F)) \to vol (A) \leq 0$
268	267	ex	$⊢ φ \to (\neg 0 < \int^{2} (F) \to vol (A) \leq 0)$
269		xrlenlt	$⊢ (vol (A) \in ℝ^{} \land 0 \in ℝ^{}) \to (vol (A) \leq 0 \leftrightarrow \neg 0 < vol (A))$
270	10 39 269	sylancl	$⊢ φ \to (vol (A) \leq 0 \leftrightarrow \neg 0 < vol (A))$
271	268 270	sylibd	$⊢ φ \to (\neg 0 < \int^{2} (F) \to \neg 0 < vol (A))$
272	2 271	mt4d	$⊢ φ \to 0 < \int^{2} (F)$

Metamath Proof Explorer

Theorem itg2gt0

Proof