Theorem itg2seq 24346

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 24359, 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 11632	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
2	1	ad2antlr 726	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → 𝑛 ∈ ℝ)
3	2	ltpnfd 12504	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → 𝑛 < +∞)
4		iftrue 4431	. . . . . . . . . . 11 ⊢ ((∫2‘𝐹) = +∞ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
5	4	adantl 485	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
6		simpr 488	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → (∫2‘𝐹) = +∞)
7	3, 5, 6	3brtr4d 5062	. . . . . . . . 9 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
8		iffalse 4434	. . . . . . . . . . 11 ⊢ (¬ (∫2‘𝐹) = +∞ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
9	8	adantl 485	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
10		itg2cl 24336	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*)
11		xrrebnd 12549	. . . . . . . . . . . . . . 15 ⊢ ((∫2‘𝐹) ∈ ℝ* → ((∫2‘𝐹) ∈ ℝ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
12	10, 11	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) ∈ ℝ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
13		itg2ge0 24339	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℝ⟶(0[,]+∞) → 0 ≤ (∫2‘𝐹))
14		mnflt0 12508	. . . . . . . . . . . . . . . . 17 ⊢ -∞ < 0
15		mnfxr 10687	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ*
16		0xr 10677	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ*
17		xrltletr 12538	. . . . . . . . . . . . . . . . . 18 ⊢ ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ < (∫2‘𝐹)))
18	15, 16, 10, 17	mp3an12i 1462	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ < (∫2‘𝐹)))
19	14, 18	mpani 695	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (0 ≤ (∫2‘𝐹) → -∞ < (∫2‘𝐹)))
20	13, 19	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → -∞ < (∫2‘𝐹))
21	20	biantrurd 536	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) < +∞ ↔ (-∞ < (∫2‘𝐹) ∧ (∫2‘𝐹) < +∞)))
22		nltpnft 12545	. . . . . . . . . . . . . . . 16 ⊢ ((∫2‘𝐹) ∈ ℝ* → ((∫2‘𝐹) = +∞ ↔ ¬ (∫2‘𝐹) < +∞))
23	10, 22	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) = +∞ ↔ ¬ (∫2‘𝐹) < +∞))
24	23	con2bid 358	. . . . . . . . . . . . . 14 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ((∫2‘𝐹) < +∞ ↔ ¬ (∫2‘𝐹) = +∞))
25	12, 21, 24	3bitr2rd 311	. . . . . . . . . . . . 13 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (¬ (∫2‘𝐹) = +∞ ↔ (∫2‘𝐹) ∈ ℝ))
26	25	biimpa 480	. . . . . . . . . . . 12 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
27	26	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
28		nnrp 12388	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
29	28	rpreccld 12429	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
30	29	ad2antlr 726	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (1 / 𝑛) ∈ ℝ+)
31	27, 30	ltsubrpd 12451	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − (1 / 𝑛)) < (∫2‘𝐹))
32	9, 31	eqbrtrd 5052	. . . . . . . . 9 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
33	7, 32	pm2.61dan 812	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹))
34		nnrecre 11667	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
35	34	ad2antlr 726	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → (1 / 𝑛) ∈ ℝ)
36	27, 35	resubcld 11057	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − (1 / 𝑛)) ∈ ℝ)
37	2, 36	ifclda 4459	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ)
38	37	rexrd 10680	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
39	10	adantr 484	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (∫2‘𝐹) ∈ ℝ*)
40		xrltnle 10697	. . . . . . . . 9 ⊢ ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
41	38, 39, 40	syl2anc 587	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
42	33, 41	mpbid 235	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
43		itg2leub 24338	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) → ((∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
44	38, 43	syldan 594	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ((∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
45	42, 44	mtbid 327	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ¬ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
46		rexanali 3224	. . . . . 6 ⊢ (∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))) ↔ ¬ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 → (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
47	45, 46	sylibr 237	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
48		itg1cl 24289	. . . . . . . 8 ⊢ (𝑓 ∈ dom ∫1 → (∫1‘𝑓) ∈ ℝ)
49		ltnle 10709	. . . . . . . 8 ⊢ ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ ∧ (∫1‘𝑓) ∈ ℝ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
50	37, 48, 49	syl2an 598	. . . . . . 7 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑓 ∈ dom ∫1) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
51	50	anbi2d 631	. . . . . 6 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑓 ∈ dom ∫1) → ((𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ (𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
52	51	rexbidva 3255	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))))
53	47, 52	mpbird 260	. . . 4 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)))
54	53	ralrimiva 3149	. . 3 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ∀𝑛 ∈ ℕ ∃𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)))
55		ovex 7168	. . . . 5 ⊢ (ℝ ↑m ℝ) ∈ V
56		i1ff 24280	. . . . . . 7 ⊢ (𝑥 ∈ dom ∫1 → 𝑥:ℝ⟶ℝ)
57		reex 10617	. . . . . . . 8 ⊢ ℝ ∈ V
58	57, 57	elmap 8418	. . . . . . 7 ⊢ (𝑥 ∈ (ℝ ↑m ℝ) ↔ 𝑥:ℝ⟶ℝ)
59	56, 58	sylibr 237	. . . . . 6 ⊢ (𝑥 ∈ dom ∫1 → 𝑥 ∈ (ℝ ↑m ℝ))
60	59	ssriv 3919	. . . . 5 ⊢ dom ∫1 ⊆ (ℝ ↑m ℝ)
61	55, 60	ssexi 5190	. . . 4 ⊢ dom ∫1 ∈ V
62		nnenom 13343	. . . 4 ⊢ ℕ ≈ ω
63		breq1 5033	. . . . 5 ⊢ (𝑓 = (𝑔‘𝑛) → (𝑓 ∘r ≤ 𝐹 ↔ (𝑔‘𝑛) ∘r ≤ 𝐹))
64		fveq2 6645	. . . . . 6 ⊢ (𝑓 = (𝑔‘𝑛) → (∫1‘𝑓) = (∫1‘(𝑔‘𝑛)))
65	64	breq2d 5042	. . . . 5 ⊢ (𝑓 = (𝑔‘𝑛) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))
66	63, 65	anbi12d 633	. . . 4 ⊢ (𝑓 = (𝑔‘𝑛) → ((𝑓 ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))))
67	61, 62, 66	axcc4 9850	. . 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 486	. . . . . . 7 ⊢ (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → (𝑔‘𝑛) ∘r ≤ 𝐹)
71	70	ralimi 3128	. . . . . 6 ⊢ (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹)
72	71	ad2antll 728	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹)
73	10	adantr 484	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ∈ ℝ*)
74		ffvelrn 6826	. . . . . . . . . . . 12 ⊢ ((𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ dom ∫1)
75		itg1cl 24289	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑛) ∈ dom ∫1 → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
76	74, 75	syl 17	. . . . . . . . . . 11 ⊢ ((𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
77	76	fmpttd 6856	. . . . . . . . . 10 ⊢ (𝑔:ℕ⟶dom ∫1 → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
78	77	ad2antrl 727	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
79	78	frnd 6494	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ)
80		ressxr 10674	. . . . . . . 8 ⊢ ℝ ⊆ ℝ*
81	79, 80	sstrdi 3927	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
82		supxrcl 12696	. . . . . . 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 714	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
85	76	adantll 713	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ)
86	85	rexrd 10680	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ*)
87		xrltle 12530	. . . . . . . . . . . . 13 ⊢ ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ* ∧ (∫1‘(𝑔‘𝑛)) ∈ ℝ*) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛))))
88	84, 86, 87	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛))))
89		2fveq3 6650	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (∫1‘(𝑔‘𝑛)) = (∫1‘(𝑔‘𝑚)))
90	89	cbvmptv 5133	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
91	90	rneqi 5771	. . . . . . . . . . . . . . 15 ⊢ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
92	77	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ)
93	92	frnd 6494	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ)
94	93, 80	sstrdi 3927	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
95	94	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ*)
96	91, 95	eqsstrrid 3964	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) ⊆ ℝ*)
97		2fveq3 6650	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (∫1‘(𝑔‘𝑚)) = (∫1‘(𝑔‘𝑛)))
98		eqid 2798	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) = (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))
99		fvex 6658	. . . . . . . . . . . . . . . . 17 ⊢ (∫1‘(𝑔‘𝑛)) ∈ V
100	97, 98, 99	fvmpt 6745	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) = (∫1‘(𝑔‘𝑛)))
101		fvex 6658	. . . . . . . . . . . . . . . . . 18 ⊢ (∫1‘(𝑔‘𝑚)) ∈ V
102	101, 98	fnmpti 6463	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) Fn ℕ
103		fnfvelrn 6825	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) Fn ℕ ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
104	102, 103	mpan 689	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
105	100, 104	eqeltrrd 2891	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
106	105	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))))
107		supxrub 12705	. . . . . . . . . . . . . 14 ⊢ ((ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))) ⊆ ℝ* ∧ (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚)))) → (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
108	96, 106, 107	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
109	91	supeq1i 8895	. . . . . . . . . . . . . . 15 ⊢ sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )
110	95, 82	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈ ℝ*)
111	109, 110	eqeltrrid 2895	. . . . . . . . . . . . . 14 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈ ℝ*)
112		xrletr 12539	. . . . . . . . . . . . . 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 1368	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛)) ∧ (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
114	108, 113	mpan2d 693	. . . . . . . . . . . 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 494	. . . . . . . . . 10 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
117	116	ralimdva 3144	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
118	117	impr 458	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))
119		breq2 5034	. . . . . . . . . . 11 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
120	119	ralbidv 3162	. . . . . . . . . 10 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
121		breq2 5034	. . . . . . . . . 10 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → ((∫2‘𝐹) ≤ 𝑥 ↔ (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < )))
122	120, 121	imbi12d 348	. . . . . . . . 9 ⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → ((∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥) ↔ (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) → (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ))))
123		elxr 12499	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ* ↔ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞))
124		simplrl 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → 𝑥 ∈ ℝ)
125		arch 11882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → ∃𝑛 ∈ ℕ 𝑥 < 𝑛)
126	124, 125	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < 𝑛)
127	4	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛)
128	127	breq2d 5042	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ 𝑥 < 𝑛))
129	128	rexbidv 3256	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ 𝑥 < 𝑛))
130	126, 129	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
131	26	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (∫2‘𝐹) ∈ ℝ)
132		simplrl 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 𝑥 ∈ ℝ)
133	131, 132	resubcld 11057	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ((∫2‘𝐹) − 𝑥) ∈ ℝ)
134		simplrr 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 𝑥 < (∫2‘𝐹))
135	132, 131	posdifd 11216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (𝑥 < (∫2‘𝐹) ↔ 0 < ((∫2‘𝐹) − 𝑥)))
136	134, 135	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → 0 < ((∫2‘𝐹) − 𝑥))
137		nnrecl 11883	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((∫2‘𝐹) − 𝑥) ∈ ℝ ∧ 0 < ((∫2‘𝐹) − 𝑥)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥))
138	133, 136, 137	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥))
139	34	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
140	131	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (∫2‘𝐹) ∈ ℝ)
141	132	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
142		ltsub13 11110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1 / 𝑛) ∈ ℝ ∧ (∫2‘𝐹) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
143	139, 140, 141, 142	syl3anc 1368	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
144	8	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛)))
145	144	breq2d 5042	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛))))
146	143, 145	bitr4d 285	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
147	146	rexbidva 3255	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → (∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
148	138, 147	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) ∧ ¬ (∫2‘𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
149	130, 148	pm2.61dan 812	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2‘𝐹))) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
150	149	expr 460	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < (∫2‘𝐹) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))
151		rexr 10676	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
152		xrltnle 10697	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → (𝑥 < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ 𝑥))
153	151, 10, 152	syl2anr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < (∫2‘𝐹) ↔ ¬ (∫2‘𝐹) ≤ 𝑥))
154	151	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ*)
155	38	adantlr 714	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
156		xrltnle 10697	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ* ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
157	154, 155, 156	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
158	157	rexbidva 3255	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
159		rexnal 3201	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑛 ∈ ℕ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ¬ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
160	158, 159	syl6bb 290	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
161	150, 153, 160	3imtr3d 296	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (¬ (∫2‘𝐹) ≤ 𝑥 → ¬ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥))
162	161	con4d 115	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
163	10	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ∈ ℝ*)
164		pnfge 12513	. . . . . . . . . . . . . . . 16 ⊢ ((∫2‘𝐹) ∈ ℝ* → (∫2‘𝐹) ≤ +∞)
165	163, 164	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ≤ +∞)
166		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → 𝑥 = +∞)
167	165, 166	breqtrrd 5058	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2‘𝐹) ≤ 𝑥)
168	167	a1d 25	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
169		1nn 11636	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ
170	169	ne0ii 4253	. . . . . . . . . . . . . . 15 ⊢ ℕ ≠ ∅
171		r19.2z 4398	. . . . . . . . . . . . . . 15 ⊢ ((ℕ ≠ ∅ ∧ ∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥) → ∃𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
172	170, 171	mpan 689	. . . . . . . . . . . . . 14 ⊢ (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → ∃𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
173	37	adantlr 714	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ)
174		mnflt 12506	. . . . . . . . . . . . . . . . . . 19 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → -∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))
175		rexr 10676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*)
176		xrltnle 10697	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-∞ ∈ ℝ* ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) → (-∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞))
177	15, 175, 176	sylancr 590	. . . . . . . . . . . . . . . . . . 19 ⊢ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → (-∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞))
178	174, 177	mpbid 235	. . . . . . . . . . . . . . . . . 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 5042	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞))
182	179, 181	mtbird 328	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)
183	182	nrexdv 3229	. . . . . . . . . . . . . . 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 1427	. . . . . . . . . . . 12 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞)) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
187	123, 186	sylan2b 596	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ*) → (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
188	187	ralrimiva 3149	. . . . . . . . . 10 ⊢ (𝐹:ℝ⟶(0[,]+∞) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
189	188	adantr 484	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥))
190	109, 83	eqeltrrid 2895	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈ ℝ*)
191	122, 189, 190	rspcdva 3573	. . . . . . . 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 5072	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))
194		itg2ub 24337	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔‘𝑛) ∈ dom ∫1 ∧ (𝑔‘𝑛) ∘r ≤ 𝐹) → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
195	194	3expia 1118	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔‘𝑛) ∈ dom ∫1) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
196	74, 195	sylan2 595	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ 𝑛 ∈ ℕ)) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
197	196	anassrs 471	. . . . . . . . . . . 12 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ∘r ≤ 𝐹 → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
198	197	adantrd 495	. . . . . . . . . . 11 ⊢ (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
199	198	ralimdva 3144	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)))
200	199	impr 458	. . . . . . . . 9 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
201		eqid 2798	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) = (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))
202	89, 201, 101	fvmpt 6745	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) = (∫1‘(𝑔‘𝑚)))
203	202	breq1d 5040	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹)))
204	203	ralbiia 3132	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹))
205	89	breq1d 5040	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → ((∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹) ↔ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹)))
206	205	cbvralvw 3396	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ (∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹))
207	204, 206	bitr4i 281	. . . . . . . . 9 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ ∀𝑛 ∈ ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))
208	200, 207	sylibr 237	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹))
209		ffn 6487	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) Fn ℕ)
210		breq1 5033	. . . . . . . . . 10 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) → (𝑧 ≤ (∫2‘𝐹) ↔ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹)))
211	210	ralrn 6831	. . . . . . . . 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 260	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹))
214		supxrleub 12707	. . . . . . . 8 ⊢ ((ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))) ⊆ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → (sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤ (∫2‘𝐹) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹)))
215	81, 73, 214	syl2anc 587	. . . . . . 7 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤ (∫2‘𝐹) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹)))
216	213, 215	mpbird 260	. . . . . 6 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤ (∫2‘𝐹))
217	73, 83, 193, 216	xrletrid 12536	. . . . 5 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ))
218	69, 72, 217	3jca 1125	. . . 4 ⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘r ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < )))
219	218	ex 416	. . 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 209   ∧ wa 399   ∨ w3o 1083   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ⊆ wss 3881  ∅c0 4243  ifcif 4425   class class class wbr 5030   ↦ cmpt 5110  dom cdm 5519  ran crn 5520   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135   ∘_r cofr 7388   ↑_m cmap 8389  supcsup 8888  ℝcr 10525  0cc0 10526  1c1 10527  +∞cpnf 10661  -∞cmnf 10662  ℝ^*cxr 10663   < clt 10664   ≤ cle 10665   − cmin 10859   / cdiv 11286  ℕcn 11625  ℝ⁺crp 12377  [,]cicc 12729  ∫₁citg1 24219  ∫₂citg2 24220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-cc 9846  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-ofr 7390  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-sup 8890  df-inf 8891  df-oi 8958  df-dju 9314  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-xadd 12496  df-ioo 12730  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-fl 13157  df-seq 13365  df-exp 13426  df-hash 13687  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-clim 14837  df-sum 15035  df-xmet 20084  df-met 20085  df-ovol 24068  df-vol 24069  df-mbf 24223  df-itg1 24224  df-itg2 24225

This theorem is referenced by: (None)