Theorem itg2seq 24326

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

Assertion

Ref	Expression
itg2seq	⊢ (𝐹:ℝ⟶(0[,]+∞) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < )))

Distinct variable group:   𝑔,𝑛,𝐹

Proof of Theorem itg2seq

Dummy variables 𝑓 𝑚 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnre 11631	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
2	1	ad2antlr 725	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → 𝑛 ∈ ℝ)
3	2	ltpnfd 12503	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → 𝑛 < +∞)
4		iftrue 4459	. . . . . . . . . . 11 ⊢ ((∫2‘𝐹) = +∞ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
5	4	adantl 484	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
6		simpr 487	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → (∫2‘𝐹) = +∞)
7	3, 5, 6	3brtr4d 5084	. . . . . . . . 9 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
8		iffalse 4462	. . . . . . . . . . 11 ⊢ (¬ (∫2‘𝐹) = +∞ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
9	8	adantl 484	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
10		itg2cl 24316	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*)
11		xrrebnd 12548	. . . . . . . . . . . . . . 15 ⊢ ((∫2‘𝐹) ∈ ℝ* → ((∫2‘𝐹) ∈ ℝ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
12	10, 11	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) ∈ ℝ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
13		itg2ge0 24319	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℝ⟶(0[,]+∞) → 0 ≤ (∫2‘𝐹))
14		mnflt0 12507	. . . . . . . . . . . . . . . . 17 ⊢ -∞ < 0
15		mnfxr 10684	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ*
16		0xr 10674	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ*
17		xrltletr 12537	. . . . . . . . . . . . . . . . . 18 ⊢ ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ < (∫2‘𝐹)))
18	15, 16, 10, 17	mp3an12i 1461	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ < (∫2‘𝐹)))
19	14, 18	mpani 694	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (0 ≤ (∫2‘𝐹) → -∞ < (∫2‘𝐹)))
20	13, 19	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → -∞ < (∫2‘𝐹))
21	20	biantrurd 535	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) < +∞ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
22		nltpnft 12544	. . . . . . . . . . . . . . . 16 ⊢ ((∫2‘𝐹) ∈ ℝ* → ((∫2‘𝐹) = +∞ ↔ ¬ (∫2‘𝐹) < +∞))
23	10, 22	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) = +∞ ↔ ¬ (∫2‘𝐹) < +∞))
24	23	con2bid 357	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) < +∞ ↔ ¬ (∫2‘𝐹) = +∞))
25	12, 21, 24	3bitr2rd 310	. . . . . . . . . . . . 13 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (¬ (∫2‘𝐹) = +∞ ↔ (∫2‘𝐹) ∈ ℝ))
26	25	biimpa 479	. . . . . . . . . . . 12 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
27	26	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
28		nnrp 12387	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
29	28	rpreccld 12428	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
30	29	ad2antlr 725	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (1 / 𝑛) ∈ ℝ+)
31	27, 30	ltsubrpd 12450	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − (1 / 𝑛)) < (∫2‘𝐹))
32	9, 31	eqbrtrd 5074	. . . . . . . . 9 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
33	7, 32	pm2.61dan 811	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
34		nnrecre 11666	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
35	34	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (1 / 𝑛) ∈ ℝ)
36	27, 35	resubcld 11054	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − (1 / 𝑛)) ∈ ℝ)
37	2, 36	ifclda 4487	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ)
38	37	rexrd 10677	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
39	10	adantr 483	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (∫2‘𝐹) ∈ ℝ*)
40		xrltnle 10694	. . . . . . . . 9 ⊢ ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
41	38, 39, 40	syl2anc 586	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
42	33, 41	mpbid 234	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
43		itg2leub 24318	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) → ((∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
44	38, 43	syldan 593	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ((∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
45	42, 44	mtbid 326	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ¬ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
46		rexanali 3265	. . . . . 6 ⊢ (∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))) ↔ ¬ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
47	45, 46	sylibr 236	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
48		itg1cl 24269	. . . . . . . 8 ⊢ (𝑓 ∈ dom ∫1 → (∫1‘𝑓) ∈ ℝ)
49		ltnle 10706	. . . . . . . 8 ⊢ ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ ∧ (∫1‘𝑓) ∈ ℝ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
50	37, 48, 49	syl2an 597	. . . . . . 7 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑓 ∈ dom ∫1) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
51	50	anbi2d 630	. . . . . 6 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑓 ∈ dom ∫1) → ((𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ (𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
52	51	rexbidva 3296	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
53	47, 52	mpbird 259	. . . 4 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)))
54	53	ralrimiva 3182	. . 3 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ∀𝑛 ∈ ℕ ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)))
55		ovex 7175	. . . . 5 ⊢ (ℝ ↑m ℝ) ∈ V
56		i1ff 24260	. . . . . . 7 ⊢ (𝑥 ∈ dom ∫1 → 𝑥:ℝ⟶ℝ)
57		reex 10614	. . . . . . . 8 ⊢ ℝ ∈ V
58	57, 57	elmap 8421	. . . . . . 7 ⊢ (𝑥 ∈ (ℝ ↑m ℝ) ↔ 𝑥:ℝ⟶ℝ)
59	56, 58	sylibr 236	. . . . . 6 ⊢ (𝑥 ∈ dom ∫1 → 𝑥 ∈ (ℝ ↑m ℝ))
60	59	ssriv 3959	. . . . 5 ⊢ dom ∫1 ⊆ (ℝ ↑m ℝ)
61	55, 60	ssexi 5212	. . . 4 ⊢ dom ∫1 ∈ V
62		nnenom 13338	. . . 4 ⊢ ℕ ≈ ω
63		breq1 5055	. . . . 5 ⊢ (𝑓 = (𝑔‘𝑛) → (𝑓 ∘r ≤ 𝐹 ↔ (𝑔‘𝑛) ∘r ≤ 𝐹))
64		fveq2 6656	. . . . . 6 ⊢ (𝑓 = (𝑔‘𝑛) → (∫1‘𝑓) = (∫1‘(𝑔‘𝑛)))
65	64	breq2d 5064	. . . . 5 ⊢ (𝑓 = (𝑔‘𝑛) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))
66	63, 65	anbi12d 632	. . . 4 ⊢ (𝑓 = (𝑔‘𝑛) → ((𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))))
67	61, 62, 66	axcc4 9847	. . 3 ⊢ (∀𝑛 ∈ ℕ ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))))
68	54, 67	syl 17	. 2 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))))
69		simprl 769	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → 𝑔:ℕ⟶dom ∫1)
70		simpl 485	. . . . . . 7 ⊢ (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → (𝑔‘𝑛) ∘r ≤ 𝐹)
71	70	ralimi 3160	. . . . . 6 ⊢ (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹)
72	71	ad2antll 727	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹)
73	10	adantr 483	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ∈ ℝ*)
74		ffvelrn 6835	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ dom ∫1)
75		itg1cl 24269	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑛) ∈ dom ∫1 → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
76	74, 75	syl 17	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
77	76	fmpttd 6865	. . . . . . . . . 10 ⊢ (𝑔:ℕ⟶dom ∫1 → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
78	77	ad2antrl 726	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
79	78	frnd 6507	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ)
80		ressxr 10671	. . . . . . . 8 ⊢ ℝ ⊆ ℝ*
81	79, 80	sstrdi 3967	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
82		supxrcl 12695	. . . . . . 7 ⊢ (ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ* → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈ ℝ*)
83	81, 82	syl 17	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈ ℝ*)
84	38	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
85	76	adantll 712	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
86	85	rexrd 10677	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ*)
87		xrltle 12529	. . . . . . . . . . . . 13 ⊢ ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ* ∧ (∫1‘(𝑔‘𝑛)) ∈ ℝ*) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛))))
88	84, 86, 87	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛))))
89		2fveq3 6661	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (∫1‘(𝑔‘𝑛)) = (∫1‘(𝑔‘𝑚)))
90	89	cbvmptv 5155	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
91	90	rneqi 5793	. . . . . . . . . . . . . . 15 ⊢ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
92	77	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
93	92	frnd 6507	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ)
94	93, 80	sstrdi 3967	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
95	94	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
96	91, 95	eqsstrrid 4004	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) ⊆ ℝ*)
97		2fveq3 6661	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (∫1‘(𝑔‘𝑚)) = (∫1‘(𝑔‘𝑛)))
98		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) = (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
99		fvex 6669	. . . . . . . . . . . . . . . . 17 ⊢ (∫1‘(𝑔‘𝑛)) ∈ V
100	97, 98, 99	fvmpt 6754	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) = (∫1‘(𝑔‘𝑛)))
101		fvex 6669	. . . . . . . . . . . . . . . . . 18 ⊢ (∫1‘(𝑔‘𝑚)) ∈ V
102	101, 98	fnmpti 6477	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) Fn ℕ
103		fnfvelrn 6834	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) Fn ℕ ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
104	102, 103	mpan 688	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
105	100, 104	eqeltrrd 2914	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
106	105	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
107		supxrub 12704	. . . . . . . . . . . . . 14 ⊢ ((ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) ⊆ ℝ* ∧ (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))) → (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
108	96, 106, 107	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
109	91	supeq1i 8897	. . . . . . . . . . . . . . 15 ⊢ sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )
110	95, 82	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈ ℝ*)
111	109, 110	eqeltrrid 2918	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈ ℝ*)
112		xrletr 12538	. . . . . . . . . . . . . 14 ⊢ ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ* ∧ (∫1‘(𝑔‘𝑛)) ∈ ℝ* ∧ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈ ℝ*) → ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛)) ∧ (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
113	84, 86, 111, 112	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛)) ∧ (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
114	108, 113	mpan2d 692	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
115	88, 114	syld 47	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
116	115	adantld 493	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
117	116	ralimdva 3177	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
118	117	impr 457	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
119		breq2 5056	. . . . . . . . . . 11 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
120	119	ralbidv 3197	. . . . . . . . . 10 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
121		breq2 5056	. . . . . . . . . 10 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → ((∫2‘𝐹) ≤ 𝑥 ↔ (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
122	120, 121	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → ((∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥) ↔ (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))))
123		elxr 12498	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ* ↔ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞))
124		simplrl 775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → 𝑥 ∈ ℝ)
125		arch 11881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → ∃𝑛 ∈ ℕ 𝑥 < 𝑛)
126	124, 125	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < 𝑛)
127	4	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
128	127	breq2d 5064	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ 𝑥 < 𝑛))
129	128	rexbidv 3297	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ 𝑥 < 𝑛))
130	126, 129	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
131	26	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
132		simplrl 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 𝑥 ∈ ℝ)
133	131, 132	resubcld 11054	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − 𝑥) ∈ ℝ)
134		simplrr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 𝑥 < (∫2‘𝐹))
135	132, 131	posdifd 11213	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (𝑥 < (∫2‘𝐹) ↔ 0 < ((∫2‘𝐹) − 𝑥)))
136	134, 135	mpbid 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 0 < ((∫2‘𝐹) − 𝑥))
137		nnrecl 11882	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((∫2‘𝐹) − 𝑥) ∈ ℝ ∧ 0 < ((∫2‘𝐹) − 𝑥)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥))
138	133, 136, 137	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥))
139	34	adantl 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
140	131	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (∫2‘𝐹) ∈ ℝ)
141	132	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
142		ltsub13 11107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1 / 𝑛) ∈ ℝ ∧ (∫2‘𝐹) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
143	139, 140, 141, 142	syl3anc 1367	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
144	8	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
145	144	breq2d 5064	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
146	143, 145	bitr4d 284	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
147	146	rexbidva 3296	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
148	138, 147	mpbid 234	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
149	130, 148	pm2.61dan 811	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
150	149	expr 459	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < (∫2‘𝐹) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
151		rexr 10673	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
152		xrltnle 10694	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → (𝑥 < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ 𝑥))
153	151, 10, 152	syl2anr 598	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ 𝑥))
154	151	ad2antlr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ*)
155	38	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
156		xrltnle 10694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ* ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
157	154, 155, 156	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
158	157	rexbidva 3296	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
159		rexnal 3238	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑛 ∈ ℕ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ¬ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
160	158, 159	syl6bb 289	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
161	150, 153, 160	3imtr3d 295	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (¬ (∫2‘𝐹) ≤ 𝑥 → ¬ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
162	161	con4d 115	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
163	10	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ∈ ℝ*)
164		pnfge 12512	. . . . . . . . . . . . . . . 16 ⊢ ((∫2‘𝐹) ∈ ℝ* → (∫2‘𝐹) ≤ +∞)
165	163, 164	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ≤ +∞)
166		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → 𝑥 = +∞)
167	165, 166	breqtrrd 5080	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ≤ 𝑥)
168	167	a1d 25	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
169		1nn 11635	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ
170	169	ne0ii 4289	. . . . . . . . . . . . . . 15 ⊢ ℕ ≠ ∅
171		r19.2z 4426	. . . . . . . . . . . . . . 15 ⊢ ((ℕ ≠ ∅ ∧ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥) → ∃𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
172	170, 171	mpan 688	. . . . . . . . . . . . . 14 ⊢ (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → ∃𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
173	37	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ)
174		mnflt 12505	. . . . . . . . . . . . . . . . . . 19 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → -∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
175		rexr 10673	. . . . . . . . . . . . . . . . . . . 20 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
176		xrltnle 10694	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-∞ ∈ ℝ* ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) → (-∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞))
177	15, 175, 176	sylancr 589	. . . . . . . . . . . . . . . . . . 19 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → (-∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞))
178	174, 177	mpbid 234	. . . . . . . . . . . . . . . . . 18 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞)
179	173, 178	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞)
180		simplr 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → 𝑥 = -∞)
181	180	breq2d 5064	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞))
182	179, 181	mtbird 327	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
183	182	nrexdv 3270	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) → ¬ ∃𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
184	183	pm2.21d 121	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) → (∃𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
185	172, 184	syl5 34	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
186	162, 168, 185	3jaodan 1426	. . . . . . . . . . . 12 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞)) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
187	123, 186	sylan2b 595	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ*) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
188	187	ralrimiva 3182	. . . . . . . . . 10 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
189	188	adantr 483	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
190	109, 83	eqeltrrid 2918	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈ ℝ*)
191	122, 189, 190	rspcdva 3617	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
192	118, 191	mpd 15	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
193	192, 109	breqtrrdi 5094	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))
194		itg2ub 24317	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔‘𝑛) ∈ dom ∫1 ∧ (𝑔‘𝑛) ∘r ≤ 𝐹) → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
195	194	3expia 1117	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔‘𝑛) ∈ dom ∫1) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
196	74, 195	sylan2 594	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ)) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
197	196	anassrs 470	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
198	197	adantrd 494	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
199	198	ralimdva 3177	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
200	199	impr 457	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
201		eqid 2821	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))
202	89, 201, 101	fvmpt 6754	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) = (∫1‘(𝑔‘𝑚)))
203	202	breq1d 5062	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹)))
204	203	ralbiia 3164	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹))
205	89	breq1d 5062	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → ((∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹) ↔ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹)))
206	205	cbvralvw 3441	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹))
207	204, 206	bitr4i 280	. . . . . . . . 9 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
208	200, 207	sylibr 236	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹))
209		ffn 6500	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) Fn ℕ)
210		breq1 5055	. . . . . . . . . 10 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) → (𝑧 ≤ (∫2‘𝐹) ↔ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹)))
211	210	ralrn 6840	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹)))
212	78, 209, 211	3syl 18	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹)))
213	208, 212	mpbird 259	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹))
214		supxrleub 12706	. . . . . . . 8 ⊢ ((ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → (sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤ (∫2‘𝐹) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹)))
215	81, 73, 214	syl2anc 586	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤ (∫2‘𝐹) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹)))
216	213, 215	mpbird 259	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤ (∫2‘𝐹))
217	73, 83, 193, 216	xrletrid 12535	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))
218	69, 72, 217	3jca 1124	. . . 4 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < )))
219	218	ex 415	. . 3 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))) → (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))))
220	219	eximdv 1918	. 2 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))))
221	68, 220	mpd 15	1 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < )))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ w3o 1082   ∧ w3a 1083   = wceq 1537  ∃wex 1780   ∈ wcel 2114   ≠ wne 3016  ∀wral 3138  ∃wrex 3139   ⊆ wss 3924  ∅c0 4279  ifcif 4453   class class class wbr 5052   ↦ cmpt 5132  dom cdm 5541  ran crn 5542   Fn wfn 6336  ⟶wf 6337  ‘cfv 6341  (class class class)co 7142   ∘_r cofr 7394   ↑_m cmap 8392  supcsup 8890  ℝcr 10522  0cc0 10523  1c1 10524  +∞cpnf 10658  -∞cmnf 10659  ℝ^*cxr 10660   < clt 10661   ≤ cle 10662   − cmin 10856   / cdiv 11283  ℕcn 11624  ℝ⁺crp 12376  [,]cicc 12728  ∫₁citg1 24199  ∫₂citg2 24200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-inf2 9090  ax-cc 9843  ax-cnex 10579  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599  ax-pre-mulgt0 10600  ax-pre-sup 10601

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-pss 3942  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-tp 4558  df-op 4560  df-uni 4825  df-int 4863  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5446  df-eprel 5451  df-po 5460  df-so 5461  df-fr 5500  df-se 5501  df-we 5502  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-pred 6134  df-ord 6180  df-on 6181  df-lim 6182  df-suc 6183  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-isom 6350  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-of 7395  df-ofr 7396  df-om 7567  df-1st 7675  df-2nd 7676  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-er 8275  df-map 8394  df-pm 8395  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-sup 8892  df-inf 8893  df-oi 8960  df-dju 9316  df-card 9354  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666  df-le 10667  df-sub 10858  df-neg 10859  df-div 11284  df-nn 11625  df-2 11687  df-3 11688  df-n0 11885  df-z 11969  df-uz 12231  df-q 12336  df-rp 12377  df-xadd 12495  df-ioo 12729  df-ico 12731  df-icc 12732  df-fz 12883  df-fzo 13024  df-fl 13152  df-seq 13360  df-exp 13420  df-hash 13681  df-cj 14443  df-re 14444  df-im 14445  df-sqrt 14579  df-abs 14580  df-clim 14830  df-sum 15028  df-xmet 20521  df-met 20522  df-ovol 24048  df-vol 24049  df-mbf 24203  df-itg1 24204  df-itg2 24205

This theorem is referenced by: (None)