Theorem itg2monolem1 25707

Description: Lemma for itg2mono 25710. We show that for any constant 𝑡 less than one, 𝑡 · ∫₁𝐻 is less than 𝑆, and so ∫₁𝐻 ≤ 𝑆, which is one half of the equality in itg2mono 25710. 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 25671. 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 12790	. 2 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12522	. 2 ⊢ (𝜑 → 1 ∈ ℤ)
3		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
4		readdcl 11109	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
5	4	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
6		itg2mono.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))
7		rge0ssre 13372	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ ℝ
8		fss 6678	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘𝑛):ℝ⟶ℝ)
9	6, 7, 8	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶ℝ)
10		itg2mono.8	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∈ dom ∫1)
11		itg2mono.7	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑇 ∈ (0(,)1))
12		0xr 11179	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ*
13		1xr 11191	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ*
14		elioo2 13302	. . . . . . . . . . . . . . . . . . . . . 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 11564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -𝑇 ∈ ℝ)
19	10, 18	i1fmulc 25660	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1)
20	19	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1)
21		i1ff 25633	. . . . . . . . . . . . . . . 16 ⊢ (((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1 → ((ℝ × {-𝑇}) ∘f · 𝐻):ℝ⟶ℝ)
22	20, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻):ℝ⟶ℝ)
23		reex 11117	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
24	23	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℝ ∈ V)
25		inidm 4179	. . . . . . . . . . . . . . 15 ⊢ (ℝ ∩ ℝ) = ℝ
26	5, 9, 22, 24, 24, 25	off 7640	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)):ℝ⟶ℝ)
27	26	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)):ℝ⟶ℝ)
28	27	ffnd 6663	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) Fn ℝ)
29		elpreima 7003	. . . . . . . . . . . 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 13360	. . . . . . . . . . . 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 7029	. . . . . . . . . . . 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 6663	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) Fn ℝ)
38	22	ffnd 6663	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) Fn ℝ)
39		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑥))
40	18	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → -𝑇 ∈ ℝ)
41		i1ff 25633	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐻 ∈ dom ∫1 → 𝐻:ℝ⟶ℝ)
42	10, 41	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻:ℝ⟶ℝ)
43	42	ffnd 6663	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻 Fn ℝ)
44	43	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐻 Fn ℝ)
45		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) = (𝐻‘𝑥))
46	24, 40, 44, 45	ofc1 7650	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ × {-𝑇}) ∘f · 𝐻)‘𝑥) = (-𝑇 · (𝐻‘𝑥)))
47	17	recnd 11160	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ ℂ)
48	47	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
49	42	ffvelcdmda 7029	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
50	49	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
51	50	recnd 11160	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℂ)
52	48, 51	mulneg1d 11590	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (-𝑇 · (𝐻‘𝑥)) = -(𝑇 · (𝐻‘𝑥)))
53	46, 52	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ × {-𝑇}) ∘f · 𝐻)‘𝑥) = -(𝑇 · (𝐻‘𝑥)))
54	37, 38, 24, 24, 25, 39, 53	ofval 7633	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))))
55	9	ffvelcdmda 7029	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ)
56	55	recnd 11160	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℂ)
57	17	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
58	57, 49	remulcld 11162	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
59	58	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
60	59	recnd 11160	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℂ)
61	56, 60	negsubd 11498	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))))
62	54, 61	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))))
63	62	breq1d 5108	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0 ↔ (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0))
64		0red 11135	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
65	55, 59, 64	ltsubaddd 11733	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0 ↔ ((𝐹‘𝑛)‘𝑥) < (0 + (𝑇 · (𝐻‘𝑥)))))
66	60	addlidd 11334	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (0 + (𝑇 · (𝐻‘𝑥))) = (𝑇 · (𝐻‘𝑥)))
67	66	breq2d 5110	. . . . . . . . . . 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 3911	. . . . . . . . . 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 11279	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ ¬ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
75	70, 73, 74	3bitr4d 311	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)))
76	75	rabbi2dva 4178	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})
77		rembl 25497	. . . . . . 7 ⊢ ℝ ∈ dom vol
78		itg2mono.2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)
79		i1fmbf 25632	. . . . . . . . . . 11 ⊢ (((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1 → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ MblFn)
80	20, 79	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ MblFn)
81	78, 80	mbfadd 25618	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) ∈ MblFn)
82		mbfima 25587	. . . . . . . . 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 25491	. . . . . . . 8 ⊢ ((◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol → (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
85	83, 84	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
86		inmbl 25499	. . . . . . 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 2837	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} ∈ dom vol)
89		itg2mono.11	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})
90	88, 89	fmptd 7059	. . . 4 ⊢ (𝜑 → 𝐴:ℕ⟶dom vol)
91		itg2mono.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
92	91	ralrimiva 3128	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
93		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
94		fvoveq1 7381	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
95	93, 94	breq12d 5111	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1))))
96	95	cbvralvw 3214	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
97	92, 96	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
98	97	r19.21bi 3228	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
99	6	ralrimiva 3128	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞))
100	93	feq1d 6644	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑗):ℝ⟶(0[,)+∞)))
101	100	cbvralvw 3214	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞))
102	99, 101	sylib 218	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞))
103	102	r19.21bi 3228	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞))
104	103	ffnd 6663	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) Fn ℝ)
105		peano2nn 12157	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
106		fveq2 6834	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑗 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑗 + 1)))
107	106	feq1d 6644	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞)))
108	107	rspccva 3575	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (𝑗 + 1) ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞))
109	99, 105, 108	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞))
110	109	ffnd 6663	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) Fn ℝ)
111	23	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℝ ∈ V)
112		eqidd 2737	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) = ((𝐹‘𝑗)‘𝑥))
113		eqidd 2737	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥))
114	104, 110, 111, 111, 25, 112, 113	ofrfval 7632	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)) ↔ ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
115	98, 114	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))
116	115	r19.21bi 3228	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))
117	17	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
118	42	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐻:ℝ⟶ℝ)
119	118	ffvelcdmda 7029	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
120	117, 119	remulcld 11162	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
121		fss 6678	. . . . . . . . . 10 ⊢ (((𝐹‘𝑗):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘𝑗):ℝ⟶ℝ)
122	103, 7, 121	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶ℝ)
123	122	ffvelcdmda 7029	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
124		fss 6678	. . . . . . . . . 10 ⊢ (((𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘(𝑗 + 1)):ℝ⟶ℝ)
125	109, 7, 124	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶ℝ)
126	125	ffvelcdmda 7029	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ)
127		letr 11227	. . . . . . . 8 ⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
128	120, 123, 126, 127	syl3anc 1373	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
129	116, 128	mpan2d 694	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
130	129	ss2rabdv 4027	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ⊆ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
131	93	fveq1d 6836	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑗)‘𝑥))
132	131	breq2d 5110	. . . . . . . 8 ⊢ (𝑛 = 𝑗 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
133	132	rabbidv 3406	. . . . . . 7 ⊢ (𝑛 = 𝑗 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
134	23	rabex 5284	. . . . . . 7 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ∈ V
135	133, 89, 134	fvmpt 6941	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
136	135	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
137	105	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
138	106	fveq1d 6836	. . . . . . . . 9 ⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥))
139	138	breq2d 5110	. . . . . . . 8 ⊢ (𝑛 = (𝑗 + 1) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
140	139	rabbidv 3406	. . . . . . 7 ⊢ (𝑛 = (𝑗 + 1) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
141	23	rabex 5284	. . . . . . 7 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)} ∈ V
142	140, 89, 141	fvmpt 6941	. . . . . 6 ⊢ ((𝑗 + 1) ∈ ℕ → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
143	137, 142	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
144	130, 136, 143	3sstr4d 3989	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ⊆ (𝐴‘(𝑗 + 1)))
145	58	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
146	49	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℝ)
147	55	an32s 652	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ)
148	147	fmpttd 7060	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ)
149	148	frnd 6670	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ)
150		1nn 12156	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ
151		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))
152	151, 147	dmmptd 6637	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ℕ)
153	150, 152	eleqtrrid 2843	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)))
154	153	ne0d 4294	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
155		dm0rn0 5873	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅)
156	155	necon3bii 2984	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
157	154, 156	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
158		itg2mono.5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
159	148	ffnd 6663	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ)
160		breq1 5101	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
161	160	ralrn 7033	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
162	159, 161	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
163		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
164	163	fveq1d 6836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑚)‘𝑥))
165		fvex 6847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑚)‘𝑥) ∈ V
166	164, 151, 165	fvmpt 6941	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥))
167	166	breq1d 5108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦))
168	167	ralbiia 3080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)
169	164	breq1d 5108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦))
170	169	cbvralvw 3214	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)
171	168, 170	bitr4i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
172	162, 171	bitrdi 287	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦))
173	172	rexbidv 3160	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦))
174	158, 173	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦)
175	149, 157, 174	suprcld 12105	. . . . . . . . . . . . . . 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 11133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 1 ∈ ℝ)
181		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 0 < (𝐻‘𝑥))
182		ltmul1 11991	. . . . . . . . . . . . . . . . 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 11160	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℂ)
186	185	mullidd 11150	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (1 · (𝐻‘𝑥)) = (𝐻‘𝑥))
187	184, 186	breqtrd 5124	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < (𝐻‘𝑥))
188		itg2mono.9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∘r ≤ 𝐺)
189		itg2mono.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
190	175, 189	fmptd 7059	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)
191	190	ffnd 6663	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 Fn ℝ)
192	23	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ∈ V)
193		eqidd 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐻‘𝑦) = (𝐻‘𝑦))
194		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑦))
195	194	mpteq2dv 5192	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)))
196	195	rneqd 5887	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)))
197	196	supeq1d 9349	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
198		ltso 11213	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < Or ℝ
199	198	supex 9367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ) ∈ V
200	197, 189, 199	fvmpt 6941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
201	200	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
202	43, 191, 192, 192, 25, 193, 201	ofrfval 7632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐻 ∘r ≤ 𝐺 ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )))
203	188, 202	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
204		fveq2 6834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦))
205	204, 197	breq12d 5111	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )))
206	205	cbvralvw 3214	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
207	203, 206	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
208	207	r19.21bi 3228	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
209	208	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
210	145, 146, 176, 187, 209	ltletrd 11293	. . . . . . . . . . . . 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 12106	. . . . . . . . . . . . . 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 5102	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) → ((𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
219	218	rexrn 7032	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
220	217, 219	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
221		fvex 6847	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑗)‘𝑥) ∈ V
222	131, 151, 221	fvmpt 6941	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) = ((𝐹‘𝑗)‘𝑥))
223	222	breq2d 5110	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → ((𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)))
224	223	rexbiia 3081	. . . . . . . . . . . . 13 ⊢ (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))
225	220, 224	bitrdi 287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)))
226	216, 225	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))
227	179, 146	remulcld 11162	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
228	103	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞))
229		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈ ℝ)
230	228, 229	ffvelcdmd 7030	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞))
231		elrege0 13370	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞) ↔ (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
232	230, 231	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
233	232	simpld 494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
234	233	adantlrr 721	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
235		ltle 11221	. . . . . . . . . . . . 13 ⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
236	227, 234, 235	syl2an2r 685	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
237	236	reximdva 3149	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
238	226, 237	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
239	238	anassrs 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 0 < (𝐻‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
240	150	ne0ii 4296	. . . . . . . . . . 11 ⊢ ℕ ≠ ∅
241	58	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
242	241	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
243		0red 11135	. . . . . . . . . . . . 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 11994	. . . . . . . . . . . . . . . 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 11160	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℂ)
256	255	mul01d 11332	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · 0) = 0)
257	254, 256	breqtrd 5124	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ 0)
258	244	simprd 495	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 ≤ ((𝐹‘𝑗)‘𝑥))
259	242, 243, 245, 257, 258	letrd 11290	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
260	259	ralrimiva 3128	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
261		r19.2z 4452	. . . . . . . . . . 11 ⊢ ((ℕ ≠ ∅ ∧ ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
262	240, 260, 261	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
263	262	anassrs 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐻‘𝑥) ≤ 0) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
264		0red 11135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
265	239, 263, 264, 49	ltlecasei 11241	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
266	265	ralrimiva 3128	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
267		rabid2 3432	. . . . . . 7 ⊢ (ℝ = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
268	266, 267	sylibr 234	. . . . . 6 ⊢ (𝜑 → ℝ = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
269		iunrab 5008	. . . . . 6 ⊢ ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}
270	268, 269	eqtr4di 2789	. . . . 5 ⊢ (𝜑 → ℝ = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
271	136	iuneq2dv 4971	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
272	90	ffnd 6663	. . . . . 6 ⊢ (𝜑 → 𝐴 Fn ℕ)
273		fniunfv 7193	. . . . . 6 ⊢ (𝐴 Fn ℕ → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴)
274	272, 273	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴)
275	270, 271, 274	3eqtr2rd 2778	. . . 4 ⊢ (𝜑 → ∪ ran 𝐴 = ℝ)
276		eqid 2736	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))
277	90, 144, 275, 10, 276	itg1climres 25671	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ⇝ (∫1‘𝐻))
278		nnex 12151	. . . . 5 ⊢ ℕ ∈ V
279	278	mptex 7169	. . . 4 ⊢ (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V
280	279	a1i 11	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V)
281		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘))
282	281	eleq2d 2822	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ (𝐴‘𝑗) ↔ 𝑥 ∈ (𝐴‘𝑘)))
283	282	ifbid 4503	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0) = if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))
284	283	mpteq2dv 5192	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))
285	284	fveq2d 6838	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
286		eqid 2736	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))
287		fvex 6847	. . . . . . 7 ⊢ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ V
288	285, 286, 287	fvmpt 6941	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
289	288	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
290	90	ffvelcdmda 7029	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ dom vol)
291		eqid 2736	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))
292	291	i1fres 25662	. . . . . . 7 ⊢ ((𝐻 ∈ dom ∫1 ∧ (𝐴‘𝑘) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1)
293	10, 290, 292	syl2an2r 685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1)
294		itg1cl 25642	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ)
295	293, 294	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ)
296	289, 295	eqeltrd 2836	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℝ)
297	296	recnd 11160	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℂ)
298	285	oveq2d 7374	. . . . . 6 ⊢ (𝑗 = 𝑘 → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
299		eqid 2736	. . . . . 6 ⊢ (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) = (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))
300		ovex 7391	. . . . . 6 ⊢ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) ∈ V
301	298, 299, 300	fvmpt 6941	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
302	288	oveq2d 7374	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝑇 · ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘)) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
303	301, 302	eqtr4d 2774	. . . 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 15560	. 2 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ⇝ (𝑇 · (∫1‘𝐻)))
306		icossicc 13352	. . . . . . 7 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
307		fss 6678	. . . . . . 7 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑛):ℝ⟶(0[,]+∞))
308	6, 306, 307	sylancl 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,]+∞))
309		itg2mono.10	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ)
310	309	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ∈ ℝ)
311		itg2cl 25689	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛):ℝ⟶(0[,]+∞) → (∫2‘(𝐹‘𝑛)) ∈ ℝ*)
312	308, 311	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ℝ*)
313	312	fmpttd 7060	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))):ℕ⟶ℝ*)
314	313	frnd 6670	. . . . . . . 8 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ*)
315		fvex 6847	. . . . . . . . . . 11 ⊢ (∫2‘(𝐹‘𝑛)) ∈ V
316	315	elabrex 7188	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))})
317	316	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))})
318		eqid 2736	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))
319	318	rnmpt 5906	. . . . . . . . 9 ⊢ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))}
320	317, 319	eleqtrrdi 2847	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))))
321		supxrub 13239	. . . . . . . 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 5140	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ 𝑆)
325		itg2lecl 25695	. . . . . 6 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ 𝑆 ∈ ℝ ∧ (∫2‘(𝐹‘𝑛)) ≤ 𝑆) → (∫2‘(𝐹‘𝑛)) ∈ ℝ)
326	308, 310, 324, 325	syl3anc 1373	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ℝ)
327	326	fmpttd 7060	. . . 4 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))):ℕ⟶ℝ)
328	308	ralrimiva 3128	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞))
329		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
330	329	feq1d 6644	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,]+∞)))
331	330	cbvralvw 3214	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞))
332	328, 331	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞))
333		peano2nn 12157	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
334		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1)))
335	334	feq1d 6644	. . . . . . . . . 10 ⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘):ℝ⟶(0[,]+∞) ↔ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞)))
336	335	rspccva 3575	. . . . . . . . 9 ⊢ ((∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞) ∧ (𝑛 + 1) ∈ ℕ) → (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞))
337	332, 333, 336	syl2an 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞))
338		itg2le 25696	. . . . . . . 8 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞) ∧ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1))) → (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
339	308, 337, 91, 338	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
340	339	ralrimiva 3128	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
341		2fveq3 6839	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘𝑘)))
342		fvex 6847	. . . . . . . . . 10 ⊢ (∫2‘(𝐹‘𝑘)) ∈ V
343	341, 318, 342	fvmpt 6941	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘)))
344		peano2nn 12157	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
345		2fveq3 6839	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑘 + 1) → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘(𝑘 + 1))))
346		fvex 6847	. . . . . . . . . . 11 ⊢ (∫2‘(𝐹‘(𝑘 + 1))) ∈ V
347	345, 318, 346	fvmpt 6941	. . . . . . . . . 10 ⊢ ((𝑘 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1))))
348	344, 347	syl 17	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1))))
349	343, 348	breq12d 5111	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))))
350	349	ralbiia 3080	. . . . . . 7 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1))))
351		fvoveq1 7381	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1)))
352	351	fveq2d 6838	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘(𝑛 + 1))) = (∫2‘(𝐹‘(𝑘 + 1))))
353	341, 352	breq12d 5111	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))))
354	353	cbvralvw 3214	. . . . . . 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 3228	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)))
358	324	ralrimiva 3128	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆)
359	343	breq1d 5108	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥))
360	359	ralbiia 3080	. . . . . . . 8 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)
361	341	breq1d 5108	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥))
362	361	cbvralvw 3214	. . . . . . . 8 ⊢ (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)
363	360, 362	bitr4i 278	. . . . . . 7 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥)
364		breq2 5102	. . . . . . . 8 ⊢ (𝑥 = 𝑆 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
365	364	ralbidv 3159	. . . . . . 7 ⊢ (𝑥 = 𝑆 → (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
366	363, 365	bitrid 283	. . . . . 6 ⊢ (𝑥 = 𝑆 → (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
367	366	rspcev 3576	. . . . 5 ⊢ ((𝑆 ∈ ℝ ∧ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)
368	309, 358, 367	syl2anc 584	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)
369	1, 2, 327, 357, 368	climsup 15593	. . 3 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
370	327	frnd 6670	. . . . 5 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ)
371	318, 312	dmmptd 6637	. . . . . . 7 ⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ℕ)
372	240	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℕ ≠ ∅)
373	371, 372	eqnetrd 2999	. . . . . 6 ⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
374		dm0rn0 5873	. . . . . . 7 ⊢ (dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ∅)
375	374	necon3bii 2984	. . . . . 6 ⊢ (dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
376	373, 375	sylib 218	. . . . 5 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
377	315, 318	fnmpti 6635	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) Fn ℕ
378		breq1 5101	. . . . . . . . 9 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) → (𝑧 ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
379	378	ralrn 7033	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
380	377, 379	mp1i 13	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
381	380	rexbidv 3160	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
382	368, 381	mpbird 257	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥)
383		supxrre 13242	. . . . 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 2784	. . 3 ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ) = 𝑆)
386	369, 385	breqtrd 5124	. 2 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⇝ 𝑆)
387	17	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℝ)
388	90	ffvelcdmda 7029	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ∈ dom vol)
389	276	i1fres 25662	. . . . . . 7 ⊢ ((𝐻 ∈ dom ∫1 ∧ (𝐴‘𝑗) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1)
390	10, 388, 389	syl2an2r 685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1)
391		itg1cl 25642	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ)
392	390, 391	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ)
393	387, 392	remulcld 11162	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ∈ ℝ)
394	393	fmpttd 7060	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))):ℕ⟶ℝ)
395	394	ffvelcdmda 7029	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ∈ ℝ)
396	327	ffvelcdmda 7029	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ∈ ℝ)
397	329	feq1d 6644	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,)+∞)))
398	397	cbvralvw 3214	. . . . . . 7 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞))
399	99, 398	sylib 218	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞))
400	399	r19.21bi 3228	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):ℝ⟶(0[,)+∞))
401		fss 6678	. . . . 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 6847	. . . . . . . . 9 ⊢ (𝐻‘𝑥) ∈ V
407		c0ex 11126	. . . . . . . . 9 ⊢ 0 ∈ V
408	406, 407	ifex 4530	. . . . . . . 8 ⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V
409	408	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V)
410		fconstmpt 5686	. . . . . . . 8 ⊢ (ℝ × {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇)
411	410	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℝ × {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇))
412		eqidd 2737	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))
413	403, 405, 409, 411, 412	offval2 7642	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
414		ovif2 7457	. . . . . . . 8 ⊢ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0))
415	47	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 ∈ ℂ)
416	415	mul01d 11332	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · 0) = 0)
417	416	ifeq2d 4500	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))
418	414, 417	eqtrid 2783	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))
419	418	mpteq2dv 5192	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
420	413, 419	eqtrd 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
421	293, 404	i1fmulc 25660	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ dom ∫1)
422	420, 421	eqeltrrd 2837	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom ∫1)
423		iftrue 4485	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥)))
424	423	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥)))
425	329	fveq1d 6836	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑘)‘𝑥))
426	425	breq2d 5110	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)))
427	426	rabbidv 3406	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
428	23	rabex 5284	. . . . . . . . . . . . 13 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ∈ V
429	427, 89, 428	fvmpt 6941	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
430	429	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
431	430	eleq2d 2822	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)}))
432	431	biimpa 476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
433		rabid 3420	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ↔ (𝑥 ∈ ℝ ∧ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)))
434	433	simprbi 496	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))
435	432, 434	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))
436	424, 435	eqbrtrd 5120	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
437		iffalse 4488	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0)
438	437	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0)
439	400	ffvelcdmda 7029	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞))
440		elrege0 13370	. . . . . . . . . . 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 5120	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
445	436, 444	pm2.61dan 812	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
446	445	ralrimiva 3128	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
447		ovex 7391	. . . . . . . 8 ⊢ (𝑇 · (𝐻‘𝑥)) ∈ V
448	447, 407	ifex 4530	. . . . . . 7 ⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V
449	448	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V)
450		fvexd 6849	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ V)
451		eqidd 2737	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
452	400	feqmptd 6902	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑘)‘𝑥)))
453	403, 449, 450, 451, 452	ofrfval2 7643	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥)))
454	446, 453	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘))
455		itg2ub 25690	. . . 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 25661	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
459	420	fveq2d 6838	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))))
460	457, 458, 459	3eqtr2d 2777	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))))
461	343	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘)))
462	456, 460, 461	3brtr4d 5130	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘))
463	1, 2, 305, 386, 395, 396, 462	climle 15563	1 ⊢ (𝜑 → (𝑇 · (∫1‘𝐻)) ≤ 𝑆)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  {cab 2714   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  {crab 3399  Vcvv 3440   ∖ cdif 3898   ∩ cin 3900   ⊆ wss 3901  ∅c0 4285  ifcif 4479  {csn 4580  ∪ cuni 4863  ∪ ciun 4946   class class class wbr 5098   ↦ cmpt 5179   × cxp 5622  ^◡ccnv 5623  dom cdm 5624  ran crn 5625   “ cima 5627   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492  (class class class)co 7358   ∘_f cof 7620   ∘_r cofr 7621  supcsup 9343  ℂcc 11024  ℝcr 11025  0cc0 11026  1c1 11027   + caddc 11029   · cmul 11031  +∞cpnf 11163  -∞cmnf 11164  ℝ^*cxr 11165   < clt 11166   ≤ cle 11167   − cmin 11364  -cneg 11365  ℕcn 12145  (,)cioo 13261  [,)cico 13263  [,]cicc 13264   ⇝ cli 15407  volcvol 25420  MblFncmbf 25571  ∫₁citg1 25572  ∫₂citg2 25573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-inf2 9550  ax-cc 10345  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103  ax-pre-sup 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-disj 5066  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7622  df-ofr 7623  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-2o 8398  df-oadd 8401  df-omul 8402  df-er 8635  df-map 8765  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9314  df-sup 9345  df-inf 9346  df-oi 9415  df-dju 9813  df-card 9851  df-acn 9854  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-div 11795  df-nn 12146  df-2 12208  df-3 12209  df-n0 12402  df-z 12489  df-uz 12752  df-q 12862  df-rp 12906  df-xneg 13026  df-xadd 13027  df-xmul 13028  df-ioo 13265  df-ioc 13266  df-ico 13267  df-icc 13268  df-fz 13424  df-fzo 13571  df-fl 13712  df-seq 13925  df-exp 13985  df-hash 14254  df-cj 15022  df-re 15023  df-im 15024  df-sqrt 15158  df-abs 15159  df-clim 15411  df-rlim 15412  df-sum 15610  df-rest 17342  df-topgen 17363  df-psmet 21301  df-xmet 21302  df-met 21303  df-bl 21304  df-mopn 21305  df-top 22838  df-topon 22855  df-bases 22890  df-cmp 23331  df-ovol 25421  df-vol 25422  df-mbf 25576  df-itg1 25577  df-itg2 25578

This theorem is referenced by:  itg2monolem3  25709