itg2seq

Description: Definitional property of the S.2 integral: for any function F there is a countable sequence g of simple functions less than F whose integrals converge to the integral of F . (This theorem is for the most part unnecessary in lieu of itg2i1fseq , but unlike that theorem this one doesn't require F to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014)

		Ref	Expression
	Assertion	itg2seq	$⊢ F : ℝ ⟶ [0, +∞] \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ g (n) \leq_{f} F \land \int^{2} (F) = sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{*} <))$

Proof

Step	Hyp	Ref	Expression
1		nnre	$⊢ n \in ℕ \to n \in ℝ$
2	1	ad2antlr	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \int^{2} (F) = +∞) \to n \in ℝ$
3	2	ltpnfd	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \int^{2} (F) = +∞) \to n < +∞$
4		iftrue	$⊢ \int^{2} (F) = +∞ \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) = n$
5	4	adantl	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \int^{2} (F) = +∞) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) = n$
6		simpr	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \int^{2} (F) = +∞) \to \int^{2} (F) = +∞$
7	3 5 6	3brtr4d	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \int^{2} (F) = +∞) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{2} (F)$
8		iffalse	$⊢ \neg \int^{2} (F) = +∞ \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) = \int^{2} (F) - (\frac{1}{n})$
9	8	adantl	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \neg \int^{2} (F) = +∞) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) = \int^{2} (F) - (\frac{1}{n})$
10		itg2cl	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) \in ℝ^{*}$
11		xrrebnd	$⊢ \int^{2} (F) \in ℝ^{*} \to (\int^{2} (F) \in ℝ \leftrightarrow (−∞ < \int^{2} (F) \land \int^{2} (F) < +∞))$
12	10 11	syl	$⊢ F : ℝ ⟶ [0, +∞] \to (\int^{2} (F) \in ℝ \leftrightarrow (−∞ < \int^{2} (F) \land \int^{2} (F) < +∞))$
13		itg2ge0	$⊢ F : ℝ ⟶ [0, +∞] \to 0 \leq \int^{2} (F)$
14		mnflt0	$⊢ −∞ < 0$
15		mnfxr	$⊢ −∞ \in ℝ^{*}$
16		0xr	$⊢ 0 \in ℝ^{*}$
17		xrltletr	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{} \land \int^{2} (F) \in ℝ^{*}) \to ((−∞ < 0 \land 0 \leq \int^{2} (F)) \to −∞ < \int^{2} (F))$
18	15 16 10 17	mp3an12i	$⊢ F : ℝ ⟶ [0, +∞] \to ((−∞ < 0 \land 0 \leq \int^{2} (F)) \to −∞ < \int^{2} (F))$
19	14 18	mpani	$⊢ F : ℝ ⟶ [0, +∞] \to (0 \leq \int^{2} (F) \to −∞ < \int^{2} (F))$
20	13 19	mpd	$⊢ F : ℝ ⟶ [0, +∞] \to −∞ < \int^{2} (F)$
21	20	biantrurd	$⊢ F : ℝ ⟶ [0, +∞] \to (\int^{2} (F) < +∞ \leftrightarrow (−∞ < \int^{2} (F) \land \int^{2} (F) < +∞))$
22		nltpnft	$⊢ \int^{2} (F) \in ℝ^{*} \to (\int^{2} (F) = +∞ \leftrightarrow \neg \int^{2} (F) < +∞)$
23	10 22	syl	$⊢ F : ℝ ⟶ [0, +∞] \to (\int^{2} (F) = +∞ \leftrightarrow \neg \int^{2} (F) < +∞)$
24	23	con2bid	$⊢ F : ℝ ⟶ [0, +∞] \to (\int^{2} (F) < +∞ \leftrightarrow \neg \int^{2} (F) = +∞)$
25	12 21 24	3bitr2rd	$⊢ F : ℝ ⟶ [0, +∞] \to (\neg \int^{2} (F) = +∞ \leftrightarrow \int^{2} (F) \in ℝ)$
26	25	biimpa	$⊢ (F : ℝ ⟶ [0, +∞] \land \neg \int^{2} (F) = +∞) \to \int^{2} (F) \in ℝ$
27	26	adantlr	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \neg \int^{2} (F) = +∞) \to \int^{2} (F) \in ℝ$
28		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
29	28	rpreccld	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
30	29	ad2antlr	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \neg \int^{2} (F) = +∞) \to \frac{1}{n} \in ℝ^{+}$
31	27 30	ltsubrpd	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \neg \int^{2} (F) = +∞) \to \int^{2} (F) - (\frac{1}{n}) < \int^{2} (F)$
32	9 31	eqbrtrd	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \neg \int^{2} (F) = +∞) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{2} (F)$
33	7 32	pm2.61dan	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{2} (F)$
34		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
35	34	ad2antlr	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \neg \int^{2} (F) = +∞) \to \frac{1}{n} \in ℝ$
36	27 35	resubcld	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land \neg \int^{2} (F) = +∞) \to \int^{2} (F) - (\frac{1}{n}) \in ℝ$
37	2 36	ifclda	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ$
38	37	rexrd	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ^{*}$
39	10	adantr	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to \int^{2} (F) \in ℝ^{*}$
40		xrltnle	$⊢ (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ^{} \land \int^{2} (F) \in ℝ^{}) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{2} (F) \leftrightarrow \neg \int^{2} (F) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})))$
41	38 39 40	syl2anc	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{2} (F) \leftrightarrow \neg \int^{2} (F) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})))$
42	33 41	mpbid	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to \neg \int^{2} (F) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n}))$
43		itg2leub	$⊢ (F : ℝ ⟶ [0, +∞] \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ^{*}) \to (\int^{2} (F) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n}))))$
44	38 43	syldan	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to (\int^{2} (F) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n}))))$
45	42 44	mtbid	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to \neg \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})))$
46		rexanali	$⊢ \exists f \in dom \int^{1} (f \leq_{f} F \land \neg \int^{1} (f) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n}))) \leftrightarrow \neg \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})))$
47	45 46	sylibr	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to \exists f \in dom \int^{1} (f \leq_{f} F \land \neg \int^{1} (f) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})))$
48		itg1cl	$⊢ f \in dom \int^{1} \to \int^{1} (f) \in ℝ$
49		ltnle	$⊢ (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ \land \int^{1} (f) \in ℝ) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (f) \leftrightarrow \neg \int^{1} (f) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})))$
50	37 48 49	syl2an	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land f \in dom \int^{1}) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (f) \leftrightarrow \neg \int^{1} (f) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})))$
51	50	anbi2d	$⊢ ((F : ℝ ⟶ [0, +∞] \land n \in ℕ) \land f \in dom \int^{1}) \to ((f \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (f)) \leftrightarrow (f \leq_{f} F \land \neg \int^{1} (f) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n}))))$
52	51	rexbidva	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to (\exists f \in dom \int^{1} (f \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (f)) \leftrightarrow \exists f \in dom \int^{1} (f \leq_{f} F \land \neg \int^{1} (f) \leq if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n}))))$
53	47 52	mpbird	$⊢ (F : ℝ ⟶ [0, +∞] \land n \in ℕ) \to \exists f \in dom \int^{1} (f \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (f))$
54	53	ralrimiva	$⊢ F : ℝ ⟶ [0, +∞] \to \forall n \in ℕ \exists f \in dom \int^{1} (f \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (f))$
55		ovex	$⊢ ℝ^{ℝ} \in V$
56		i1ff	$⊢ x \in dom \int^{1} \to x : ℝ ⟶ ℝ$
57		reex	$⊢ ℝ \in V$
58	57 57	elmap	$⊢ x \in (ℝ^{ℝ}) \leftrightarrow x : ℝ ⟶ ℝ$
59	56 58	sylibr	$⊢ x \in dom \int^{1} \to x \in (ℝ^{ℝ})$
60	59	ssriv	$⊢ dom \int^{1} \subseteq ℝ^{ℝ}$
61	55 60	ssexi	$⊢ dom \int^{1} \in V$
62		nnenom	$⊢ ℕ \approx ω$
63		breq1	$⊢ f = g (n) \to (f \leq_{f} F \leftrightarrow g (n) \leq_{f} F)$
64		fveq2	$⊢ f = g (n) \to \int^{1} (f) = \int^{1} (g (n))$
65	64	breq2d	$⊢ f = g (n) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (f) \leftrightarrow if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n)))$
66	63 65	anbi12d	$⊢ f = g (n) \to ((f \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (f)) \leftrightarrow (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))$
67	61 62 66	axcc4	$⊢ \forall n \in ℕ \exists f \in dom \int^{1} (f \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (f)) \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))$
68	54 67	syl	$⊢ F : ℝ ⟶ [0, +∞] \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))$
69		simprl	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to g : ℕ ⟶ dom \int^{1}$
70		simpl	$⊢ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))) \to g (n) \leq_{f} F$
71	70	ralimi	$⊢ \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))) \to \forall n \in ℕ g (n) \leq_{f} F$
72	71	ad2antll	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to \forall n \in ℕ g (n) \leq_{f} F$
73	10	adantr	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to \int^{2} (F) \in ℝ^{*}$
74		ffvelrn	$⊢ (g : ℕ ⟶ dom \int^{1} \land n \in ℕ) \to g (n) \in dom \int^{1}$
75		itg1cl	$⊢ g (n) \in dom \int^{1} \to \int^{1} (g (n)) \in ℝ$
76	74 75	syl	$⊢ (g : ℕ ⟶ dom \int^{1} \land n \in ℕ) \to \int^{1} (g (n)) \in ℝ$
77	76	fmpttd	$⊢ g : ℕ ⟶ dom \int^{1} \to (n \in ℕ ⟼ \int^{1} (g (n))) : ℕ ⟶ ℝ$
78	77	ad2antrl	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to (n \in ℕ ⟼ \int^{1} (g (n))) : ℕ ⟶ ℝ$
79	78	frnd	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to ran (n \in ℕ ⟼ \int^{1} (g (n))) \subseteq ℝ$
80		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
81	79 80	sstrdi	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to ran (n \in ℕ ⟼ \int^{1} (g (n))) \subseteq ℝ^{*}$
82		supxrcl	$⊢ ran (n \in ℕ ⟼ \int^{1} (g (n))) \subseteq ℝ^{} \to sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{} <) \in ℝ^{*}$
83	81 82	syl	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{} <) \in ℝ^{}$
84	38	adantlr	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ^{*}$
85	76	adantll	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to \int^{1} (g (n)) \in ℝ$
86	85	rexrd	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to \int^{1} (g (n)) \in ℝ^{*}$
87		xrltle	$⊢ (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ^{} \land \int^{1} (g (n)) \in ℝ^{}) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n)) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq \int^{1} (g (n)))$
88	84 86 87	syl2anc	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n)) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq \int^{1} (g (n)))$
89		2fveq3	$⊢ n = m \to \int^{1} (g (n)) = \int^{1} (g (m))$
90	89	cbvmptv	$⊢ (n \in ℕ ⟼ \int^{1} (g (n))) = (m \in ℕ ⟼ \int^{1} (g (m)))$
91	90	rneqi	$⊢ ran (n \in ℕ ⟼ \int^{1} (g (n))) = ran (m \in ℕ ⟼ \int^{1} (g (m)))$
92	77	adantl	$⊢ (F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \to (n \in ℕ ⟼ \int^{1} (g (n))) : ℕ ⟶ ℝ$
93	92	frnd	$⊢ (F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \to ran (n \in ℕ ⟼ \int^{1} (g (n))) \subseteq ℝ$
94	93 80	sstrdi	$⊢ (F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \to ran (n \in ℕ ⟼ \int^{1} (g (n))) \subseteq ℝ^{*}$
95	94	adantr	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to ran (n \in ℕ ⟼ \int^{1} (g (n))) \subseteq ℝ^{*}$
96	91 95	eqsstrrid	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to ran (m \in ℕ ⟼ \int^{1} (g (m))) \subseteq ℝ^{*}$
97		2fveq3	$⊢ m = n \to \int^{1} (g (m)) = \int^{1} (g (n))$
98		eqid	$⊢ (m \in ℕ ⟼ \int^{1} (g (m))) = (m \in ℕ ⟼ \int^{1} (g (m)))$
99		fvex	$⊢ \int^{1} (g (n)) \in V$
100	97 98 99	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ \int^{1} (g (m))) (n) = \int^{1} (g (n))$
101		fvex	$⊢ \int^{1} (g (m)) \in V$
102	101 98	fnmpti	$⊢ (m \in ℕ ⟼ \int^{1} (g (m))) Fn ℕ$
103		fnfvelrn	$⊢ ((m \in ℕ ⟼ \int^{1} (g (m))) Fn ℕ \land n \in ℕ) \to (m \in ℕ ⟼ \int^{1} (g (m))) (n) \in ran (m \in ℕ ⟼ \int^{1} (g (m)))$
104	102 103	mpan	$⊢ n \in ℕ \to (m \in ℕ ⟼ \int^{1} (g (m))) (n) \in ran (m \in ℕ ⟼ \int^{1} (g (m)))$
105	100 104	eqeltrrd	$⊢ n \in ℕ \to \int^{1} (g (n)) \in ran (m \in ℕ ⟼ \int^{1} (g (m)))$
106	105	adantl	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to \int^{1} (g (n)) \in ran (m \in ℕ ⟼ \int^{1} (g (m)))$
107		supxrub	$⊢ (ran (m \in ℕ ⟼ \int^{1} (g (m))) \subseteq ℝ^{} \land \int^{1} (g (n)) \in ran (m \in ℕ ⟼ \int^{1} (g (m)))) \to \int^{1} (g (n)) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <)$
108	96 106 107	syl2anc	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to \int^{1} (g (n)) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{*} <)$
109	91	supeq1i	$⊢ sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{} <) = sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <)$
110	95 82	syl	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{} <) \in ℝ^{}$
111	109 110	eqeltrrid	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <) \in ℝ^{}$
112		xrletr	$⊢ (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ^{} \land \int^{1} (g (n)) \in ℝ^{} \land sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <) \in ℝ^{}) \to ((if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq \int^{1} (g (n)) \land \int^{1} (g (n)) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <)) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <))$
113	84 86 111 112	syl3anc	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to ((if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq \int^{1} (g (n)) \land \int^{1} (g (n)) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <)) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <))$
114	108 113	mpan2d	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq \int^{1} (g (n)) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{*} <))$
115	88 114	syld	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n)) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{*} <))$
116	115	adantld	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to ((g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{*} <))$
117	116	ralimdva	$⊢ (F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \to (\forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))) \to \forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{*} <))$
118	117	impr	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to \forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{*} <)$
119		breq2	$⊢ x = sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \leftrightarrow if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <))$
120	119	ralbidv	$⊢ x = sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <) \to (\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \leftrightarrow \forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <))$
121		breq2	$⊢ x = sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <) \to (\int^{2} (F) \leq x \leftrightarrow \int^{2} (F) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <))$
122	120 121	imbi12d	$⊢ x = sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <) \to ((\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \to \int^{2} (F) \leq x) \leftrightarrow (\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <) \to \int^{2} (F) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{*} <)))$
123		elxr	$⊢ x \in ℝ^{*} \leftrightarrow (x \in ℝ \lor x = +∞ \lor x = −∞)$
124		simplrl	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \int^{2} (F) = +∞) \to x \in ℝ$
125		arch	$⊢ x \in ℝ \to \exists n \in ℕ x < n$
126	124 125	syl	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \int^{2} (F) = +∞) \to \exists n \in ℕ x < n$
127	4	adantl	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \int^{2} (F) = +∞) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) = n$
128	127	breq2d	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \int^{2} (F) = +∞) \to (x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow x < n)$
129	128	rexbidv	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \int^{2} (F) = +∞) \to (\exists n \in ℕ x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow \exists n \in ℕ x < n)$
130	126 129	mpbird	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \int^{2} (F) = +∞) \to \exists n \in ℕ x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n}))$
131	26	adantlr	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \to \int^{2} (F) \in ℝ$
132		simplrl	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \to x \in ℝ$
133	131 132	resubcld	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \to \int^{2} (F) - x \in ℝ$
134		simplrr	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \to x < \int^{2} (F)$
135	132 131	posdifd	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \to (x < \int^{2} (F) \leftrightarrow 0 < \int^{2} (F) - x)$
136	134 135	mpbid	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \to 0 < \int^{2} (F) - x$
137		nnrecl	$⊢ (\int^{2} (F) - x \in ℝ \land 0 < \int^{2} (F) - x) \to \exists n \in ℕ \frac{1}{n} < \int^{2} (F) - x$
138	133 136 137	syl2anc	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \to \exists n \in ℕ \frac{1}{n} < \int^{2} (F) - x$
139	34	adantl	$⊢ (((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \land n \in ℕ) \to \frac{1}{n} \in ℝ$
140	131	adantr	$⊢ (((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \land n \in ℕ) \to \int^{2} (F) \in ℝ$
141	132	adantr	$⊢ (((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \land n \in ℕ) \to x \in ℝ$
142		ltsub13	$⊢ (\frac{1}{n} \in ℝ \land \int^{2} (F) \in ℝ \land x \in ℝ) \to (\frac{1}{n} < \int^{2} (F) - x \leftrightarrow x < \int^{2} (F) - (\frac{1}{n}))$
143	139 140 141 142	syl3anc	$⊢ (((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \land n \in ℕ) \to (\frac{1}{n} < \int^{2} (F) - x \leftrightarrow x < \int^{2} (F) - (\frac{1}{n}))$
144	8	ad2antlr	$⊢ (((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \land n \in ℕ) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) = \int^{2} (F) - (\frac{1}{n})$
145	144	breq2d	$⊢ (((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \land n \in ℕ) \to (x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow x < \int^{2} (F) - (\frac{1}{n}))$
146	143 145	bitr4d	$⊢ (((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \land n \in ℕ) \to (\frac{1}{n} < \int^{2} (F) - x \leftrightarrow x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})))$
147	146	rexbidva	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \to (\exists n \in ℕ \frac{1}{n} < \int^{2} (F) - x \leftrightarrow \exists n \in ℕ x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})))$
148	138 147	mpbid	$⊢ ((F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \land \neg \int^{2} (F) = +∞) \to \exists n \in ℕ x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n}))$
149	130 148	pm2.61dan	$⊢ (F : ℝ ⟶ [0, +∞] \land (x \in ℝ \land x < \int^{2} (F))) \to \exists n \in ℕ x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n}))$
150	149	expr	$⊢ (F : ℝ ⟶ [0, +∞] \land x \in ℝ) \to (x < \int^{2} (F) \to \exists n \in ℕ x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})))$
151		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
152		xrltnle	$⊢ (x \in ℝ^{} \land \int^{2} (F) \in ℝ^{}) \to (x < \int^{2} (F) \leftrightarrow \neg \int^{2} (F) \leq x)$
153	151 10 152	syl2anr	$⊢ (F : ℝ ⟶ [0, +∞] \land x \in ℝ) \to (x < \int^{2} (F) \leftrightarrow \neg \int^{2} (F) \leq x)$
154	151	ad2antlr	$⊢ ((F : ℝ ⟶ [0, +∞] \land x \in ℝ) \land n \in ℕ) \to x \in ℝ^{*}$
155	38	adantlr	$⊢ ((F : ℝ ⟶ [0, +∞] \land x \in ℝ) \land n \in ℕ) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ^{*}$
156		xrltnle	$⊢ (x \in ℝ^{} \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ^{}) \to (x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow \neg if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x)$
157	154 155 156	syl2anc	$⊢ ((F : ℝ ⟶ [0, +∞] \land x \in ℝ) \land n \in ℕ) \to (x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow \neg if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x)$
158	157	rexbidva	$⊢ (F : ℝ ⟶ [0, +∞] \land x \in ℝ) \to (\exists n \in ℕ x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow \exists n \in ℕ \neg if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x)$
159		rexnal	$⊢ \exists n \in ℕ \neg if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \leftrightarrow \neg \forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x$
160	158 159	syl6bb	$⊢ (F : ℝ ⟶ [0, +∞] \land x \in ℝ) \to (\exists n \in ℕ x < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow \neg \forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x)$
161	150 153 160	3imtr3d	$⊢ (F : ℝ ⟶ [0, +∞] \land x \in ℝ) \to (\neg \int^{2} (F) \leq x \to \neg \forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x)$
162	161	con4d	$⊢ (F : ℝ ⟶ [0, +∞] \land x \in ℝ) \to (\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \to \int^{2} (F) \leq x)$
163	10	adantr	$⊢ (F : ℝ ⟶ [0, +∞] \land x = +∞) \to \int^{2} (F) \in ℝ^{*}$
164		pnfge	$⊢ \int^{2} (F) \in ℝ^{*} \to \int^{2} (F) \leq +∞$
165	163 164	syl	$⊢ (F : ℝ ⟶ [0, +∞] \land x = +∞) \to \int^{2} (F) \leq +∞$
166		simpr	$⊢ (F : ℝ ⟶ [0, +∞] \land x = +∞) \to x = +∞$
167	165 166	breqtrrd	$⊢ (F : ℝ ⟶ [0, +∞] \land x = +∞) \to \int^{2} (F) \leq x$
168	167	a1d	$⊢ (F : ℝ ⟶ [0, +∞] \land x = +∞) \to (\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \to \int^{2} (F) \leq x)$
169		1nn	$⊢ 1 \in ℕ$
170	169	ne0ii	$⊢ ℕ \neq \emptyset$
171		r19.2z	$⊢ (ℕ \neq \emptyset \land \forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x) \to \exists n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x$
172	170 171	mpan	$⊢ \forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \to \exists n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x$
173	37	adantlr	$⊢ ((F : ℝ ⟶ [0, +∞] \land x = −∞) \land n \in ℕ) \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ$
174		mnflt	$⊢ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ \to −∞ < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n}))$
175		rexr	$⊢ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ \to if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ^{*}$
176		xrltnle	$⊢ (−∞ \in ℝ^{} \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ^{}) \to (−∞ < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow \neg if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq −∞)$
177	15 175 176	sylancr	$⊢ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ \to (−∞ < if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leftrightarrow \neg if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq −∞)$
178	174 177	mpbid	$⊢ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \in ℝ \to \neg if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq −∞$
179	173 178	syl	$⊢ ((F : ℝ ⟶ [0, +∞] \land x = −∞) \land n \in ℕ) \to \neg if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq −∞$
180		simplr	$⊢ ((F : ℝ ⟶ [0, +∞] \land x = −∞) \land n \in ℕ) \to x = −∞$
181	180	breq2d	$⊢ ((F : ℝ ⟶ [0, +∞] \land x = −∞) \land n \in ℕ) \to (if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \leftrightarrow if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq −∞)$
182	179 181	mtbird	$⊢ ((F : ℝ ⟶ [0, +∞] \land x = −∞) \land n \in ℕ) \to \neg if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x$
183	182	nrexdv	$⊢ (F : ℝ ⟶ [0, +∞] \land x = −∞) \to \neg \exists n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x$
184	183	pm2.21d	$⊢ (F : ℝ ⟶ [0, +∞] \land x = −∞) \to (\exists n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \to \int^{2} (F) \leq x)$
185	172 184	syl5	$⊢ (F : ℝ ⟶ [0, +∞] \land x = −∞) \to (\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \to \int^{2} (F) \leq x)$
186	162 168 185	3jaodan	$⊢ (F : ℝ ⟶ [0, +∞] \land (x \in ℝ \lor x = +∞ \lor x = −∞)) \to (\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \to \int^{2} (F) \leq x)$
187	123 186	sylan2b	$⊢ (F : ℝ ⟶ [0, +∞] \land x \in ℝ^{*}) \to (\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \to \int^{2} (F) \leq x)$
188	187	ralrimiva	$⊢ F : ℝ ⟶ [0, +∞] \to \forall x \in ℝ^{*} (\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \to \int^{2} (F) \leq x)$
189	188	adantr	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to \forall x \in ℝ^{*} (\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq x \to \int^{2} (F) \leq x)$
190	109 83	eqeltrrid	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <) \in ℝ^{}$
191	122 189 190	rspcdva	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to (\forall n \in ℕ if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <) \to \int^{2} (F) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{} <))$
192	118 191	mpd	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to \int^{2} (F) \leq sup (ran (m \in ℕ ⟼ \int^{1} (g (m))) ℝ^{*} <)$
193	192 109	breqtrrdi	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to \int^{2} (F) \leq sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{*} <)$
194		itg2ub	$⊢ (F : ℝ ⟶ [0, +∞] \land g (n) \in dom \int^{1} \land g (n) \leq_{f} F) \to \int^{1} (g (n)) \leq \int^{2} (F)$
195	194	3expia	$⊢ (F : ℝ ⟶ [0, +∞] \land g (n) \in dom \int^{1}) \to (g (n) \leq_{f} F \to \int^{1} (g (n)) \leq \int^{2} (F))$
196	74 195	sylan2	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land n \in ℕ)) \to (g (n) \leq_{f} F \to \int^{1} (g (n)) \leq \int^{2} (F))$
197	196	anassrs	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to (g (n) \leq_{f} F \to \int^{1} (g (n)) \leq \int^{2} (F))$
198	197	adantrd	$⊢ ((F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \land n \in ℕ) \to ((g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))) \to \int^{1} (g (n)) \leq \int^{2} (F))$
199	198	ralimdva	$⊢ (F : ℝ ⟶ [0, +∞] \land g : ℕ ⟶ dom \int^{1}) \to (\forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))) \to \forall n \in ℕ \int^{1} (g (n)) \leq \int^{2} (F))$
200	199	impr	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to \forall n \in ℕ \int^{1} (g (n)) \leq \int^{2} (F)$
201		eqid	$⊢ (n \in ℕ ⟼ \int^{1} (g (n))) = (n \in ℕ ⟼ \int^{1} (g (n)))$
202	89 201 101	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ \int^{1} (g (n))) (m) = \int^{1} (g (m))$
203	202	breq1d	$⊢ m \in ℕ \to ((n \in ℕ ⟼ \int^{1} (g (n))) (m) \leq \int^{2} (F) \leftrightarrow \int^{1} (g (m)) \leq \int^{2} (F))$
204	203	ralbiia	$⊢ \forall m \in ℕ (n \in ℕ ⟼ \int^{1} (g (n))) (m) \leq \int^{2} (F) \leftrightarrow \forall m \in ℕ \int^{1} (g (m)) \leq \int^{2} (F)$
205	89	breq1d	$⊢ n = m \to (\int^{1} (g (n)) \leq \int^{2} (F) \leftrightarrow \int^{1} (g (m)) \leq \int^{2} (F))$
206	205	cbvralvw	$⊢ \forall n \in ℕ \int^{1} (g (n)) \leq \int^{2} (F) \leftrightarrow \forall m \in ℕ \int^{1} (g (m)) \leq \int^{2} (F)$
207	204 206	bitr4i	$⊢ \forall m \in ℕ (n \in ℕ ⟼ \int^{1} (g (n))) (m) \leq \int^{2} (F) \leftrightarrow \forall n \in ℕ \int^{1} (g (n)) \leq \int^{2} (F)$
208	200 207	sylibr	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to \forall m \in ℕ (n \in ℕ ⟼ \int^{1} (g (n))) (m) \leq \int^{2} (F)$
209		ffn	$⊢ (n \in ℕ ⟼ \int^{1} (g (n))) : ℕ ⟶ ℝ \to (n \in ℕ ⟼ \int^{1} (g (n))) Fn ℕ$
210		breq1	$⊢ z = (n \in ℕ ⟼ \int^{1} (g (n))) (m) \to (z \leq \int^{2} (F) \leftrightarrow (n \in ℕ ⟼ \int^{1} (g (n))) (m) \leq \int^{2} (F))$
211	210	ralrn	$⊢ (n \in ℕ ⟼ \int^{1} (g (n))) Fn ℕ \to (\forall z \in ran (n \in ℕ ⟼ \int^{1} (g (n))) z \leq \int^{2} (F) \leftrightarrow \forall m \in ℕ (n \in ℕ ⟼ \int^{1} (g (n))) (m) \leq \int^{2} (F))$
212	78 209 211	3syl	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to (\forall z \in ran (n \in ℕ ⟼ \int^{1} (g (n))) z \leq \int^{2} (F) \leftrightarrow \forall m \in ℕ (n \in ℕ ⟼ \int^{1} (g (n))) (m) \leq \int^{2} (F))$
213	208 212	mpbird	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to \forall z \in ran (n \in ℕ ⟼ \int^{1} (g (n))) z \leq \int^{2} (F)$
214		supxrleub	$⊢ (ran (n \in ℕ ⟼ \int^{1} (g (n))) \subseteq ℝ^{} \land \int^{2} (F) \in ℝ^{}) \to (sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{*} <) \leq \int^{2} (F) \leftrightarrow \forall z \in ran (n \in ℕ ⟼ \int^{1} (g (n))) z \leq \int^{2} (F))$
215	81 73 214	syl2anc	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to (sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{*} <) \leq \int^{2} (F) \leftrightarrow \forall z \in ran (n \in ℕ ⟼ \int^{1} (g (n))) z \leq \int^{2} (F))$
216	213 215	mpbird	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{*} <) \leq \int^{2} (F)$
217	73 83 193 216	xrletrid	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to \int^{2} (F) = sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{*} <)$
218	69 72 217	3jca	$⊢ (F : ℝ ⟶ [0, +∞] \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n))))) \to (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ g (n) \leq_{f} F \land \int^{2} (F) = sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{*} <))$
219	218	ex	$⊢ F : ℝ ⟶ [0, +∞] \to ((g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n)))) \to (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ g (n) \leq_{f} F \land \int^{2} (F) = sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{*} <)))$
220	219	eximdv	$⊢ F : ℝ ⟶ [0, +∞] \to (\exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (g (n) \leq_{f} F \land if (\int^{2} (F) = +∞, n, \int^{2} (F) - (\frac{1}{n})) < \int^{1} (g (n)))) \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ g (n) \leq_{f} F \land \int^{2} (F) = sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{*} <)))$
221	68 220	mpd	$⊢ F : ℝ ⟶ [0, +∞] \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ g (n) \leq_{f} F \land \int^{2} (F) = sup (ran (n \in ℕ ⟼ \int^{1} (g (n))) ℝ^{*} <))$

Metamath Proof Explorer

Theorem itg2seq

Proof