Theorem itg2monolem1 25654

Description: Lemma for itg2mono 25657. We show that for any constant 𝑡 less than one, 𝑡 · ∫₁𝐻 is less than 𝑆, and so ∫₁𝐻 ≤ 𝑆, which is one half of the equality in itg2mono 25657. Consider the sequence 𝐴(𝑛) = {𝑥 ∣ 𝑡 · 𝐻 ≤ 𝐹(𝑛)}. This is an increasing sequence of measurable sets whose union is ℝ, and so 𝐻 ↾ 𝐴(𝑛) has an integral which equals ∫₁𝐻 in the limit, by itg1climres 25618. Then by taking the limit in (𝑡 · 𝐻) ↾ 𝐴(𝑛) ≤ 𝐹(𝑛), we get 𝑡 · ∫₁𝐻 ≤ 𝑆 as desired. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)

Hypotheses

Ref	Expression
itg2mono.1	⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
itg2mono.2	⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)
itg2mono.3	⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))
itg2mono.4	⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
itg2mono.5	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
itg2mono.6	⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )
itg2mono.7	⊢ (𝜑 → 𝑇 ∈ (0(,)1))
itg2mono.8	⊢ (𝜑 → 𝐻 ∈ dom ∫1)
itg2mono.9	⊢ (𝜑 → 𝐻 ∘r ≤ 𝐺)
itg2mono.10	⊢ (𝜑 → 𝑆 ∈ ℝ)
itg2mono.11	⊢ 𝐴 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})

Assertion

Ref	Expression
itg2monolem1	⊢ (𝜑 → (𝑇 · (∫1‘𝐻)) ≤ 𝑆)

Distinct variable groups:   𝑥,𝐴   𝑥,𝑛,𝑦,𝐺   𝑛,𝐻,𝑥,𝑦   𝑛,𝐹,𝑥,𝑦   𝜑,𝑛,𝑥,𝑦   𝑆,𝑛,𝑥,𝑦   𝑇,𝑛,𝑥,𝑦

Allowed substitution hints:   𝐴(𝑦,𝑛)

Proof of Theorem itg2monolem1

Dummy variables 𝑗 𝑘 𝑚 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 12881	. 2 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12609	. 2 ⊢ (𝜑 → 1 ∈ ℤ)
3		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
4		readdcl 11207	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
5	4	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
6		itg2mono.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))
7		rge0ssre 13451	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ ℝ
8		fss 6733	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘𝑛):ℝ⟶ℝ)
9	6, 7, 8	sylancl 585	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶ℝ)
10		itg2mono.8	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∈ dom ∫1)
11		itg2mono.7	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑇 ∈ (0(,)1))
12		0xr 11277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ*
13		1xr 11289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ*
14		elioo2 13383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑇 ∈ (0(,)1) ↔ (𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1)))
15	12, 13, 14	mp2an 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ (0(,)1) ↔ (𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1))
16	11, 15	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1))
17	16	simp1d 1140	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ℝ)
18	17	renegcld 11657	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -𝑇 ∈ ℝ)
19	10, 18	i1fmulc 25607	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1)
20	19	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1)
21		i1ff 25579	. . . . . . . . . . . . . . . 16 ⊢ (((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1 → ((ℝ × {-𝑇}) ∘f · 𝐻):ℝ⟶ℝ)
22	20, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻):ℝ⟶ℝ)
23		reex 11215	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
24	23	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℝ ∈ V)
25		inidm 4214	. . . . . . . . . . . . . . 15 ⊢ (ℝ ∩ ℝ) = ℝ
26	5, 9, 22, 24, 24, 25	off 7695	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)):ℝ⟶ℝ)
27	26	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)):ℝ⟶ℝ)
28	27	ffnd 6717	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) Fn ℝ)
29		elpreima 7061	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) Fn ℝ → (𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ (𝑥 ∈ ℝ ∧ (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0))))
30	28, 29	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ (𝑥 ∈ ℝ ∧ (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0))))
31	3, 30	mpbirand 706	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0)))
32		elioomnf 13439	. . . . . . . . . . . 12 ⊢ (0 ∈ ℝ* → ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0) ↔ ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ ℝ ∧ (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0)))
33	12, 32	ax-mp 5	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0) ↔ ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ ℝ ∧ (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0))
34	26	ffvelcdmda 7088	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ ℝ)
35	34	biantrurd 532	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0 ↔ ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ ℝ ∧ (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0)))
36	33, 35	bitr4id 290	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0) ↔ (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0))
37	6	ffnd 6717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) Fn ℝ)
38	22	ffnd 6717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) Fn ℝ)
39		eqidd 2728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑥))
40	18	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → -𝑇 ∈ ℝ)
41		i1ff 25579	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐻 ∈ dom ∫1 → 𝐻:ℝ⟶ℝ)
42	10, 41	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻:ℝ⟶ℝ)
43	42	ffnd 6717	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻 Fn ℝ)
44	43	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐻 Fn ℝ)
45		eqidd 2728	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) = (𝐻‘𝑥))
46	24, 40, 44, 45	ofc1 7703	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ × {-𝑇}) ∘f · 𝐻)‘𝑥) = (-𝑇 · (𝐻‘𝑥)))
47	17	recnd 11258	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ ℂ)
48	47	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
49	42	ffvelcdmda 7088	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
50	49	adantlr 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
51	50	recnd 11258	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℂ)
52	48, 51	mulneg1d 11683	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (-𝑇 · (𝐻‘𝑥)) = -(𝑇 · (𝐻‘𝑥)))
53	46, 52	eqtrd 2767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ × {-𝑇}) ∘f · 𝐻)‘𝑥) = -(𝑇 · (𝐻‘𝑥)))
54	37, 38, 24, 24, 25, 39, 53	ofval 7688	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))))
55	9	ffvelcdmda 7088	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ)
56	55	recnd 11258	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℂ)
57	17	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
58	57, 49	remulcld 11260	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
59	58	adantlr 714	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
60	59	recnd 11258	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℂ)
61	56, 60	negsubd 11593	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))))
62	54, 61	eqtrd 2767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))))
63	62	breq1d 5152	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0 ↔ (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0))
64		0red 11233	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
65	55, 59, 64	ltsubaddd 11826	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0 ↔ ((𝐹‘𝑛)‘𝑥) < (0 + (𝑇 · (𝐻‘𝑥)))))
66	60	addlidd 11431	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (0 + (𝑇 · (𝐻‘𝑥))) = (𝑇 · (𝐻‘𝑥)))
67	66	breq2d 5154	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛)‘𝑥) < (0 + (𝑇 · (𝐻‘𝑥))) ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
68	63, 65, 67	3bitrd 305	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0 ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
69	31, 36, 68	3bitrd 305	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
70	69	notbid 318	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ ¬ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
71		eldif 3954	. . . . . . . . . 10 ⊢ (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))))
72	71	baib 535	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ ¬ 𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))))
73	72	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ ¬ 𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))))
74	59, 55	lenltd 11376	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ ¬ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
75	70, 73, 74	3bitr4d 311	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)))
76	75	rabbi2dva 4213	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})
77		rembl 25443	. . . . . . 7 ⊢ ℝ ∈ dom vol
78		itg2mono.2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)
79		i1fmbf 25578	. . . . . . . . . . 11 ⊢ (((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1 → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ MblFn)
80	20, 79	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ MblFn)
81	78, 80	mbfadd 25564	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) ∈ MblFn)
82		mbfima 25533	. . . . . . . . 9 ⊢ ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) ∈ MblFn ∧ ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)):ℝ⟶ℝ) → (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol)
83	81, 26, 82	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol)
84		cmmbl 25437	. . . . . . . 8 ⊢ ((◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol → (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
85	83, 84	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
86		inmbl 25445	. . . . . . 7 ⊢ ((ℝ ∈ dom vol ∧ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) ∈ dom vol)
87	77, 85, 86	sylancr 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) ∈ dom vol)
88	76, 87	eqeltrrd 2829	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} ∈ dom vol)
89		itg2mono.11	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})
90	88, 89	fmptd 7118	. . . 4 ⊢ (𝜑 → 𝐴:ℕ⟶dom vol)
91		itg2mono.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
92	91	ralrimiva 3141	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
93		fveq2 6891	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
94		fvoveq1 7437	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
95	93, 94	breq12d 5155	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1))))
96	95	cbvralvw 3229	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
97	92, 96	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
98	97	r19.21bi 3243	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
99	6	ralrimiva 3141	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞))
100	93	feq1d 6701	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑗):ℝ⟶(0[,)+∞)))
101	100	cbvralvw 3229	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞))
102	99, 101	sylib 217	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞))
103	102	r19.21bi 3243	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞))
104	103	ffnd 6717	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) Fn ℝ)
105		peano2nn 12240	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
106		fveq2 6891	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑗 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑗 + 1)))
107	106	feq1d 6701	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞)))
108	107	rspccva 3606	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (𝑗 + 1) ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞))
109	99, 105, 108	syl2an 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞))
110	109	ffnd 6717	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) Fn ℝ)
111	23	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℝ ∈ V)
112		eqidd 2728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) = ((𝐹‘𝑗)‘𝑥))
113		eqidd 2728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥))
114	104, 110, 111, 111, 25, 112, 113	ofrfval 7687	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)) ↔ ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
115	98, 114	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))
116	115	r19.21bi 3243	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))
117	17	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
118	42	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐻:ℝ⟶ℝ)
119	118	ffvelcdmda 7088	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
120	117, 119	remulcld 11260	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
121		fss 6733	. . . . . . . . . 10 ⊢ (((𝐹‘𝑗):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘𝑗):ℝ⟶ℝ)
122	103, 7, 121	sylancl 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶ℝ)
123	122	ffvelcdmda 7088	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
124		fss 6733	. . . . . . . . . 10 ⊢ (((𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘(𝑗 + 1)):ℝ⟶ℝ)
125	109, 7, 124	sylancl 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶ℝ)
126	125	ffvelcdmda 7088	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ)
127		letr 11324	. . . . . . . 8 ⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
128	120, 123, 126, 127	syl3anc 1369	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
129	116, 128	mpan2d 693	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
130	129	ss2rabdv 4069	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ⊆ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
131	93	fveq1d 6893	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑗)‘𝑥))
132	131	breq2d 5154	. . . . . . . 8 ⊢ (𝑛 = 𝑗 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
133	132	rabbidv 3435	. . . . . . 7 ⊢ (𝑛 = 𝑗 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
134	23	rabex 5328	. . . . . . 7 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ∈ V
135	133, 89, 134	fvmpt 6999	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
136	135	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
137	105	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
138	106	fveq1d 6893	. . . . . . . . 9 ⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥))
139	138	breq2d 5154	. . . . . . . 8 ⊢ (𝑛 = (𝑗 + 1) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
140	139	rabbidv 3435	. . . . . . 7 ⊢ (𝑛 = (𝑗 + 1) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
141	23	rabex 5328	. . . . . . 7 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)} ∈ V
142	140, 89, 141	fvmpt 6999	. . . . . 6 ⊢ ((𝑗 + 1) ∈ ℕ → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
143	137, 142	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
144	130, 136, 143	3sstr4d 4025	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ⊆ (𝐴‘(𝑗 + 1)))
145	58	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
146	49	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℝ)
147	55	an32s 651	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ)
148	147	fmpttd 7119	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ)
149	148	frnd 6724	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ)
150		1nn 12239	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ
151		eqid 2727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))
152	151, 147	dmmptd 6694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ℕ)
153	150, 152	eleqtrrid 2835	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)))
154	153	ne0d 4331	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
155		dm0rn0 5921	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅)
156	155	necon3bii 2988	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
157	154, 156	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
158		itg2mono.5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
159	148	ffnd 6717	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ)
160		breq1 5145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
161	160	ralrn 7092	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
162	159, 161	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
163		fveq2 6891	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
164	163	fveq1d 6893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑚)‘𝑥))
165		fvex 6904	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑚)‘𝑥) ∈ V
166	164, 151, 165	fvmpt 6999	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥))
167	166	breq1d 5152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦))
168	167	ralbiia 3086	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)
169	164	breq1d 5152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦))
170	169	cbvralvw 3229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)
171	168, 170	bitr4i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
172	162, 171	bitrdi 287	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦))
173	172	rexbidv 3173	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦))
174	158, 173	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦)
175	149, 157, 174	suprcld 12193	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈ ℝ)
176	175	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈ ℝ)
177	16	simp3d 1142	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 < 1)
178	177	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 𝑇 < 1)
179	17	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 𝑇 ∈ ℝ)
180		1red 11231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 1 ∈ ℝ)
181		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 0 < (𝐻‘𝑥))
182		ltmul1 12080	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐻‘𝑥) ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 < 1 ↔ (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥))))
183	179, 180, 146, 181, 182	syl112anc 1372	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 < 1 ↔ (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥))))
184	178, 183	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥)))
185	146	recnd 11258	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℂ)
186	185	mullidd 11248	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (1 · (𝐻‘𝑥)) = (𝐻‘𝑥))
187	184, 186	breqtrd 5168	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < (𝐻‘𝑥))
188		itg2mono.9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∘r ≤ 𝐺)
189		itg2mono.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
190	175, 189	fmptd 7118	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)
191	190	ffnd 6717	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 Fn ℝ)
192	23	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ∈ V)
193		eqidd 2728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐻‘𝑦) = (𝐻‘𝑦))
194		fveq2 6891	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑦))
195	194	mpteq2dv 5244	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)))
196	195	rneqd 5934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)))
197	196	supeq1d 9455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
198		ltso 11310	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < Or ℝ
199	198	supex 9472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ) ∈ V
200	197, 189, 199	fvmpt 6999	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
201	200	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
202	43, 191, 192, 192, 25, 193, 201	ofrfval 7687	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐻 ∘r ≤ 𝐺 ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )))
203	188, 202	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
204		fveq2 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦))
205	204, 197	breq12d 5155	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )))
206	205	cbvralvw 3229	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
207	203, 206	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
208	207	r19.21bi 3243	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
209	208	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
210	145, 146, 176, 187, 209	ltletrd 11390	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
211	149	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ)
212	157	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
213	174	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦)
214		suprlub 12194	. . . . . . . . . . . . . 14 ⊢ (((ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) ∧ (𝑇 · (𝐻‘𝑥)) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤))
215	211, 212, 213, 145, 214	syl31anc 1371	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ((𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤))
216	210, 215	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤)
217	159	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ)
218		breq2 5146	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) → ((𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
219	218	rexrn 7091	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
220	217, 219	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
221		fvex 6904	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑗)‘𝑥) ∈ V
222	131, 151, 221	fvmpt 6999	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) = ((𝐹‘𝑗)‘𝑥))
223	222	breq2d 5154	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → ((𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)))
224	223	rexbiia 3087	. . . . . . . . . . . . 13 ⊢ (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))
225	220, 224	bitrdi 287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)))
226	216, 225	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))
227	179, 146	remulcld 11260	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
228	103	adantlr 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞))
229		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈ ℝ)
230	228, 229	ffvelcdmd 7089	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞))
231		elrege0 13449	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞) ↔ (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
232	230, 231	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
233	232	simpld 494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
234	233	adantlrr 720	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
235		ltle 11318	. . . . . . . . . . . . 13 ⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
236	227, 234, 235	syl2an2r 684	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
237	236	reximdva 3163	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
238	226, 237	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
239	238	anassrs 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 0 < (𝐻‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
240	150	ne0ii 4333	. . . . . . . . . . 11 ⊢ ℕ ≠ ∅
241	58	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
242	241	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
243		0red 11233	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 ∈ ℝ)
244	232	adantlrr 720	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
245	244	simpld 494	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
246		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑥) ≤ 0)
247	49	adantrr 716	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → (𝐻‘𝑥) ∈ ℝ)
248	247	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑥) ∈ ℝ)
249	17	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℝ)
250	16	simp2d 1141	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑇)
251	250	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 < 𝑇)
252		lemul2 12083	. . . . . . . . . . . . . . . 16 ⊢ (((𝐻‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) → ((𝐻‘𝑥) ≤ 0 ↔ (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0)))
253	248, 243, 249, 251, 252	syl112anc 1372	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑥) ≤ 0 ↔ (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0)))
254	246, 253	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0))
255	249	recnd 11258	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℂ)
256	255	mul01d 11429	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · 0) = 0)
257	254, 256	breqtrd 5168	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ 0)
258	244	simprd 495	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 ≤ ((𝐹‘𝑗)‘𝑥))
259	242, 243, 245, 257, 258	letrd 11387	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
260	259	ralrimiva 3141	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
261		r19.2z 4490	. . . . . . . . . . 11 ⊢ ((ℕ ≠ ∅ ∧ ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
262	240, 260, 261	sylancr 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
263	262	anassrs 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐻‘𝑥) ≤ 0) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
264		0red 11233	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
265	239, 263, 264, 49	ltlecasei 11338	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
266	265	ralrimiva 3141	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
267		rabid2 3459	. . . . . . 7 ⊢ (ℝ = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
268	266, 267	sylibr 233	. . . . . 6 ⊢ (𝜑 → ℝ = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
269		iunrab 5049	. . . . . 6 ⊢ ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}
270	268, 269	eqtr4di 2785	. . . . 5 ⊢ (𝜑 → ℝ = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
271	136	iuneq2dv 5015	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
272	90	ffnd 6717	. . . . . 6 ⊢ (𝜑 → 𝐴 Fn ℕ)
273		fniunfv 7251	. . . . . 6 ⊢ (𝐴 Fn ℕ → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴)
274	272, 273	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴)
275	270, 271, 274	3eqtr2rd 2774	. . . 4 ⊢ (𝜑 → ∪ ran 𝐴 = ℝ)
276		eqid 2727	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))
277	90, 144, 275, 10, 276	itg1climres 25618	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ⇝ (∫1‘𝐻))
278		nnex 12234	. . . . 5 ⊢ ℕ ∈ V
279	278	mptex 7229	. . . 4 ⊢ (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V
280	279	a1i 11	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V)
281		fveq2 6891	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘))
282	281	eleq2d 2814	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ (𝐴‘𝑗) ↔ 𝑥 ∈ (𝐴‘𝑘)))
283	282	ifbid 4547	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0) = if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))
284	283	mpteq2dv 5244	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))
285	284	fveq2d 6895	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
286		eqid 2727	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))
287		fvex 6904	. . . . . . 7 ⊢ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ V
288	285, 286, 287	fvmpt 6999	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
289	288	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
290	90	ffvelcdmda 7088	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ dom vol)
291		eqid 2727	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))
292	291	i1fres 25609	. . . . . . 7 ⊢ ((𝐻 ∈ dom ∫1 ∧ (𝐴‘𝑘) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1)
293	10, 290, 292	syl2an2r 684	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1)
294		itg1cl 25588	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ)
295	293, 294	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ)
296	289, 295	eqeltrd 2828	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℝ)
297	296	recnd 11258	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℂ)
298	285	oveq2d 7430	. . . . . 6 ⊢ (𝑗 = 𝑘 → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
299		eqid 2727	. . . . . 6 ⊢ (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) = (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))
300		ovex 7447	. . . . . 6 ⊢ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) ∈ V
301	298, 299, 300	fvmpt 6999	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
302	288	oveq2d 7430	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝑇 · ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘)) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
303	301, 302	eqtr4d 2770	. . . 4 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘)))
304	303	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘)))
305	1, 2, 277, 47, 280, 297, 304	climmulc2 15599	. 2 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ⇝ (𝑇 · (∫1‘𝐻)))
306		icossicc 13431	. . . . . . 7 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
307		fss 6733	. . . . . . 7 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑛):ℝ⟶(0[,]+∞))
308	6, 306, 307	sylancl 585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,]+∞))
309		itg2mono.10	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ)
310	309	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ∈ ℝ)
311		itg2cl 25636	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛):ℝ⟶(0[,]+∞) → (∫2‘(𝐹‘𝑛)) ∈ ℝ*)
312	308, 311	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ℝ*)
313	312	fmpttd 7119	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))):ℕ⟶ℝ*)
314	313	frnd 6724	. . . . . . . 8 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ*)
315		fvex 6904	. . . . . . . . . . 11 ⊢ (∫2‘(𝐹‘𝑛)) ∈ V
316	315	elabrex 7246	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))})
317	316	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))})
318		eqid 2727	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))
319	318	rnmpt 5951	. . . . . . . . 9 ⊢ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))}
320	317, 319	eleqtrrdi 2839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))))
321		supxrub 13321	. . . . . . . 8 ⊢ ((ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ* ∧ (∫2‘(𝐹‘𝑛)) ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))) → (∫2‘(𝐹‘𝑛)) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ))
322	314, 320, 321	syl2an2r 684	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ))
323		itg2mono.6	. . . . . . 7 ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )
324	322, 323	breqtrrdi 5184	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ 𝑆)
325		itg2lecl 25642	. . . . . 6 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ 𝑆 ∈ ℝ ∧ (∫2‘(𝐹‘𝑛)) ≤ 𝑆) → (∫2‘(𝐹‘𝑛)) ∈ ℝ)
326	308, 310, 324, 325	syl3anc 1369	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ℝ)
327	326	fmpttd 7119	. . . 4 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))):ℕ⟶ℝ)
328	308	ralrimiva 3141	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞))
329		fveq2 6891	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
330	329	feq1d 6701	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,]+∞)))
331	330	cbvralvw 3229	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞))
332	328, 331	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞))
333		peano2nn 12240	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
334		fveq2 6891	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1)))
335	334	feq1d 6701	. . . . . . . . . 10 ⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘):ℝ⟶(0[,]+∞) ↔ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞)))
336	335	rspccva 3606	. . . . . . . . 9 ⊢ ((∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞) ∧ (𝑛 + 1) ∈ ℕ) → (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞))
337	332, 333, 336	syl2an 595	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞))
338		itg2le 25643	. . . . . . . 8 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞) ∧ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1))) → (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
339	308, 337, 91, 338	syl3anc 1369	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
340	339	ralrimiva 3141	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
341		2fveq3 6896	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘𝑘)))
342		fvex 6904	. . . . . . . . . 10 ⊢ (∫2‘(𝐹‘𝑘)) ∈ V
343	341, 318, 342	fvmpt 6999	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘)))
344		peano2nn 12240	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
345		2fveq3 6896	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑘 + 1) → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘(𝑘 + 1))))
346		fvex 6904	. . . . . . . . . . 11 ⊢ (∫2‘(𝐹‘(𝑘 + 1))) ∈ V
347	345, 318, 346	fvmpt 6999	. . . . . . . . . 10 ⊢ ((𝑘 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1))))
348	344, 347	syl 17	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1))))
349	343, 348	breq12d 5155	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))))
350	349	ralbiia 3086	. . . . . . 7 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1))))
351		fvoveq1 7437	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1)))
352	351	fveq2d 6895	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘(𝑛 + 1))) = (∫2‘(𝐹‘(𝑘 + 1))))
353	341, 352	breq12d 5155	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))))
354	353	cbvralvw 3229	. . . . . . 7 ⊢ (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))) ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1))))
355	350, 354	bitr4i 278	. . . . . 6 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
356	340, 355	sylibr 233	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)))
357	356	r19.21bi 3243	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)))
358	324	ralrimiva 3141	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆)
359	343	breq1d 5152	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥))
360	359	ralbiia 3086	. . . . . . . 8 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)
361	341	breq1d 5152	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥))
362	361	cbvralvw 3229	. . . . . . . 8 ⊢ (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)
363	360, 362	bitr4i 278	. . . . . . 7 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥)
364		breq2 5146	. . . . . . . 8 ⊢ (𝑥 = 𝑆 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
365	364	ralbidv 3172	. . . . . . 7 ⊢ (𝑥 = 𝑆 → (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
366	363, 365	bitrid 283	. . . . . 6 ⊢ (𝑥 = 𝑆 → (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
367	366	rspcev 3607	. . . . 5 ⊢ ((𝑆 ∈ ℝ ∧ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)
368	309, 358, 367	syl2anc 583	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)
369	1, 2, 327, 357, 368	climsup 15634	. . 3 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
370	327	frnd 6724	. . . . 5 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ)
371	318, 312	dmmptd 6694	. . . . . . 7 ⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ℕ)
372	240	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℕ ≠ ∅)
373	371, 372	eqnetrd 3003	. . . . . 6 ⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
374		dm0rn0 5921	. . . . . . 7 ⊢ (dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ∅)
375	374	necon3bii 2988	. . . . . 6 ⊢ (dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
376	373, 375	sylib 217	. . . . 5 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
377	315, 318	fnmpti 6692	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) Fn ℕ
378		breq1 5145	. . . . . . . . 9 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) → (𝑧 ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
379	378	ralrn 7092	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
380	377, 379	mp1i 13	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
381	380	rexbidv 3173	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
382	368, 381	mpbird 257	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥)
383		supxrre 13324	. . . . 5 ⊢ ((ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥) → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
384	370, 376, 382, 383	syl3anc 1369	. . . 4 ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
385	323, 384	eqtr2id 2780	. . 3 ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ) = 𝑆)
386	369, 385	breqtrd 5168	. 2 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⇝ 𝑆)
387	17	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℝ)
388	90	ffvelcdmda 7088	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ∈ dom vol)
389	276	i1fres 25609	. . . . . . 7 ⊢ ((𝐻 ∈ dom ∫1 ∧ (𝐴‘𝑗) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1)
390	10, 388, 389	syl2an2r 684	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1)
391		itg1cl 25588	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ)
392	390, 391	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ)
393	387, 392	remulcld 11260	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ∈ ℝ)
394	393	fmpttd 7119	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))):ℕ⟶ℝ)
395	394	ffvelcdmda 7088	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ∈ ℝ)
396	327	ffvelcdmda 7088	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ∈ ℝ)
397	329	feq1d 6701	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,)+∞)))
398	397	cbvralvw 3229	. . . . . . 7 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞))
399	99, 398	sylib 217	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞))
400	399	r19.21bi 3243	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):ℝ⟶(0[,)+∞))
401		fss 6733	. . . . 5 ⊢ (((𝐹‘𝑘):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑘):ℝ⟶(0[,]+∞))
402	400, 306, 401	sylancl 585	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):ℝ⟶(0[,]+∞))
403	23	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℝ ∈ V)
404	17	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 ∈ ℝ)
405	404	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
406		fvex 6904	. . . . . . . . 9 ⊢ (𝐻‘𝑥) ∈ V
407		c0ex 11224	. . . . . . . . 9 ⊢ 0 ∈ V
408	406, 407	ifex 4574	. . . . . . . 8 ⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V
409	408	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V)
410		fconstmpt 5734	. . . . . . . 8 ⊢ (ℝ × {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇)
411	410	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℝ × {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇))
412		eqidd 2728	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))
413	403, 405, 409, 411, 412	offval2 7697	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
414		ovif2 7512	. . . . . . . 8 ⊢ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0))
415	47	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 ∈ ℂ)
416	415	mul01d 11429	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · 0) = 0)
417	416	ifeq2d 4544	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))
418	414, 417	eqtrid 2779	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))
419	418	mpteq2dv 5244	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
420	413, 419	eqtrd 2767	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
421	293, 404	i1fmulc 25607	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ dom ∫1)
422	420, 421	eqeltrrd 2829	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom ∫1)
423		iftrue 4530	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥)))
424	423	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥)))
425	329	fveq1d 6893	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑘)‘𝑥))
426	425	breq2d 5154	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)))
427	426	rabbidv 3435	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
428	23	rabex 5328	. . . . . . . . . . . . 13 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ∈ V
429	427, 89, 428	fvmpt 6999	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
430	429	ad2antlr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
431	430	eleq2d 2814	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)}))
432	431	biimpa 476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
433		rabid 3447	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ↔ (𝑥 ∈ ℝ ∧ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)))
434	433	simprbi 496	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))
435	432, 434	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))
436	424, 435	eqbrtrd 5164	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
437		iffalse 4533	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0)
438	437	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0)
439	400	ffvelcdmda 7088	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞))
440		elrege0 13449	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞) ↔ (((𝐹‘𝑘)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑘)‘𝑥)))
441	440	simprbi 496	. . . . . . . . . 10 ⊢ (((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞) → 0 ≤ ((𝐹‘𝑘)‘𝑥))
442	439, 441	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘𝑘)‘𝑥))
443	442	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → 0 ≤ ((𝐹‘𝑘)‘𝑥))
444	438, 443	eqbrtrd 5164	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
445	436, 444	pm2.61dan 812	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
446	445	ralrimiva 3141	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
447		ovex 7447	. . . . . . . 8 ⊢ (𝑇 · (𝐻‘𝑥)) ∈ V
448	447, 407	ifex 4574	. . . . . . 7 ⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V
449	448	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V)
450		fvexd 6906	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ V)
451		eqidd 2728	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
452	400	feqmptd 6961	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑘)‘𝑥)))
453	403, 449, 450, 451, 452	ofrfval2 7698	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥)))
454	446, 453	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘))
455		itg2ub 25637	. . . 4 ⊢ (((𝐹‘𝑘):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) ≤ (∫2‘(𝐹‘𝑘)))
456	402, 422, 454, 455	syl3anc 1369	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) ≤ (∫2‘(𝐹‘𝑘)))
457	301	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
458	293, 404	itg1mulc 25608	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
459	420	fveq2d 6895	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))))
460	457, 458, 459	3eqtr2d 2773	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))))
461	343	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘)))
462	456, 460, 461	3brtr4d 5174	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘))
463	1, 2, 305, 386, 395, 396, 462	climle 15602	1 ⊢ (𝜑 → (𝑇 · (∫1‘𝐻)) ≤ 𝑆)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  {cab 2704   ≠ wne 2935  ∀wral 3056  ∃wrex 3065  {crab 3427  Vcvv 3469   ∖ cdif 3941   ∩ cin 3943   ⊆ wss 3944  ∅c0 4318  ifcif 4524  {csn 4624  ∪ cuni 4903  ∪ ciun 4991   class class class wbr 5142   ↦ cmpt 5225   × cxp 5670  ^◡ccnv 5671  dom cdm 5672  ran crn 5673   “ cima 5675   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542  (class class class)co 7414   ∘_f cof 7675   ∘_r cofr 7676  supcsup 9449  ℂcc 11122  ℝcr 11123  0cc0 11124  1c1 11125   + caddc 11127   · cmul 11129  +∞cpnf 11261  -∞cmnf 11262  ℝ^*cxr 11263   < clt 11264   ≤ cle 11265   − cmin 11460  -cneg 11461  ℕcn 12228  (,)cioo 13342  [,)cico 13344  [,]cicc 13345   ⇝ cli 15446  volcvol 25366  MblFncmbf 25517  ∫₁citg1 25518  ∫₂citg2 25519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-inf2 9650  ax-cc 10444  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201  ax-pre-sup 11202

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-disj 5108  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7677  df-ofr 7678  df-om 7863  df-1st 7985  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-oadd 8482  df-omul 8483  df-er 8716  df-map 8836  df-pm 8837  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-fi 9420  df-sup 9451  df-inf 9452  df-oi 9519  df-dju 9910  df-card 9948  df-acn 9951  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-sub 11462  df-neg 11463  df-div 11888  df-nn 12229  df-2 12291  df-3 12292  df-n0 12489  df-z 12575  df-uz 12839  df-q 12949  df-rp 12993  df-xneg 13110  df-xadd 13111  df-xmul 13112  df-ioo 13346  df-ioc 13347  df-ico 13348  df-icc 13349  df-fz 13503  df-fzo 13646  df-fl 13775  df-seq 13985  df-exp 14045  df-hash 14308  df-cj 15064  df-re 15065  df-im 15066  df-sqrt 15200  df-abs 15201  df-clim 15450  df-rlim 15451  df-sum 15651  df-rest 17389  df-topgen 17410  df-psmet 21251  df-xmet 21252  df-met 21253  df-bl 21254  df-mopn 21255  df-top 22770  df-topon 22787  df-bases 22823  df-cmp 23265  df-ovol 25367  df-vol 25368  df-mbf 25522  df-itg1 25523  df-itg2 25524

This theorem is referenced by:  itg2monolem3  25656