Theorem itg2monolem1 25786

Description: Lemma for itg2mono 25789. We show that for any constant 𝑡 less than one, 𝑡 · ∫₁𝐻 is less than 𝑆, and so ∫₁𝐻 ≤ 𝑆, which is one half of the equality in itg2mono 25789. 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 25750. 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 12922	. 2 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12650	. 2 ⊢ (𝜑 → 1 ∈ ℤ)
3		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
4		readdcl 11239	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
5	4	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
6		itg2mono.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))
7		rge0ssre 13497	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ ℝ
8		fss 6751	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘𝑛):ℝ⟶ℝ)
9	6, 7, 8	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶ℝ)
10		itg2mono.8	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∈ dom ∫1)
11		itg2mono.7	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑇 ∈ (0(,)1))
12		0xr 11309	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ*
13		1xr 11321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ*
14		elioo2 13429	. . . . . . . . . . . . . . . . . . . . . 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 11691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -𝑇 ∈ ℝ)
19	10, 18	i1fmulc 25739	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1)
20	19	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1)
21		i1ff 25712	. . . . . . . . . . . . . . . 16 ⊢ (((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1 → ((ℝ × {-𝑇}) ∘f · 𝐻):ℝ⟶ℝ)
22	20, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻):ℝ⟶ℝ)
23		reex 11247	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
24	23	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℝ ∈ V)
25		inidm 4226	. . . . . . . . . . . . . . 15 ⊢ (ℝ ∩ ℝ) = ℝ
26	5, 9, 22, 24, 24, 25	off 7716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)):ℝ⟶ℝ)
27	26	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)):ℝ⟶ℝ)
28	27	ffnd 6736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) Fn ℝ)
29		elpreima 7077	. . . . . . . . . . . 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 13485	. . . . . . . . . . . 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 7103	. . . . . . . . . . . 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 6736	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) Fn ℝ)
38	22	ffnd 6736	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) Fn ℝ)
39		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑥))
40	18	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → -𝑇 ∈ ℝ)
41		i1ff 25712	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐻 ∈ dom ∫1 → 𝐻:ℝ⟶ℝ)
42	10, 41	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻:ℝ⟶ℝ)
43	42	ffnd 6736	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻 Fn ℝ)
44	43	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐻 Fn ℝ)
45		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) = (𝐻‘𝑥))
46	24, 40, 44, 45	ofc1 7726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ × {-𝑇}) ∘f · 𝐻)‘𝑥) = (-𝑇 · (𝐻‘𝑥)))
47	17	recnd 11290	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ ℂ)
48	47	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
49	42	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
50	49	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
51	50	recnd 11290	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℂ)
52	48, 51	mulneg1d 11717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (-𝑇 · (𝐻‘𝑥)) = -(𝑇 · (𝐻‘𝑥)))
53	46, 52	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ × {-𝑇}) ∘f · 𝐻)‘𝑥) = -(𝑇 · (𝐻‘𝑥)))
54	37, 38, 24, 24, 25, 39, 53	ofval 7709	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))))
55	9	ffvelcdmda 7103	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ)
56	55	recnd 11290	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℂ)
57	17	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
58	57, 49	remulcld 11292	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
59	58	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
60	59	recnd 11290	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℂ)
61	56, 60	negsubd 11627	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))))
62	54, 61	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))))
63	62	breq1d 5152	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0 ↔ (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0))
64		0red 11265	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
65	55, 59, 64	ltsubaddd 11860	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0 ↔ ((𝐹‘𝑛)‘𝑥) < (0 + (𝑇 · (𝐻‘𝑥)))))
66	60	addlidd 11463	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (0 + (𝑇 · (𝐻‘𝑥))) = (𝑇 · (𝐻‘𝑥)))
67	66	breq2d 5154	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛)‘𝑥) < (0 + (𝑇 · (𝐻‘𝑥))) ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
68	63, 65, 67	3bitrd 305	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻))‘𝑥) < 0 ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
69	31, 36, 68	3bitrd 305	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
70	69	notbid 318	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ↔ ¬ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
71		eldif 3960	. . . . . . . . . 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 11408	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ ¬ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥))))
75	70, 73, 74	3bitr4d 311	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)))
76	75	rabbi2dva 4225	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)))) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})
77		rembl 25576	. . . . . . 7 ⊢ ℝ ∈ dom vol
78		itg2mono.2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)
79		i1fmbf 25711	. . . . . . . . . . 11 ⊢ (((ℝ × {-𝑇}) ∘f · 𝐻) ∈ dom ∫1 → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ MblFn)
80	20, 79	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ × {-𝑇}) ∘f · 𝐻) ∈ MblFn)
81	78, 80	mbfadd 25697	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) ∈ MblFn)
82		mbfima 25666	. . . . . . . . 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 25570	. . . . . . . 8 ⊢ ((◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0)) ∈ dom vol → (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
85	83, 84	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∖ (◡((𝐹‘𝑛) ∘f + ((ℝ × {-𝑇}) ∘f · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
86		inmbl 25578	. . . . . . 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 2841	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} ∈ dom vol)
89		itg2mono.11	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})
90	88, 89	fmptd 7133	. . . 4 ⊢ (𝜑 → 𝐴:ℕ⟶dom vol)
91		itg2mono.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
92	91	ralrimiva 3145	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))
93		fveq2 6905	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
94		fvoveq1 7455	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1)))
95	93, 94	breq12d 5155	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1))))
96	95	cbvralvw 3236	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
97	92, 96	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
98	97	r19.21bi 3250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)))
99	6	ralrimiva 3145	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞))
100	93	feq1d 6719	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑗):ℝ⟶(0[,)+∞)))
101	100	cbvralvw 3236	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞))
102	99, 101	sylib 218	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞))
103	102	r19.21bi 3250	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞))
104	103	ffnd 6736	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) Fn ℝ)
105		peano2nn 12279	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
106		fveq2 6905	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑗 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑗 + 1)))
107	106	feq1d 6719	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞)))
108	107	rspccva 3620	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (𝑗 + 1) ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞))
109	99, 105, 108	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞))
110	109	ffnd 6736	. . . . . . . . . 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 7708	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∘r ≤ (𝐹‘(𝑗 + 1)) ↔ ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
115	98, 114	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))
116	115	r19.21bi 3250	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))
117	17	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
118	42	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐻:ℝ⟶ℝ)
119	118	ffvelcdmda 7103	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ)
120	117, 119	remulcld 11292	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
121		fss 6751	. . . . . . . . . 10 ⊢ (((𝐹‘𝑗):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘𝑗):ℝ⟶ℝ)
122	103, 7, 121	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶ℝ)
123	122	ffvelcdmda 7103	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
124		fss 6751	. . . . . . . . . 10 ⊢ (((𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹‘(𝑗 + 1)):ℝ⟶ℝ)
125	109, 7, 124	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)):ℝ⟶ℝ)
126	125	ffvelcdmda 7103	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ)
127		letr 11356	. . . . . . . 8 ⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
128	120, 123, 126, 127	syl3anc 1372	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
129	116, 128	mpan2d 694	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
130	129	ss2rabdv 4075	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ⊆ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
131	93	fveq1d 6907	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑗)‘𝑥))
132	131	breq2d 5154	. . . . . . . 8 ⊢ (𝑛 = 𝑗 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
133	132	rabbidv 3443	. . . . . . 7 ⊢ (𝑛 = 𝑗 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
134	23	rabex 5338	. . . . . . 7 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ∈ V
135	133, 89, 134	fvmpt 7015	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
136	135	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
137	105	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
138	106	fveq1d 6907	. . . . . . . . 9 ⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥))
139	138	breq2d 5154	. . . . . . . 8 ⊢ (𝑛 = (𝑗 + 1) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)))
140	139	rabbidv 3443	. . . . . . 7 ⊢ (𝑛 = (𝑗 + 1) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
141	23	rabex 5338	. . . . . . 7 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)} ∈ V
142	140, 89, 141	fvmpt 7015	. . . . . 6 ⊢ ((𝑗 + 1) ∈ ℕ → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
143	137, 142	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)})
144	130, 136, 143	3sstr4d 4038	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ⊆ (𝐴‘(𝑗 + 1)))
145	58	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
146	49	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℝ)
147	55	an32s 652	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ)
148	147	fmpttd 7134	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ)
149	148	frnd 6743	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ)
150		1nn 12278	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ
151		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))
152	151, 147	dmmptd 6712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ℕ)
153	150, 152	eleqtrrid 2847	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)))
154	153	ne0d 4341	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
155		dm0rn0 5934	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅)
156	155	necon3bii 2992	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
157	154, 156	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅)
158		itg2mono.5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
159	148	ffnd 6736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ)
160		breq1 5145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
161	160	ralrn 7107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
162	159, 161	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦))
163		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
164	163	fveq1d 6907	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑚)‘𝑥))
165		fvex 6918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑚)‘𝑥) ∈ V
166	164, 151, 165	fvmpt 7015	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥))
167	166	breq1d 5152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦))
168	167	ralbiia 3090	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)
169	164	breq1d 5152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦))
170	169	cbvralvw 3236	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)
171	168, 170	bitr4i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)
172	162, 171	bitrdi 287	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦))
173	172	rexbidv 3178	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦))
174	158, 173	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦)
175	149, 157, 174	suprcld 12232	. . . . . . . . . . . . . . 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 11263	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 1 ∈ ℝ)
181		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 0 < (𝐻‘𝑥))
182		ltmul1 12118	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐻‘𝑥) ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 < 1 ↔ (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥))))
183	179, 180, 146, 181, 182	syl112anc 1375	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 < 1 ↔ (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥))))
184	178, 183	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥)))
185	146	recnd 11290	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℂ)
186	185	mullidd 11280	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (1 · (𝐻‘𝑥)) = (𝐻‘𝑥))
187	184, 186	breqtrd 5168	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < (𝐻‘𝑥))
188		itg2mono.9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ∘r ≤ 𝐺)
189		itg2mono.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
190	175, 189	fmptd 7133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)
191	190	ffnd 6736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 Fn ℝ)
192	23	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ∈ V)
193		eqidd 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐻‘𝑦) = (𝐻‘𝑦))
194		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑦))
195	194	mpteq2dv 5243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)))
196	195	rneqd 5948	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)))
197	196	supeq1d 9487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
198		ltso 11342	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < Or ℝ
199	198	supex 9504	. . . . . . . . . . . . . . . . . . . . 21 ⊢ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ) ∈ V
200	197, 189, 199	fvmpt 7015	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℝ → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
201	200	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
202	43, 191, 192, 192, 25, 193, 201	ofrfval 7708	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐻 ∘r ≤ 𝐺 ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )))
203	188, 202	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
204		fveq2 6905	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦))
205	204, 197	breq12d 5155	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )))
206	205	cbvralvw 3236	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))
207	203, 206	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
208	207	r19.21bi 3250	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
209	208	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))
210	145, 146, 176, 187, 209	ltletrd 11422	. . . . . . . . . . . . 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 12233	. . . . . . . . . . . . . 14 ⊢ (((ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) ∧ (𝑇 · (𝐻‘𝑥)) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤))
215	211, 212, 213, 145, 214	syl31anc 1374	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ((𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤))
216	210, 215	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤)
217	159	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ)
218		breq2 5146	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) → ((𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
219	218	rexrn 7106	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
220	217, 219	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗)))
221		fvex 6918	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑗)‘𝑥) ∈ V
222	131, 151, 221	fvmpt 7015	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) = ((𝐹‘𝑗)‘𝑥))
223	222	breq2d 5154	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → ((𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)))
224	223	rexbiia 3091	. . . . . . . . . . . . 13 ⊢ (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))
225	220, 224	bitrdi 287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)))
226	216, 225	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))
227	179, 146	remulcld 11292	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
228	103	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞))
229		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈ ℝ)
230	228, 229	ffvelcdmd 7104	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞))
231		elrege0 13495	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞) ↔ (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
232	230, 231	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥)))
233	232	simpld 494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
234	233	adantlrr 721	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ)
235		ltle 11350	. . . . . . . . . . . . 13 ⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
236	227, 234, 235	syl2an2r 685	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
237	236	reximdva 3167	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)))
238	226, 237	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
239	238	anassrs 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 0 < (𝐻‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
240	150	ne0ii 4343	. . . . . . . . . . 11 ⊢ ℕ ≠ ∅
241	58	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
242	241	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ)
243		0red 11265	. . . . . . . . . . . . 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 12121	. . . . . . . . . . . . . . . 16 ⊢ (((𝐻‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) → ((𝐻‘𝑥) ≤ 0 ↔ (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0)))
253	248, 243, 249, 251, 252	syl112anc 1375	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑥) ≤ 0 ↔ (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0)))
254	246, 253	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0))
255	249	recnd 11290	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℂ)
256	255	mul01d 11461	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · 0) = 0)
257	254, 256	breqtrd 5168	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ 0)
258	244	simprd 495	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 ≤ ((𝐹‘𝑗)‘𝑥))
259	242, 243, 245, 257, 258	letrd 11419	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
260	259	ralrimiva 3145	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
261		r19.2z 4494	. . . . . . . . . . 11 ⊢ ((ℕ ≠ ∅ ∧ ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
262	240, 260, 261	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
263	262	anassrs 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐻‘𝑥) ≤ 0) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
264		0red 11265	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
265	239, 263, 264, 49	ltlecasei 11370	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
266	265	ralrimiva 3145	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
267		rabid2 3469	. . . . . . 7 ⊢ (ℝ = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))
268	266, 267	sylibr 234	. . . . . 6 ⊢ (𝜑 → ℝ = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
269		iunrab 5051	. . . . . 6 ⊢ ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}
270	268, 269	eqtr4di 2794	. . . . 5 ⊢ (𝜑 → ℝ = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
271	136	iuneq2dv 5015	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)})
272	90	ffnd 6736	. . . . . 6 ⊢ (𝜑 → 𝐴 Fn ℕ)
273		fniunfv 7268	. . . . . 6 ⊢ (𝐴 Fn ℕ → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴)
274	272, 273	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴)
275	270, 271, 274	3eqtr2rd 2783	. . . 4 ⊢ (𝜑 → ∪ ran 𝐴 = ℝ)
276		eqid 2736	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))
277	90, 144, 275, 10, 276	itg1climres 25750	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ⇝ (∫1‘𝐻))
278		nnex 12273	. . . . 5 ⊢ ℕ ∈ V
279	278	mptex 7244	. . . 4 ⊢ (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V
280	279	a1i 11	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V)
281		fveq2 6905	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘))
282	281	eleq2d 2826	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ (𝐴‘𝑗) ↔ 𝑥 ∈ (𝐴‘𝑘)))
283	282	ifbid 4548	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0) = if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))
284	283	mpteq2dv 5243	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))
285	284	fveq2d 6909	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
286		eqid 2736	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))
287		fvex 6918	. . . . . . 7 ⊢ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ V
288	285, 286, 287	fvmpt 7015	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
289	288	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
290	90	ffvelcdmda 7103	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ dom vol)
291		eqid 2736	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))
292	291	i1fres 25741	. . . . . . 7 ⊢ ((𝐻 ∈ dom ∫1 ∧ (𝐴‘𝑘) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1)
293	10, 290, 292	syl2an2r 685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1)
294		itg1cl 25721	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ)
295	293, 294	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ)
296	289, 295	eqeltrd 2840	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℝ)
297	296	recnd 11290	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℂ)
298	285	oveq2d 7448	. . . . . 6 ⊢ (𝑗 = 𝑘 → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
299		eqid 2736	. . . . . 6 ⊢ (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) = (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))
300		ovex 7465	. . . . . 6 ⊢ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) ∈ V
301	298, 299, 300	fvmpt 7015	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
302	288	oveq2d 7448	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝑇 · ((𝑗 ∈ ℕ ↦ (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘)) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
303	301, 302	eqtr4d 2779	. . . 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 15674	. 2 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ⇝ (𝑇 · (∫1‘𝐻)))
306		icossicc 13477	. . . . . . 7 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
307		fss 6751	. . . . . . 7 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑛):ℝ⟶(0[,]+∞))
308	6, 306, 307	sylancl 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,]+∞))
309		itg2mono.10	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ)
310	309	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ∈ ℝ)
311		itg2cl 25768	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛):ℝ⟶(0[,]+∞) → (∫2‘(𝐹‘𝑛)) ∈ ℝ*)
312	308, 311	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ℝ*)
313	312	fmpttd 7134	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))):ℕ⟶ℝ*)
314	313	frnd 6743	. . . . . . . 8 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ*)
315		fvex 6918	. . . . . . . . . . 11 ⊢ (∫2‘(𝐹‘𝑛)) ∈ V
316	315	elabrex 7263	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))})
317	316	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))})
318		eqid 2736	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))
319	318	rnmpt 5967	. . . . . . . . 9 ⊢ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))}
320	317, 319	eleqtrrdi 2851	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))))
321		supxrub 13367	. . . . . . . 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 5184	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ 𝑆)
325		itg2lecl 25774	. . . . . 6 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ 𝑆 ∈ ℝ ∧ (∫2‘(𝐹‘𝑛)) ≤ 𝑆) → (∫2‘(𝐹‘𝑛)) ∈ ℝ)
326	308, 310, 324, 325	syl3anc 1372	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ∈ ℝ)
327	326	fmpttd 7134	. . . 4 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))):ℕ⟶ℝ)
328	308	ralrimiva 3145	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞))
329		fveq2 6905	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
330	329	feq1d 6719	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,]+∞)))
331	330	cbvralvw 3236	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞))
332	328, 331	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞))
333		peano2nn 12279	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
334		fveq2 6905	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1)))
335	334	feq1d 6719	. . . . . . . . . 10 ⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘):ℝ⟶(0[,]+∞) ↔ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞)))
336	335	rspccva 3620	. . . . . . . . 9 ⊢ ((∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞) ∧ (𝑛 + 1) ∈ ℕ) → (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞))
337	332, 333, 336	syl2an 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞))
338		itg2le 25775	. . . . . . . 8 ⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞) ∧ (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1))) → (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
339	308, 337, 91, 338	syl3anc 1372	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
340	339	ralrimiva 3145	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))))
341		2fveq3 6910	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘𝑘)))
342		fvex 6918	. . . . . . . . . 10 ⊢ (∫2‘(𝐹‘𝑘)) ∈ V
343	341, 318, 342	fvmpt 7015	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘)))
344		peano2nn 12279	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
345		2fveq3 6910	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑘 + 1) → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘(𝑘 + 1))))
346		fvex 6918	. . . . . . . . . . 11 ⊢ (∫2‘(𝐹‘(𝑘 + 1))) ∈ V
347	345, 318, 346	fvmpt 7015	. . . . . . . . . 10 ⊢ ((𝑘 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1))))
348	344, 347	syl 17	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1))))
349	343, 348	breq12d 5155	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))))
350	349	ralbiia 3090	. . . . . . 7 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1))))
351		fvoveq1 7455	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1)))
352	351	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘(𝑛 + 1))) = (∫2‘(𝐹‘(𝑘 + 1))))
353	341, 352	breq12d 5155	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))))
354	353	cbvralvw 3236	. . . . . . 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 3250	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)))
358	324	ralrimiva 3145	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆)
359	343	breq1d 5152	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥))
360	359	ralbiia 3090	. . . . . . . 8 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)
361	341	breq1d 5152	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥))
362	361	cbvralvw 3236	. . . . . . . 8 ⊢ (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)
363	360, 362	bitr4i 278	. . . . . . 7 ⊢ (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥)
364		breq2 5146	. . . . . . . 8 ⊢ (𝑥 = 𝑆 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
365	364	ralbidv 3177	. . . . . . 7 ⊢ (𝑥 = 𝑆 → (∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
366	363, 365	bitrid 283	. . . . . 6 ⊢ (𝑥 = 𝑆 → (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆))
367	366	rspcev 3621	. . . . 5 ⊢ ((𝑆 ∈ ℝ ∧ ∀𝑛 ∈ ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑆) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)
368	309, 358, 367	syl2anc 584	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)
369	1, 2, 327, 357, 368	climsup 15707	. . 3 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
370	327	frnd 6743	. . . . 5 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ)
371	318, 312	dmmptd 6712	. . . . . . 7 ⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ℕ)
372	240	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℕ ≠ ∅)
373	371, 372	eqnetrd 3007	. . . . . 6 ⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
374		dm0rn0 5934	. . . . . . 7 ⊢ (dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) = ∅)
375	374	necon3bii 2992	. . . . . 6 ⊢ (dom (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
376	373, 375	sylib 218	. . . . 5 ⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅)
377	315, 318	fnmpti 6710	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) Fn ℕ
378		breq1 5145	. . . . . . . . 9 ⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) → (𝑧 ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
379	378	ralrn 7107	. . . . . . . 8 ⊢ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
380	377, 379	mp1i 13	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
381	380	rexbidv 3178	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥))
382	368, 381	mpbird 257	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥)
383		supxrre 13370	. . . . 5 ⊢ ((ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥) → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
384	370, 376, 382, 383	syl3anc 1372	. . . 4 ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ))
385	323, 384	eqtr2id 2789	. . 3 ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ, < ) = 𝑆)
386	369, 385	breqtrd 5168	. 2 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))) ⇝ 𝑆)
387	17	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℝ)
388	90	ffvelcdmda 7103	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ∈ dom vol)
389	276	i1fres 25741	. . . . . . 7 ⊢ ((𝐻 ∈ dom ∫1 ∧ (𝐴‘𝑗) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1)
390	10, 388, 389	syl2an2r 685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1)
391		itg1cl 25721	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ)
392	390, 391	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ)
393	387, 392	remulcld 11292	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ∈ ℝ)
394	393	fmpttd 7134	. . 3 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))):ℕ⟶ℝ)
395	394	ffvelcdmda 7103	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ∈ ℝ)
396	327	ffvelcdmda 7103	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ∈ ℝ)
397	329	feq1d 6719	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,)+∞)))
398	397	cbvralvw 3236	. . . . . . 7 ⊢ (∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞))
399	99, 398	sylib 218	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞))
400	399	r19.21bi 3250	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):ℝ⟶(0[,)+∞))
401		fss 6751	. . . . 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 6918	. . . . . . . . 9 ⊢ (𝐻‘𝑥) ∈ V
407		c0ex 11256	. . . . . . . . 9 ⊢ 0 ∈ V
408	406, 407	ifex 4575	. . . . . . . 8 ⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V
409	408	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V)
410		fconstmpt 5746	. . . . . . . 8 ⊢ (ℝ × {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇)
411	410	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℝ × {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇))
412		eqidd 2737	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))
413	403, 405, 409, 411, 412	offval2 7718	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))
414		ovif2 7533	. . . . . . . 8 ⊢ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0))
415	47	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 ∈ ℂ)
416	415	mul01d 11461	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · 0) = 0)
417	416	ifeq2d 4545	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))
418	414, 417	eqtrid 2788	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))
419	418	mpteq2dv 5243	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
420	413, 419	eqtrd 2776	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
421	293, 404	i1fmulc 25739	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ dom ∫1)
422	420, 421	eqeltrrd 2841	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom ∫1)
423		iftrue 4530	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥)))
424	423	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥)))
425	329	fveq1d 6907	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑘)‘𝑥))
426	425	breq2d 5154	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)))
427	426	rabbidv 3443	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
428	23	rabex 5338	. . . . . . . . . . . . 13 ⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ∈ V
429	427, 89, 428	fvmpt 7015	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
430	429	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
431	430	eleq2d 2826	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)}))
432	431	biimpa 476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})
433		rabid 3457	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ↔ (𝑥 ∈ ℝ ∧ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)))
434	433	simprbi 496	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))
435	432, 434	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))
436	424, 435	eqbrtrd 5164	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
437		iffalse 4533	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0)
438	437	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0)
439	400	ffvelcdmda 7103	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞))
440		elrege0 13495	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞) ↔ (((𝐹‘𝑘)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑘)‘𝑥)))
441	440	simprbi 496	. . . . . . . . . 10 ⊢ (((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞) → 0 ≤ ((𝐹‘𝑘)‘𝑥))
442	439, 441	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘𝑘)‘𝑥))
443	442	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → 0 ≤ ((𝐹‘𝑘)‘𝑥))
444	438, 443	eqbrtrd 5164	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
445	436, 444	pm2.61dan 812	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
446	445	ralrimiva 3145	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))
447		ovex 7465	. . . . . . . 8 ⊢ (𝑇 · (𝐻‘𝑥)) ∈ V
448	447, 407	ifex 4575	. . . . . . 7 ⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V
449	448	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V)
450		fvexd 6920	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ V)
451		eqidd 2737	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))
452	400	feqmptd 6976	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑘)‘𝑥)))
453	403, 449, 450, 451, 452	ofrfval2 7719	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥)))
454	446, 453	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘))
455		itg2ub 25769	. . . 4 ⊢ (((𝐹‘𝑘):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘r ≤ (𝐹‘𝑘)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) ≤ (∫2‘(𝐹‘𝑘)))
456	402, 422, 454, 455	syl3anc 1372	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) ≤ (∫2‘(𝐹‘𝑘)))
457	301	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
458	293, 404	itg1mulc 25740	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))))
459	420	fveq2d 6909	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘((ℝ × {𝑇}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))))
460	457, 458, 459	3eqtr2d 2782	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))))
461	343	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘)))
462	456, 460, 461	3brtr4d 5174	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛)))‘𝑘))
463	1, 2, 305, 386, 395, 396, 462	climle 15677	1 ⊢ (𝜑 → (𝑇 · (∫1‘𝐻)) ≤ 𝑆)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  {cab 2713   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  {crab 3435  Vcvv 3479   ∖ cdif 3947   ∩ cin 3949   ⊆ wss 3950  ∅c0 4332  ifcif 4524  {csn 4625  ∪ cuni 4906  ∪ ciun 4990   class class class wbr 5142   ↦ cmpt 5224   × cxp 5682  ^◡ccnv 5683  dom cdm 5684  ran crn 5685   “ cima 5687   Fn wfn 6555  ⟶wf 6556  ‘cfv 6560  (class class class)co 7432   ∘_f cof 7696   ∘_r cofr 7697  supcsup 9481  ℂcc 11154  ℝcr 11155  0cc0 11156  1c1 11157   + caddc 11159   · cmul 11161  +∞cpnf 11293  -∞cmnf 11294  ℝ^*cxr 11295   < clt 11296   ≤ cle 11297   − cmin 11493  -cneg 11494  ℕcn 12267  (,)cioo 13388  [,)cico 13390  [,]cicc 13391   ⇝ cli 15521  volcvol 25499  MblFncmbf 25650  ∫₁citg1 25651  ∫₂citg2 25652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-inf2 9682  ax-cc 10476  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-disj 5110  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-of 7698  df-ofr 7699  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-oadd 8511  df-omul 8512  df-er 8746  df-map 8869  df-pm 8870  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-fi 9452  df-sup 9483  df-inf 9484  df-oi 9551  df-dju 9942  df-card 9980  df-acn 9983  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-n0 12529  df-z 12616  df-uz 12880  df-q 12992  df-rp 13036  df-xneg 13155  df-xadd 13156  df-xmul 13157  df-ioo 13392  df-ioc 13393  df-ico 13394  df-icc 13395  df-fz 13549  df-fzo 13696  df-fl 13833  df-seq 14044  df-exp 14104  df-hash 14371  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-clim 15525  df-rlim 15526  df-sum 15724  df-rest 17468  df-topgen 17489  df-psmet 21357  df-xmet 21358  df-met 21359  df-bl 21360  df-mopn 21361  df-top 22901  df-topon 22918  df-bases 22954  df-cmp 23396  df-ovol 25500  df-vol 25501  df-mbf 25655  df-itg1 25656  df-itg2 25657

This theorem is referenced by:  itg2monolem3  25788