Theorem itg2monolem1 25657

Description: Lemma for itg2mono 25660. We show that for any constant 𝑡 less than one, 𝑡 · ∫₁𝐻 is less than 𝑆, and so ∫₁𝐻 ≤ 𝑆, which is one half of the equality in itg2mono 25660. 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 25621. 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 12842	. 2 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12570	. 2 ⊢ (𝜑 → 1 ∈ ℤ)
3		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
4		readdcl 11157	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
5	4	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
6		itg2mono.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))
7		rge0ssre 13423	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ ℝ
8		fss 6706	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘𝑛):ℝ⟶ℝ)
9	6, 7, 8	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶ℝ)
10		itg2mono.8	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∈ dom ∫1)
11		itg2mono.7	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑇 ∈ (0(,)1))
12		0xr 11227	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ*
13		1xr 11239	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ*
14		elioo2 13353	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑇 ∈ (0(,)1) ↔ (𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1)))
15	12, 13, 14	mp2an 692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ (0(,)1) ↔ (𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1))
16	11, 15	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1))
17	16	simp1d 1142	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ℝ)
18	17	renegcld 11611	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -𝑇 ∈ ℝ)
19	10, 18	i1fmulc 25610	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1)
20	19	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1)
21		i1ff 25583	. . . . . . . . . . . . . . . 16 ⊢ (((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1 → ((ℝ × {-𝑇}) ∘f · 𝐻):ℝ⟶ℝ)
22	20, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻):ℝ⟶ℝ)
23		reex 11165	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
24	23	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℝ ∈ V)
25		inidm 4192	. . . . . . . . . . . . . . 15 ⊢ (ℝ ∩ ℝ) = ℝ
26	5, 9, 22, 24, 24, 25	off 7673	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)):ℝ⟶ℝ)
27	26	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)):ℝ⟶ℝ)
28	27	ffnd 6691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) Fn ℝ)
29		elpreima 7032	. . . . . . . . . . . 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 707	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0)))
32		elioomnf 13411	. . . . . . . . . . . 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 7058	. . . . . . . . . . . 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 6691	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) Fn ℝ)
38	22	ffnd 6691	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) Fn ℝ)
39		eqidd 2731	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑥))
40	18	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → -𝑇 ∈ ℝ)
41		i1ff 25583	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐻 ∈ dom ∫1 → 𝐻:ℝ⟶ℝ)
42	10, 41	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻:ℝ⟶ℝ)
43	42	ffnd 6691	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻 Fn ℝ)
44	43	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐻 Fn ℝ)
45		eqidd 2731	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) = (𝐻‘𝑥))
46	24, 40, 44, 45	ofc1 7683	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ × {-𝑇}) ∘f · 𝐻)‘𝑥) = (-𝑇 · (𝐻‘𝑥)))
47	17	recnd 11208	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ ℂ)
48	47	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
49	42	ffvelcdmda 7058	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
50	49	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
51	50	recnd 11208	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℂ)
52	48, 51	mulneg1d 11637	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (-𝑇 · (𝐻‘𝑥)) = -(𝑇 · (𝐻‘𝑥)))
53	46, 52	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ × {-𝑇}) ∘f · 𝐻)‘𝑥) = -(𝑇 · (𝐻‘𝑥)))
54	37, 38, 24, 24, 25, 39, 53	ofval 7666	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))))
55	9	ffvelcdmda 7058	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ)
56	55	recnd 11208	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℂ)
57	17	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
58	57, 49	remulcld 11210	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
59	58	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
60	59	recnd 11208	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℂ)
61	56, 60	negsubd 11545	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))))
62	54, 61	eqtrd 2765	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))))
63	62	breq1d 5119	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0 ↔ (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0))
64		0red 11183	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
65	55, 59, 64	ltsubaddd 11780	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0 ↔ ((𝐹‘𝑛)‘𝑥) < (0 + (𝑇 · (𝐻‘𝑥)))))
66	60	addlidd 11381	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (0 + (𝑇 · (𝐻‘𝑥))) = (𝑇 · (𝐻‘𝑥)))
67	66	breq2d 5121	. . . . . . . . . . 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 3926	. . . . . . . . . 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 11326	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ ¬ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
75	70, 73, 74	3bitr4d 311	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)))
76	75	rabbi2dva 4191	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})
77		rembl 25447	. . . . . . 7 ⊢ ℝ ∈ dom vol
78		itg2mono.2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)
79		i1fmbf 25582	. . . . . . . . . . 11 ⊢ (((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1 → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ MblFn)
80	20, 79	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ MblFn)
81	78, 80	mbfadd 25568	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) ∈ MblFn)
82		mbfima 25537	. . . . . . . . 9 ⊢ ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) ∈ MblFn ∧ ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)):ℝ⟶ℝ) → (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol)
83	81, 26, 82	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol)
84		cmmbl 25441	. . . . . . . 8 ⊢ ((◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol → (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
85	83, 84	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
86		inmbl 25449	. . . . . . 7 ⊢ ((ℝ ∈ dom vol ∧ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) ∈ dom vol)
87	77, 85, 86	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) ∈ dom vol)
88	76, 87	eqeltrrd 2830	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} ∈ dom vol)
89		itg2mono.11	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})
90	88, 89	fmptd 7088	. . . 4 ⊢ (𝜑 → 𝐴:ℕ⟶dom vol)
91		itg2mono.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
92	91	ralrimiva 3126	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
93		fveq2 6860	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
94		fvoveq1 7412	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
95	93, 94	breq12d 5122	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1))))
96	95	cbvralvw 3216	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
97	92, 96	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
98	97	r19.21bi 3230	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
99	6	ralrimiva 3126	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞))
100	93	feq1d 6672	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑗):ℝ⟶(0[,)+∞)))
101	100	cbvralvw 3216	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞))
102	99, 101	sylib 218	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞))
103	102	r19.21bi 3230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞))
104	103	ffnd 6691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) Fn ℝ)
105		peano2nn 12199	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
106		fveq2 6860	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑗 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑗 + 1)))
107	106	feq1d 6672	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞)))
108	107	rspccva 3590	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (𝑗 + 1) ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞))
109	99, 105, 108	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞))
110	109	ffnd 6691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) Fn ℝ)
111	23	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℝ ∈ V)
112		eqidd 2731	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) = ((𝐹‘𝑗)‘𝑥))
113		eqidd 2731	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥))
114	104, 110, 111, 111, 25, 112, 113	ofrfval 7665	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)) ↔ ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
115	98, 114	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))
116	115	r19.21bi 3230	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))
117	17	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
118	42	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐻:ℝ⟶ℝ)
119	118	ffvelcdmda 7058	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
120	117, 119	remulcld 11210	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
121		fss 6706	. . . . . . . . . 10 ⊢ (((𝐹‘𝑗):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘𝑗):ℝ⟶ℝ)
122	103, 7, 121	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶ℝ)
123	122	ffvelcdmda 7058	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
124		fss 6706	. . . . . . . . . 10 ⊢ (((𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘(𝑗 + 1)):ℝ⟶ℝ)
125	109, 7, 124	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶ℝ)
126	125	ffvelcdmda 7058	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ)
127		letr 11274	. . . . . . . 8 ⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
128	120, 123, 126, 127	syl3anc 1373	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
129	116, 128	mpan2d 694	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
130	129	ss2rabdv 4041	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ⊆ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
131	93	fveq1d 6862	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑗)‘𝑥))
132	131	breq2d 5121	. . . . . . . 8 ⊢ (𝑛 = 𝑗 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
133	132	rabbidv 3416	. . . . . . 7 ⊢ (𝑛 = 𝑗 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
134	23	rabex 5296	. . . . . . 7 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ∈ V
135	133, 89, 134	fvmpt 6970	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
136	135	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
137	105	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
138	106	fveq1d 6862	. . . . . . . . 9 ⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥))
139	138	breq2d 5121	. . . . . . . 8 ⊢ (𝑛 = (𝑗 + 1) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
140	139	rabbidv 3416	. . . . . . 7 ⊢ (𝑛 = (𝑗 + 1) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
141	23	rabex 5296	. . . . . . 7 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)} ∈ V
142	140, 89, 141	fvmpt 6970	. . . . . 6 ⊢ ((𝑗 + 1) ∈ ℕ → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
143	137, 142	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
144	130, 136, 143	3sstr4d 4004	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ⊆ (𝐴‘(𝑗 + 1)))
145	58	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
146	49	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℝ)
147	55	an32s 652	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ)
148	147	fmpttd 7089	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ)
149	148	frnd 6698	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ)
150		1nn 12198	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ
151		eqid 2730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))
152	151, 147	dmmptd 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ℕ)
153	150, 152	eleqtrrid 2836	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)))
154	153	ne0d 4307	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
155		dm0rn0 5890	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅)
156	155	necon3bii 2978	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
157	154, 156	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
158		itg2mono.5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
159	148	ffnd 6691	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ)
160		breq1 5112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
161	160	ralrn 7062	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
162	159, 161	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
163		fveq2 6860	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
164	163	fveq1d 6862	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑚)‘𝑥))
165		fvex 6873	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑚)‘𝑥) ∈ V
166	164, 151, 165	fvmpt 6970	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥))
167	166	breq1d 5119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦))
168	167	ralbiia 3074	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)
169	164	breq1d 5119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦))
170	169	cbvralvw 3216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)
171	168, 170	bitr4i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
172	162, 171	bitrdi 287	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦))
173	172	rexbidv 3158	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦))
174	158, 173	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦)
175	149, 157, 174	suprcld 12152	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈ ℝ)
176	175	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈ ℝ)
177	16	simp3d 1144	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 < 1)
178	177	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 𝑇 < 1)
179	17	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 𝑇 ∈ ℝ)
180		1red 11181	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 1 ∈ ℝ)
181		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 0 < (𝐻‘𝑥))
182		ltmul1 12038	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐻‘𝑥) ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 < 1 ↔ (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥))))
183	179, 180, 146, 181, 182	syl112anc 1376	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 < 1 ↔ (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥))))
184	178, 183	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥)))
185	146	recnd 11208	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℂ)
186	185	mullidd 11198	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (1 · (𝐻‘𝑥)) = (𝐻‘𝑥))
187	184, 186	breqtrd 5135	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < (𝐻‘𝑥))
188		itg2mono.9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∘r ≤ 𝐺)
189		itg2mono.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
190	175, 189	fmptd 7088	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)
191	190	ffnd 6691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 Fn ℝ)
192	23	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ∈ V)
193		eqidd 2731	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐻‘𝑦) = (𝐻‘𝑦))
194		fveq2 6860	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑦))
195	194	mpteq2dv 5203	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)))
196	195	rneqd 5904	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)))
197	196	supeq1d 9403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
198		ltso 11260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < Or ℝ
199	198	supex 9421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ) ∈ V
200	197, 189, 199	fvmpt 6970	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
201	200	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
202	43, 191, 192, 192, 25, 193, 201	ofrfval 7665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐻 ∘r ≤ 𝐺 ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )))
203	188, 202	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
204		fveq2 6860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦))
205	204, 197	breq12d 5122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )))
206	205	cbvralvw 3216	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
207	203, 206	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
208	207	r19.21bi 3230	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
209	208	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
210	145, 146, 176, 187, 209	ltletrd 11340	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
211	149	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ)
212	157	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
213	174	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦)
214		suprlub 12153	. . . . . . . . . . . . . 14 ⊢ (((ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) ∧ (𝑇 · (𝐻‘𝑥)) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤))
215	211, 212, 213, 145, 214	syl31anc 1375	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ((𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤))
216	210, 215	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤)
217	159	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ)
218		breq2 5113	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) → ((𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
219	218	rexrn 7061	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
220	217, 219	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
221		fvex 6873	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑗)‘𝑥) ∈ V
222	131, 151, 221	fvmpt 6970	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) = ((𝐹‘𝑗)‘𝑥))
223	222	breq2d 5121	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → ((𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)))
224	223	rexbiia 3075	. . . . . . . . . . . . 13 ⊢ (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))
225	220, 224	bitrdi 287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)))
226	216, 225	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))
227	179, 146	remulcld 11210	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
228	103	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞))
229		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈ ℝ)
230	228, 229	ffvelcdmd 7059	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞))
231		elrege0 13421	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞) ↔ (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
232	230, 231	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
233	232	simpld 494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
234	233	adantlrr 721	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
235		ltle 11268	. . . . . . . . . . . . 13 ⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
236	227, 234, 235	syl2an2r 685	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
237	236	reximdva 3147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
238	226, 237	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
239	238	anassrs 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 0 < (𝐻‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
240	150	ne0ii 4309	. . . . . . . . . . 11 ⊢ ℕ ≠ ∅
241	58	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
242	241	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
243		0red 11183	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 ∈ ℝ)
244	232	adantlrr 721	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
245	244	simpld 494	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
246		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑥) ≤ 0)
247	49	adantrr 717	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → (𝐻‘𝑥) ∈ ℝ)
248	247	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑥) ∈ ℝ)
249	17	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℝ)
250	16	simp2d 1143	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑇)
251	250	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 < 𝑇)
252		lemul2 12041	. . . . . . . . . . . . . . . 16 ⊢ (((𝐻‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) → ((𝐻‘𝑥) ≤ 0 ↔ (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0)))
253	248, 243, 249, 251, 252	syl112anc 1376	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑥) ≤ 0 ↔ (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0)))
254	246, 253	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0))
255	249	recnd 11208	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℂ)
256	255	mul01d 11379	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · 0) = 0)
257	254, 256	breqtrd 5135	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ 0)
258	244	simprd 495	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 ≤ ((𝐹‘𝑗)‘𝑥))
259	242, 243, 245, 257, 258	letrd 11337	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
260	259	ralrimiva 3126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
261		r19.2z 4460	. . . . . . . . . . 11 ⊢ ((ℕ ≠ ∅ ∧ ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
262	240, 260, 261	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
263	262	anassrs 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐻‘𝑥) ≤ 0) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
264		0red 11183	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
265	239, 263, 264, 49	ltlecasei 11288	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
266	265	ralrimiva 3126	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
267		rabid2 3442	. . . . . . 7 ⊢ (ℝ = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
268	266, 267	sylibr 234	. . . . . 6 ⊢ (𝜑 → ℝ = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
269		iunrab 5018	. . . . . 6 ⊢ ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}
270	268, 269	eqtr4di 2783	. . . . 5 ⊢ (𝜑 → ℝ = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
271	136	iuneq2dv 4982	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
272	90	ffnd 6691	. . . . . 6 ⊢ (𝜑 → 𝐴 Fn ℕ)
273		fniunfv 7223	. . . . . 6 ⊢ (𝐴 Fn ℕ → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴)
274	272, 273	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴)
275	270, 271, 274	3eqtr2rd 2772	. . . 4 ⊢ (𝜑 → ∪ ran 𝐴 = ℝ)
276		eqid 2730	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))
277	90, 144, 275, 10, 276	itg1climres 25621	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ⇝ (∫1‘𝐻))
278		nnex 12193	. . . . 5 ⊢ ℕ ∈ V
279	278	mptex 7199	. . . 4 ⊢ (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V
280	279	a1i 11	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V)
281		fveq2 6860	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘))
282	281	eleq2d 2815	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ (𝐴‘𝑗) ↔ 𝑥 ∈ (𝐴‘𝑘)))
283	282	ifbid 4514	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0) = if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))
284	283	mpteq2dv 5203	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))
285	284	fveq2d 6864	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
286		eqid 2730	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))
287		fvex 6873	. . . . . . 7 ⊢ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ V
288	285, 286, 287	fvmpt 6970	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
289	288	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
290	90	ffvelcdmda 7058	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ dom vol)
291		eqid 2730	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))
292	291	i1fres 25612	. . . . . . 7 ⊢ ((𝐻 ∈ dom ∫1 ∧ (𝐴‘𝑘) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1)
293	10, 290, 292	syl2an2r 685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1)
294		itg1cl 25592	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ)
295	293, 294	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ)
296	289, 295	eqeltrd 2829	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℝ)
297	296	recnd 11208	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℂ)
298	285	oveq2d 7405	. . . . . 6 ⊢ (𝑗 = 𝑘 → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
299		eqid 2730	. . . . . 6 ⊢ (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) = (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))
300		ovex 7422	. . . . . 6 ⊢ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) ∈ V
301	298, 299, 300	fvmpt 6970	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
302	288	oveq2d 7405	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝑇 · ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘)) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
303	301, 302	eqtr4d 2768	. . . 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 15609	. 2 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ⇝ (𝑇 · (∫1‘𝐻)))
306		icossicc 13403	. . . . . . 7 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
307		fss 6706	. . . . . . 7 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑛):ℝ⟶(0[,]+∞))
308	6, 306, 307	sylancl 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,]+∞))
309		itg2mono.10	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ)
310	309	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ∈ ℝ)
311		itg2cl 25639	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛):ℝ⟶(0[,]+∞) → (∫2‘(𝐹‘𝑛)) ∈ ℝ*)
312	308, 311	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ℝ*)
313	312	fmpttd 7089	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))):ℕ⟶ℝ*)
314	313	frnd 6698	. . . . . . . 8 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ*)
315		fvex 6873	. . . . . . . . . . 11 ⊢ (∫2‘(𝐹‘𝑛)) ∈ V
316	315	elabrex 7218	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))})
317	316	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))})
318		eqid 2730	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))
319	318	rnmpt 5923	. . . . . . . . 9 ⊢ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))}
320	317, 319	eleqtrrdi 2840	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))))
321		supxrub 13290	. . . . . . . 8 ⊢ ((ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ* ∧ (∫2‘(𝐹‘𝑛)) ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))) → (∫2‘(𝐹‘𝑛)) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ))
322	314, 320, 321	syl2an2r 685	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ))
323		itg2mono.6	. . . . . . 7 ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )
324	322, 323	breqtrrdi 5151	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ 𝑆)
325		itg2lecl 25645	. . . . . 6 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ 𝑆 ∈ ℝ ∧ (∫2‘(𝐹‘𝑛)) ≤ 𝑆) → (∫2‘(𝐹‘𝑛)) ∈ ℝ)
326	308, 310, 324, 325	syl3anc 1373	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ℝ)
327	326	fmpttd 7089	. . . 4 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))):ℕ⟶ℝ)
328	308	ralrimiva 3126	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞))
329		fveq2 6860	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
330	329	feq1d 6672	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,]+∞)))
331	330	cbvralvw 3216	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞))
332	328, 331	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞))
333		peano2nn 12199	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
334		fveq2 6860	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1)))
335	334	feq1d 6672	. . . . . . . . . 10 ⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘):ℝ⟶(0[,]+∞) ↔ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞)))
336	335	rspccva 3590	. . . . . . . . 9 ⊢ ((∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞) ∧ (𝑛 + 1) ∈ ℕ) → (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞))
337	332, 333, 336	syl2an 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞))
338		itg2le 25646	. . . . . . . 8 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞) ∧ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1))) → (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
339	308, 337, 91, 338	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
340	339	ralrimiva 3126	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
341		2fveq3 6865	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘𝑘)))
342		fvex 6873	. . . . . . . . . 10 ⊢ (∫2‘(𝐹‘𝑘)) ∈ V
343	341, 318, 342	fvmpt 6970	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘)))
344		peano2nn 12199	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
345		2fveq3 6865	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑘 + 1) → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘(𝑘 + 1))))
346		fvex 6873	. . . . . . . . . . 11 ⊢ (∫2‘(𝐹‘(𝑘 + 1))) ∈ V
347	345, 318, 346	fvmpt 6970	. . . . . . . . . 10 ⊢ ((𝑘 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1))))
348	344, 347	syl 17	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1))))
349	343, 348	breq12d 5122	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))))
350	349	ralbiia 3074	. . . . . . 7 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1))))
351		fvoveq1 7412	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1)))
352	351	fveq2d 6864	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘(𝑛 + 1))) = (∫2‘(𝐹‘(𝑘 + 1))))
353	341, 352	breq12d 5122	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))))
354	353	cbvralvw 3216	. . . . . . 7 ⊢ (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))) ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1))))
355	350, 354	bitr4i 278	. . . . . 6 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
356	340, 355	sylibr 234	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)))
357	356	r19.21bi 3230	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)))
358	324	ralrimiva 3126	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆)
359	343	breq1d 5119	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥))
360	359	ralbiia 3074	. . . . . . . 8 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)
361	341	breq1d 5119	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥))
362	361	cbvralvw 3216	. . . . . . . 8 ⊢ (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)
363	360, 362	bitr4i 278	. . . . . . 7 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥)
364		breq2 5113	. . . . . . . 8 ⊢ (𝑥 = 𝑆 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
365	364	ralbidv 3157	. . . . . . 7 ⊢ (𝑥 = 𝑆 → (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
366	363, 365	bitrid 283	. . . . . 6 ⊢ (𝑥 = 𝑆 → (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
367	366	rspcev 3591	. . . . 5 ⊢ ((𝑆 ∈ ℝ ∧ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)
368	309, 358, 367	syl2anc 584	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)
369	1, 2, 327, 357, 368	climsup 15642	. . 3 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
370	327	frnd 6698	. . . . 5 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ)
371	318, 312	dmmptd 6665	. . . . . . 7 ⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ℕ)
372	240	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℕ ≠ ∅)
373	371, 372	eqnetrd 2993	. . . . . 6 ⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
374		dm0rn0 5890	. . . . . . 7 ⊢ (dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ∅)
375	374	necon3bii 2978	. . . . . 6 ⊢ (dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
376	373, 375	sylib 218	. . . . 5 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
377	315, 318	fnmpti 6663	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) Fn ℕ
378		breq1 5112	. . . . . . . . 9 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) → (𝑧 ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
379	378	ralrn 7062	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
380	377, 379	mp1i 13	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
381	380	rexbidv 3158	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
382	368, 381	mpbird 257	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥)
383		supxrre 13293	. . . . 5 ⊢ ((ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥) → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
384	370, 376, 382, 383	syl3anc 1373	. . . 4 ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
385	323, 384	eqtr2id 2778	. . 3 ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ) = 𝑆)
386	369, 385	breqtrd 5135	. 2 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⇝ 𝑆)
387	17	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℝ)
388	90	ffvelcdmda 7058	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ∈ dom vol)
389	276	i1fres 25612	. . . . . . 7 ⊢ ((𝐻 ∈ dom ∫1 ∧ (𝐴‘𝑗) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1)
390	10, 388, 389	syl2an2r 685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1)
391		itg1cl 25592	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ)
392	390, 391	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ)
393	387, 392	remulcld 11210	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ∈ ℝ)
394	393	fmpttd 7089	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))):ℕ⟶ℝ)
395	394	ffvelcdmda 7058	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ∈ ℝ)
396	327	ffvelcdmda 7058	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ∈ ℝ)
397	329	feq1d 6672	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,)+∞)))
398	397	cbvralvw 3216	. . . . . . 7 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞))
399	99, 398	sylib 218	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞))
400	399	r19.21bi 3230	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):ℝ⟶(0[,)+∞))
401		fss 6706	. . . . 5 ⊢ (((𝐹‘𝑘):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑘):ℝ⟶(0[,]+∞))
402	400, 306, 401	sylancl 586	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):ℝ⟶(0[,]+∞))
403	23	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℝ ∈ V)
404	17	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 ∈ ℝ)
405	404	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
406		fvex 6873	. . . . . . . . 9 ⊢ (𝐻‘𝑥) ∈ V
407		c0ex 11174	. . . . . . . . 9 ⊢ 0 ∈ V
408	406, 407	ifex 4541	. . . . . . . 8 ⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V
409	408	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V)
410		fconstmpt 5702	. . . . . . . 8 ⊢ (ℝ × {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇)
411	410	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℝ × {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇))
412		eqidd 2731	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))
413	403, 405, 409, 411, 412	offval2 7675	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
414		ovif2 7490	. . . . . . . 8 ⊢ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0))
415	47	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 ∈ ℂ)
416	415	mul01d 11379	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · 0) = 0)
417	416	ifeq2d 4511	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))
418	414, 417	eqtrid 2777	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))
419	418	mpteq2dv 5203	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
420	413, 419	eqtrd 2765	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
421	293, 404	i1fmulc 25610	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ dom ∫1)
422	420, 421	eqeltrrd 2830	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom ∫1)
423		iftrue 4496	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥)))
424	423	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥)))
425	329	fveq1d 6862	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑘)‘𝑥))
426	425	breq2d 5121	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)))
427	426	rabbidv 3416	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
428	23	rabex 5296	. . . . . . . . . . . . 13 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ∈ V
429	427, 89, 428	fvmpt 6970	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
430	429	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
431	430	eleq2d 2815	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)}))
432	431	biimpa 476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
433		rabid 3430	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ↔ (𝑥 ∈ ℝ ∧ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)))
434	433	simprbi 496	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))
435	432, 434	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))
436	424, 435	eqbrtrd 5131	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
437		iffalse 4499	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0)
438	437	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0)
439	400	ffvelcdmda 7058	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞))
440		elrege0 13421	. . . . . . . . . . 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 5131	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
445	436, 444	pm2.61dan 812	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
446	445	ralrimiva 3126	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
447		ovex 7422	. . . . . . . 8 ⊢ (𝑇 · (𝐻‘𝑥)) ∈ V
448	447, 407	ifex 4541	. . . . . . 7 ⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V
449	448	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V)
450		fvexd 6875	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ V)
451		eqidd 2731	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
452	400	feqmptd 6931	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑘)‘𝑥)))
453	403, 449, 450, 451, 452	ofrfval2 7676	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥)))
454	446, 453	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘))
455		itg2ub 25640	. . . 4 ⊢ (((𝐹‘𝑘):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) ≤ (∫2‘(𝐹‘𝑘)))
456	402, 422, 454, 455	syl3anc 1373	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) ≤ (∫2‘(𝐹‘𝑘)))
457	301	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
458	293, 404	itg1mulc 25611	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
459	420	fveq2d 6864	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))))
460	457, 458, 459	3eqtr2d 2771	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))))
461	343	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘)))
462	456, 460, 461	3brtr4d 5141	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘))
463	1, 2, 305, 386, 395, 396, 462	climle 15612	1 ⊢ (𝜑 → (𝑇 · (∫1‘𝐻)) ≤ 𝑆)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {cab 2708   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  {crab 3408  Vcvv 3450   ∖ cdif 3913   ∩ cin 3915   ⊆ wss 3916  ∅c0 4298  ifcif 4490  {csn 4591  ∪ cuni 4873  ∪ ciun 4957   class class class wbr 5109   ↦ cmpt 5190   × cxp 5638  ^◡ccnv 5639  dom cdm 5640  ran crn 5641   “ cima 5643   Fn wfn 6508  ⟶wf 6509  ‘cfv 6513  (class class class)co 7389   ∘_f cof 7653   ∘_r cofr 7654  supcsup 9397  ℂcc 11072  ℝcr 11073  0cc0 11074  1c1 11075   + caddc 11077   · cmul 11079  +∞cpnf 11211  -∞cmnf 11212  ℝ^*cxr 11213   < clt 11214   ≤ cle 11215   − cmin 11411  -cneg 11412  ℕcn 12187  (,)cioo 13312  [,)cico 13314  [,]cicc 13315   ⇝ cli 15456  volcvol 25370  MblFncmbf 25521  ∫₁citg1 25522  ∫₂citg2 25523

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 2702  ax-rep 5236  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-inf2 9600  ax-cc 10394  ax-cnex 11130  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150  ax-pre-mulgt0 11151  ax-pre-sup 11152

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-pss 3936  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-int 4913  df-iun 4959  df-disj 5077  df-br 5110  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5535  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-se 5594  df-we 5595  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-pred 6276  df-ord 6337  df-on 6338  df-lim 6339  df-suc 6340  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-isom 6522  df-riota 7346  df-ov 7392  df-oprab 7393  df-mpo 7394  df-of 7655  df-ofr 7656  df-om 7845  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8380  df-1o 8436  df-2o 8437  df-oadd 8440  df-omul 8441  df-er 8673  df-map 8803  df-pm 8804  df-en 8921  df-dom 8922  df-sdom 8923  df-fin 8924  df-fi 9368  df-sup 9399  df-inf 9400  df-oi 9469  df-dju 9860  df-card 9898  df-acn 9901  df-pnf 11216  df-mnf 11217  df-xr 11218  df-ltxr 11219  df-le 11220  df-sub 11413  df-neg 11414  df-div 11842  df-nn 12188  df-2 12250  df-3 12251  df-n0 12449  df-z 12536  df-uz 12800  df-q 12914  df-rp 12958  df-xneg 13078  df-xadd 13079  df-xmul 13080  df-ioo 13316  df-ioc 13317  df-ico 13318  df-icc 13319  df-fz 13475  df-fzo 13622  df-fl 13760  df-seq 13973  df-exp 14033  df-hash 14302  df-cj 15071  df-re 15072  df-im 15073  df-sqrt 15207  df-abs 15208  df-clim 15460  df-rlim 15461  df-sum 15659  df-rest 17391  df-topgen 17412  df-psmet 21262  df-xmet 21263  df-met 21264  df-bl 21265  df-mopn 21266  df-top 22787  df-topon 22804  df-bases 22839  df-cmp 23280  df-ovol 25371  df-vol 25372  df-mbf 25526  df-itg1 25527  df-itg2 25528

This theorem is referenced by:  itg2monolem3  25659