Theorem 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:ℝ⟶\left[0,\mathrm{+\infty }\right]\to \exists g\left(g:\mathbb{N}⟶\mathrm{dom}{\int }^1\wedge \forall n\in \mathbb{N}g\left(n\right){\le }_{f}F\wedge {\int }^2\left(F\right)=sup\left(\mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^1\left(g\left(n\right)\right)\right),{ℝ}^{*},<\right)\right)$$

Proof

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