Theorem itg2monolem1 26104

Description: Lemma for itg2mono 26107. We show that for any constant 𝑡 less than one, 𝑡 · ∫₁𝐻 is less than 𝑆, and so ∫₁𝐻 ≤ 𝑆, which is one half of the equality in itg2mono 26107. 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 26068. 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 13034	. 2 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12757	. 2 ⊢ (𝜑 → 1 ∈ ℤ)
3		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
4		readdcl 11313	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
5	4	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
6		itg2mono.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))
7		rge0ssre 13617	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ ℝ
8		fss 6751	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘𝑛):ℝ⟶ℝ)
9	6, 7, 8	sylancl 598	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶ℝ)
10		itg2mono.8	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∈ dom ∫1)
11		itg2mono.7	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑇 ∈ (0(,)1))
12		0xr 11386	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ*
13		1xr 11398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ*
14		elioo2 13547	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑇 ∈ (0(,)1) ↔ (𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1)))
15	12, 13, 14	mp2an 705	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ (0(,)1) ↔ (𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1))
16	11, 15	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1))
17	16	simp1d 1160	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ℝ)
18	17	renegcld 11773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -𝑇 ∈ ℝ)
19	10, 18	i1fmulc 26057	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((ℝ × { -𝑇}) ∘f · 𝐻) ∈ dom ∫1)
20	19	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × { -𝑇}) ∘f · 𝐻) ∈ dom ∫1)
21		i1ff 26030	. . . . . . . . . . . . . . . 16 ⊢ (((ℝ × { -𝑇}) ∘f · 𝐻) ∈ dom ∫1 → ((ℝ × { -𝑇}) ∘f · 𝐻):ℝ⟶ℝ)
22	20, 21	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × { -𝑇}) ∘f · 𝐻):ℝ⟶ℝ)
23		reex 11321	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
24	23	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℝ ∈ V)
25		inidm 4126	. . . . . . . . . . . . . . 15 ⊢ (ℝ ∩ ℝ) = ℝ
26	5, 9, 22, 24, 24, 25	off 7738	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)):ℝ⟶ℝ)
27	26	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)):ℝ⟶ℝ)
28	27	ffnd 6735	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) Fn ℝ)
29		elpreima 7083	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) Fn ℝ → (𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ (𝑥 ∈ ℝ ∧ (((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0))))
30	28, 29	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ (𝑥 ∈ ℝ ∧ (((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0))))
31	3, 30	mpbirand 720	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ (((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0)))
32		elioomnf 13605	. . . . . . . . . . . 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 7111	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) ∈ ℝ)
35	34	biantrurd 542	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) < 0 ↔ ((((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) ∈ ℝ ∧ (((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) < 0)))
36	33, 35	bitr4id 293	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) ∈ (-∞(,)0) ↔ (((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) < 0))
37	6	ffnd 6735	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) Fn ℝ)
38	22	ffnd 6735	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × { -𝑇}) ∘f · 𝐻) Fn ℝ)
39		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑥))
40	18	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → -𝑇 ∈ ℝ)
41		i1ff 26030	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐻 ∈ dom ∫1 → 𝐻:ℝ⟶ℝ)
42	10, 41	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻:ℝ⟶ℝ)
43	42	ffnd 6735	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻 Fn ℝ)
44	43	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐻 Fn ℝ)
45		eqidd 2764	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) = (𝐻‘𝑥))
46	24, 40, 44, 45	ofc1 7748	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ × { -𝑇}) ∘f · 𝐻)‘𝑥) = ( -𝑇 · (𝐻‘𝑥)))
47	17	recnd 11367	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ ℂ)
48	47	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
49	42	ffvelcdmda 7111	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
50	49	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
51	50	recnd 11367	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℂ)
52	48, 51	mulneg1d 11799	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ( -𝑇 · (𝐻‘𝑥)) = -(𝑇 · (𝐻‘𝑥)))
53	46, 52	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ × { -𝑇}) ∘f · 𝐻)‘𝑥) = -(𝑇 · (𝐻‘𝑥)))
54	37, 38, 24, 24, 25, 39, 53	ofval 7731	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))))
55	9	ffvelcdmda 7111	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ)
56	55	recnd 11367	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℂ)
57	17	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
58	57, 49	remulcld 11369	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
59	58	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
60	59	recnd 11367	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℂ)
61	56, 60	negsubd 11705	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))))
62	54, 61	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))))
63	62	breq1d 5116	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) < 0 ↔ (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0))
64		0red 11341	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
65	55, 59, 64	ltsubaddd 11942	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0 ↔ ((𝐹‘𝑛)‘𝑥) < (0 + (𝑇 · (𝐻‘𝑥)))))
66	60	addlidd 11541	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (0 + (𝑇 · (𝐻‘𝑥))) = (𝑇 · (𝐻‘𝑥)))
67	66	breq2d 5118	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛)‘𝑥) < (0 + (𝑇 · (𝐻‘𝑥))) ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
68	63, 65, 67	3bitrd 308	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻))‘𝑥) < 0 ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
69	31, 36, 68	3bitrd 308	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
70	69	notbid 321	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ ¬ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
71		eldif 4052	. . . . . . . . . 10 ⊢ (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0))))
72	71	baib 545	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ ¬ 𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0))))
73	72	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ ¬ 𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0))))
74	59, 55	lenltd 11486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ ¬ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
75	70, 73, 74	3bitr4d 314	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)))
76	75	rabbi2dva 4125	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})
77		rembl 25894	. . . . . . 7 ⊢ ℝ ∈ dom vol
78		itg2mono.2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)
79		i1fmbf 26029	. . . . . . . . . . 11 ⊢ (((ℝ × { -𝑇}) ∘f · 𝐻) ∈ dom ∫1 → ((ℝ × { -𝑇}) ∘f · 𝐻) ∈ MblFn)
80	20, 79	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × { -𝑇}) ∘f · 𝐻) ∈ MblFn)
81	78, 80	mbfadd 26015	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) ∈ MblFn)
82		mbfima 25984	. . . . . . . . 9 ⊢ ((((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) ∈ MblFn ∧ ((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)):ℝ⟶ℝ) → (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol)
83	81, 26, 82	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol)
84		cmmbl 25888	. . . . . . . 8 ⊢ ((◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol → (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
85	83, 84	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
86		inmbl 25896	. . . . . . 7 ⊢ ((ℝ ∈ dom vol ∧ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) ∈ dom vol)
87	77, 85, 86	sylancr 599	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × { -𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) ∈ dom vol)
88	76, 87	eqeltrrd 2865	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} ∈ dom vol)
89		itg2mono.11	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})
90	88, 89	fmptd 7141	. . . 4 ⊢ (𝜑 → 𝐴:ℕ⟶dom vol)
91		itg2mono.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
92	91	ralrimiva 3158	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
93		fveq2 6911	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
94		fvoveq1 7469	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
95	93, 94	breq12d 5119	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1))))
96	95	cbvralvw 3244	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
97	92, 96	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
98	97	r19.21bi 3258	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
99	6	ralrimiva 3158	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞))
100	93	feq1d 6716	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑗):ℝ⟶(0[,)+∞)))
101	100	cbvralvw 3244	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞))
102	99, 101	sylib 221	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞))
103	102	r19.21bi 3258	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞))
104	103	ffnd 6735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) Fn ℝ)
105		peano2nn 12377	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
106		fveq2 6911	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑗 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑗 + 1)))
107	106	feq1d 6716	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞)))
108	107	rspccva 3579	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (𝑗 + 1) ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞))
109	99, 105, 108	syl2an 608	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞))
110	109	ffnd 6735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) Fn ℝ)
111	23	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℝ ∈ V)
112		eqidd 2764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) = ((𝐹‘𝑗)‘𝑥))
113		eqidd 2764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥))
114	104, 110, 111, 111, 25, 112, 113	ofrfval 7730	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)) ↔ ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
115	98, 114	mpbid 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))
116	115	r19.21bi 3258	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))
117	17	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
118	42	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐻:ℝ⟶ℝ)
119	118	ffvelcdmda 7111	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
120	117, 119	remulcld 11369	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
121		fss 6751	. . . . . . . . . 10 ⊢ (((𝐹‘𝑗):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘𝑗):ℝ⟶ℝ)
122	103, 7, 121	sylancl 598	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶ℝ)
123	122	ffvelcdmda 7111	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
124		fss 6751	. . . . . . . . . 10 ⊢ (((𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘(𝑗 + 1)):ℝ⟶ℝ)
125	109, 7, 124	sylancl 598	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶ℝ)
126	125	ffvelcdmda 7111	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ)
127		letr 11434	. . . . . . . 8 ⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
128	120, 123, 126, 127	syl3anc 1399	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
129	116, 128	mpan2d 707	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
130	129	ss2rabdv 4003	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ⊆ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
131	93	fveq1d 6913	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑗)‘𝑥))
132	131	breq2d 5118	. . . . . . . 8 ⊢ (𝑛 = 𝑗 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
133	132	rabbidv 3423	. . . . . . 7 ⊢ (𝑛 = 𝑗 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
134	23	rabex 5305	. . . . . . 7 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ∈ V
135	133, 89, 134	fvmpt 7019	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
136	135	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
137	105	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
138	106	fveq1d 6913	. . . . . . . . 9 ⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥))
139	138	breq2d 5118	. . . . . . . 8 ⊢ (𝑛 = (𝑗 + 1) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
140	139	rabbidv 3423	. . . . . . 7 ⊢ (𝑛 = (𝑗 + 1) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
141	23	rabex 5305	. . . . . . 7 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)} ∈ V
142	140, 89, 141	fvmpt 7019	. . . . . 6 ⊢ ((𝑗 + 1) ∈ ℕ → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
143	137, 142	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
144	130, 136, 143	3sstr4d 3968	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ⊆ (𝐴‘(𝑗 + 1)))
145	58	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
146	49	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℝ)
147	55	an32s 665	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ)
148	147	fmpttd 7142	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ)
149	148	frnd 6743	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ)
150		1nn 12376	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ
151		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))
152	151, 147	dmmptd 6709	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ℕ)
153	150, 152	eleqtrrid 2871	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)))
154	153	ne0d 4291	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
155		dm0rn0 5914	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅)
156	155	necon3bii 3011	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
157	154, 156	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
158		itg2mono.5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
159	148	ffnd 6735	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ)
160		breq1 5109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
161	160	ralrn 7115	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
162	159, 161	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
163		fveq2 6911	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
164	163	fveq1d 6913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑚)‘𝑥))
165		fvex 6924	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑚)‘𝑥) ∈ V
166	164, 151, 165	fvmpt 7019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥))
167	166	breq1d 5116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦))
168	167	ralbiia 3110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)
169	164	breq1d 5116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦))
170	169	cbvralvw 3244	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)
171	168, 170	bitr4i 281	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
172	162, 171	bitrdi 290	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦))
173	172	rexbidv 3190	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦))
174	158, 173	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦)
175	149, 157, 174	suprcld 12310	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈ ℝ)
176	175	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈ ℝ)
177	16	simp3d 1162	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 < 1)
178	177	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 𝑇 < 1)
179	17	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 𝑇 ∈ ℝ)
180		1red 11339	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 1 ∈ ℝ)
181		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 0 < (𝐻‘𝑥))
182		ltmul1 12197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐻‘𝑥) ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 < 1 ↔ (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥))))
183	179, 180, 146, 181, 182	syl112anc 1402	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 < 1 ↔ (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥))))
184	178, 183	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥)))
185	146	recnd 11367	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℂ)
186	185	mullidd 11357	. . . . . . . . . . . . . . 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 7141	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)
191	190	ffnd 6735	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 Fn ℝ)
192	23	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ∈ V)
193		eqidd 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐻‘𝑦) = (𝐻‘𝑦))
194		fveq2 6911	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑦))
195	194	mpteq2dv 5203	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)))
196	195	rneqd 5928	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)))
197	196	supeq1d 9468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
198		ltso 11420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < Or ℝ
199	198	supex 9486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ) ∈ V
200	197, 189, 199	fvmpt 7019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
201	200	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
202	43, 191, 192, 192, 25, 193, 201	ofrfval 7730	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐻 ∘r ≤ 𝐺 ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )))
203	188, 202	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
204		fveq2 6911	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦))
205	204, 197	breq12d 5119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )))
206	205	cbvralvw 3244	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
207	203, 206	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
208	207	r19.21bi 3258	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
209	208	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
210	145, 146, 176, 187, 209	ltletrd 11500	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
211	149	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ)
212	157	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
213	174	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦)
214		suprlub 12311	. . . . . . . . . . . . . 14 ⊢ (((ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) ∧ (𝑇 · (𝐻‘𝑥)) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤))
215	211, 212, 213, 145, 214	syl31anc 1401	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ((𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤))
216	210, 215	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤)
217	159	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ)
218		breq2 5110	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) → ((𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
219	218	rexrn 7114	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
220	217, 219	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
221		fvex 6924	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑗)‘𝑥) ∈ V
222	131, 151, 221	fvmpt 7019	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) = ((𝐹‘𝑗)‘𝑥))
223	222	breq2d 5118	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → ((𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)))
224	223	rexbiia 3111	. . . . . . . . . . . . 13 ⊢ (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))
225	220, 224	bitrdi 290	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)))
226	216, 225	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))
227	179, 146	remulcld 11369	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
228	103	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞))
229		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈ ℝ)
230	228, 229	ffvelcdmd 7112	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞))
231		elrege0 13615	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞) ↔ (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
232	230, 231	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
233	232	simpld 500	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
234	233	adantlrr 734	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
235		ltle 11428	. . . . . . . . . . . . 13 ⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
236	227, 234, 235	syl2an2r 698	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
237	236	reximdva 3179	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
238	226, 237	mpd 16	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
239	238	anassrs 473	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 0 < (𝐻‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
240	150	ne0ii 4293	. . . . . . . . . . 11 ⊢ ℕ ≠ ∅
241	58	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
242	241	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
243		0red 11341	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 ∈ ℝ)
244	232	adantlrr 734	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
245	244	simpld 500	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
246		simplrr 790	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑥) ≤ 0)
247	49	adantrr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → (𝐻‘𝑥) ∈ ℝ)
248	247	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑥) ∈ ℝ)
249	17	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℝ)
250	16	simp2d 1161	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑇)
251	250	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 < 𝑇)
252		lemul2 12200	. . . . . . . . . . . . . . . 16 ⊢ (((𝐻‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) → ((𝐻‘𝑥) ≤ 0 ↔ (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0)))
253	248, 243, 249, 251, 252	syl112anc 1402	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑥) ≤ 0 ↔ (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0)))
254	246, 253	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0))
255	249	recnd 11367	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℂ)
256	255	mul01d 11539	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · 0) = 0)
257	254, 256	breqtrd 5135	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ 0)
258	244	simprd 501	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 ≤ ((𝐹‘𝑗)‘𝑥))
259	242, 243, 245, 257, 258	letrd 11497	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
260	259	ralrimiva 3158	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
261		r19.2z 4458	. . . . . . . . . . 11 ⊢ ((ℕ ≠ ∅ ∧ ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
262	240, 260, 261	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
263	262	anassrs 473	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐻‘𝑥) ≤ 0) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
264		0red 11341	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
265	239, 263, 264, 49	ltlecasei 11448	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
266	265	ralrimiva 3158	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
267		rabid2 3448	. . . . . . 7 ⊢ (ℝ = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
268	266, 267	sylibr 237	. . . . . 6 ⊢ (𝜑 → ℝ = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
269		iunrab 5014	. . . . . 6 ⊢ ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}
270	268, 269	eqtr4di 2816	. . . . 5 ⊢ (𝜑 → ℝ = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
271	136	iuneq2dv 4979	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
272	90	ffnd 6735	. . . . . 6 ⊢ (𝜑 → 𝐴 Fn ℕ)
273		fniunfv 7277	. . . . . 6 ⊢ (𝐴 Fn ℕ → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴)
274	272, 273	syl 18	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴)
275	270, 271, 274	3eqtr2rd 2805	. . . 4 ⊢ (𝜑 → ∪ ran 𝐴 = ℝ)
276		eqid 2763	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))
277	90, 144, 275, 10, 276	itg1climres 26068	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ⇝ (∫1‘𝐻))
278		nnex 12371	. . . . 5 ⊢ ℕ ∈ V
279	278	mptex 7255	. . . 4 ⊢ (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V
280	279	a1i 11	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V)
281		fveq2 6911	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘))
282	281	eleq2d 2850	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ (𝐴‘𝑗) ↔ 𝑥 ∈ (𝐴‘𝑘)))
283	282	ifbid 4509	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0) = if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))
284	283	mpteq2dv 5203	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))
285	284	fveq2d 6915	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
286		eqid 2763	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))
287		fvex 6924	. . . . . . 7 ⊢ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ V
288	285, 286, 287	fvmpt 7019	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
289	288	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
290	90	ffvelcdmda 7111	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ dom vol)
291		eqid 2763	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))
292	291	i1fres 26059	. . . . . . 7 ⊢ ((𝐻 ∈ dom ∫1 ∧ (𝐴‘𝑘) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1)
293	10, 290, 292	syl2an2r 698	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1)
294		itg1cl 26039	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ)
295	293, 294	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ)
296	289, 295	eqeltrd 2864	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℝ)
297	296	recnd 11367	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℂ)
298	285	oveq2d 7462	. . . . . 6 ⊢ (𝑗 = 𝑘 → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
299		eqid 2763	. . . . . 6 ⊢ (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) = (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))
300		ovex 7479	. . . . . 6 ⊢ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) ∈ V
301	298, 299, 300	fvmpt 7019	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
302	288	oveq2d 7462	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝑇 · ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘)) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
303	301, 302	eqtr4d 2801	. . . 4 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘)))
304	303	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘)))
305	1, 2, 277, 47, 280, 297, 304	climmulc2 15836	. 2 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ⇝ (𝑇 · (∫1‘𝐻)))
306		icossicc 13597	. . . . . . 7 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
307		fss 6751	. . . . . . 7 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑛):ℝ⟶(0[,]+∞))
308	6, 306, 307	sylancl 598	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,]+∞))
309		itg2mono.10	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ)
310	309	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ∈ ℝ)
311		itg2cl 26086	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛):ℝ⟶(0[,]+∞) → (∫2‘(𝐹‘𝑛)) ∈ ℝ*)
312	308, 311	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ℝ*)
313	312	fmpttd 7142	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))):ℕ⟶ℝ*)
314	313	frnd 6743	. . . . . . . 8 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ*)
315		fvex 6924	. . . . . . . . . . 11 ⊢ (∫2‘(𝐹‘𝑛)) ∈ V
316	315	elabrex 7272	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))})
317	316	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))})
318		eqid 2763	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))
319	318	rnmpt 5947	. . . . . . . . 9 ⊢ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))}
320	317, 319	eleqtrrdi 2875	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))))
321		supxrub 13484	. . . . . . . 8 ⊢ ((ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ* ∧ (∫2‘(𝐹‘𝑛)) ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))) → (∫2‘(𝐹‘𝑛)) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ))
322	314, 320, 321	syl2an2r 698	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ))
323		itg2mono.6	. . . . . . 7 ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )
324	322, 323	breqtrrdi 5151	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ 𝑆)
325		itg2lecl 26092	. . . . . 6 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ 𝑆 ∈ ℝ ∧ (∫2‘(𝐹‘𝑛)) ≤ 𝑆) → (∫2‘(𝐹‘𝑛)) ∈ ℝ)
326	308, 310, 324, 325	syl3anc 1399	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ℝ)
327	326	fmpttd 7142	. . . 4 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))):ℕ⟶ℝ)
328	308	ralrimiva 3158	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞))
329		fveq2 6911	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
330	329	feq1d 6716	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,]+∞)))
331	330	cbvralvw 3244	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞))
332	328, 331	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞))
333		peano2nn 12377	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
334		fveq2 6911	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1)))
335	334	feq1d 6716	. . . . . . . . . 10 ⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘):ℝ⟶(0[,]+∞) ↔ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞)))
336	335	rspccva 3579	. . . . . . . . 9 ⊢ ((∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞) ∧ (𝑛 + 1) ∈ ℕ) → (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞))
337	332, 333, 336	syl2an 608	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞))
338		itg2le 26093	. . . . . . . 8 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞) ∧ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1))) → (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
339	308, 337, 91, 338	syl3anc 1399	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
340	339	ralrimiva 3158	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
341		2fveq3 6916	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘𝑘)))
342		fvex 6924	. . . . . . . . . 10 ⊢ (∫2‘(𝐹‘𝑘)) ∈ V
343	341, 318, 342	fvmpt 7019	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘)))
344		peano2nn 12377	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
345		2fveq3 6916	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑘 + 1) → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘(𝑘 + 1))))
346		fvex 6924	. . . . . . . . . . 11 ⊢ (∫2‘(𝐹‘(𝑘 + 1))) ∈ V
347	345, 318, 346	fvmpt 7019	. . . . . . . . . 10 ⊢ ((𝑘 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1))))
348	344, 347	syl 18	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1))))
349	343, 348	breq12d 5119	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))))
350	349	ralbiia 3110	. . . . . . 7 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1))))
351		fvoveq1 7469	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1)))
352	351	fveq2d 6915	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘(𝑛 + 1))) = (∫2‘(𝐹‘(𝑘 + 1))))
353	341, 352	breq12d 5119	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))))
354	353	cbvralvw 3244	. . . . . . 7 ⊢ (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))) ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1))))
355	350, 354	bitr4i 281	. . . . . 6 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
356	340, 355	sylibr 237	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)))
357	356	r19.21bi 3258	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)))
358	324	ralrimiva 3158	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆)
359	343	breq1d 5116	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥))
360	359	ralbiia 3110	. . . . . . . 8 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)
361	341	breq1d 5116	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥))
362	361	cbvralvw 3244	. . . . . . . 8 ⊢ (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)
363	360, 362	bitr4i 281	. . . . . . 7 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥)
364		breq2 5110	. . . . . . . 8 ⊢ (𝑥 = 𝑆 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
365	364	ralbidv 3189	. . . . . . 7 ⊢ (𝑥 = 𝑆 → (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
366	363, 365	bitrid 286	. . . . . 6 ⊢ (𝑥 = 𝑆 → (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
367	366	rspcev 3580	. . . . 5 ⊢ ((𝑆 ∈ ℝ ∧ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)
368	309, 358, 367	syl2anc 596	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)
369	1, 2, 327, 357, 368	climsup 15869	. . 3 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
370	327	frnd 6743	. . . . 5 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ)
371	318, 312	dmmptd 6709	. . . . . . 7 ⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ℕ)
372	240	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℕ ≠ ∅)
373	371, 372	eqnetrd 3026	. . . . . 6 ⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
374		dm0rn0 5914	. . . . . . 7 ⊢ (dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ∅)
375	374	necon3bii 3011	. . . . . 6 ⊢ (dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
376	373, 375	sylib 221	. . . . 5 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
377	315, 318	fnmpti 6707	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) Fn ℕ
378		breq1 5109	. . . . . . . . 9 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) → (𝑧 ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
379	378	ralrn 7115	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
380	377, 379	mp1i 14	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
381	380	rexbidv 3190	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
382	368, 381	mpbird 260	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥)
383		supxrre 13487	. . . . 5 ⊢ ((ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥) → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
384	370, 376, 382, 383	syl3anc 1399	. . . 4 ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
385	323, 384	eqtr2id 2811	. . 3 ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ) = 𝑆)
386	369, 385	breqtrd 5135	. 2 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⇝ 𝑆)
387	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℝ)
388	90	ffvelcdmda 7111	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ∈ dom vol)
389	276	i1fres 26059	. . . . . . 7 ⊢ ((𝐻 ∈ dom ∫1 ∧ (𝐴‘𝑗) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1)
390	10, 388, 389	syl2an2r 698	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1)
391		itg1cl 26039	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ)
392	390, 391	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ)
393	387, 392	remulcld 11369	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ∈ ℝ)
394	393	fmpttd 7142	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))):ℕ⟶ℝ)
395	394	ffvelcdmda 7111	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ∈ ℝ)
396	327	ffvelcdmda 7111	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ∈ ℝ)
397	329	feq1d 6716	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,)+∞)))
398	397	cbvralvw 3244	. . . . . . 7 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞))
399	99, 398	sylib 221	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞))
400	399	r19.21bi 3258	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):ℝ⟶(0[,)+∞))
401		fss 6751	. . . . 5 ⊢ (((𝐹‘𝑘):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑘):ℝ⟶(0[,]+∞))
402	400, 306, 401	sylancl 598	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):ℝ⟶(0[,]+∞))
403	23	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℝ ∈ V)
404	17	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 ∈ ℝ)
405	404	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
406		fvex 6924	. . . . . . . . 9 ⊢ (𝐻‘𝑥) ∈ V
407		c0ex 11330	. . . . . . . . 9 ⊢ 0 ∈ V
408	406, 407	ifex 4536	. . . . . . . 8 ⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V
409	408	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V)
410		fconstmpt 5718	. . . . . . . 8 ⊢ (ℝ × {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇)
411	410	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℝ × {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇))
412		eqidd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))
413	403, 405, 409, 411, 412	offval2 7740	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
414		ovif2 7545	. . . . . . . 8 ⊢ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0))
415	47	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 ∈ ℂ)
416	415	mul01d 11539	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · 0) = 0)
417	416	ifeq2d 4506	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))
418	414, 417	eqtrid 2810	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))
419	418	mpteq2dv 5203	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
420	413, 419	eqtrd 2798	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
421	293, 404	i1fmulc 26057	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ dom ∫1)
422	420, 421	eqeltrrd 2865	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom ∫1)
423		iftrue 4491	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥)))
424	423	adantl 487	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥)))
425	329	fveq1d 6913	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑘)‘𝑥))
426	425	breq2d 5118	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)))
427	426	rabbidv 3423	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
428	23	rabex 5305	. . . . . . . . . . . . 13 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ∈ V
429	427, 89, 428	fvmpt 7019	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
430	429	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
431	430	eleq2d 2850	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)}))
432	431	biimpa 482	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
433		rabid 3436	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ↔ (𝑥 ∈ ℝ ∧ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)))
434	433	simprbi 503	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))
435	432, 434	syl 18	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))
436	424, 435	eqbrtrd 5131	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
437		iffalse 4494	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0)
438	437	adantl 487	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0)
439	400	ffvelcdmda 7111	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞))
440		elrege0 13615	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞) ↔ (((𝐹‘𝑘)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑘)‘𝑥)))
441	440	simprbi 503	. . . . . . . . . 10 ⊢ (((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞) → 0 ≤ ((𝐹‘𝑘)‘𝑥))
442	439, 441	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘𝑘)‘𝑥))
443	442	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → 0 ≤ ((𝐹‘𝑘)‘𝑥))
444	438, 443	eqbrtrd 5131	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
445	436, 444	pm2.61dan 825	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
446	445	ralrimiva 3158	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
447		ovex 7479	. . . . . . . 8 ⊢ (𝑇 · (𝐻‘𝑥)) ∈ V
448	447, 407	ifex 4536	. . . . . . 7 ⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V
449	448	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V)
450		fvexd 6926	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ V)
451		eqidd 2764	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
452	400	feqmptd 6979	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑘)‘𝑥)))
453	403, 449, 450, 451, 452	ofrfval2 7741	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥)))
454	446, 453	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘))
455		itg2ub 26087	. . . 4 ⊢ (((𝐹‘𝑘):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) ≤ (∫2‘(𝐹‘𝑘)))
456	402, 422, 454, 455	syl3anc 1399	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) ≤ (∫2‘(𝐹‘𝑘)))
457	301	adantl 487	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
458	293, 404	itg1mulc 26058	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
459	420	fveq2d 6915	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))))
460	457, 458, 459	3eqtr2d 2804	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))))
461	343	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘)))
462	456, 460, 461	3brtr4d 5141	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘))
463	1, 2, 305, 386, 395, 396, 462	climle 15839	1 ⊢ (𝜑 → (𝑇 · (∫1‘𝐻)) ≤ 𝑆)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  {cab 2741   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092  ∅c0 4281  ifcif 4485  {csn 4588  ∪ cuni 4870  ∪ ciun 4954   class class class wbr 5106   ↦ cmpt 5190   × cxp 5654  ^◡ccnv 5655  dom cdm 5656  ran crn 5657   “ cima 5659   Fn wfn 6556  ⟶wf 6557  ‘cfv 6561  (class class class)co 7446   ∘_f cof 7718   ∘_r cofr 7719  supcsup 9462  ℂcc 11228  ℝcr 11229  0cc0 11230  1c1 11231   + caddc 11233   · cmul 11235  +∞cpnf 11370  -∞cmnf 11371  ℝ^*cxr 11372   < clt 11373   ≤ cle 11374   − cmin 11571   -cneg 11572  ℕcn 12365  (,)cioo 13506  [,)cico 13508  [,]cicc 13509   ⇝ cli 15683  volcvol 25817  MblFncmbf 25968  ∫₁citg1 25969  ∫₂citg2 25970

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-inf2 9672  ax-cc 10543  ax-cnex 11286  ax-resscn 11287  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-mulcom 11294  ax-addass 11295  ax-mulass 11296  ax-distr 11297  ax-i2m1 11298  ax-1ne0 11299  ax-1rid 11300  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303  ax-pre-lttri 11304  ax-pre-lttrn 11305  ax-pre-ltadd 11306  ax-pre-mulgt0 11307  ax-pre-sup 11308

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-disj 5074  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-se 5610  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-of 7720  df-ofr 7721  df-om 7905  df-1st 8028  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-1o 8507  df-2o 8508  df-oadd 8511  df-omul 8512  df-er 8748  df-map 8880  df-pm 8881  df-en 9005  df-dom 9006  df-sdom 9007  df-fin 9008  df-fi 9433  df-sup 9464  df-inf 9465  df-oi 9534  df-dju 10012  df-card 10050  df-acn 10053  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-sub 11573  df-neg 11574  df-div 12004  df-nn 12366  df-2 12435  df-3 12436  df-n0 12637  df-z 12724  df-uz 12996  df-q 13106  df-rp 13151  df-xneg 13271  df-xadd 13272  df-xmul 13273  df-ioo 13510  df-ioc 13511  df-ico 13512  df-icc 13513  df-fz 13670  df-fzo 13819  df-fl 13962  df-seq 14175  df-exp 14235  df-hash 14505  df-cj 15298  df-re 15299  df-im 15300  df-sqrt 15434  df-abs 15435  df-clim 15687  df-rlim 15688  df-sum 15886  df-rest 17625  df-topgen 17646  df-psmet 21703  df-xmet 21704  df-met 21705  df-bl 21706  df-mopn 21707  df-top 23245  df-topon 23262  df-bases 23297  df-cmp 23738  df-ovol 25818  df-vol 25819  df-mbf 25973  df-itg1 25974  df-itg2 25975

This theorem is used by:  itg2monolem3  26106