Theorem itg2seq 25643

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 25656, 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 12193	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
2	1	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → 𝑛 ∈ ℝ)
3	2	ltpnfd 13081	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → 𝑛 < +∞)
4		iftrue 4494	. . . . . . . . . . 11 ⊢ ((∫2‘𝐹) = +∞ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
5	4	adantl 481	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
6		simpr 484	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → (∫2‘𝐹) = +∞)
7	3, 5, 6	3brtr4d 5139	. . . . . . . . 9 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
8		iffalse 4497	. . . . . . . . . . 11 ⊢ (¬ (∫2‘𝐹) = +∞ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
9	8	adantl 481	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
10		itg2cl 25633	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*)
11		xrrebnd 13128	. . . . . . . . . . . . . . 15 ⊢ ((∫2‘𝐹) ∈ ℝ* → ((∫2‘𝐹) ∈ ℝ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
12	10, 11	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) ∈ ℝ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
13		itg2ge0 25636	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℝ⟶(0[,]+∞) → 0 ≤ (∫2‘𝐹))
14		mnflt0 13085	. . . . . . . . . . . . . . . . 17 ⊢ -∞ < 0
15		mnfxr 11231	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ*
16		0xr 11221	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ*
17		xrltletr 13117	. . . . . . . . . . . . . . . . . 18 ⊢ ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ < (∫2‘𝐹)))
18	15, 16, 10, 17	mp3an12i 1467	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ < (∫2‘𝐹)))
19	14, 18	mpani 696	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (0 ≤ (∫2‘𝐹) → -∞ < (∫2‘𝐹)))
20	13, 19	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → -∞ < (∫2‘𝐹))
21	20	biantrurd 532	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) < +∞ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
22		nltpnft 13124	. . . . . . . . . . . . . . . 16 ⊢ ((∫2‘𝐹) ∈ ℝ* → ((∫2‘𝐹) = +∞ ↔ ¬ (∫2‘𝐹) < +∞))
23	10, 22	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) = +∞ ↔ ¬ (∫2‘𝐹) < +∞))
24	23	con2bid 354	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) < +∞ ↔ ¬ (∫2‘𝐹) = +∞))
25	12, 21, 24	3bitr2rd 308	. . . . . . . . . . . . 13 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (¬ (∫2‘𝐹) = +∞ ↔ (∫2‘𝐹) ∈ ℝ))
26	25	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
27	26	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
28		nnrp 12963	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
29	28	rpreccld 13005	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
30	29	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (1 / 𝑛) ∈ ℝ+)
31	27, 30	ltsubrpd 13027	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − (1 / 𝑛)) < (∫2‘𝐹))
32	9, 31	eqbrtrd 5129	. . . . . . . . 9 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
33	7, 32	pm2.61dan 812	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
34		nnrecre 12228	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
35	34	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (1 / 𝑛) ∈ ℝ)
36	27, 35	resubcld 11606	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − (1 / 𝑛)) ∈ ℝ)
37	2, 36	ifclda 4524	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ)
38	37	rexrd 11224	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
39	10	adantr 480	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (∫2‘𝐹) ∈ ℝ*)
40		xrltnle 11241	. . . . . . . . 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 232	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
43		itg2leub 25635	. . . . . . . 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 3084	. . . . . 6 ⊢ (∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))) ↔ ¬ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
47	45, 46	sylibr 234	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
48		itg1cl 25586	. . . . . . . 8 ⊢ (𝑓 ∈ dom ∫1 → (∫1‘𝑓) ∈ ℝ)
49		ltnle 11253	. . . . . . . 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 630	. . . . . 6 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑓 ∈ dom ∫1) → ((𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ (𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
52	51	rexbidva 3155	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
53	47, 52	mpbird 257	. . . 4 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)))
54	53	ralrimiva 3125	. . 3 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ∀𝑛 ∈ ℕ ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)))
55		ovex 7420	. . . . 5 ⊢ (ℝ ↑m ℝ) ∈ V
56		i1ff 25577	. . . . . . 7 ⊢ (𝑥 ∈ dom ∫1 → 𝑥:ℝ⟶ℝ)
57		reex 11159	. . . . . . . 8 ⊢ ℝ ∈ V
58	57, 57	elmap 8844	. . . . . . 7 ⊢ (𝑥 ∈ (ℝ ↑m ℝ) ↔ 𝑥:ℝ⟶ℝ)
59	56, 58	sylibr 234	. . . . . 6 ⊢ (𝑥 ∈ dom ∫1 → 𝑥 ∈ (ℝ ↑m ℝ))
60	59	ssriv 3950	. . . . 5 ⊢ dom ∫1 ⊆ (ℝ ↑m ℝ)
61	55, 60	ssexi 5277	. . . 4 ⊢ dom ∫1 ∈ V
62		nnenom 13945	. . . 4 ⊢ ℕ ≈ ω
63		breq1 5110	. . . . 5 ⊢ (𝑓 = (𝑔‘𝑛) → (𝑓 ∘r ≤ 𝐹 ↔ (𝑔‘𝑛) ∘r ≤ 𝐹))
64		fveq2 6858	. . . . . 6 ⊢ (𝑓 = (𝑔‘𝑛) → (∫1‘𝑓) = (∫1‘(𝑔‘𝑛)))
65	64	breq2d 5119	. . . . 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 10392	. . 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 770	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → 𝑔:ℕ⟶dom ∫1)
70		simpl 482	. . . . . . 7 ⊢ (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → (𝑔‘𝑛) ∘r ≤ 𝐹)
71	70	ralimi 3066	. . . . . 6 ⊢ (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹)
72	71	ad2antll 729	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹)
73	10	adantr 480	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ∈ ℝ*)
74		ffvelcdm 7053	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ dom ∫1)
75		itg1cl 25586	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑛) ∈ dom ∫1 → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
76	74, 75	syl 17	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
77	76	fmpttd 7087	. . . . . . . . . 10 ⊢ (𝑔:ℕ⟶dom ∫1 → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
78	77	ad2antrl 728	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
79	78	frnd 6696	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ)
80		ressxr 11218	. . . . . . . 8 ⊢ ℝ ⊆ ℝ*
81	79, 80	sstrdi 3959	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
82		supxrcl 13275	. . . . . . 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 715	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
85	76	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
86	85	rexrd 11224	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ*)
87		xrltle 13109	. . . . . . . . . . . . 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 6863	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (∫1‘(𝑔‘𝑛)) = (∫1‘(𝑔‘𝑚)))
90	89	cbvmptv 5211	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
91	90	rneqi 5901	. . . . . . . . . . . . . . 15 ⊢ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
92	77	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
93	92	frnd 6696	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ)
94	93, 80	sstrdi 3959	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
95	94	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
96	91, 95	eqsstrrid 3986	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) ⊆ ℝ*)
97		2fveq3 6863	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (∫1‘(𝑔‘𝑚)) = (∫1‘(𝑔‘𝑛)))
98		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) = (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
99		fvex 6871	. . . . . . . . . . . . . . . . 17 ⊢ (∫1‘(𝑔‘𝑛)) ∈ V
100	97, 98, 99	fvmpt 6968	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) = (∫1‘(𝑔‘𝑛)))
101		fvex 6871	. . . . . . . . . . . . . . . . . 18 ⊢ (∫1‘(𝑔‘𝑚)) ∈ V
102	101, 98	fnmpti 6661	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) Fn ℕ
103		fnfvelrn 7052	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) Fn ℕ ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
104	102, 103	mpan 690	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
105	100, 104	eqeltrrd 2829	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
106	105	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
107		supxrub 13284	. . . . . . . . . . . . . 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 9398	. . . . . . . . . . . . . . 15 ⊢ sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )
110	95, 82	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈ ℝ*)
111	109, 110	eqeltrrid 2833	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈ ℝ*)
112		xrletr 13118	. . . . . . . . . . . . . 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 1373	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛)) ∧ (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
114	108, 113	mpan2d 694	. . . . . . . . . . . 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 490	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
117	116	ralimdva 3145	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
118	117	impr 454	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
119		breq2 5111	. . . . . . . . . . 11 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
120	119	ralbidv 3156	. . . . . . . . . 10 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
121		breq2 5111	. . . . . . . . . 10 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → ((∫2‘𝐹) ≤ 𝑥 ↔ (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
122	120, 121	imbi12d 344	. . . . . . . . 9 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → ((∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥) ↔ (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))))
123		elxr 13076	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ* ↔ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞))
124		simplrl 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → 𝑥 ∈ ℝ)
125		arch 12439	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → ∃𝑛 ∈ ℕ 𝑥 < 𝑛)
126	124, 125	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < 𝑛)
127	4	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
128	127	breq2d 5119	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ 𝑥 < 𝑛))
129	128	rexbidv 3157	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ 𝑥 < 𝑛))
130	126, 129	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
131	26	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
132		simplrl 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 𝑥 ∈ ℝ)
133	131, 132	resubcld 11606	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − 𝑥) ∈ ℝ)
134		simplrr 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 𝑥 < (∫2‘𝐹))
135	132, 131	posdifd 11765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (𝑥 < (∫2‘𝐹) ↔ 0 < ((∫2‘𝐹) − 𝑥)))
136	134, 135	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 0 < ((∫2‘𝐹) − 𝑥))
137		nnrecl 12440	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((∫2‘𝐹) − 𝑥) ∈ ℝ ∧ 0 < ((∫2‘𝐹) − 𝑥)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥))
138	133, 136, 137	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥))
139	34	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
140	131	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (∫2‘𝐹) ∈ ℝ)
141	132	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
142		ltsub13 11659	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1 / 𝑛) ∈ ℝ ∧ (∫2‘𝐹) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
143	139, 140, 141, 142	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
144	8	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
145	144	breq2d 5119	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
146	143, 145	bitr4d 282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
147	146	rexbidva 3155	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
148	138, 147	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
149	130, 148	pm2.61dan 812	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
150	149	expr 456	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < (∫2‘𝐹) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
151		rexr 11220	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
152		xrltnle 11241	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → (𝑥 < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ 𝑥))
153	151, 10, 152	syl2anr 597	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ 𝑥))
154	151	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ*)
155	38	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
156		xrltnle 11241	. . . . . . . . . . . . . . . . . 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 3155	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
159		rexnal 3082	. . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ∈ ℝ*)
164		pnfge 13090	. . . . . . . . . . . . . . . 16 ⊢ ((∫2‘𝐹) ∈ ℝ* → (∫2‘𝐹) ≤ +∞)
165	163, 164	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ≤ +∞)
166		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → 𝑥 = +∞)
167	165, 166	breqtrrd 5135	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ≤ 𝑥)
168	167	a1d 25	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
169		1nn 12197	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ
170	169	ne0ii 4307	. . . . . . . . . . . . . . 15 ⊢ ℕ ≠ ∅
171		r19.2z 4458	. . . . . . . . . . . . . . 15 ⊢ ((ℕ ≠ ∅ ∧ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥) → ∃𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
172	170, 171	mpan 690	. . . . . . . . . . . . . 14 ⊢ (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → ∃𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
173	37	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ)
174		mnflt 13083	. . . . . . . . . . . . . . . . . . 19 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → -∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
175		rexr 11220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
176		xrltnle 11241	. . . . . . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . . . . . 18 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞)
179	173, 178	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞)
180		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → 𝑥 = -∞)
181	180	breq2d 5119	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞))
182	179, 181	mtbird 325	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
183	182	nrexdv 3128	. . . . . . . . . . . . . . 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 1433	. . . . . . . . . . . 12 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞)) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
187	123, 186	sylan2b 594	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ*) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
188	187	ralrimiva 3125	. . . . . . . . . 10 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
189	188	adantr 480	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
190	109, 83	eqeltrrid 2833	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈ ℝ*)
191	122, 189, 190	rspcdva 3589	. . . . . . . 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 5149	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))
194		itg2ub 25634	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔‘𝑛) ∈ dom ∫1 ∧ (𝑔‘𝑛) ∘r ≤ 𝐹) → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
195	194	3expia 1121	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔‘𝑛) ∈ dom ∫1) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
196	74, 195	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ)) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
197	196	anassrs 467	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
198	197	adantrd 491	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
199	198	ralimdva 3145	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
200	199	impr 454	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
201		eqid 2729	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))
202	89, 201, 101	fvmpt 6968	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) = (∫1‘(𝑔‘𝑚)))
203	202	breq1d 5117	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹)))
204	203	ralbiia 3073	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹))
205	89	breq1d 5117	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → ((∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹) ↔ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹)))
206	205	cbvralvw 3215	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹))
207	204, 206	bitr4i 278	. . . . . . . . 9 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
208	200, 207	sylibr 234	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹))
209		ffn 6688	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) Fn ℕ)
210		breq1 5110	. . . . . . . . . 10 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) → (𝑧 ≤ (∫2‘𝐹) ↔ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹)))
211	210	ralrn 7060	. . . . . . . . 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 257	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹))
214		supxrleub 13286	. . . . . . . 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 257	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤ (∫2‘𝐹))
217	73, 83, 193, 216	xrletrid 13115	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))
218	69, 72, 217	3jca 1128	. . . 4 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < )))
219	218	ex 412	. . 3 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))) → (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))))
220	219	eximdv 1917	. 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 206   ∧ wa 395   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053   ⊆ wss 3914  ∅c0 4296  ifcif 4488   class class class wbr 5107   ↦ cmpt 5188  dom cdm 5638  ran crn 5639   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387   ∘_r cofr 7652   ↑_m cmap 8799  supcsup 9391  ℝcr 11067  0cc0 11068  1c1 11069  +∞cpnf 11205  -∞cmnf 11206  ℝ^*cxr 11207   < clt 11208   ≤ cle 11209   − cmin 11405   / cdiv 11835  ℕcn 12186  ℝ⁺crp 12951  [,]cicc 13309  ∫₁citg1 25516  ∫₂citg2 25517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-inf2 9594  ax-cc 10388  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145  ax-pre-sup 11146

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-of 7653  df-ofr 7654  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-2o 8435  df-er 8671  df-map 8801  df-pm 8802  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-sup 9393  df-inf 9394  df-oi 9463  df-dju 9854  df-card 9892  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-div 11836  df-nn 12187  df-2 12249  df-3 12250  df-n0 12443  df-z 12530  df-uz 12794  df-q 12908  df-rp 12952  df-xadd 13073  df-ioo 13310  df-ico 13312  df-icc 13313  df-fz 13469  df-fzo 13616  df-fl 13754  df-seq 13967  df-exp 14027  df-hash 14296  df-cj 15065  df-re 15066  df-im 15067  df-sqrt 15201  df-abs 15202  df-clim 15454  df-sum 15653  df-xmet 21257  df-met 21258  df-ovol 25365  df-vol 25366  df-mbf 25520  df-itg1 25521  df-itg2 25522

This theorem is referenced by: (None)