Theorem itg2seq 24916

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 24929, 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 11989	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
2	1	ad2antlr 724	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → 𝑛 ∈ ℝ)
3	2	ltpnfd 12866	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → 𝑛 < +∞)
4		iftrue 4466	. . . . . . . . . . 11 ⊢ ((∫2‘𝐹) = +∞ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
5	4	adantl 482	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
6		simpr 485	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → (∫2‘𝐹) = +∞)
7	3, 5, 6	3brtr4d 5107	. . . . . . . . 9 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
8		iffalse 4469	. . . . . . . . . . 11 ⊢ (¬ (∫2‘𝐹) = +∞ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
9	8	adantl 482	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
10		itg2cl 24906	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*)
11		xrrebnd 12911	. . . . . . . . . . . . . . 15 ⊢ ((∫2‘𝐹) ∈ ℝ* → ((∫2‘𝐹) ∈ ℝ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
12	10, 11	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) ∈ ℝ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
13		itg2ge0 24909	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℝ⟶(0[,]+∞) → 0 ≤ (∫2‘𝐹))
14		mnflt0 12870	. . . . . . . . . . . . . . . . 17 ⊢ -∞ < 0
15		mnfxr 11041	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ*
16		0xr 11031	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ*
17		xrltletr 12900	. . . . . . . . . . . . . . . . . 18 ⊢ ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ < (∫2‘𝐹)))
18	15, 16, 10, 17	mp3an12i 1464	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ < (∫2‘𝐹)))
19	14, 18	mpani 693	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (0 ≤ (∫2‘𝐹) → -∞ < (∫2‘𝐹)))
20	13, 19	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → -∞ < (∫2‘𝐹))
21	20	biantrurd 533	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) < +∞ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
22		nltpnft 12907	. . . . . . . . . . . . . . . 16 ⊢ ((∫2‘𝐹) ∈ ℝ* → ((∫2‘𝐹) = +∞ ↔ ¬ (∫2‘𝐹) < +∞))
23	10, 22	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) = +∞ ↔ ¬ (∫2‘𝐹) < +∞))
24	23	con2bid 355	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) < +∞ ↔ ¬ (∫2‘𝐹) = +∞))
25	12, 21, 24	3bitr2rd 308	. . . . . . . . . . . . 13 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (¬ (∫2‘𝐹) = +∞ ↔ (∫2‘𝐹) ∈ ℝ))
26	25	biimpa 477	. . . . . . . . . . . 12 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
27	26	adantlr 712	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
28		nnrp 12750	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
29	28	rpreccld 12791	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
30	29	ad2antlr 724	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (1 / 𝑛) ∈ ℝ+)
31	27, 30	ltsubrpd 12813	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − (1 / 𝑛)) < (∫2‘𝐹))
32	9, 31	eqbrtrd 5097	. . . . . . . . 9 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
33	7, 32	pm2.61dan 810	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
34		nnrecre 12024	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
35	34	ad2antlr 724	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (1 / 𝑛) ∈ ℝ)
36	27, 35	resubcld 11412	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − (1 / 𝑛)) ∈ ℝ)
37	2, 36	ifclda 4495	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ)
38	37	rexrd 11034	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
39	10	adantr 481	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (∫2‘𝐹) ∈ ℝ*)
40		xrltnle 11051	. . . . . . . . 9 ⊢ ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
41	38, 39, 40	syl2anc 584	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
42	33, 41	mpbid 231	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
43		itg2leub 24908	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) → ((∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
44	38, 43	syldan 591	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ((∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
45	42, 44	mtbid 324	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ¬ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
46		rexanali 3193	. . . . . 6 ⊢ (∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))) ↔ ¬ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
47	45, 46	sylibr 233	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
48		itg1cl 24858	. . . . . . . 8 ⊢ (𝑓 ∈ dom ∫1 → (∫1‘𝑓) ∈ ℝ)
49		ltnle 11063	. . . . . . . 8 ⊢ ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ ∧ (∫1‘𝑓) ∈ ℝ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
50	37, 48, 49	syl2an 596	. . . . . . 7 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑓 ∈ dom ∫1) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
51	50	anbi2d 629	. . . . . 6 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑓 ∈ dom ∫1) → ((𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ (𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
52	51	rexbidva 3226	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
53	47, 52	mpbird 256	. . . 4 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)))
54	53	ralrimiva 3104	. . 3 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ∀𝑛 ∈ ℕ ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)))
55		ovex 7317	. . . . 5 ⊢ (ℝ ↑m ℝ) ∈ V
56		i1ff 24849	. . . . . . 7 ⊢ (𝑥 ∈ dom ∫1 → 𝑥:ℝ⟶ℝ)
57		reex 10971	. . . . . . . 8 ⊢ ℝ ∈ V
58	57, 57	elmap 8668	. . . . . . 7 ⊢ (𝑥 ∈ (ℝ ↑m ℝ) ↔ 𝑥:ℝ⟶ℝ)
59	56, 58	sylibr 233	. . . . . 6 ⊢ (𝑥 ∈ dom ∫1 → 𝑥 ∈ (ℝ ↑m ℝ))
60	59	ssriv 3926	. . . . 5 ⊢ dom ∫1 ⊆ (ℝ ↑m ℝ)
61	55, 60	ssexi 5247	. . . 4 ⊢ dom ∫1 ∈ V
62		nnenom 13709	. . . 4 ⊢ ℕ ≈ ω
63		breq1 5078	. . . . 5 ⊢ (𝑓 = (𝑔‘𝑛) → (𝑓 ∘r ≤ 𝐹 ↔ (𝑔‘𝑛) ∘r ≤ 𝐹))
64		fveq2 6783	. . . . . 6 ⊢ (𝑓 = (𝑔‘𝑛) → (∫1‘𝑓) = (∫1‘(𝑔‘𝑛)))
65	64	breq2d 5087	. . . . 5 ⊢ (𝑓 = (𝑔‘𝑛) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))
66	63, 65	anbi12d 631	. . . 4 ⊢ (𝑓 = (𝑔‘𝑛) → ((𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))))
67	61, 62, 66	axcc4 10204	. . 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 768	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → 𝑔:ℕ⟶dom ∫1)
70		simpl 483	. . . . . . 7 ⊢ (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → (𝑔‘𝑛) ∘r ≤ 𝐹)
71	70	ralimi 3088	. . . . . 6 ⊢ (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹)
72	71	ad2antll 726	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹)
73	10	adantr 481	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ∈ ℝ*)
74		ffvelrn 6968	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ dom ∫1)
75		itg1cl 24858	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑛) ∈ dom ∫1 → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
76	74, 75	syl 17	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
77	76	fmpttd 6998	. . . . . . . . . 10 ⊢ (𝑔:ℕ⟶dom ∫1 → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
78	77	ad2antrl 725	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
79	78	frnd 6617	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ)
80		ressxr 11028	. . . . . . . 8 ⊢ ℝ ⊆ ℝ*
81	79, 80	sstrdi 3934	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
82		supxrcl 13058	. . . . . . 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 712	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
85	76	adantll 711	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
86	85	rexrd 11034	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ*)
87		xrltle 12892	. . . . . . . . . . . . 13 ⊢ ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ* ∧ (∫1‘(𝑔‘𝑛)) ∈ ℝ*) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛))))
88	84, 86, 87	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛))))
89		2fveq3 6788	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (∫1‘(𝑔‘𝑛)) = (∫1‘(𝑔‘𝑚)))
90	89	cbvmptv 5188	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
91	90	rneqi 5849	. . . . . . . . . . . . . . 15 ⊢ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
92	77	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
93	92	frnd 6617	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ)
94	93, 80	sstrdi 3934	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
95	94	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
96	91, 95	eqsstrrid 3971	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) ⊆ ℝ*)
97		2fveq3 6788	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (∫1‘(𝑔‘𝑚)) = (∫1‘(𝑔‘𝑛)))
98		eqid 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) = (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
99		fvex 6796	. . . . . . . . . . . . . . . . 17 ⊢ (∫1‘(𝑔‘𝑛)) ∈ V
100	97, 98, 99	fvmpt 6884	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) = (∫1‘(𝑔‘𝑛)))
101		fvex 6796	. . . . . . . . . . . . . . . . . 18 ⊢ (∫1‘(𝑔‘𝑚)) ∈ V
102	101, 98	fnmpti 6585	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) Fn ℕ
103		fnfvelrn 6967	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) Fn ℕ ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
104	102, 103	mpan 687	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
105	100, 104	eqeltrrd 2841	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
106	105	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
107		supxrub 13067	. . . . . . . . . . . . . 14 ⊢ ((ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) ⊆ ℝ* ∧ (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))) → (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
108	96, 106, 107	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
109	91	supeq1i 9215	. . . . . . . . . . . . . . 15 ⊢ sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )
110	95, 82	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈ ℝ*)
111	109, 110	eqeltrrid 2845	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈ ℝ*)
112		xrletr 12901	. . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛)) ∧ (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
114	108, 113	mpan2d 691	. . . . . . . . . . . 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 491	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
117	116	ralimdva 3109	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
118	117	impr 455	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
119		breq2 5079	. . . . . . . . . . 11 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
120	119	ralbidv 3113	. . . . . . . . . 10 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
121		breq2 5079	. . . . . . . . . 10 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → ((∫2‘𝐹) ≤ 𝑥 ↔ (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
122	120, 121	imbi12d 345	. . . . . . . . 9 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → ((∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥) ↔ (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))))
123		elxr 12861	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ* ↔ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞))
124		simplrl 774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → 𝑥 ∈ ℝ)
125		arch 12239	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → ∃𝑛 ∈ ℕ 𝑥 < 𝑛)
126	124, 125	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < 𝑛)
127	4	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
128	127	breq2d 5087	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ 𝑥 < 𝑛))
129	128	rexbidv 3227	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ 𝑥 < 𝑛))
130	126, 129	mpbird 256	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
131	26	adantlr 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
132		simplrl 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 𝑥 ∈ ℝ)
133	131, 132	resubcld 11412	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − 𝑥) ∈ ℝ)
134		simplrr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 𝑥 < (∫2‘𝐹))
135	132, 131	posdifd 11571	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (𝑥 < (∫2‘𝐹) ↔ 0 < ((∫2‘𝐹) − 𝑥)))
136	134, 135	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 0 < ((∫2‘𝐹) − 𝑥))
137		nnrecl 12240	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((∫2‘𝐹) − 𝑥) ∈ ℝ ∧ 0 < ((∫2‘𝐹) − 𝑥)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥))
138	133, 136, 137	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥))
139	34	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
140	131	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (∫2‘𝐹) ∈ ℝ)
141	132	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
142		ltsub13 11465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1 / 𝑛) ∈ ℝ ∧ (∫2‘𝐹) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
143	139, 140, 141, 142	syl3anc 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
144	8	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
145	144	breq2d 5087	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
146	143, 145	bitr4d 281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
147	146	rexbidva 3226	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
148	138, 147	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
149	130, 148	pm2.61dan 810	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
150	149	expr 457	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < (∫2‘𝐹) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
151		rexr 11030	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
152		xrltnle 11051	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → (𝑥 < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ 𝑥))
153	151, 10, 152	syl2anr 597	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ 𝑥))
154	151	ad2antlr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ*)
155	38	adantlr 712	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
156		xrltnle 11051	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ* ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
157	154, 155, 156	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
158	157	rexbidva 3226	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
159		rexnal 3170	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑛 ∈ ℕ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ¬ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
160	158, 159	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
161	150, 153, 160	3imtr3d 293	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (¬ (∫2‘𝐹) ≤ 𝑥 → ¬ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
162	161	con4d 115	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
163	10	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ∈ ℝ*)
164		pnfge 12875	. . . . . . . . . . . . . . . 16 ⊢ ((∫2‘𝐹) ∈ ℝ* → (∫2‘𝐹) ≤ +∞)
165	163, 164	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ≤ +∞)
166		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → 𝑥 = +∞)
167	165, 166	breqtrrd 5103	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ≤ 𝑥)
168	167	a1d 25	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
169		1nn 11993	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ
170	169	ne0ii 4272	. . . . . . . . . . . . . . 15 ⊢ ℕ ≠ ∅
171		r19.2z 4426	. . . . . . . . . . . . . . 15 ⊢ ((ℕ ≠ ∅ ∧ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥) → ∃𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
172	170, 171	mpan 687	. . . . . . . . . . . . . 14 ⊢ (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → ∃𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
173	37	adantlr 712	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ)
174		mnflt 12868	. . . . . . . . . . . . . . . . . . 19 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → -∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
175		rexr 11030	. . . . . . . . . . . . . . . . . . . 20 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
176		xrltnle 11051	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-∞ ∈ ℝ* ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) → (-∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞))
177	15, 175, 176	sylancr 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → (-∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞))
178	174, 177	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞)
179	173, 178	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞)
180		simplr 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → 𝑥 = -∞)
181	180	breq2d 5087	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞))
182	179, 181	mtbird 325	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
183	182	nrexdv 3199	. . . . . . . . . . . . . . 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 1429	. . . . . . . . . . . 12 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞)) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
187	123, 186	sylan2b 594	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ*) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
188	187	ralrimiva 3104	. . . . . . . . . 10 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
189	188	adantr 481	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
190	109, 83	eqeltrrid 2845	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈ ℝ*)
191	122, 189, 190	rspcdva 3563	. . . . . . . 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 5117	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))
194		itg2ub 24907	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔‘𝑛) ∈ dom ∫1 ∧ (𝑔‘𝑛) ∘r ≤ 𝐹) → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
195	194	3expia 1120	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔‘𝑛) ∈ dom ∫1) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
196	74, 195	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ)) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
197	196	anassrs 468	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
198	197	adantrd 492	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
199	198	ralimdva 3109	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
200	199	impr 455	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
201		eqid 2739	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))
202	89, 201, 101	fvmpt 6884	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) = (∫1‘(𝑔‘𝑚)))
203	202	breq1d 5085	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹)))
204	203	ralbiia 3092	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹))
205	89	breq1d 5085	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → ((∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹) ↔ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹)))
206	205	cbvralvw 3384	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹))
207	204, 206	bitr4i 277	. . . . . . . . 9 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
208	200, 207	sylibr 233	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹))
209		ffn 6609	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) Fn ℕ)
210		breq1 5078	. . . . . . . . . 10 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) → (𝑧 ≤ (∫2‘𝐹) ↔ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹)))
211	210	ralrn 6973	. . . . . . . . 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 256	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹))
214		supxrleub 13069	. . . . . . . 8 ⊢ ((ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → (sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤ (∫2‘𝐹) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹)))
215	81, 73, 214	syl2anc 584	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤ (∫2‘𝐹) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹)))
216	213, 215	mpbird 256	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤ (∫2‘𝐹))
217	73, 83, 193, 216	xrletrid 12898	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))
218	69, 72, 217	3jca 1127	. . . 4 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < )))
219	218	ex 413	. . 3 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))) → (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))))
220	219	eximdv 1921	. 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 205   ∧ wa 396   ∨ w3o 1085   ∧ w3a 1086   = wceq 1539  ∃wex 1782   ∈ wcel 2107   ≠ wne 2944  ∀wral 3065  ∃wrex 3066   ⊆ wss 3888  ∅c0 4257  ifcif 4460   class class class wbr 5075   ↦ cmpt 5158  dom cdm 5590  ran crn 5591   Fn wfn 6432  ⟶wf 6433  ‘cfv 6437  (class class class)co 7284   ∘_r cofr 7541   ↑_m cmap 8624  supcsup 9208  ℝcr 10879  0cc0 10880  1c1 10881  +∞cpnf 11015  -∞cmnf 11016  ℝ^*cxr 11017   < clt 11018   ≤ cle 11019   − cmin 11214   / cdiv 11641  ℕcn 11982  ℝ⁺crp 12739  [,]cicc 13091  ∫₁citg1 24788  ∫₂citg2 24789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cc 10200  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-ofr 7543  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-er 8507  df-map 8626  df-pm 8627  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-sup 9210  df-inf 9211  df-oi 9278  df-dju 9668  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-n0 12243  df-z 12329  df-uz 12592  df-q 12698  df-rp 12740  df-xadd 12858  df-ioo 13092  df-ico 13094  df-icc 13095  df-fz 13249  df-fzo 13392  df-fl 13521  df-seq 13731  df-exp 13792  df-hash 14054  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-clim 15206  df-sum 15407  df-xmet 20599  df-met 20600  df-ovol 24637  df-vol 24638  df-mbf 24792  df-itg1 24793  df-itg2 24794

This theorem is referenced by: (None)