ovoliunlem1

	Ref	Expression
Hypotheses	ovoliun.t	⊢ 𝑇 = seq 1 ( + , 𝐺 )
	ovoliun.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) )
	ovoliun.a	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
	ovoliun.v	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
	ovoliun.r	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ^* , < ) ∈ ℝ )
	ovoliun.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ⁺ )
	ovoliun.s	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) )
	ovoliun.u	⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
	ovoliun.h	⊢ 𝐻 = ( 𝑘 ∈ ℕ ↦ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ) )
	ovoliun.j	⊢ ( 𝜑 → 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
	ovoliun.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
	ovoliun.x1	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝐹 ‘ 𝑛 ) ) )
	ovoliun.x2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
	ovoliun.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
	ovoliun.l1	⊢ ( 𝜑 → 𝐿 ∈ ℤ )
	ovoliun.l2	⊢ ( 𝜑 → ∀ 𝑤 ∈ ( 1 ... 𝐾 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝐿 )
Assertion	ovoliunlem1	⊢ ( 𝜑 → ( 𝑈 ‘ 𝐾 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ovoliun.t	⊢ 𝑇 = seq 1 ( + , 𝐺 )
2		ovoliun.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) )
3		ovoliun.a	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
4		ovoliun.v	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
5		ovoliun.r	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ^* , < ) ∈ ℝ )
6		ovoliun.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ⁺ )
7		ovoliun.s	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) )
8		ovoliun.u	⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
9		ovoliun.h	⊢ 𝐻 = ( 𝑘 ∈ ℕ ↦ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ) )
10		ovoliun.j	⊢ ( 𝜑 → 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
11		ovoliun.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
12		ovoliun.x1	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝐹 ‘ 𝑛 ) ) )
13		ovoliun.x2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
14		ovoliun.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
15		ovoliun.l1	⊢ ( 𝜑 → 𝐿 ∈ ℤ )
16		ovoliun.l2	⊢ ( 𝜑 → ∀ 𝑤 ∈ ( 1 ... 𝐾 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝐿 )
17		2fveq3	⊢ ( 𝑗 = ( 𝐽 ‘ 𝑚 ) → ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) = ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) )
18		fveq2	⊢ ( 𝑗 = ( 𝐽 ‘ 𝑚 ) → ( 2^nd ‘ 𝑗 ) = ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) )
19	17 18	fveq12d	⊢ ( 𝑗 = ( 𝐽 ‘ 𝑚 ) → ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) = ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) )
20	19	fveq2d	⊢ ( 𝑗 = ( 𝐽 ‘ 𝑚 ) → ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) = ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) )
21	19	fveq2d	⊢ ( 𝑗 = ( 𝐽 ‘ 𝑚 ) → ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) = ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) )
22	20 21	oveq12d	⊢ ( 𝑗 = ( 𝐽 ‘ 𝑚 ) → ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) = ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) ) )
23		fzfid	⊢ ( 𝜑 → ( 1 ... 𝐾 ) ∈ Fin )
24		f1of1	⊢ ( 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) → 𝐽 : ℕ –1-1→ ( ℕ × ℕ ) )
25	10 24	syl	⊢ ( 𝜑 → 𝐽 : ℕ –1-1→ ( ℕ × ℕ ) )
26		fz1ssnn	⊢ ( 1 ... 𝐾 ) ⊆ ℕ
27		f1ores	⊢ ( ( 𝐽 : ℕ –1-1→ ( ℕ × ℕ ) ∧ ( 1 ... 𝐾 ) ⊆ ℕ ) → ( 𝐽 ↾ ( 1 ... 𝐾 ) ) : ( 1 ... 𝐾 ) –1-1-onto→ ( 𝐽 “ ( 1 ... 𝐾 ) ) )
28	25 26 27	sylancl	⊢ ( 𝜑 → ( 𝐽 ↾ ( 1 ... 𝐾 ) ) : ( 1 ... 𝐾 ) –1-1-onto→ ( 𝐽 “ ( 1 ... 𝐾 ) ) )
29		fvres	⊢ ( 𝑚 ∈ ( 1 ... 𝐾 ) → ( ( 𝐽 ↾ ( 1 ... 𝐾 ) ) ‘ 𝑚 ) = ( 𝐽 ‘ 𝑚 ) )
30	29	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝐽 ↾ ( 1 ... 𝐾 ) ) ‘ 𝑚 ) = ( 𝐽 ‘ 𝑚 ) )
31	11	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → 𝐹 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
32		imassrn	⊢ ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ran 𝐽
33		f1of	⊢ ( 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) → 𝐽 : ℕ ⟶ ( ℕ × ℕ ) )
34	10 33	syl	⊢ ( 𝜑 → 𝐽 : ℕ ⟶ ( ℕ × ℕ ) )
35	34	frnd	⊢ ( 𝜑 → ran 𝐽 ⊆ ( ℕ × ℕ ) )
36	32 35	sstrid	⊢ ( 𝜑 → ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ( ℕ × ℕ ) )
37	36	sselda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → 𝑗 ∈ ( ℕ × ℕ ) )
38		xp1st	⊢ ( 𝑗 ∈ ( ℕ × ℕ ) → ( 1^st ‘ 𝑗 ) ∈ ℕ )
39	37 38	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( 1^st ‘ 𝑗 ) ∈ ℕ )
40	31 39	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
41		elovolmlem	⊢ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ↔ ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
42	40 41	sylib	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
43		xp2nd	⊢ ( 𝑗 ∈ ( ℕ × ℕ ) → ( 2^nd ‘ 𝑗 ) ∈ ℕ )
44	37 43	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( 2^nd ‘ 𝑗 ) ∈ ℕ )
45	42 44	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
46	45	elin2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ∈ ( ℝ × ℝ ) )
47		xp2nd	⊢ ( ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ∈ ℝ )
48	46 47	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ∈ ℝ )
49		xp1st	⊢ ( ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ∈ ℝ )
50	46 49	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ∈ ℝ )
51	48 50	resubcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) ∈ ℝ )
52	51	recnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) ∈ ℂ )
53	22 23 28 30 52	fsumf1o	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) = Σ 𝑚 ∈ ( 1 ... 𝐾 ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) ) )
54	11	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
55	34	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐽 ‘ 𝑘 ) ∈ ( ℕ × ℕ ) )
56		xp1st	⊢ ( ( 𝐽 ‘ 𝑘 ) ∈ ( ℕ × ℕ ) → ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ∈ ℕ )
57	55 56	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ∈ ℕ )
58	54 57	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
59		elovolmlem	⊢ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ↔ ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
60	58 59	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
61		xp2nd	⊢ ( ( 𝐽 ‘ 𝑘 ) ∈ ( ℕ × ℕ ) → ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ∈ ℕ )
62	55 61	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ∈ ℕ )
63	60 62	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
64	63 9	fmptd	⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
65		elfznn	⊢ ( 𝑚 ∈ ( 1 ... 𝐾 ) → 𝑚 ∈ ℕ )
66		eqid	⊢ ( ( abs ∘ − ) ∘ 𝐻 ) = ( ( abs ∘ − ) ∘ 𝐻 )
67	66	ovolfsval	⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑚 ) = ( ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) ) )
68	64 65 67	syl2an	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑚 ) = ( ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) ) )
69	65	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → 𝑚 ∈ ℕ )
70		2fveq3	⊢ ( 𝑘 = 𝑚 → ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) )
71	70	fveq2d	⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) )
72		2fveq3	⊢ ( 𝑘 = 𝑚 → ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) )
73	71 72	fveq12d	⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ) = ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) )
74		fvex	⊢ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ∈ V
75	73 9 74	fvmpt	⊢ ( 𝑚 ∈ ℕ → ( 𝐻 ‘ 𝑚 ) = ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) )
76	69 75	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( 𝐻 ‘ 𝑚 ) = ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) )
77	76	fveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) = ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) )
78	76	fveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) = ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) )
79	77 78	oveq12d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) ) = ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) ) )
80	68 79	eqtrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑚 ) = ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) ) )
81		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
82	14 81	eleqtrdi	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ_≥ ‘ 1 ) )
83		ffvelrn	⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
84	64 65 83	syl2an	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( 𝐻 ‘ 𝑚 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
85	84	elin2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( 𝐻 ‘ 𝑚 ) ∈ ( ℝ × ℝ ) )
86		xp2nd	⊢ ( ( 𝐻 ‘ 𝑚 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ∈ ℝ )
87	85 86	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ∈ ℝ )
88		xp1st	⊢ ( ( 𝐻 ‘ 𝑚 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) ∈ ℝ )
89	85 88	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) ∈ ℝ )
90	87 89	resubcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) ) ∈ ℝ )
91	90	recnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) ) ∈ ℂ )
92	79 91	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝐾 ) ) → ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) ) ∈ ℂ )
93	80 82 92	fsumser	⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... 𝐾 ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑚 ) ) ) ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝐾 ) )
94	53 93	eqtrd	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝐾 ) )
95	8	fveq1i	⊢ ( 𝑈 ‘ 𝐾 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝐾 )
96	94 95	eqtr4di	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) = ( 𝑈 ‘ 𝐾 ) )
97		f1oeng	⊢ ( ( ( 1 ... 𝐾 ) ∈ Fin ∧ ( 𝐽 ↾ ( 1 ... 𝐾 ) ) : ( 1 ... 𝐾 ) –1-1-onto→ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( 1 ... 𝐾 ) ≈ ( 𝐽 “ ( 1 ... 𝐾 ) ) )
98	23 28 97	syl2anc	⊢ ( 𝜑 → ( 1 ... 𝐾 ) ≈ ( 𝐽 “ ( 1 ... 𝐾 ) ) )
99	98	ensymd	⊢ ( 𝜑 → ( 𝐽 “ ( 1 ... 𝐾 ) ) ≈ ( 1 ... 𝐾 ) )
100		enfii	⊢ ( ( ( 1 ... 𝐾 ) ∈ Fin ∧ ( 𝐽 “ ( 1 ... 𝐾 ) ) ≈ ( 1 ... 𝐾 ) ) → ( 𝐽 “ ( 1 ... 𝐾 ) ) ∈ Fin )
101	23 99 100	syl2anc	⊢ ( 𝜑 → ( 𝐽 “ ( 1 ... 𝐾 ) ) ∈ Fin )
102	101 51	fsumrecl	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) ∈ ℝ )
103		fzfid	⊢ ( 𝜑 → ( 1 ... 𝐿 ) ∈ Fin )
104		elfznn	⊢ ( 𝑛 ∈ ( 1 ... 𝐿 ) → 𝑛 ∈ ℕ )
105	104 4	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
106	103 105	fsumrecl	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( vol* ‘ 𝐴 ) ∈ ℝ )
107	6	rpred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
108		2nn	⊢ 2 ∈ ℕ
109		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀ )
110		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ₀ ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
111	108 109 110	sylancr	⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℕ )
112	104 111	syl	⊢ ( 𝑛 ∈ ( 1 ... 𝐿 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
113		nndivre	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 2 ↑ 𝑛 ) ∈ ℕ ) → ( 𝐵 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
114	107 112 113	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( 𝐵 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
115	103 114	fsumrecl	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( 𝐵 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
116	106 115	readdcld	⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( vol* ‘ 𝐴 ) + Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
117	5 107	readdcld	⊢ ( 𝜑 → ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ∈ ℝ )
118		relxp	⊢ Rel ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) )
119		relres	⊢ Rel ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ↾ { 𝑛 } )
120		elsni	⊢ ( 𝑥 ∈ { 𝑛 } → 𝑥 = 𝑛 )
121	120	opeq1d	⊢ ( 𝑥 ∈ { 𝑛 } → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑛 , 𝑦 ⟩ )
122	121	eleq1d	⊢ ( 𝑥 ∈ { 𝑛 } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ↔ ⟨ 𝑛 , 𝑦 ⟩ ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) )
123		vex	⊢ 𝑛 ∈ V
124		vex	⊢ 𝑦 ∈ V
125	123 124	elimasn	⊢ ( 𝑦 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ↔ ⟨ 𝑛 , 𝑦 ⟩ ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) )
126	122 125	bitr4di	⊢ ( 𝑥 ∈ { 𝑛 } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ↔ 𝑦 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) )
127	126	pm5.32i	⊢ ( ( 𝑥 ∈ { 𝑛 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) ↔ ( 𝑥 ∈ { 𝑛 } ∧ 𝑦 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) )
128	124	opelresi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ↾ { 𝑛 } ) ↔ ( 𝑥 ∈ { 𝑛 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) )
129		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ↔ ( 𝑥 ∈ { 𝑛 } ∧ 𝑦 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) )
130	127 128 129	3bitr4ri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ↾ { 𝑛 } ) )
131	118 119 130	eqrelriiv	⊢ ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) = ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ↾ { 𝑛 } )
132		df-res	⊢ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ↾ { 𝑛 } ) = ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ∩ ( { 𝑛 } × V ) )
133	131 132	eqtri	⊢ ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) = ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ∩ ( { 𝑛 } × V ) )
134	133	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) = ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ∩ ( { 𝑛 } × V ) ) )
135	134	iuneq2dv	⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) = ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ∩ ( { 𝑛 } × V ) ) )
136		iunin2	⊢ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ∩ ( { 𝑛 } × V ) ) = ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ∩ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × V ) )
137	135 136	eqtrdi	⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) = ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ∩ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × V ) ) )
138		relxp	⊢ Rel ( ℕ × ℕ )
139		relss	⊢ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ( ℕ × ℕ ) → ( Rel ( ℕ × ℕ ) → Rel ( 𝐽 “ ( 1 ... 𝐾 ) ) ) )
140	36 138 139	mpisyl	⊢ ( 𝜑 → Rel ( 𝐽 “ ( 1 ... 𝐾 ) ) )
141	34	ffnd	⊢ ( 𝜑 → 𝐽 Fn ℕ )
142		fveq2	⊢ ( 𝑗 = ( 𝐽 ‘ 𝑤 ) → ( 1^st ‘ 𝑗 ) = ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) )
143	142	breq1d	⊢ ( 𝑗 = ( 𝐽 ‘ 𝑤 ) → ( ( 1^st ‘ 𝑗 ) ≤ 𝐿 ↔ ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝐿 ) )
144	143	ralima	⊢ ( ( 𝐽 Fn ℕ ∧ ( 1 ... 𝐾 ) ⊆ ℕ ) → ( ∀ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( 1^st ‘ 𝑗 ) ≤ 𝐿 ↔ ∀ 𝑤 ∈ ( 1 ... 𝐾 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝐿 ) )
145	141 26 144	sylancl	⊢ ( 𝜑 → ( ∀ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( 1^st ‘ 𝑗 ) ≤ 𝐿 ↔ ∀ 𝑤 ∈ ( 1 ... 𝐾 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝐿 ) )
146	16 145	mpbird	⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( 1^st ‘ 𝑗 ) ≤ 𝐿 )
147	146	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( 1^st ‘ 𝑗 ) ≤ 𝐿 )
148	39 81	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( 1^st ‘ 𝑗 ) ∈ ( ℤ_≥ ‘ 1 ) )
149	15	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → 𝐿 ∈ ℤ )
150		elfz5	⊢ ( ( ( 1^st ‘ 𝑗 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝐿 ∈ ℤ ) → ( ( 1^st ‘ 𝑗 ) ∈ ( 1 ... 𝐿 ) ↔ ( 1^st ‘ 𝑗 ) ≤ 𝐿 ) )
151	148 149 150	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( ( 1^st ‘ 𝑗 ) ∈ ( 1 ... 𝐿 ) ↔ ( 1^st ‘ 𝑗 ) ≤ 𝐿 ) )
152	147 151	mpbird	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ) → ( 1^st ‘ 𝑗 ) ∈ ( 1 ... 𝐿 ) )
153	152	ralrimiva	⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( 1^st ‘ 𝑗 ) ∈ ( 1 ... 𝐿 ) )
154		vex	⊢ 𝑥 ∈ V
155	154 124	op1std	⊢ ( 𝑗 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑗 ) = 𝑥 )
156	155	eleq1d	⊢ ( 𝑗 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑗 ) ∈ ( 1 ... 𝐿 ) ↔ 𝑥 ∈ ( 1 ... 𝐿 ) ) )
157	156	rspccv	⊢ ( ∀ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( 1^st ‘ 𝑗 ) ∈ ( 1 ... 𝐿 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) → 𝑥 ∈ ( 1 ... 𝐿 ) ) )
158	153 157	syl	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) → 𝑥 ∈ ( 1 ... 𝐿 ) ) )
159		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ∪ 𝑛 ∈ ( 1 ... 𝐿 ) { 𝑛 } × V ) ↔ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) { 𝑛 } ∧ 𝑦 ∈ V ) )
160	124	biantru	⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) { 𝑛 } ↔ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) { 𝑛 } ∧ 𝑦 ∈ V ) )
161		iunid	⊢ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) { 𝑛 } = ( 1 ... 𝐿 )
162	161	eleq2i	⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) { 𝑛 } ↔ 𝑥 ∈ ( 1 ... 𝐿 ) )
163	159 160 162	3bitr2i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ∪ 𝑛 ∈ ( 1 ... 𝐿 ) { 𝑛 } × V ) ↔ 𝑥 ∈ ( 1 ... 𝐿 ) )
164	158 163	syl6ibr	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ∪ 𝑛 ∈ ( 1 ... 𝐿 ) { 𝑛 } × V ) ) )
165	140 164	relssdv	⊢ ( 𝜑 → ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ( ∪ 𝑛 ∈ ( 1 ... 𝐿 ) { 𝑛 } × V ) )
166		xpiundir	⊢ ( ∪ 𝑛 ∈ ( 1 ... 𝐿 ) { 𝑛 } × V ) = ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × V )
167	165 166	sseqtrdi	⊢ ( 𝜑 → ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × V ) )
168		df-ss	⊢ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × V ) ↔ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ∩ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × V ) ) = ( 𝐽 “ ( 1 ... 𝐾 ) ) )
169	167 168	sylib	⊢ ( 𝜑 → ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ∩ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × V ) ) = ( 𝐽 “ ( 1 ... 𝐾 ) ) )
170	137 169	eqtrd	⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) = ( 𝐽 “ ( 1 ... 𝐾 ) ) )
171	170 101	eqeltrd	⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ∈ Fin )
172		ssiun2	⊢ ( 𝑛 ∈ ( 1 ... 𝐿 ) → ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ⊆ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) )
173		ssfi	⊢ ( ( ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ∈ Fin ∧ ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ⊆ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) → ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ∈ Fin )
174	171 172 173	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ∈ Fin )
175		2ndconst	⊢ ( 𝑛 ∈ V → ( 2^nd ↾ ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) : ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) –1-1-onto→ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) )
176	175	elv	⊢ ( 2^nd ↾ ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) : ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) –1-1-onto→ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } )
177		f1oeng	⊢ ( ( ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ∈ Fin ∧ ( 2^nd ↾ ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) : ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) –1-1-onto→ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) → ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ≈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) )
178	174 176 177	sylancl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ≈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) )
179	178	ensymd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ≈ ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) )
180		enfii	⊢ ( ( ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ∈ Fin ∧ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ≈ ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) → ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ∈ Fin )
181	174 179 180	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ∈ Fin )
182		ffvelrn	⊢ ( ( 𝐹 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
183	11 104 182	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
184		elovolmlem	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ↔ ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
185	183 184	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
186	185	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝐿 ) ∧ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) → ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
187		imassrn	⊢ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ⊆ ran ( 𝐽 “ ( 1 ... 𝐾 ) )
188	36	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ( ℕ × ℕ ) )
189		rnss	⊢ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ( ℕ × ℕ ) → ran ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ran ( ℕ × ℕ ) )
190	188 189	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ran ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ran ( ℕ × ℕ ) )
191		rnxpid	⊢ ran ( ℕ × ℕ ) = ℕ
192	190 191	sseqtrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ran ( 𝐽 “ ( 1 ... 𝐾 ) ) ⊆ ℕ )
193	187 192	sstrid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ⊆ ℕ )
194	193	sseld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) → 𝑖 ∈ ℕ ) )
195	194	impr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝐿 ) ∧ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) → 𝑖 ∈ ℕ )
196	186 195	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝐿 ) ∧ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
197	196	elin2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝐿 ) ∧ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ∈ ( ℝ × ℝ ) )
198		xp2nd	⊢ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ∈ ℝ )
199	197 198	syl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝐿 ) ∧ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) → ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ∈ ℝ )
200		xp1st	⊢ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ∈ ℝ )
201	197 200	syl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝐿 ) ∧ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) → ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ∈ ℝ )
202	199 201	resubcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝐿 ) ∧ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) → ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ∈ ℝ )
203	202	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) ∧ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) → ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ∈ ℝ )
204	181 203	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → Σ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ∈ ℝ )
205	107 111 113	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
206	4 205	readdcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
207	104 206	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
208		eqid	⊢ ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) = ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) )
209	208 7	ovolsf	⊢ ( ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
210	185 209	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
211	210	frnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
212		icossxr	⊢ ( 0 [,) +∞ ) ⊆ ℝ^*
213	211 212	sstrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ran 𝑆 ⊆ ℝ^* )
214		supxrcl	⊢ ( ran 𝑆 ⊆ ℝ^* → sup ( ran 𝑆 , ℝ^* , < ) ∈ ℝ^* )
215	213 214	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → sup ( ran 𝑆 , ℝ^* , < ) ∈ ℝ^* )
216		mnfxr	⊢ -∞ ∈ ℝ^*
217	216	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → -∞ ∈ ℝ^* )
218	105	rexrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ^* )
219	105	mnfltd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → -∞ < ( vol* ‘ 𝐴 ) )
220	104 12	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝐹 ‘ 𝑛 ) ) )
221	7	ovollb	⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝐹 ‘ 𝑛 ) ) ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
222	185 220 221	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
223	217 218 215 219 222	xrltletrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → -∞ < sup ( ran 𝑆 , ℝ^* , < ) )
224	104 13	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
225		xrre	⊢ ( ( ( sup ( ran 𝑆 , ℝ^* , < ) ∈ ℝ^* ∧ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ ) ∧ ( -∞ < sup ( ran 𝑆 , ℝ^* , < ) ∧ sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ) ) → sup ( ran 𝑆 , ℝ^* , < ) ∈ ℝ )
226	215 207 223 224 225	syl22anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → sup ( ran 𝑆 , ℝ^* , < ) ∈ ℝ )
227		1zzd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → 1 ∈ ℤ )
228	208	ovolfsval	⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑖 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) = ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) )
229	185 228	sylan	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) ∧ 𝑖 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) = ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) )
230	208	ovolfsf	⊢ ( ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
231	185 230	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
232	231	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) ∧ 𝑖 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑖 ) ∈ ( 0 [,) +∞ ) )
233	229 232	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) ∧ 𝑖 ∈ ℕ ) → ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ∈ ( 0 [,) +∞ ) )
234		elrege0	⊢ ( ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ∈ ℝ ∧ 0 ≤ ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ) )
235	233 234	sylib	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) ∧ 𝑖 ∈ ℕ ) → ( ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ∈ ℝ ∧ 0 ≤ ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ) )
236	235	simpld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) ∧ 𝑖 ∈ ℕ ) → ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ∈ ℝ )
237	235	simprd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) ∧ 𝑖 ∈ ℕ ) → 0 ≤ ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) )
238		supxrub	⊢ ( ( ran 𝑆 ⊆ ℝ^* ∧ 𝑧 ∈ ran 𝑆 ) → 𝑧 ≤ sup ( ran 𝑆 , ℝ^* , < ) )
239	213 238	sylan	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) ∧ 𝑧 ∈ ran 𝑆 ) → 𝑧 ≤ sup ( ran 𝑆 , ℝ^* , < ) )
240	239	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ sup ( ran 𝑆 , ℝ^* , < ) )
241		brralrspcev	⊢ ( ( sup ( ran 𝑆 , ℝ^* , < ) ∈ ℝ ∧ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ sup ( ran 𝑆 , ℝ^* , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 )
242	226 240 241	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 )
243	210	ffnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → 𝑆 Fn ℕ )
244		breq1	⊢ ( 𝑧 = ( 𝑆 ‘ 𝑘 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) )
245	244	ralrn	⊢ ( 𝑆 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) )
246	243 245	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) )
247	246	rexbidv	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) )
248	242 247	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 )
249	81 7 227 229 236 237 248	isumsup2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → 𝑆 ⇝ sup ( ran 𝑆 , ℝ , < ) )
250	7 249	eqbrtrrid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) ) ⇝ sup ( ran 𝑆 , ℝ , < ) )
251		climrel	⊢ Rel ⇝
252	251	releldmi	⊢ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) ) ⇝ sup ( ran 𝑆 , ℝ , < ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ dom ⇝ )
253	250 252	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ dom ⇝ )
254	81 227 181 193 229 236 237 253	isumless	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → Σ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ≤ Σ 𝑖 ∈ ℕ ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) )
255	81 7 227 229 236 237 248	isumsup	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → Σ 𝑖 ∈ ℕ ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) = sup ( ran 𝑆 , ℝ , < ) )
256		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
257	211 256	sstrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ran 𝑆 ⊆ ℝ )
258		1nn	⊢ 1 ∈ ℕ
259	210	fdmd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → dom 𝑆 = ℕ )
260	258 259	eleqtrrid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → 1 ∈ dom 𝑆 )
261	260	ne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → dom 𝑆 ≠ ∅ )
262		dm0rn0	⊢ ( dom 𝑆 = ∅ ↔ ran 𝑆 = ∅ )
263	262	necon3bii	⊢ ( dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅ )
264	261 263	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ran 𝑆 ≠ ∅ )
265		supxrre	⊢ ( ( ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ) → sup ( ran 𝑆 , ℝ^* , < ) = sup ( ran 𝑆 , ℝ , < ) )
266	257 264 242 265	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → sup ( ran 𝑆 , ℝ^* , < ) = sup ( ran 𝑆 , ℝ , < ) )
267	255 266	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → Σ 𝑖 ∈ ℕ ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) = sup ( ran 𝑆 , ℝ^* , < ) )
268	254 267	breqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → Σ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
269	204 226 207 268 224	letrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → Σ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
270	103 204 207 269	fsumle	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) Σ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
271		vex	⊢ 𝑖 ∈ V
272	123 271	op1std	⊢ ( 𝑗 = ⟨ 𝑛 , 𝑖 ⟩ → ( 1^st ‘ 𝑗 ) = 𝑛 )
273	272	fveq2d	⊢ ( 𝑗 = ⟨ 𝑛 , 𝑖 ⟩ → ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) = ( 𝐹 ‘ 𝑛 ) )
274	123 271	op2ndd	⊢ ( 𝑗 = ⟨ 𝑛 , 𝑖 ⟩ → ( 2^nd ‘ 𝑗 ) = 𝑖 )
275	273 274	fveq12d	⊢ ( 𝑗 = ⟨ 𝑛 , 𝑖 ⟩ → ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) )
276	275	fveq2d	⊢ ( 𝑗 = ⟨ 𝑛 , 𝑖 ⟩ → ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) = ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) )
277	275	fveq2d	⊢ ( 𝑗 = ⟨ 𝑛 , 𝑖 ⟩ → ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) = ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) )
278	276 277	oveq12d	⊢ ( 𝑗 = ⟨ 𝑛 , 𝑖 ⟩ → ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) = ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) )
279	202	recnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝐿 ) ∧ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ) → ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) ∈ ℂ )
280	278 103 181 279	fsum2d	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) Σ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) = Σ 𝑗 ∈ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) )
281	170	sumeq1d	⊢ ( 𝜑 → Σ 𝑗 ∈ ∪ 𝑛 ∈ ( 1 ... 𝐿 ) ( { 𝑛 } × ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) = Σ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) )
282	280 281	eqtrd	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) Σ 𝑖 ∈ ( ( 𝐽 “ ( 1 ... 𝐾 ) ) “ { 𝑛 } ) ( ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) − ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑖 ) ) ) = Σ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) )
283	105	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( vol* ‘ 𝐴 ) ∈ ℂ )
284	114	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( 𝐵 / ( 2 ↑ 𝑛 ) ) ∈ ℂ )
285	103 283 284	fsumadd	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( vol* ‘ 𝐴 ) + Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
286	270 282 285	3brtr3d	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( vol* ‘ 𝐴 ) + Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
287		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
288		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
289	2	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) → ( 𝐺 ‘ 𝑛 ) = ( vol* ‘ 𝐴 ) )
290	288 4 289	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ( vol* ‘ 𝐴 ) )
291	290 4	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
292	81 287 291	serfre	⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
293	1	feq1i	⊢ ( 𝑇 : ℕ ⟶ ℝ ↔ seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
294	292 293	sylibr	⊢ ( 𝜑 → 𝑇 : ℕ ⟶ ℝ )
295	294	frnd	⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ )
296		ressxr	⊢ ℝ ⊆ ℝ^*
297	295 296	sstrdi	⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ^* )
298	104 290	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝐿 ) ) → ( 𝐺 ‘ 𝑛 ) = ( vol* ‘ 𝐴 ) )
299		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
300		ffvelrn	⊢ ( ( 𝐽 : ℕ ⟶ ( ℕ × ℕ ) ∧ 1 ∈ ℕ ) → ( 𝐽 ‘ 1 ) ∈ ( ℕ × ℕ ) )
301	34 258 300	sylancl	⊢ ( 𝜑 → ( 𝐽 ‘ 1 ) ∈ ( ℕ × ℕ ) )
302		xp1st	⊢ ( ( 𝐽 ‘ 1 ) ∈ ( ℕ × ℕ ) → ( 1^st ‘ ( 𝐽 ‘ 1 ) ) ∈ ℕ )
303	301 302	syl	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐽 ‘ 1 ) ) ∈ ℕ )
304	303	nnred	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐽 ‘ 1 ) ) ∈ ℝ )
305	15	zred	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
306	303	nnge1d	⊢ ( 𝜑 → 1 ≤ ( 1^st ‘ ( 𝐽 ‘ 1 ) ) )
307		2fveq3	⊢ ( 𝑤 = 1 → ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) = ( 1^st ‘ ( 𝐽 ‘ 1 ) ) )
308	307	breq1d	⊢ ( 𝑤 = 1 → ( ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝐿 ↔ ( 1^st ‘ ( 𝐽 ‘ 1 ) ) ≤ 𝐿 ) )
309		eluzfz1	⊢ ( 𝐾 ∈ ( ℤ_≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝐾 ) )
310	82 309	syl	⊢ ( 𝜑 → 1 ∈ ( 1 ... 𝐾 ) )
311	308 16 310	rspcdva	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐽 ‘ 1 ) ) ≤ 𝐿 )
312	299 304 305 306 311	letrd	⊢ ( 𝜑 → 1 ≤ 𝐿 )
313		elnnz1	⊢ ( 𝐿 ∈ ℕ ↔ ( 𝐿 ∈ ℤ ∧ 1 ≤ 𝐿 ) )
314	15 312 313	sylanbrc	⊢ ( 𝜑 → 𝐿 ∈ ℕ )
315	314 81	eleqtrdi	⊢ ( 𝜑 → 𝐿 ∈ ( ℤ_≥ ‘ 1 ) )
316	298 315 283	fsumser	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( vol* ‘ 𝐴 ) = ( seq 1 ( + , 𝐺 ) ‘ 𝐿 ) )
317		seqfn	⊢ ( 1 ∈ ℤ → seq 1 ( + , 𝐺 ) Fn ( ℤ_≥ ‘ 1 ) )
318	287 317	syl	⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) Fn ( ℤ_≥ ‘ 1 ) )
319		fnfvelrn	⊢ ( ( seq 1 ( + , 𝐺 ) Fn ( ℤ_≥ ‘ 1 ) ∧ 𝐿 ∈ ( ℤ_≥ ‘ 1 ) ) → ( seq 1 ( + , 𝐺 ) ‘ 𝐿 ) ∈ ran seq 1 ( + , 𝐺 ) )
320	318 315 319	syl2anc	⊢ ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝐿 ) ∈ ran seq 1 ( + , 𝐺 ) )
321	1	rneqi	⊢ ran 𝑇 = ran seq 1 ( + , 𝐺 )
322	320 321	eleqtrrdi	⊢ ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝐿 ) ∈ ran 𝑇 )
323	316 322	eqeltrd	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( vol* ‘ 𝐴 ) ∈ ran 𝑇 )
324		supxrub	⊢ ( ( ran 𝑇 ⊆ ℝ^* ∧ Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( vol* ‘ 𝐴 ) ∈ ran 𝑇 ) → Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ^* , < ) )
325	297 323 324	syl2anc	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ^* , < ) )
326	107	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
327		geo2sum	⊢ ( ( 𝐿 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( 𝐵 / ( 2 ↑ 𝑛 ) ) = ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝐿 ) ) ) )
328	314 326 327	syl2anc	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( 𝐵 / ( 2 ↑ 𝑛 ) ) = ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝐿 ) ) ) )
329	314	nnnn0d	⊢ ( 𝜑 → 𝐿 ∈ ℕ₀ )
330		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝐿 ∈ ℕ₀ ) → ( 2 ↑ 𝐿 ) ∈ ℕ )
331	108 329 330	sylancr	⊢ ( 𝜑 → ( 2 ↑ 𝐿 ) ∈ ℕ )
332	331	nnrpd	⊢ ( 𝜑 → ( 2 ↑ 𝐿 ) ∈ ℝ⁺ )
333	6 332	rpdivcld	⊢ ( 𝜑 → ( 𝐵 / ( 2 ↑ 𝐿 ) ) ∈ ℝ⁺ )
334	333	rpge0d	⊢ ( 𝜑 → 0 ≤ ( 𝐵 / ( 2 ↑ 𝐿 ) ) )
335	107 331	nndivred	⊢ ( 𝜑 → ( 𝐵 / ( 2 ↑ 𝐿 ) ) ∈ ℝ )
336	107 335	subge02d	⊢ ( 𝜑 → ( 0 ≤ ( 𝐵 / ( 2 ↑ 𝐿 ) ) ↔ ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝐿 ) ) ) ≤ 𝐵 ) )
337	334 336	mpbid	⊢ ( 𝜑 → ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝐿 ) ) ) ≤ 𝐵 )
338	328 337	eqbrtrd	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( 𝐵 / ( 2 ↑ 𝑛 ) ) ≤ 𝐵 )
339	106 115 5 107 325 338	le2addd	⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( vol* ‘ 𝐴 ) + Σ 𝑛 ∈ ( 1 ... 𝐿 ) ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )
340	102 116 117 286 339	letrd	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝐽 “ ( 1 ... 𝐾 ) ) ( ( 2^nd ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) − ( 1^st ‘ ( ( 𝐹 ‘ ( 1^st ‘ 𝑗 ) ) ‘ ( 2^nd ‘ 𝑗 ) ) ) ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )
341	96 340	eqbrtrrd	⊢ ( 𝜑 → ( 𝑈 ‘ 𝐾 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )

Metamath Proof Explorer

Theorem ovoliunlem1

Proof