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 25380

Description: Lemma for ovolun 25383. (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 25358	. . . . . . . . . 10 ⊢ (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
3	1, 2	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
4	3	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
5	4	ffvelcdmda 7080	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
6		nneo 12650	. . . . . . . . . . 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 25358	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
12	10, 11	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
13	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
14	13	ffvelcdmda 7080	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
15	9, 14	syldan 590	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
16	5, 15	ifclda 4558	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
17		ovolun.h	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
18	16, 17	fmptd 7109	. . . . 5 ⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
19		eqid 2726	. . . . . 6 ⊢ ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
20		ovolun.u	. . . . . 6 ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
21	19, 20	ovolsf 25356	. . . . 5 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
22	18, 21	syl 17	. . . 4 ⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞))
23		rge0ssre 13439	. . . 4 ⊢ (0[,)+∞) ⊆ ℝ
24		fss 6728	. . . 4 ⊢ ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
25	22, 23, 24	sylancl 585	. . 3 ⊢ (𝜑 → 𝑈:ℕ⟶ℝ)
26	25	ffvelcdmda 7080	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ∈ ℝ)
27		2nn 12289	. . . 4 ⊢ 2 ∈ ℕ
28		peano2nn 12228	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
29	28	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
30	29	nnred 12231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
31	30	rehalfcld 12463	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ)
32	31	flcld 13769	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℤ)
33		ax-1cn 11170	. . . . . . . . 9 ⊢ 1 ∈ ℂ
34	33	2timesi 12354	. . . . . . . 8 ⊢ (2 · 1) = (1 + 1)
35		nnge1 12244	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ≤ 𝑘)
36	35	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
37		nnre 12223	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
38	37	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
39		1re 11218	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
40		leadd1 11686	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
41	39, 39, 40	mp3an13 1448	. . . . . . . . . 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 5176	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 1) ≤ (𝑘 + 1))
45		2re 12290	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
46		2pos 12319	. . . . . . . . . 10 ⊢ 0 < 2
47	45, 46	pm3.2i 470	. . . . . . . . 9 ⊢ (2 ∈ ℝ ∧ 0 < 2)
48		lemuldiv2 12099	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
49	39, 47, 48	mp3an13 1448	. . . . . . . 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 12596	. . . . . . 7 ⊢ 1 ∈ ℤ
53		flge 13776	. . . . . . 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 12592	. . . . 5 ⊢ ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
57	32, 55, 56	sylanbrc 582	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
58		nnmulcl 12240	. . . 4 ⊢ ((2 ∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
59	27, 57, 58	sylancr 586	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
60	25	ffvelcdmda 7080	. . 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 11247	. . . 4 ⊢ (𝜑 → ((vol‘𝐴) + (vol‘𝐵)) ∈ ℝ)
67		ovolun.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
68	67	rpred 13022	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
69	66, 68	readdcld 11247	. . 3 ⊢ (𝜑 → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) ∈ ℝ)
70	69	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) ∈ ℝ)
71		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
72		nnuz 12869	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
73	71, 72	eleqtrdi 2837	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
74		nnz 12583	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
75	74	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
76		flhalf 13801	. . . . . 6 ⊢ (𝑘 ∈ ℤ → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
77	75, 76	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
78		nnz 12583	. . . . . . 7 ⊢ ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ)
79		eluz 12840	. . . . . . 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 257	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘))
83		elfznn 13536	. . . . 5 ⊢ (𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ ℕ)
84	19	ovolfsf 25355	. . . . . . . . . 10 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
85	18, 84	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
86	85	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
87	86	ffvelcdmda 7080	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞))
88		elrege0 13437	. . . . . . 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 13503	. . . . . 6 ⊢ (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ (ℤ_≥‘(𝑘 + 1)))
93		eluznn 12906	. . . . . 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 14005	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))))
98	20	fveq1i 6886	. . 3 ⊢ (𝑈‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘)
99	20	fveq1i 6886	. . 3 ⊢ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2))))
100	97, 98, 99	3brtr4g 5175	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
101		eqid 2726	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
102		ovolun.s	. . . . . . . . . 10 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
103	101, 102	ovolsf 25356	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
104	12, 103	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
105	104	frnd 6719	. . . . . . 7 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
106	105, 23	sstrdi 3989	. . . . . 6 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
107	106	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ)
108	104	ffnd 6712	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn ℕ)
109		fnfvelrn 7076	. . . . . 6 ⊢ ((𝑆 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
110	108, 57, 109	syl2an2r 682	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
111	107, 110	sseldd 3978	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
112		eqid 2726	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
113		ovolun.t	. . . . . . . . . 10 ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
114	112, 113	ovolsf 25356	. . . . . . . . 9 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
115	3, 114	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
116	115	frnd 6719	. . . . . . 7 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
117	116, 23	sstrdi 3989	. . . . . 6 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ)
118	117	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ)
119	115	ffnd 6712	. . . . . 6 ⊢ (𝜑 → 𝑇 Fn ℕ)
120		fnfvelrn 7076	. . . . . 6 ⊢ ((𝑇 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
121	119, 57, 120	syl2an2r 682	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
122	118, 121	sseldd 3978	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
123	68	rehalfcld 12463	. . . . . 6 ⊢ (𝜑 → (𝐶 / 2) ∈ ℝ)
124	63, 123	readdcld 11247	. . . . 5 ⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
125	124	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
126	65, 123	readdcld 11247	. . . . 5 ⊢ (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
127	126	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
128		ressxr 11262	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ^*
129	106, 128	sstrdi 3989	. . . . . . . 8 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ^*)
130		supxrcl 13300	. . . . . . . 8 ⊢ (ran 𝑆 ⊆ ℝ^* → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
131	129, 130	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
132		1nn 12227	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
133	104	fdmd 6722	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑆 = ℕ)
134	132, 133	eleqtrrid 2834	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ dom 𝑆)
135	134	ne0d 4330	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑆 ≠ ∅)
136		dm0rn0 5918	. . . . . . . . . 10 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
137	136	necon3bii 2987	. . . . . . . . 9 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
138	135, 137	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ran 𝑆 ≠ ∅)
139		supxrgtmnf 13314	. . . . . . . 8 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → -∞ < sup(ran 𝑆, ℝ^*, < ))
140	106, 138, 139	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → -∞ < sup(ran 𝑆, ℝ^*, < ))
141		ovolun.f3	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
142		xrre 13154	. . . . . . 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 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
145		supxrub 13309	. . . . . 6 ⊢ ((ran 𝑆 ⊆ ℝ^* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ^*, < ))
146	129, 110, 145	syl2an2r 682	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ^*, < ))
147	141	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
148	111, 144, 125, 146, 147	letrd 11375	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
149	117, 128	sstrdi 3989	. . . . . . . 8 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ^*)
150		supxrcl 13300	. . . . . . . 8 ⊢ (ran 𝑇 ⊆ ℝ^* → sup(ran 𝑇, ℝ^, < ) ∈ ℝ^)
151	149, 150	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ∈ ℝ^)
152	115	fdmd 6722	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑇 = ℕ)
153	132, 152	eleqtrrid 2834	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ dom 𝑇)
154	153	ne0d 4330	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑇 ≠ ∅)
155		dm0rn0 5918	. . . . . . . . . 10 ⊢ (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
156	155	necon3bii 2987	. . . . . . . . 9 ⊢ (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
157	154, 156	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ran 𝑇 ≠ ∅)
158		supxrgtmnf 13314	. . . . . . . 8 ⊢ ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅) → -∞ < sup(ran 𝑇, ℝ^*, < ))
159	117, 157, 158	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → -∞ < sup(ran 𝑇, ℝ^*, < ))
160		ovolun.g3	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
161		xrre 13154	. . . . . . 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 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
164		supxrub 13309	. . . . . 6 ⊢ ((ran 𝑇 ⊆ ℝ^* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ^*, < ))
165	149, 121, 164	syl2an2r 682	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ^*, < ))
166	160	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
167	122, 163, 127, 165, 166	letrd 11375	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
168	111, 122, 125, 127, 148, 167	le2addd 11837	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))))
169		oveq2 7413	. . . . . . . . 9 ⊢ (𝑧 = 1 → (2 · 𝑧) = (2 · 1))
170	169	fveq2d 6889	. . . . . . . 8 ⊢ (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1)))
171		fveq2 6885	. . . . . . . . 9 ⊢ (𝑧 = 1 → (𝑆‘𝑧) = (𝑆‘1))
172		fveq2 6885	. . . . . . . . 9 ⊢ (𝑧 = 1 → (𝑇‘𝑧) = (𝑇‘1))
173	171, 172	oveq12d 7423	. . . . . . . 8 ⊢ (𝑧 = 1 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘1) + (𝑇‘1)))
174	170, 173	eqeq12d 2742	. . . . . . 7 ⊢ (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))
175	174	imbi2d 340	. . . . . 6 ⊢ (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))))
176		oveq2 7413	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘))
177	176	fveq2d 6889	. . . . . . . 8 ⊢ (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘)))
178		fveq2 6885	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (𝑆‘𝑧) = (𝑆‘𝑘))
179		fveq2 6885	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (𝑇‘𝑧) = (𝑇‘𝑘))
180	178, 179	oveq12d 7423	. . . . . . . 8 ⊢ (𝑧 = 𝑘 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))
181	177, 180	eqeq12d 2742	. . . . . . 7 ⊢ (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))))
182	181	imbi2d 340	. . . . . 6 ⊢ (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))))
183		oveq2 7413	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1)))
184	183	fveq2d 6889	. . . . . . . 8 ⊢ (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1))))
185		fveq2 6885	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (𝑆‘𝑧) = (𝑆‘(𝑘 + 1)))
186		fveq2 6885	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (𝑇‘𝑧) = (𝑇‘(𝑘 + 1)))
187	185, 186	oveq12d 7423	. . . . . . . 8 ⊢ (𝑧 = (𝑘 + 1) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))
188	184, 187	eqeq12d 2742	. . . . . . 7 ⊢ (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
189	188	imbi2d 340	. . . . . 6 ⊢ (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
190		oveq2 7413	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 · 𝑧) = (2 · (⌊‘((𝑘 + 1) / 2))))
191	190	fveq2d 6889	. . . . . . . 8 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
192		fveq2 6885	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆‘𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2))))
193		fveq2 6885	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇‘𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2))))
194	192, 193	oveq12d 7423	. . . . . . . 8 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
195	191, 194	eqeq12d 2742	. . . . . . 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 6886	. . . . . . . 8 ⊢ (𝑈‘(2 · 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1))
198	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℕ)
199	19	ovolfsval 25354	. . . . . . . . . . . 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 12644	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ (1 / 2) ∈ ℤ
202		nnz 12583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 / 2) ∈ ℕ → (𝑛 / 2) ∈ ℤ)
203		oveq1 7412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 / 2) = (1 / 2))
204	203	eleq1d 2812	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → ((𝑛 / 2) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
205	202, 204	imbitrid 243	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → ((𝑛 / 2) ∈ ℕ → (1 / 2) ∈ ℤ))
206	201, 205	mtoi 198	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → ¬ (𝑛 / 2) ∈ ℕ)
207	206	iffalsed 4534	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2)))
208		oveq1 7412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
209		df-2 12279	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
210	208, 209	eqtr4di 2784	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑛 + 1) = 2)
211	210	oveq1d 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2))
212		2div2e1 12357	. . . . . . . . . . . . . . . . . 18 ⊢ (2 / 2) = 1
213	211, 212	eqtrdi 2782	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = 1)
214	213	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1))
215	207, 214	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1))
216		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘1) ∈ V
217	215, 17, 216	fvmpt 6992	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → (𝐻‘1) = (𝐹‘1))
218	132, 217	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐻‘1) = (𝐹‘1)
219	218	fveq2i 6888	. . . . . . . . . . . 12 ⊢ (2^nd ‘(𝐻‘1)) = (2^nd ‘(𝐹‘1))
220	218	fveq2i 6888	. . . . . . . . . . . 12 ⊢ (1^st ‘(𝐻‘1)) = (1^st ‘(𝐹‘1))
221	219, 220	oveq12i 7417	. . . . . . . . . . 11 ⊢ ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1)))
222	200, 221	eqtrdi 2782	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
223	52, 222	seq1i 13986	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
224		2t1e2 12379	. . . . . . . . . . 11 ⊢ (2 · 1) = 2
225	224	fveq2i 6888	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘ − ) ∘ 𝐻)‘2)
226	19	ovolfsval 25354	. . . . . . . . . . . 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 7412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 2 → (𝑛 / 2) = (2 / 2))
229	228, 212	eqtrdi 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 2 → (𝑛 / 2) = 1)
230	229, 132	eqeltrdi 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 2 → (𝑛 / 2) ∈ ℕ)
231	230	iftrued 4531	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2)))
232	229	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1))
233	231, 232	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1))
234		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘1) ∈ V
235	233, 17, 234	fvmpt 6992	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℕ → (𝐻‘2) = (𝐺‘1))
236	27, 235	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐻‘2) = (𝐺‘1)
237	236	fveq2i 6888	. . . . . . . . . . . 12 ⊢ (2^nd ‘(𝐻‘2)) = (2^nd ‘(𝐺‘1))
238	236	fveq2i 6888	. . . . . . . . . . . 12 ⊢ (1^st ‘(𝐻‘2)) = (1^st ‘(𝐺‘1))
239	237, 238	oveq12i 7417	. . . . . . . . . . 11 ⊢ ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))
240	227, 239	eqtrdi 2782	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
241	225, 240	eqtrid 2778	. . . . . . . . 9 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
242	72, 198, 34, 223, 241	seqp1d 13989	. . . . . . . 8 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
243	197, 242	eqtrid 2778	. . . . . . 7 ⊢ (𝜑 → (𝑈‘(2 · 1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
244	102	fveq1i 6886	. . . . . . . . 9 ⊢ (𝑆‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1)
245	101	ovolfsval 25354	. . . . . . . . . . 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 13986	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
248	244, 247	eqtrid 2778	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
249	113	fveq1i 6886	. . . . . . . . 9 ⊢ (𝑇‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1)
250	112	ovolfsval 25354	. . . . . . . . . . 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 13986	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
253	249, 252	eqtrid 2778	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
254	248, 253	oveq12d 7423	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
255	243, 254	eqtr4d 2769	. . . . . 6 ⊢ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))
256		oveq1 7412	. . . . . . . . 9 ⊢ ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
257	34	oveq2i 7416	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
258		2cnd 12294	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
259	38	recnd 11246	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
260		1cnd 11213	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
261	258, 259, 260	adddid 11242	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
262		nnmulcl 12240	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
263	27, 262	mpan 687	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
264	263	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
265	264	nncnd 12232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
266	265, 260, 260	addassd 11240	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
267	257, 261, 266	3eqtr4a 2792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1))
268	267	fveq2d 6889	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1)))
269	20	fveq1i 6886	. . . . . . . . . . . 12 ⊢ (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1))
270	264	peano2nnd 12233	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
271	270, 72	eleqtrdi 2837	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ (ℤ_≥‘1))
272		seqp1 13987	. . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ (ℤ_≥‘1))
275		seqp1 13987	. . . . . . . . . . . . . . . 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 6886	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘))
278	277	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)))
279		oveq1 7412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2))
280	279	eleq1d 2812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
281	279	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2)))
282		oveq1 7412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1))
283	282	fvoveq1d 7427	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
284	280, 281, 283	ifbieq12d 4551	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
285		fvex 6898	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈ V
286		fvex 6898	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈ V
287	285, 286	ifex 4573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V
288	284, 17, 287	fvmpt 6992	. . . . . . . . . . . . . . . . . . . . 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 12320	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ≠ 0
291	290	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ≠ 0)
292	259, 258, 291	divcan3d 11999	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘)
293	292, 71	eqeltrd 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈ ℕ)
294		nneo 12650	. . . . . . . . . . . . . . . . . . . . . . 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 4534	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
298	267	oveq1d 7420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
299	29	nncnd 12232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
300		2cn 12291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℂ
301		divcan3 11902	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
302	300, 290, 301	mp3an23 1449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 + 1) ∈ ℂ → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
303	299, 302	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
304	298, 303	eqtr3d 2768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1))
305	304	fveq2d 6889	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1)))
306	289, 297, 305	3eqtrd 2770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1)))
307	306	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐻‘((2 · 𝑘) + 1))) = (2^nd ‘(𝐹‘(𝑘 + 1))))
308	306	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐻‘((2 · 𝑘) + 1))) = (1^st ‘(𝐹‘(𝑘 + 1))))
309	307, 308	oveq12d 7423	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2^nd ‘(𝐹‘(𝑘 + 1))) − (1^st ‘(𝐹‘(𝑘 + 1)))))
310	19	ovolfsval 25354	. . . . . . . . . . . . . . . . . 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 25354	. . . . . . . . . . . . . . . . . 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 2777	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))
315	278, 314	oveq12d 7423	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
316	276, 315	eqtr4d 2769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
317	267	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1)))
318	270	peano2nnd 12233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈ ℕ)
319	267, 318	eqeltrd 2827	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈ ℕ)
320		oveq1 7412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2))
321	320	eleq1d 2812	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · (𝑘 + 1)) / 2) ∈ ℕ))
322	320	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
323		oveq1 7412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1))
324	323	fvoveq1d 7427	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))
325	321, 322, 324	ifbieq12d 4551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
326		fvex 6898	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈ V
327		fvex 6898	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈ V
328	326, 327	ifex 4573	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V
329	325, 17, 328	fvmpt 6992	. . . . . . . . . . . . . . . . . . . 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 2827	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈ ℕ)
332	331	iftrued 4531	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
333	303	fveq2d 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1)))
334	330, 332, 333	3eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1)))
335	317, 334	eqtr3d 2768	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1)))
336	335	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (2^nd ‘(𝐺‘(𝑘 + 1))))
337	335	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (1^st ‘(𝐺‘(𝑘 + 1))))
338	336, 337	oveq12d 7423	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2^nd ‘(𝐺‘(𝑘 + 1))) − (1^st ‘(𝐺‘(𝑘 + 1)))))
339	19	ovolfsval 25354	. . . . . . . . . . . . . . . 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 25354	. . . . . . . . . . . . . . . 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 2776	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
344	316, 343	oveq12d 7423	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
345	273, 344	eqtrd 2766	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
346	269, 345	eqtrid 2778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
347		ffvelcdm 7077	. . . . . . . . . . . . . . 15 ⊢ ((𝑈:ℕ⟶(0[,)+∞) ∧ (2 · 𝑘) ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
348	22, 263, 347	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
349	23, 348	sselid 3975	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ)
350	349	recnd 11246	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ)
351	101	ovolfsf 25355	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
352	12, 351	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
353		ffvelcdm 7077	. . . . . . . . . . . . . . 15 ⊢ ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
354	352, 28, 353	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
355	23, 354	sselid 3975	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ)
356	355	recnd 11246	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ)
357	112	ovolfsf 25355	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
358	3, 357	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
359		ffvelcdm 7077	. . . . . . . . . . . . . . 15 ⊢ ((((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
360	358, 28, 359	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
361	23, 360	sselid 3975	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ)
362	361	recnd 11246	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ)
363	350, 356, 362	addassd 11240	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
364	268, 346, 363	3eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
365		seqp1 13987	. . . . . . . . . . . . . 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 6886	. . . . . . . . . . . . 13 ⊢ (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1))
368	102	fveq1i 6886	. . . . . . . . . . . . . 14 ⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
369	368	oveq1i 7415	. . . . . . . . . . . . 13 ⊢ ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))
370	366, 367, 369	3eqtr4g 2791	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
371		seqp1 13987	. . . . . . . . . . . . . 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 6886	. . . . . . . . . . . . 13 ⊢ (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1))
374	113	fveq1i 6886	. . . . . . . . . . . . . 14 ⊢ (𝑇‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
375	374	oveq1i 7415	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
376	372, 373, 375	3eqtr4g 2791	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
377	370, 376	oveq12d 7423	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
378	104	ffvelcdmda 7080	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ (0[,)+∞))
379	23, 378	sselid 3975	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ)
380	379	recnd 11246	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℂ)
381	115	ffvelcdmda 7080	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ (0[,)+∞))
382	23, 381	sselid 3975	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℝ)
383	382	recnd 11246	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℂ)
384	380, 356, 383, 362	add4d 11446	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
385	377, 384	eqtrd 2766	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
386	364, 385	eqeq12d 2742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) ↔ ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))))
387	256, 386	imbitrrid 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 12234	. . . . 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 11246	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℂ)
395	68	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℝ)
396	395	rehalfcld 12463	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ)
397	396	recnd 11246	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ)
398	65	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℝ)
399	398	recnd 11246	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℂ)
400	394, 397, 399, 397	add4d 11446	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))) = (((vol‘𝐴) + (vol‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))))
401	395	recnd 11246	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
402	401	2halvesd 12462	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
403	402	oveq2d 7421	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))
404	400, 403	eqtr2d 2767	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) = (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))))
405	168, 392, 404	3brtr4d 5173	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))
406	26, 61, 70, 100, 405	letrd 11375	1 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ≠ wne 2934 ∩ cin 3942 ⊆ wss 3943 ∅c0 4317 ifcif 4523 ∪ cuni 4902 class class class wbr 5141 ↦ cmpt 5224 × cxp 5667 dom cdm 5669 ran crn 5670 ∘ ccom 5673 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7405 1^st c1st 7972 2^nd c2nd 7973 ↑_m cmap 8822 supcsup 9437 ℂcc 11110 ℝcr 11111 0cc0 11112 1c1 11113 + caddc 11115 · cmul 11117 +∞cpnf 11249 -∞cmnf 11250 ℝ^*cxr 11251 < clt 11252 ≤ cle 11253 − cmin 11448 / cdiv 11875 ℕcn 12216 2c2 12271 ℤcz 12562 ℤ_≥cuz 12826 ℝ⁺crp 12980 (,)cioo 13330 [,)cico 13332 ...cfz 13490 ⌊cfl 13761 seqcseq 13972 abscabs 15187 vol*covol 25346

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7722 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6294 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7853 df-1st 7974 df-2nd 7975 df-frecs 8267 df-wrecs 8298 df-recs 8372 df-rdg 8411 df-er 8705 df-map 8824 df-en 8942 df-dom 8943 df-sdom 8944 df-sup 9439 df-inf 9440 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-n0 12477 df-z 12563 df-uz 12827 df-rp 12981 df-ico 13336 df-fz 13491 df-fl 13763 df-seq 13973 df-exp 14033 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189

This theorem is referenced by: ovolunlem1 25381

W3C validator