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 24565

Description: Lemma for ovolun 24568. (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 24543	. . . . . . . . . 10 ⊢ (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
3	1, 2	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
4	3	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
5	4	ffvelrnda 6943	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
6		nneo 12334	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
7	6	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
8	7	con2bid 354	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈ ℕ))
9	8	biimpar 477	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → ((𝑛 + 1) / 2) ∈ ℕ)
10		ovolun.f1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ))
11		elovolmlem 24543	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
12	10, 11	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
13	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
14	13	ffvelrnda 6943	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
15	9, 14	syldan 590	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
16	5, 15	ifclda 4491	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
17		ovolun.h	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
18	16, 17	fmptd 6970	. . . . 5 ⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
19		eqid 2738	. . . . . 6 ⊢ ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
20		ovolun.u	. . . . . 6 ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
21	19, 20	ovolsf 24541	. . . . 5 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
22	18, 21	syl 17	. . . 4 ⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞))
23		rge0ssre 13117	. . . 4 ⊢ (0[,)+∞) ⊆ ℝ
24		fss 6601	. . . 4 ⊢ ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
25	22, 23, 24	sylancl 585	. . 3 ⊢ (𝜑 → 𝑈:ℕ⟶ℝ)
26	25	ffvelrnda 6943	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ∈ ℝ)
27		2nn 11976	. . . 4 ⊢ 2 ∈ ℕ
28		peano2nn 11915	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
29	28	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
30	29	nnred 11918	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
31	30	rehalfcld 12150	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ)
32	31	flcld 13446	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℤ)
33		ax-1cn 10860	. . . . . . . . 9 ⊢ 1 ∈ ℂ
34	33	2timesi 12041	. . . . . . . 8 ⊢ (2 · 1) = (1 + 1)
35		nnge1 11931	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ≤ 𝑘)
36	35	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
37		nnre 11910	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
38	37	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
39		1re 10906	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
40		leadd1 11373	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
41	39, 39, 40	mp3an13 1450	. . . . . . . . . 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 5105	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 1) ≤ (𝑘 + 1))
45		2re 11977	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
46		2pos 12006	. . . . . . . . . 10 ⊢ 0 < 2
47	45, 46	pm3.2i 470	. . . . . . . . 9 ⊢ (2 ∈ ℝ ∧ 0 < 2)
48		lemuldiv2 11786	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
49	39, 47, 48	mp3an13 1450	. . . . . . . 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 12280	. . . . . . 7 ⊢ 1 ∈ ℤ
53		flge 13453	. . . . . . 7 ⊢ ((((𝑘 + 1) / 2) ∈ ℝ ∧ 1 ∈ ℤ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
54	31, 52, 53	sylancl 585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
55	51, 54	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ (⌊‘((𝑘 + 1) / 2)))
56		elnnz1 12276	. . . . 5 ⊢ ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
57	32, 55, 56	sylanbrc 582	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
58		nnmulcl 11927	. . . 4 ⊢ ((2 ∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
59	27, 57, 58	sylancr 586	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
60	25	ffvelrnda 6943	. . 3 ⊢ ((𝜑 ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
61	59, 60	syldan 590	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
62		ovolun.a	. . . . . 6 ⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
63	62	simprd 495	. . . . 5 ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)
64		ovolun.b	. . . . . 6 ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
65	64	simprd 495	. . . . 5 ⊢ (𝜑 → (vol*‘𝐵) ∈ ℝ)
66	63, 65	readdcld 10935	. . . 4 ⊢ (𝜑 → ((vol‘𝐴) + (vol‘𝐵)) ∈ ℝ)
67		ovolun.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
68	67	rpred 12701	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
69	66, 68	readdcld 10935	. . 3 ⊢ (𝜑 → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) ∈ ℝ)
70	69	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) ∈ ℝ)
71		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
72		nnuz 12550	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
73	71, 72	eleqtrdi 2849	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
74		nnz 12272	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
75	74	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
76		flhalf 13478	. . . . . 6 ⊢ (𝑘 ∈ ℤ → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
77	75, 76	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
78		nnz 12272	. . . . . . 7 ⊢ ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ)
79		eluz 12525	. . . . . . 7 ⊢ ((𝑘 ∈ ℤ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
80	74, 78, 79	syl2an 595	. . . . . 6 ⊢ ((𝑘 ∈ ℕ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
81	71, 59, 80	syl2anc 583	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
82	77, 81	mpbird 256	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘))
83		elfznn 13214	. . . . 5 ⊢ (𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ ℕ)
84	19	ovolfsf 24540	. . . . . . . . . 10 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
85	18, 84	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
86	85	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
87	86	ffvelrnda 6943	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞))
88		elrege0 13115	. . . . . . 7 ⊢ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
89	87, 88	sylib 217	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
90	89	simpld 494	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
91	83, 90	sylan2 592	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2))))) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
92		elfzuz 13181	. . . . . 6 ⊢ (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ (ℤ_≥‘(𝑘 + 1)))
93		eluznn 12587	. . . . . 6 ⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
94	29, 92, 93	syl2an 595	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 𝑗 ∈ ℕ)
95	89	simprd 495	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
96	94, 95	syldan 590	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
97	73, 82, 91, 96	sermono 13683	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))))
98	20	fveq1i 6757	. . 3 ⊢ (𝑈‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘)
99	20	fveq1i 6757	. . 3 ⊢ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2))))
100	97, 98, 99	3brtr4g 5104	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
101		eqid 2738	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
102		ovolun.s	. . . . . . . . . 10 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
103	101, 102	ovolsf 24541	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
104	12, 103	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
105	104	frnd 6592	. . . . . . 7 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
106	105, 23	sstrdi 3929	. . . . . 6 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
107	106	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ)
108	104	ffnd 6585	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn ℕ)
109		fnfvelrn 6940	. . . . . 6 ⊢ ((𝑆 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
110	108, 57, 109	syl2an2r 681	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
111	107, 110	sseldd 3918	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
112		eqid 2738	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
113		ovolun.t	. . . . . . . . . 10 ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
114	112, 113	ovolsf 24541	. . . . . . . . 9 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
115	3, 114	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
116	115	frnd 6592	. . . . . . 7 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
117	116, 23	sstrdi 3929	. . . . . 6 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ)
118	117	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ)
119	115	ffnd 6585	. . . . . 6 ⊢ (𝜑 → 𝑇 Fn ℕ)
120		fnfvelrn 6940	. . . . . 6 ⊢ ((𝑇 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
121	119, 57, 120	syl2an2r 681	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
122	118, 121	sseldd 3918	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
123	68	rehalfcld 12150	. . . . . 6 ⊢ (𝜑 → (𝐶 / 2) ∈ ℝ)
124	63, 123	readdcld 10935	. . . . 5 ⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
125	124	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
126	65, 123	readdcld 10935	. . . . 5 ⊢ (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
127	126	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
128		ressxr 10950	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ^*
129	106, 128	sstrdi 3929	. . . . . . . 8 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ^*)
130		supxrcl 12978	. . . . . . . 8 ⊢ (ran 𝑆 ⊆ ℝ^* → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
131	129, 130	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
132		1nn 11914	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
133	104	fdmd 6595	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑆 = ℕ)
134	132, 133	eleqtrrid 2846	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ dom 𝑆)
135	134	ne0d 4266	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑆 ≠ ∅)
136		dm0rn0 5823	. . . . . . . . . 10 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
137	136	necon3bii 2995	. . . . . . . . 9 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
138	135, 137	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ran 𝑆 ≠ ∅)
139		supxrgtmnf 12992	. . . . . . . 8 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → -∞ < sup(ran 𝑆, ℝ^*, < ))
140	106, 138, 139	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → -∞ < sup(ran 𝑆, ℝ^*, < ))
141		ovolun.f3	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
142		xrre 12832	. . . . . . 7 ⊢ (((sup(ran 𝑆, ℝ^, < ) ∈ ℝ^ ∧ ((vol‘𝐴) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ^, < ) ∧ sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))) → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
143	131, 124, 140, 141, 142	syl22anc 835	. . . . . 6 ⊢ (𝜑 → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
144	143	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
145		supxrub 12987	. . . . . 6 ⊢ ((ran 𝑆 ⊆ ℝ^* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ^*, < ))
146	129, 110, 145	syl2an2r 681	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ^*, < ))
147	141	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
148	111, 144, 125, 146, 147	letrd 11062	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
149	117, 128	sstrdi 3929	. . . . . . . 8 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ^*)
150		supxrcl 12978	. . . . . . . 8 ⊢ (ran 𝑇 ⊆ ℝ^* → sup(ran 𝑇, ℝ^, < ) ∈ ℝ^)
151	149, 150	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ∈ ℝ^)
152	115	fdmd 6595	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑇 = ℕ)
153	132, 152	eleqtrrid 2846	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ dom 𝑇)
154	153	ne0d 4266	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑇 ≠ ∅)
155		dm0rn0 5823	. . . . . . . . . 10 ⊢ (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
156	155	necon3bii 2995	. . . . . . . . 9 ⊢ (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
157	154, 156	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ran 𝑇 ≠ ∅)
158		supxrgtmnf 12992	. . . . . . . 8 ⊢ ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅) → -∞ < sup(ran 𝑇, ℝ^*, < ))
159	117, 157, 158	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → -∞ < sup(ran 𝑇, ℝ^*, < ))
160		ovolun.g3	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
161		xrre 12832	. . . . . . 7 ⊢ (((sup(ran 𝑇, ℝ^, < ) ∈ ℝ^ ∧ ((vol‘𝐵) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑇, ℝ^, < ) ∧ sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
162	151, 126, 159, 160, 161	syl22anc 835	. . . . . 6 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
163	162	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
164		supxrub 12987	. . . . . 6 ⊢ ((ran 𝑇 ⊆ ℝ^* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ^*, < ))
165	149, 121, 164	syl2an2r 681	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ^*, < ))
166	160	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
167	122, 163, 127, 165, 166	letrd 11062	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
168	111, 122, 125, 127, 148, 167	le2addd 11524	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))))
169		oveq2 7263	. . . . . . . . 9 ⊢ (𝑧 = 1 → (2 · 𝑧) = (2 · 1))
170	169	fveq2d 6760	. . . . . . . 8 ⊢ (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1)))
171		fveq2 6756	. . . . . . . . 9 ⊢ (𝑧 = 1 → (𝑆‘𝑧) = (𝑆‘1))
172		fveq2 6756	. . . . . . . . 9 ⊢ (𝑧 = 1 → (𝑇‘𝑧) = (𝑇‘1))
173	171, 172	oveq12d 7273	. . . . . . . 8 ⊢ (𝑧 = 1 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘1) + (𝑇‘1)))
174	170, 173	eqeq12d 2754	. . . . . . 7 ⊢ (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))
175	174	imbi2d 340	. . . . . 6 ⊢ (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))))
176		oveq2 7263	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘))
177	176	fveq2d 6760	. . . . . . . 8 ⊢ (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘)))
178		fveq2 6756	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (𝑆‘𝑧) = (𝑆‘𝑘))
179		fveq2 6756	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (𝑇‘𝑧) = (𝑇‘𝑘))
180	178, 179	oveq12d 7273	. . . . . . . 8 ⊢ (𝑧 = 𝑘 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))
181	177, 180	eqeq12d 2754	. . . . . . 7 ⊢ (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))))
182	181	imbi2d 340	. . . . . 6 ⊢ (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))))
183		oveq2 7263	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1)))
184	183	fveq2d 6760	. . . . . . . 8 ⊢ (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1))))
185		fveq2 6756	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (𝑆‘𝑧) = (𝑆‘(𝑘 + 1)))
186		fveq2 6756	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (𝑇‘𝑧) = (𝑇‘(𝑘 + 1)))
187	185, 186	oveq12d 7273	. . . . . . . 8 ⊢ (𝑧 = (𝑘 + 1) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))
188	184, 187	eqeq12d 2754	. . . . . . 7 ⊢ (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
189	188	imbi2d 340	. . . . . 6 ⊢ (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
190		oveq2 7263	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 · 𝑧) = (2 · (⌊‘((𝑘 + 1) / 2))))
191	190	fveq2d 6760	. . . . . . . 8 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
192		fveq2 6756	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆‘𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2))))
193		fveq2 6756	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇‘𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2))))
194	192, 193	oveq12d 7273	. . . . . . . 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 340	. . . . . 6 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))))
197	20	fveq1i 6757	. . . . . . . 8 ⊢ (𝑈‘(2 · 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1))
198	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℕ)
199	19	ovolfsval 24539	. . . . . . . . . . . 12 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))))
200	18, 132, 199	sylancl 585	. . . . . . . . . . 11 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))))
201		halfnz 12328	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ (1 / 2) ∈ ℤ
202		nnz 12272	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 / 2) ∈ ℕ → (𝑛 / 2) ∈ ℤ)
203		oveq1 7262	. . . . . . . . . . . . . . . . . . . 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 4467	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2)))
208		oveq1 7262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
209		df-2 11966	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
210	208, 209	eqtr4di 2797	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑛 + 1) = 2)
211	210	oveq1d 7270	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2))
212		2div2e1 12044	. . . . . . . . . . . . . . . . . 18 ⊢ (2 / 2) = 1
213	211, 212	eqtrdi 2795	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = 1)
214	213	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1))
215	207, 214	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1))
216		fvex 6769	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘1) ∈ V
217	215, 17, 216	fvmpt 6857	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → (𝐻‘1) = (𝐹‘1))
218	132, 217	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐻‘1) = (𝐹‘1)
219	218	fveq2i 6759	. . . . . . . . . . . 12 ⊢ (2^nd ‘(𝐻‘1)) = (2^nd ‘(𝐹‘1))
220	218	fveq2i 6759	. . . . . . . . . . . 12 ⊢ (1^st ‘(𝐻‘1)) = (1^st ‘(𝐹‘1))
221	219, 220	oveq12i 7267	. . . . . . . . . . 11 ⊢ ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1)))
222	200, 221	eqtrdi 2795	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
223	52, 222	seq1i 13663	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
224		2t1e2 12066	. . . . . . . . . . 11 ⊢ (2 · 1) = 2
225	224	fveq2i 6759	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘ − ) ∘ 𝐻)‘2)
226	19	ovolfsval 24539	. . . . . . . . . . . 12 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 2 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))))
227	18, 27, 226	sylancl 585	. . . . . . . . . . 11 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))))
228		oveq1 7262	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 2 → (𝑛 / 2) = (2 / 2))
229	228, 212	eqtrdi 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 2 → (𝑛 / 2) = 1)
230	229, 132	eqeltrdi 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 2 → (𝑛 / 2) ∈ ℕ)
231	230	iftrued 4464	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2)))
232	229	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1))
233	231, 232	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1))
234		fvex 6769	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘1) ∈ V
235	233, 17, 234	fvmpt 6857	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℕ → (𝐻‘2) = (𝐺‘1))
236	27, 235	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐻‘2) = (𝐺‘1)
237	236	fveq2i 6759	. . . . . . . . . . . 12 ⊢ (2^nd ‘(𝐻‘2)) = (2^nd ‘(𝐺‘1))
238	236	fveq2i 6759	. . . . . . . . . . . 12 ⊢ (1^st ‘(𝐻‘2)) = (1^st ‘(𝐺‘1))
239	237, 238	oveq12i 7267	. . . . . . . . . . 11 ⊢ ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))
240	227, 239	eqtrdi 2795	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
241	225, 240	syl5eq 2791	. . . . . . . . 9 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
242	72, 198, 34, 223, 241	seqp1d 13666	. . . . . . . 8 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
243	197, 242	syl5eq 2791	. . . . . . 7 ⊢ (𝜑 → (𝑈‘(2 · 1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
244	102	fveq1i 6757	. . . . . . . . 9 ⊢ (𝑆‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1)
245	101	ovolfsval 24539	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
246	12, 132, 245	sylancl 585	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
247	52, 246	seq1i 13663	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
248	244, 247	syl5eq 2791	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
249	113	fveq1i 6757	. . . . . . . . 9 ⊢ (𝑇‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1)
250	112	ovolfsval 24539	. . . . . . . . . . 11 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
251	3, 132, 250	sylancl 585	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
252	52, 251	seq1i 13663	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
253	249, 252	syl5eq 2791	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
254	248, 253	oveq12d 7273	. . . . . . 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 7262	. . . . . . . . 9 ⊢ ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
257	34	oveq2i 7266	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
258		2cnd 11981	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
259	38	recnd 10934	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
260		1cnd 10901	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
261	258, 259, 260	adddid 10930	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
262		nnmulcl 11927	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
263	27, 262	mpan 686	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
264	263	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
265	264	nncnd 11919	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
266	265, 260, 260	addassd 10928	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
267	257, 261, 266	3eqtr4a 2805	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1))
268	267	fveq2d 6760	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1)))
269	20	fveq1i 6757	. . . . . . . . . . . 12 ⊢ (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1))
270	264	peano2nnd 11920	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
271	270, 72	eleqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ (ℤ_≥‘1))
272		seqp1 13664	. . . . . . . . . . . . . 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 13664	. . . . . . . . . . . . . . . 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 6757	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘))
278	277	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)))
279		oveq1 7262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2))
280	279	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
281	279	fveq2d 6760	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2)))
282		oveq1 7262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1))
283	282	fvoveq1d 7277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
284	280, 281, 283	ifbieq12d 4484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
285		fvex 6769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈ V
286		fvex 6769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈ V
287	285, 286	ifex 4506	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V
288	284, 17, 287	fvmpt 6857	. . . . . . . . . . . . . . . . . . . . 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 12007	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ≠ 0
291	290	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ≠ 0)
292	259, 258, 291	divcan3d 11686	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘)
293	292, 71	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈ ℕ)
294		nneo 12334	. . . . . . . . . . . . . . . . . . . . . . 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 4467	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
298	267	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
299	29	nncnd 11919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
300		2cn 11978	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℂ
301		divcan3 11589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
302	300, 290, 301	mp3an23 1451	. . . . . . . . . . . . . . . . . . . . . . 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 6760	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1)))
306	289, 297, 305	3eqtrd 2782	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1)))
307	306	fveq2d 6760	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐻‘((2 · 𝑘) + 1))) = (2^nd ‘(𝐹‘(𝑘 + 1))))
308	306	fveq2d 6760	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐻‘((2 · 𝑘) + 1))) = (1^st ‘(𝐹‘(𝑘 + 1))))
309	307, 308	oveq12d 7273	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2^nd ‘(𝐹‘(𝑘 + 1))) − (1^st ‘(𝐹‘(𝑘 + 1)))))
310	19	ovolfsval 24539	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))))
311	18, 270, 310	syl2an2r 681	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))))
312	101	ovolfsval 24539	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2^nd ‘(𝐹‘(𝑘 + 1))) − (1^st ‘(𝐹‘(𝑘 + 1)))))
313	12, 28, 312	syl2an 595	. . . . . . . . . . . . . . . . 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 7273	. . . . . . . . . . . . . . 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 6760	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1)))
318	270	peano2nnd 11920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈ ℕ)
319	267, 318	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈ ℕ)
320		oveq1 7262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2))
321	320	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · (𝑘 + 1)) / 2) ∈ ℕ))
322	320	fveq2d 6760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
323		oveq1 7262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1))
324	323	fvoveq1d 7277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))
325	321, 322, 324	ifbieq12d 4484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
326		fvex 6769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈ V
327		fvex 6769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈ V
328	326, 327	ifex 4506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V
329	325, 17, 328	fvmpt 6857	. . . . . . . . . . . . . . . . . . . 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 4464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
333	303	fveq2d 6760	. . . . . . . . . . . . . . . . . . 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 6760	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (2^nd ‘(𝐺‘(𝑘 + 1))))
337	335	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (1^st ‘(𝐺‘(𝑘 + 1))))
338	336, 337	oveq12d 7273	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2^nd ‘(𝐺‘(𝑘 + 1))) − (1^st ‘(𝐺‘(𝑘 + 1)))))
339	19	ovolfsval 24539	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
340	18, 318, 339	syl2an2r 681	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
341	112	ovolfsval 24539	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2^nd ‘(𝐺‘(𝑘 + 1))) − (1^st ‘(𝐺‘(𝑘 + 1)))))
342	3, 28, 341	syl2an 595	. . . . . . . . . . . . . . 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 7273	. . . . . . . . . . . . 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	syl5eq 2791	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
347		ffvelrn 6941	. . . . . . . . . . . . . . 15 ⊢ ((𝑈:ℕ⟶(0[,)+∞) ∧ (2 · 𝑘) ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
348	22, 263, 347	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
349	23, 348	sselid 3915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ)
350	349	recnd 10934	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ)
351	101	ovolfsf 24540	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
352	12, 351	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
353		ffvelrn 6941	. . . . . . . . . . . . . . 15 ⊢ ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
354	352, 28, 353	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
355	23, 354	sselid 3915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ)
356	355	recnd 10934	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ)
357	112	ovolfsf 24540	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
358	3, 357	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
359		ffvelrn 6941	. . . . . . . . . . . . . . 15 ⊢ ((((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
360	358, 28, 359	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
361	23, 360	sselid 3915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ)
362	361	recnd 10934	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ)
363	350, 356, 362	addassd 10928	. . . . . . . . . . 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 13664	. . . . . . . . . . . . . 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 6757	. . . . . . . . . . . . 13 ⊢ (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1))
368	102	fveq1i 6757	. . . . . . . . . . . . . 14 ⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
369	368	oveq1i 7265	. . . . . . . . . . . . 13 ⊢ ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))
370	366, 367, 369	3eqtr4g 2804	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
371		seqp1 13664	. . . . . . . . . . . . . 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 6757	. . . . . . . . . . . . 13 ⊢ (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1))
374	113	fveq1i 6757	. . . . . . . . . . . . . 14 ⊢ (𝑇‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
375	374	oveq1i 7265	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
376	372, 373, 375	3eqtr4g 2804	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
377	370, 376	oveq12d 7273	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
378	104	ffvelrnda 6943	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ (0[,)+∞))
379	23, 378	sselid 3915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ)
380	379	recnd 10934	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℂ)
381	115	ffvelrnda 6943	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ (0[,)+∞))
382	23, 381	sselid 3915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℝ)
383	382	recnd 10934	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℂ)
384	380, 356, 383, 362	add4d 11133	. . . . . . . . . . 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 413	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝜑 → ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
389	388	a2d 29	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))) → (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
390	175, 182, 189, 196, 255, 389	nnind 11921	. . . . 5 ⊢ ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ → (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
391	390	impcom 407	. . . 4 ⊢ ((𝜑 ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
392	57, 391	syldan 590	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
393	63	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
394	393	recnd 10934	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℂ)
395	68	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℝ)
396	395	rehalfcld 12150	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ)
397	396	recnd 10934	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ)
398	65	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℝ)
399	398	recnd 10934	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℂ)
400	394, 397, 399, 397	add4d 11133	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))) = (((vol‘𝐴) + (vol‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))))
401	395	recnd 10934	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
402	401	2halvesd 12149	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
403	402	oveq2d 7271	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))
404	400, 403	eqtr2d 2779	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) = (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))))
405	168, 392, 404	3brtr4d 5102	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))
406	26, 61, 70, 100, 405	letrd 11062	1 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 ifcif 4456 ∪ cuni 4836 class class class wbr 5070 ↦ cmpt 5153 × cxp 5578 dom cdm 5580 ran crn 5581 ∘ ccom 5584 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 1^st c1st 7802 2^nd c2nd 7803 ↑_m cmap 8573 supcsup 9129 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 +∞cpnf 10937 -∞cmnf 10938 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 − cmin 11135 / cdiv 11562 ℕcn 11903 2c2 11958 ℤcz 12249 ℤ_≥cuz 12511 ℝ⁺crp 12659 (,)cioo 13008 [,)cico 13010 ...cfz 13168 ⌊cfl 13438 seqcseq 13649 abscabs 14873 vol*covol 24531

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-inf 9132 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-ico 13014 df-fz 13169 df-fl 13440 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875

This theorem is referenced by: ovolunlem1 24566

W3C validator