ovolunlem1a - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ovolunlem1a		Structured version Visualization version GIF version

Theorem ovolunlem1a 24660

Description: Lemma for ovolun 24663. (Contributed by Mario Carneiro, 7-May-2015.)

**Hypotheses**
Ref	Expression
ovolun.a	⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
ovolun.b	⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
ovolun.c	⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
ovolun.s	⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ovolun.t	⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
ovolun.u	⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
ovolun.f1	⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ))
ovolun.f2	⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))
ovolun.f3	⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
ovolun.g1	⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ))
ovolun.g2	⊢ (𝜑 → 𝐵 ⊆ ∪ ran ((,) ∘ 𝐺))
ovolun.g3	⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
ovolun.h	⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))

**Assertion**
Ref	Expression
ovolunlem1a	⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))

Distinct variable groups: 𝑘,𝑛,𝐶 𝑘,𝐹,𝑛 𝑘,𝐻 𝐴,𝑘,𝑛 𝐵,𝑘,𝑛 𝑆,𝑘 𝑇,𝑘 𝑘,𝐺,𝑛 𝜑,𝑘,𝑛 𝑈,𝑘 Allowed substitution hints: 𝑆(𝑛) 𝑇(𝑛) 𝑈(𝑛) 𝐻(𝑛)

Proof of Theorem ovolunlem1a Dummy variables 𝑧 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovolun.g1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ))
2		elovolmlem 24638	. . . . . . . . . 10 ⊢ (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
3	1, 2	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
4	3	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
5	4	ffvelrnda 6961	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
6		nneo 12404	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
7	6	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
8	7	con2bid 355	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈ ℕ))
9	8	biimpar 478	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → ((𝑛 + 1) / 2) ∈ ℕ)
10		ovolun.f1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ))
11		elovolmlem 24638	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
12	10, 11	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
13	12	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
14	13	ffvelrnda 6961	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
15	9, 14	syldan 591	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
16	5, 15	ifclda 4494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
17		ovolun.h	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
18	16, 17	fmptd 6988	. . . . 5 ⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
19		eqid 2738	. . . . . 6 ⊢ ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
20		ovolun.u	. . . . . 6 ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
21	19, 20	ovolsf 24636	. . . . 5 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
22	18, 21	syl 17	. . . 4 ⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞))
23		rge0ssre 13188	. . . 4 ⊢ (0[,)+∞) ⊆ ℝ
24		fss 6617	. . . 4 ⊢ ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
25	22, 23, 24	sylancl 586	. . 3 ⊢ (𝜑 → 𝑈:ℕ⟶ℝ)
26	25	ffvelrnda 6961	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ∈ ℝ)
27		2nn 12046	. . . 4 ⊢ 2 ∈ ℕ
28		peano2nn 11985	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
29	28	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
30	29	nnred 11988	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
31	30	rehalfcld 12220	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ)
32	31	flcld 13518	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℤ)
33		ax-1cn 10929	. . . . . . . . 9 ⊢ 1 ∈ ℂ
34	33	2timesi 12111	. . . . . . . 8 ⊢ (2 · 1) = (1 + 1)
35		nnge1 12001	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ≤ 𝑘)
36	35	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
37		nnre 11980	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
38	37	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
39		1re 10975	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
40		leadd1 11443	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
41	39, 39, 40	mp3an13 1451	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℝ → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
42	38, 41	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
43	36, 42	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 + 1) ≤ (𝑘 + 1))
44	34, 43	eqbrtrid 5109	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 1) ≤ (𝑘 + 1))
45		2re 12047	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
46		2pos 12076	. . . . . . . . . 10 ⊢ 0 < 2
47	45, 46	pm3.2i 471	. . . . . . . . 9 ⊢ (2 ∈ ℝ ∧ 0 < 2)
48		lemuldiv2 11856	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
49	39, 47, 48	mp3an13 1451	. . . . . . . 8 ⊢ ((𝑘 + 1) ∈ ℝ → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
50	30, 49	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
51	44, 50	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ ((𝑘 + 1) / 2))
52		1z 12350	. . . . . . 7 ⊢ 1 ∈ ℤ
53		flge 13525	. . . . . . 7 ⊢ ((((𝑘 + 1) / 2) ∈ ℝ ∧ 1 ∈ ℤ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
54	31, 52, 53	sylancl 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
55	51, 54	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ (⌊‘((𝑘 + 1) / 2)))
56		elnnz1 12346	. . . . 5 ⊢ ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
57	32, 55, 56	sylanbrc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
58		nnmulcl 11997	. . . 4 ⊢ ((2 ∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
59	27, 57, 58	sylancr 587	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
60	25	ffvelrnda 6961	. . 3 ⊢ ((𝜑 ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
61	59, 60	syldan 591	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
62		ovolun.a	. . . . . 6 ⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
63	62	simprd 496	. . . . 5 ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)
64		ovolun.b	. . . . . 6 ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
65	64	simprd 496	. . . . 5 ⊢ (𝜑 → (vol*‘𝐵) ∈ ℝ)
66	63, 65	readdcld 11004	. . . 4 ⊢ (𝜑 → ((vol‘𝐴) + (vol‘𝐵)) ∈ ℝ)
67		ovolun.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
68	67	rpred 12772	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
69	66, 68	readdcld 11004	. . 3 ⊢ (𝜑 → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) ∈ ℝ)
70	69	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) ∈ ℝ)
71		simpr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
72		nnuz 12621	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
73	71, 72	eleqtrdi 2849	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
74		nnz 12342	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
75	74	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
76		flhalf 13550	. . . . . 6 ⊢ (𝑘 ∈ ℤ → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
77	75, 76	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
78		nnz 12342	. . . . . . 7 ⊢ ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ)
79		eluz 12596	. . . . . . 7 ⊢ ((𝑘 ∈ ℤ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
80	74, 78, 79	syl2an 596	. . . . . 6 ⊢ ((𝑘 ∈ ℕ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
81	71, 59, 80	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
82	77, 81	mpbird 256	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘))
83		elfznn 13285	. . . . 5 ⊢ (𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ ℕ)
84	19	ovolfsf 24635	. . . . . . . . . 10 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
85	18, 84	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
86	85	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
87	86	ffvelrnda 6961	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞))
88		elrege0 13186	. . . . . . 7 ⊢ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
89	87, 88	sylib 217	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
90	89	simpld 495	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
91	83, 90	sylan2 593	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2))))) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
92		elfzuz 13252	. . . . . 6 ⊢ (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ (ℤ_≥‘(𝑘 + 1)))
93		eluznn 12658	. . . . . 6 ⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
94	29, 92, 93	syl2an 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 𝑗 ∈ ℕ)
95	89	simprd 496	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
96	94, 95	syldan 591	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
97	73, 82, 91, 96	sermono 13755	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))))
98	20	fveq1i 6775	. . 3 ⊢ (𝑈‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘)
99	20	fveq1i 6775	. . 3 ⊢ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2))))
100	97, 98, 99	3brtr4g 5108	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
101		eqid 2738	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
102		ovolun.s	. . . . . . . . . 10 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
103	101, 102	ovolsf 24636	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
104	12, 103	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
105	104	frnd 6608	. . . . . . 7 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
106	105, 23	sstrdi 3933	. . . . . 6 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
107	106	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ)
108	104	ffnd 6601	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn ℕ)
109		fnfvelrn 6958	. . . . . 6 ⊢ ((𝑆 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
110	108, 57, 109	syl2an2r 682	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
111	107, 110	sseldd 3922	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
112		eqid 2738	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
113		ovolun.t	. . . . . . . . . 10 ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
114	112, 113	ovolsf 24636	. . . . . . . . 9 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
115	3, 114	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
116	115	frnd 6608	. . . . . . 7 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
117	116, 23	sstrdi 3933	. . . . . 6 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ)
118	117	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ)
119	115	ffnd 6601	. . . . . 6 ⊢ (𝜑 → 𝑇 Fn ℕ)
120		fnfvelrn 6958	. . . . . 6 ⊢ ((𝑇 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
121	119, 57, 120	syl2an2r 682	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
122	118, 121	sseldd 3922	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
123	68	rehalfcld 12220	. . . . . 6 ⊢ (𝜑 → (𝐶 / 2) ∈ ℝ)
124	63, 123	readdcld 11004	. . . . 5 ⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
125	124	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
126	65, 123	readdcld 11004	. . . . 5 ⊢ (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
127	126	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
128		ressxr 11019	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ^*
129	106, 128	sstrdi 3933	. . . . . . . 8 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ^*)
130		supxrcl 13049	. . . . . . . 8 ⊢ (ran 𝑆 ⊆ ℝ^* → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
131	129, 130	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
132		1nn 11984	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
133	104	fdmd 6611	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑆 = ℕ)
134	132, 133	eleqtrrid 2846	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ dom 𝑆)
135	134	ne0d 4269	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑆 ≠ ∅)
136		dm0rn0 5834	. . . . . . . . . 10 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
137	136	necon3bii 2996	. . . . . . . . 9 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
138	135, 137	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ran 𝑆 ≠ ∅)
139		supxrgtmnf 13063	. . . . . . . 8 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → -∞ < sup(ran 𝑆, ℝ^*, < ))
140	106, 138, 139	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → -∞ < sup(ran 𝑆, ℝ^*, < ))
141		ovolun.f3	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
142		xrre 12903	. . . . . . 7 ⊢ (((sup(ran 𝑆, ℝ^, < ) ∈ ℝ^ ∧ ((vol‘𝐴) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ^, < ) ∧ sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))) → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
143	131, 124, 140, 141, 142	syl22anc 836	. . . . . 6 ⊢ (𝜑 → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
144	143	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
145		supxrub 13058	. . . . . 6 ⊢ ((ran 𝑆 ⊆ ℝ^* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ^*, < ))
146	129, 110, 145	syl2an2r 682	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ^*, < ))
147	141	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
148	111, 144, 125, 146, 147	letrd 11132	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
149	117, 128	sstrdi 3933	. . . . . . . 8 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ^*)
150		supxrcl 13049	. . . . . . . 8 ⊢ (ran 𝑇 ⊆ ℝ^* → sup(ran 𝑇, ℝ^, < ) ∈ ℝ^)
151	149, 150	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ∈ ℝ^)
152	115	fdmd 6611	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑇 = ℕ)
153	132, 152	eleqtrrid 2846	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ dom 𝑇)
154	153	ne0d 4269	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑇 ≠ ∅)
155		dm0rn0 5834	. . . . . . . . . 10 ⊢ (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
156	155	necon3bii 2996	. . . . . . . . 9 ⊢ (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
157	154, 156	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ran 𝑇 ≠ ∅)
158		supxrgtmnf 13063	. . . . . . . 8 ⊢ ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅) → -∞ < sup(ran 𝑇, ℝ^*, < ))
159	117, 157, 158	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → -∞ < sup(ran 𝑇, ℝ^*, < ))
160		ovolun.g3	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
161		xrre 12903	. . . . . . 7 ⊢ (((sup(ran 𝑇, ℝ^, < ) ∈ ℝ^ ∧ ((vol‘𝐵) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑇, ℝ^, < ) ∧ sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
162	151, 126, 159, 160, 161	syl22anc 836	. . . . . 6 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
163	162	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
164		supxrub 13058	. . . . . 6 ⊢ ((ran 𝑇 ⊆ ℝ^* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ^*, < ))
165	149, 121, 164	syl2an2r 682	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ^*, < ))
166	160	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
167	122, 163, 127, 165, 166	letrd 11132	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
168	111, 122, 125, 127, 148, 167	le2addd 11594	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))))
169		oveq2 7283	. . . . . . . . 9 ⊢ (𝑧 = 1 → (2 · 𝑧) = (2 · 1))
170	169	fveq2d 6778	. . . . . . . 8 ⊢ (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1)))
171		fveq2 6774	. . . . . . . . 9 ⊢ (𝑧 = 1 → (𝑆‘𝑧) = (𝑆‘1))
172		fveq2 6774	. . . . . . . . 9 ⊢ (𝑧 = 1 → (𝑇‘𝑧) = (𝑇‘1))
173	171, 172	oveq12d 7293	. . . . . . . 8 ⊢ (𝑧 = 1 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘1) + (𝑇‘1)))
174	170, 173	eqeq12d 2754	. . . . . . 7 ⊢ (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))
175	174	imbi2d 341	. . . . . 6 ⊢ (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))))
176		oveq2 7283	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘))
177	176	fveq2d 6778	. . . . . . . 8 ⊢ (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘)))
178		fveq2 6774	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (𝑆‘𝑧) = (𝑆‘𝑘))
179		fveq2 6774	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (𝑇‘𝑧) = (𝑇‘𝑘))
180	178, 179	oveq12d 7293	. . . . . . . 8 ⊢ (𝑧 = 𝑘 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))
181	177, 180	eqeq12d 2754	. . . . . . 7 ⊢ (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))))
182	181	imbi2d 341	. . . . . 6 ⊢ (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))))
183		oveq2 7283	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1)))
184	183	fveq2d 6778	. . . . . . . 8 ⊢ (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1))))
185		fveq2 6774	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (𝑆‘𝑧) = (𝑆‘(𝑘 + 1)))
186		fveq2 6774	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (𝑇‘𝑧) = (𝑇‘(𝑘 + 1)))
187	185, 186	oveq12d 7293	. . . . . . . 8 ⊢ (𝑧 = (𝑘 + 1) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))
188	184, 187	eqeq12d 2754	. . . . . . 7 ⊢ (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
189	188	imbi2d 341	. . . . . 6 ⊢ (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
190		oveq2 7283	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 · 𝑧) = (2 · (⌊‘((𝑘 + 1) / 2))))
191	190	fveq2d 6778	. . . . . . . 8 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
192		fveq2 6774	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆‘𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2))))
193		fveq2 6774	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇‘𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2))))
194	192, 193	oveq12d 7293	. . . . . . . 8 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
195	191, 194	eqeq12d 2754	. . . . . . 7 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
196	195	imbi2d 341	. . . . . 6 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))))
197	20	fveq1i 6775	. . . . . . . 8 ⊢ (𝑈‘(2 · 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1))
198	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℕ)
199	19	ovolfsval 24634	. . . . . . . . . . . 12 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))))
200	18, 132, 199	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))))
201		halfnz 12398	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ (1 / 2) ∈ ℤ
202		nnz 12342	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 / 2) ∈ ℕ → (𝑛 / 2) ∈ ℤ)
203		oveq1 7282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 / 2) = (1 / 2))
204	203	eleq1d 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → ((𝑛 / 2) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
205	202, 204	syl5ib 243	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → ((𝑛 / 2) ∈ ℕ → (1 / 2) ∈ ℤ))
206	201, 205	mtoi 198	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → ¬ (𝑛 / 2) ∈ ℕ)
207	206	iffalsed 4470	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2)))
208		oveq1 7282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
209		df-2 12036	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
210	208, 209	eqtr4di 2796	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑛 + 1) = 2)
211	210	oveq1d 7290	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2))
212		2div2e1 12114	. . . . . . . . . . . . . . . . . 18 ⊢ (2 / 2) = 1
213	211, 212	eqtrdi 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = 1)
214	213	fveq2d 6778	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1))
215	207, 214	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1))
216		fvex 6787	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘1) ∈ V
217	215, 17, 216	fvmpt 6875	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → (𝐻‘1) = (𝐹‘1))
218	132, 217	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐻‘1) = (𝐹‘1)
219	218	fveq2i 6777	. . . . . . . . . . . 12 ⊢ (2^nd ‘(𝐻‘1)) = (2^nd ‘(𝐹‘1))
220	218	fveq2i 6777	. . . . . . . . . . . 12 ⊢ (1^st ‘(𝐻‘1)) = (1^st ‘(𝐹‘1))
221	219, 220	oveq12i 7287	. . . . . . . . . . 11 ⊢ ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1)))
222	200, 221	eqtrdi 2794	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
223	52, 222	seq1i 13735	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
224		2t1e2 12136	. . . . . . . . . . 11 ⊢ (2 · 1) = 2
225	224	fveq2i 6777	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘ − ) ∘ 𝐻)‘2)
226	19	ovolfsval 24634	. . . . . . . . . . . 12 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 2 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))))
227	18, 27, 226	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))))
228		oveq1 7282	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 2 → (𝑛 / 2) = (2 / 2))
229	228, 212	eqtrdi 2794	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 2 → (𝑛 / 2) = 1)
230	229, 132	eqeltrdi 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 2 → (𝑛 / 2) ∈ ℕ)
231	230	iftrued 4467	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2)))
232	229	fveq2d 6778	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1))
233	231, 232	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1))
234		fvex 6787	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘1) ∈ V
235	233, 17, 234	fvmpt 6875	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℕ → (𝐻‘2) = (𝐺‘1))
236	27, 235	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐻‘2) = (𝐺‘1)
237	236	fveq2i 6777	. . . . . . . . . . . 12 ⊢ (2^nd ‘(𝐻‘2)) = (2^nd ‘(𝐺‘1))
238	236	fveq2i 6777	. . . . . . . . . . . 12 ⊢ (1^st ‘(𝐻‘2)) = (1^st ‘(𝐺‘1))
239	237, 238	oveq12i 7287	. . . . . . . . . . 11 ⊢ ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))
240	227, 239	eqtrdi 2794	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
241	225, 240	eqtrid 2790	. . . . . . . . 9 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
242	72, 198, 34, 223, 241	seqp1d 13738	. . . . . . . 8 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
243	197, 242	eqtrid 2790	. . . . . . 7 ⊢ (𝜑 → (𝑈‘(2 · 1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
244	102	fveq1i 6775	. . . . . . . . 9 ⊢ (𝑆‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1)
245	101	ovolfsval 24634	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
246	12, 132, 245	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
247	52, 246	seq1i 13735	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
248	244, 247	eqtrid 2790	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
249	113	fveq1i 6775	. . . . . . . . 9 ⊢ (𝑇‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1)
250	112	ovolfsval 24634	. . . . . . . . . . 11 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
251	3, 132, 250	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
252	52, 251	seq1i 13735	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
253	249, 252	eqtrid 2790	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
254	248, 253	oveq12d 7293	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
255	243, 254	eqtr4d 2781	. . . . . 6 ⊢ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))
256		oveq1 7282	. . . . . . . . 9 ⊢ ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
257	34	oveq2i 7286	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
258		2cnd 12051	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
259	38	recnd 11003	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
260		1cnd 10970	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
261	258, 259, 260	adddid 10999	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
262		nnmulcl 11997	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
263	27, 262	mpan 687	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
264	263	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
265	264	nncnd 11989	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
266	265, 260, 260	addassd 10997	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
267	257, 261, 266	3eqtr4a 2804	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1))
268	267	fveq2d 6778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1)))
269	20	fveq1i 6775	. . . . . . . . . . . 12 ⊢ (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1))
270	264	peano2nnd 11990	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
271	270, 72	eleqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ (ℤ_≥‘1))
272		seqp1 13736	. . . . . . . . . . . . . 14 ⊢ (((2 · 𝑘) + 1) ∈ (ℤ_≥‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))))
273	271, 272	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))))
274	264, 72	eleqtrdi 2849	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ (ℤ_≥‘1))
275		seqp1 13736	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑘) ∈ (ℤ_≥‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
276	274, 275	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
277	20	fveq1i 6775	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘))
278	277	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)))
279		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2))
280	279	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
281	279	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2)))
282		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1))
283	282	fvoveq1d 7297	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
284	280, 281, 283	ifbieq12d 4487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
285		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈ V
286		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈ V
287	285, 286	ifex 4509	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V
288	284, 17, 287	fvmpt 6875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 · 𝑘) + 1) ∈ ℕ → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
289	270, 288	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
290		2ne0 12077	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ≠ 0
291	290	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ≠ 0)
292	259, 258, 291	divcan3d 11756	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘)
293	292, 71	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈ ℕ)
294		nneo 12404	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 · 𝑘) ∈ ℕ → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
295	264, 294	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
296	293, 295	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ)
297	296	iffalsed 4470	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
298	267	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
299	29	nncnd 11989	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
300		2cn 12048	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℂ
301		divcan3 11659	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
302	300, 290, 301	mp3an23 1452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 + 1) ∈ ℂ → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
303	299, 302	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
304	298, 303	eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1))
305	304	fveq2d 6778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1)))
306	289, 297, 305	3eqtrd 2782	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1)))
307	306	fveq2d 6778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐻‘((2 · 𝑘) + 1))) = (2^nd ‘(𝐹‘(𝑘 + 1))))
308	306	fveq2d 6778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐻‘((2 · 𝑘) + 1))) = (1^st ‘(𝐹‘(𝑘 + 1))))
309	307, 308	oveq12d 7293	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2^nd ‘(𝐹‘(𝑘 + 1))) − (1^st ‘(𝐹‘(𝑘 + 1)))))
310	19	ovolfsval 24634	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))))
311	18, 270, 310	syl2an2r 682	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))))
312	101	ovolfsval 24634	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2^nd ‘(𝐹‘(𝑘 + 1))) − (1^st ‘(𝐹‘(𝑘 + 1)))))
313	12, 28, 312	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2^nd ‘(𝐹‘(𝑘 + 1))) − (1^st ‘(𝐹‘(𝑘 + 1)))))
314	309, 311, 313	3eqtr4rd 2789	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))
315	278, 314	oveq12d 7293	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
316	276, 315	eqtr4d 2781	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
317	267	fveq2d 6778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1)))
318	270	peano2nnd 11990	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈ ℕ)
319	267, 318	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈ ℕ)
320		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2))
321	320	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · (𝑘 + 1)) / 2) ∈ ℕ))
322	320	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
323		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1))
324	323	fvoveq1d 7297	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))
325	321, 322, 324	ifbieq12d 4487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
326		fvex 6787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈ V
327		fvex 6787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈ V
328	326, 327	ifex 4509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V
329	325, 17, 328	fvmpt 6875	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · (𝑘 + 1)) ∈ ℕ → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
330	319, 329	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
331	303, 29	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈ ℕ)
332	331	iftrued 4467	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
333	303	fveq2d 6778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1)))
334	330, 332, 333	3eqtrd 2782	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1)))
335	317, 334	eqtr3d 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1)))
336	335	fveq2d 6778	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (2^nd ‘(𝐺‘(𝑘 + 1))))
337	335	fveq2d 6778	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (1^st ‘(𝐺‘(𝑘 + 1))))
338	336, 337	oveq12d 7293	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2^nd ‘(𝐺‘(𝑘 + 1))) − (1^st ‘(𝐺‘(𝑘 + 1)))))
339	19	ovolfsval 24634	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
340	18, 318, 339	syl2an2r 682	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
341	112	ovolfsval 24634	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2^nd ‘(𝐺‘(𝑘 + 1))) − (1^st ‘(𝐺‘(𝑘 + 1)))))
342	3, 28, 341	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2^nd ‘(𝐺‘(𝑘 + 1))) − (1^st ‘(𝐺‘(𝑘 + 1)))))
343	338, 340, 342	3eqtr4d 2788	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
344	316, 343	oveq12d 7293	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
345	273, 344	eqtrd 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
346	269, 345	eqtrid 2790	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
347		ffvelrn 6959	. . . . . . . . . . . . . . 15 ⊢ ((𝑈:ℕ⟶(0[,)+∞) ∧ (2 · 𝑘) ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
348	22, 263, 347	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
349	23, 348	sselid 3919	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ)
350	349	recnd 11003	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ)
351	101	ovolfsf 24635	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
352	12, 351	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
353		ffvelrn 6959	. . . . . . . . . . . . . . 15 ⊢ ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
354	352, 28, 353	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
355	23, 354	sselid 3919	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ)
356	355	recnd 11003	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ)
357	112	ovolfsf 24635	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
358	3, 357	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
359		ffvelrn 6959	. . . . . . . . . . . . . . 15 ⊢ ((((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
360	358, 28, 359	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
361	23, 360	sselid 3919	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ)
362	361	recnd 11003	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ)
363	350, 356, 362	addassd 10997	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
364	268, 346, 363	3eqtrd 2782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
365		seqp1 13736	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
366	73, 365	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
367	102	fveq1i 6775	. . . . . . . . . . . . 13 ⊢ (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1))
368	102	fveq1i 6775	. . . . . . . . . . . . . 14 ⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
369	368	oveq1i 7285	. . . . . . . . . . . . 13 ⊢ ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))
370	366, 367, 369	3eqtr4g 2803	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
371		seqp1 13736	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
372	73, 371	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
373	113	fveq1i 6775	. . . . . . . . . . . . 13 ⊢ (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1))
374	113	fveq1i 6775	. . . . . . . . . . . . . 14 ⊢ (𝑇‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
375	374	oveq1i 7285	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
376	372, 373, 375	3eqtr4g 2803	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
377	370, 376	oveq12d 7293	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
378	104	ffvelrnda 6961	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ (0[,)+∞))
379	23, 378	sselid 3919	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ)
380	379	recnd 11003	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℂ)
381	115	ffvelrnda 6961	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ (0[,)+∞))
382	23, 381	sselid 3919	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℝ)
383	382	recnd 11003	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℂ)
384	380, 356, 383, 362	add4d 11203	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
385	377, 384	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
386	364, 385	eqeq12d 2754	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) ↔ ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))))
387	256, 386	syl5ibr 245	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
388	387	expcom 414	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝜑 → ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
389	388	a2d 29	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))) → (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
390	175, 182, 189, 196, 255, 389	nnind 11991	. . . . 5 ⊢ ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ → (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
391	390	impcom 408	. . . 4 ⊢ ((𝜑 ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
392	57, 391	syldan 591	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
393	63	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
394	393	recnd 11003	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℂ)
395	68	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℝ)
396	395	rehalfcld 12220	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ)
397	396	recnd 11003	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ)
398	65	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℝ)
399	398	recnd 11003	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℂ)
400	394, 397, 399, 397	add4d 11203	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))) = (((vol‘𝐴) + (vol‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))))
401	395	recnd 11003	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
402	401	2halvesd 12219	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
403	402	oveq2d 7291	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))
404	400, 403	eqtr2d 2779	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) = (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))))
405	168, 392, 404	3brtr4d 5106	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))
406	26, 61, 70, 100, 405	letrd 11132	1 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∩ cin 3886 ⊆ wss 3887 ∅c0 4256 ifcif 4459 ∪ cuni 4839 class class class wbr 5074 ↦ cmpt 5157 × cxp 5587 dom cdm 5589 ran crn 5590 ∘ ccom 5593 Fn wfn 6428 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 1^st c1st 7829 2^nd c2nd 7830 ↑_m cmap 8615 supcsup 9199 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 +∞cpnf 11006 -∞cmnf 11007 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 − cmin 11205 / cdiv 11632 ℕcn 11973 2c2 12028 ℤcz 12319 ℤ_≥cuz 12582 ℝ⁺crp 12730 (,)cioo 13079 [,)cico 13081 ...cfz 13239 ⌊cfl 13510 seqcseq 13721 abscabs 14945 vol*covol 24626

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-map 8617 df-en 8734 df-dom 8735 df-sdom 8736 df-sup 9201 df-inf 9202 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-z 12320 df-uz 12583 df-rp 12731 df-ico 13085 df-fz 13240 df-fl 13512 df-seq 13722 df-exp 13783 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947

This theorem is referenced by: ovolunlem1 24661

W3C validator