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 24860

Description: Lemma for ovolun 24863. (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 24838	. . . . . . . . . 10 ⊢ (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
3	1, 2	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
4	3	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
5	4	ffvelcdmda 7035	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
6		nneo 12587	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
7	6	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
8	7	con2bid 354	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈ ℕ))
9	8	biimpar 478	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → ((𝑛 + 1) / 2) ∈ ℕ)
10		ovolun.f1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ))
11		elovolmlem 24838	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_m ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
12	10, 11	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
13	12	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
14	13	ffvelcdmda 7035	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
15	9, 14	syldan 591	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
16	5, 15	ifclda 4521	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
17		ovolun.h	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
18	16, 17	fmptd 7062	. . . . 5 ⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
19		eqid 2736	. . . . . 6 ⊢ ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
20		ovolun.u	. . . . . 6 ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
21	19, 20	ovolsf 24836	. . . . 5 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
22	18, 21	syl 17	. . . 4 ⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞))
23		rge0ssre 13373	. . . 4 ⊢ (0[,)+∞) ⊆ ℝ
24		fss 6685	. . . 4 ⊢ ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
25	22, 23, 24	sylancl 586	. . 3 ⊢ (𝜑 → 𝑈:ℕ⟶ℝ)
26	25	ffvelcdmda 7035	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ∈ ℝ)
27		2nn 12226	. . . 4 ⊢ 2 ∈ ℕ
28		peano2nn 12165	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
29	28	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
30	29	nnred 12168	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
31	30	rehalfcld 12400	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ)
32	31	flcld 13703	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℤ)
33		ax-1cn 11109	. . . . . . . . 9 ⊢ 1 ∈ ℂ
34	33	2timesi 12291	. . . . . . . 8 ⊢ (2 · 1) = (1 + 1)
35		nnge1 12181	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ≤ 𝑘)
36	35	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
37		nnre 12160	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
38	37	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
39		1re 11155	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
40		leadd1 11623	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
41	39, 39, 40	mp3an13 1452	. . . . . . . . . 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 5140	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 1) ≤ (𝑘 + 1))
45		2re 12227	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
46		2pos 12256	. . . . . . . . . 10 ⊢ 0 < 2
47	45, 46	pm3.2i 471	. . . . . . . . 9 ⊢ (2 ∈ ℝ ∧ 0 < 2)
48		lemuldiv2 12036	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
49	39, 47, 48	mp3an13 1452	. . . . . . . 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 12533	. . . . . . 7 ⊢ 1 ∈ ℤ
53		flge 13710	. . . . . . 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 12529	. . . . 5 ⊢ ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
57	32, 55, 56	sylanbrc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
58		nnmulcl 12177	. . . 4 ⊢ ((2 ∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
59	27, 57, 58	sylancr 587	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
60	25	ffvelcdmda 7035	. . 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 11184	. . . 4 ⊢ (𝜑 → ((vol‘𝐴) + (vol‘𝐵)) ∈ ℝ)
67		ovolun.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
68	67	rpred 12957	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
69	66, 68	readdcld 11184	. . 3 ⊢ (𝜑 → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) ∈ ℝ)
70	69	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) ∈ ℝ)
71		simpr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
72		nnuz 12806	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
73	71, 72	eleqtrdi 2848	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
74		nnz 12520	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
75	74	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
76		flhalf 13735	. . . . . 6 ⊢ (𝑘 ∈ ℤ → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
77	75, 76	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
78		nnz 12520	. . . . . . 7 ⊢ ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ)
79		eluz 12777	. . . . . . 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 13470	. . . . 5 ⊢ (𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ ℕ)
84	19	ovolfsf 24835	. . . . . . . . . 10 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
85	18, 84	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
86	85	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
87	86	ffvelcdmda 7035	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞))
88		elrege0 13371	. . . . . . 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 13437	. . . . . 6 ⊢ (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ (ℤ_≥‘(𝑘 + 1)))
93		eluznn 12843	. . . . . 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 13940	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))))
98	20	fveq1i 6843	. . 3 ⊢ (𝑈‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘)
99	20	fveq1i 6843	. . 3 ⊢ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2))))
100	97, 98, 99	3brtr4g 5139	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
101		eqid 2736	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
102		ovolun.s	. . . . . . . . . 10 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
103	101, 102	ovolsf 24836	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
104	12, 103	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
105	104	frnd 6676	. . . . . . 7 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
106	105, 23	sstrdi 3956	. . . . . 6 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
107	106	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ)
108	104	ffnd 6669	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn ℕ)
109		fnfvelrn 7031	. . . . . 6 ⊢ ((𝑆 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
110	108, 57, 109	syl2an2r 683	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
111	107, 110	sseldd 3945	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
112		eqid 2736	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
113		ovolun.t	. . . . . . . . . 10 ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
114	112, 113	ovolsf 24836	. . . . . . . . 9 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
115	3, 114	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
116	115	frnd 6676	. . . . . . 7 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
117	116, 23	sstrdi 3956	. . . . . 6 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ)
118	117	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ)
119	115	ffnd 6669	. . . . . 6 ⊢ (𝜑 → 𝑇 Fn ℕ)
120		fnfvelrn 7031	. . . . . 6 ⊢ ((𝑇 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
121	119, 57, 120	syl2an2r 683	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
122	118, 121	sseldd 3945	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
123	68	rehalfcld 12400	. . . . . 6 ⊢ (𝜑 → (𝐶 / 2) ∈ ℝ)
124	63, 123	readdcld 11184	. . . . 5 ⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
125	124	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
126	65, 123	readdcld 11184	. . . . 5 ⊢ (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
127	126	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
128		ressxr 11199	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ^*
129	106, 128	sstrdi 3956	. . . . . . . 8 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ^*)
130		supxrcl 13234	. . . . . . . 8 ⊢ (ran 𝑆 ⊆ ℝ^* → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
131	129, 130	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
132		1nn 12164	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
133	104	fdmd 6679	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑆 = ℕ)
134	132, 133	eleqtrrid 2845	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ dom 𝑆)
135	134	ne0d 4295	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑆 ≠ ∅)
136		dm0rn0 5880	. . . . . . . . . 10 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
137	136	necon3bii 2996	. . . . . . . . 9 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
138	135, 137	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ran 𝑆 ≠ ∅)
139		supxrgtmnf 13248	. . . . . . . 8 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → -∞ < sup(ran 𝑆, ℝ^*, < ))
140	106, 138, 139	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → -∞ < sup(ran 𝑆, ℝ^*, < ))
141		ovolun.f3	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
142		xrre 13088	. . . . . . 7 ⊢ (((sup(ran 𝑆, ℝ^, < ) ∈ ℝ^ ∧ ((vol‘𝐴) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ^, < ) ∧ sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))) → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
143	131, 124, 140, 141, 142	syl22anc 837	. . . . . 6 ⊢ (𝜑 → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
144	143	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
145		supxrub 13243	. . . . . 6 ⊢ ((ran 𝑆 ⊆ ℝ^* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ^*, < ))
146	129, 110, 145	syl2an2r 683	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ^*, < ))
147	141	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
148	111, 144, 125, 146, 147	letrd 11312	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
149	117, 128	sstrdi 3956	. . . . . . . 8 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ^*)
150		supxrcl 13234	. . . . . . . 8 ⊢ (ran 𝑇 ⊆ ℝ^* → sup(ran 𝑇, ℝ^, < ) ∈ ℝ^)
151	149, 150	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ∈ ℝ^)
152	115	fdmd 6679	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑇 = ℕ)
153	132, 152	eleqtrrid 2845	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ dom 𝑇)
154	153	ne0d 4295	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑇 ≠ ∅)
155		dm0rn0 5880	. . . . . . . . . 10 ⊢ (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
156	155	necon3bii 2996	. . . . . . . . 9 ⊢ (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
157	154, 156	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ran 𝑇 ≠ ∅)
158		supxrgtmnf 13248	. . . . . . . 8 ⊢ ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅) → -∞ < sup(ran 𝑇, ℝ^*, < ))
159	117, 157, 158	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → -∞ < sup(ran 𝑇, ℝ^*, < ))
160		ovolun.g3	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
161		xrre 13088	. . . . . . 7 ⊢ (((sup(ran 𝑇, ℝ^, < ) ∈ ℝ^ ∧ ((vol‘𝐵) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑇, ℝ^, < ) ∧ sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
162	151, 126, 159, 160, 161	syl22anc 837	. . . . . 6 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
163	162	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
164		supxrub 13243	. . . . . 6 ⊢ ((ran 𝑇 ⊆ ℝ^* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ^*, < ))
165	149, 121, 164	syl2an2r 683	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ^*, < ))
166	160	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
167	122, 163, 127, 165, 166	letrd 11312	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
168	111, 122, 125, 127, 148, 167	le2addd 11774	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))))
169		oveq2 7365	. . . . . . . . 9 ⊢ (𝑧 = 1 → (2 · 𝑧) = (2 · 1))
170	169	fveq2d 6846	. . . . . . . 8 ⊢ (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1)))
171		fveq2 6842	. . . . . . . . 9 ⊢ (𝑧 = 1 → (𝑆‘𝑧) = (𝑆‘1))
172		fveq2 6842	. . . . . . . . 9 ⊢ (𝑧 = 1 → (𝑇‘𝑧) = (𝑇‘1))
173	171, 172	oveq12d 7375	. . . . . . . 8 ⊢ (𝑧 = 1 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘1) + (𝑇‘1)))
174	170, 173	eqeq12d 2752	. . . . . . 7 ⊢ (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))
175	174	imbi2d 340	. . . . . 6 ⊢ (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))))
176		oveq2 7365	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘))
177	176	fveq2d 6846	. . . . . . . 8 ⊢ (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘)))
178		fveq2 6842	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (𝑆‘𝑧) = (𝑆‘𝑘))
179		fveq2 6842	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (𝑇‘𝑧) = (𝑇‘𝑘))
180	178, 179	oveq12d 7375	. . . . . . . 8 ⊢ (𝑧 = 𝑘 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))
181	177, 180	eqeq12d 2752	. . . . . . 7 ⊢ (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))))
182	181	imbi2d 340	. . . . . 6 ⊢ (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))))
183		oveq2 7365	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1)))
184	183	fveq2d 6846	. . . . . . . 8 ⊢ (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1))))
185		fveq2 6842	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (𝑆‘𝑧) = (𝑆‘(𝑘 + 1)))
186		fveq2 6842	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (𝑇‘𝑧) = (𝑇‘(𝑘 + 1)))
187	185, 186	oveq12d 7375	. . . . . . . 8 ⊢ (𝑧 = (𝑘 + 1) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))
188	184, 187	eqeq12d 2752	. . . . . . 7 ⊢ (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
189	188	imbi2d 340	. . . . . 6 ⊢ (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
190		oveq2 7365	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 · 𝑧) = (2 · (⌊‘((𝑘 + 1) / 2))))
191	190	fveq2d 6846	. . . . . . . 8 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
192		fveq2 6842	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆‘𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2))))
193		fveq2 6842	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇‘𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2))))
194	192, 193	oveq12d 7375	. . . . . . . 8 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
195	191, 194	eqeq12d 2752	. . . . . . 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 6843	. . . . . . . 8 ⊢ (𝑈‘(2 · 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1))
198	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℕ)
199	19	ovolfsval 24834	. . . . . . . . . . . 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 12581	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ (1 / 2) ∈ ℤ
202		nnz 12520	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 / 2) ∈ ℕ → (𝑛 / 2) ∈ ℤ)
203		oveq1 7364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 / 2) = (1 / 2))
204	203	eleq1d 2822	. . . . . . . . . . . . . . . . . . 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 4497	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2)))
208		oveq1 7364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
209		df-2 12216	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
210	208, 209	eqtr4di 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑛 + 1) = 2)
211	210	oveq1d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2))
212		2div2e1 12294	. . . . . . . . . . . . . . . . . 18 ⊢ (2 / 2) = 1
213	211, 212	eqtrdi 2792	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = 1)
214	213	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1))
215	207, 214	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1))
216		fvex 6855	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘1) ∈ V
217	215, 17, 216	fvmpt 6948	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → (𝐻‘1) = (𝐹‘1))
218	132, 217	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐻‘1) = (𝐹‘1)
219	218	fveq2i 6845	. . . . . . . . . . . 12 ⊢ (2^nd ‘(𝐻‘1)) = (2^nd ‘(𝐹‘1))
220	218	fveq2i 6845	. . . . . . . . . . . 12 ⊢ (1^st ‘(𝐻‘1)) = (1^st ‘(𝐹‘1))
221	219, 220	oveq12i 7369	. . . . . . . . . . 11 ⊢ ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1)))
222	200, 221	eqtrdi 2792	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
223	52, 222	seq1i 13920	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
224		2t1e2 12316	. . . . . . . . . . 11 ⊢ (2 · 1) = 2
225	224	fveq2i 6845	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘ − ) ∘ 𝐻)‘2)
226	19	ovolfsval 24834	. . . . . . . . . . . 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 7364	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 2 → (𝑛 / 2) = (2 / 2))
229	228, 212	eqtrdi 2792	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 2 → (𝑛 / 2) = 1)
230	229, 132	eqeltrdi 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 2 → (𝑛 / 2) ∈ ℕ)
231	230	iftrued 4494	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2)))
232	229	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1))
233	231, 232	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1))
234		fvex 6855	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘1) ∈ V
235	233, 17, 234	fvmpt 6948	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℕ → (𝐻‘2) = (𝐺‘1))
236	27, 235	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐻‘2) = (𝐺‘1)
237	236	fveq2i 6845	. . . . . . . . . . . 12 ⊢ (2^nd ‘(𝐻‘2)) = (2^nd ‘(𝐺‘1))
238	236	fveq2i 6845	. . . . . . . . . . . 12 ⊢ (1^st ‘(𝐻‘2)) = (1^st ‘(𝐺‘1))
239	237, 238	oveq12i 7369	. . . . . . . . . . 11 ⊢ ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))
240	227, 239	eqtrdi 2792	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
241	225, 240	eqtrid 2788	. . . . . . . . 9 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
242	72, 198, 34, 223, 241	seqp1d 13923	. . . . . . . 8 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
243	197, 242	eqtrid 2788	. . . . . . 7 ⊢ (𝜑 → (𝑈‘(2 · 1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
244	102	fveq1i 6843	. . . . . . . . 9 ⊢ (𝑆‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1)
245	101	ovolfsval 24834	. . . . . . . . . . 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 13920	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
248	244, 247	eqtrid 2788	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
249	113	fveq1i 6843	. . . . . . . . 9 ⊢ (𝑇‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1)
250	112	ovolfsval 24834	. . . . . . . . . . 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 13920	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
253	249, 252	eqtrid 2788	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
254	248, 253	oveq12d 7375	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
255	243, 254	eqtr4d 2779	. . . . . 6 ⊢ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))
256		oveq1 7364	. . . . . . . . 9 ⊢ ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
257	34	oveq2i 7368	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
258		2cnd 12231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
259	38	recnd 11183	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
260		1cnd 11150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
261	258, 259, 260	adddid 11179	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
262		nnmulcl 12177	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
263	27, 262	mpan 688	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
264	263	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
265	264	nncnd 12169	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
266	265, 260, 260	addassd 11177	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
267	257, 261, 266	3eqtr4a 2802	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1))
268	267	fveq2d 6846	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1)))
269	20	fveq1i 6843	. . . . . . . . . . . 12 ⊢ (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1))
270	264	peano2nnd 12170	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
271	270, 72	eleqtrdi 2848	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ (ℤ_≥‘1))
272		seqp1 13921	. . . . . . . . . . . . . 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 2848	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ (ℤ_≥‘1))
275		seqp1 13921	. . . . . . . . . . . . . . . 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 6843	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘))
278	277	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)))
279		oveq1 7364	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2))
280	279	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
281	279	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2)))
282		oveq1 7364	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1))
283	282	fvoveq1d 7379	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
284	280, 281, 283	ifbieq12d 4514	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
285		fvex 6855	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈ V
286		fvex 6855	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈ V
287	285, 286	ifex 4536	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V
288	284, 17, 287	fvmpt 6948	. . . . . . . . . . . . . . . . . . . . 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 12257	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ≠ 0
291	290	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ≠ 0)
292	259, 258, 291	divcan3d 11936	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘)
293	292, 71	eqeltrd 2838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈ ℕ)
294		nneo 12587	. . . . . . . . . . . . . . . . . . . . . . 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 4497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
298	267	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
299	29	nncnd 12169	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
300		2cn 12228	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℂ
301		divcan3 11839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
302	300, 290, 301	mp3an23 1453	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 + 1) ∈ ℂ → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
303	299, 302	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
304	298, 303	eqtr3d 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1))
305	304	fveq2d 6846	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1)))
306	289, 297, 305	3eqtrd 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1)))
307	306	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐻‘((2 · 𝑘) + 1))) = (2^nd ‘(𝐹‘(𝑘 + 1))))
308	306	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐻‘((2 · 𝑘) + 1))) = (1^st ‘(𝐹‘(𝑘 + 1))))
309	307, 308	oveq12d 7375	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2^nd ‘(𝐹‘(𝑘 + 1))) − (1^st ‘(𝐹‘(𝑘 + 1)))))
310	19	ovolfsval 24834	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))))
311	18, 270, 310	syl2an2r 683	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))))
312	101	ovolfsval 24834	. . . . . . . . . . . . . . . . . 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 2787	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))
315	278, 314	oveq12d 7375	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
316	276, 315	eqtr4d 2779	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
317	267	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1)))
318	270	peano2nnd 12170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈ ℕ)
319	267, 318	eqeltrd 2838	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈ ℕ)
320		oveq1 7364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2))
321	320	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · (𝑘 + 1)) / 2) ∈ ℕ))
322	320	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
323		oveq1 7364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1))
324	323	fvoveq1d 7379	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))
325	321, 322, 324	ifbieq12d 4514	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
326		fvex 6855	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈ V
327		fvex 6855	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈ V
328	326, 327	ifex 4536	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V
329	325, 17, 328	fvmpt 6948	. . . . . . . . . . . . . . . . . . . 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 2838	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈ ℕ)
332	331	iftrued 4494	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
333	303	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1)))
334	330, 332, 333	3eqtrd 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1)))
335	317, 334	eqtr3d 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1)))
336	335	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (2^nd ‘(𝐺‘(𝑘 + 1))))
337	335	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (1^st ‘(𝐺‘(𝑘 + 1))))
338	336, 337	oveq12d 7375	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2^nd ‘(𝐺‘(𝑘 + 1))) − (1^st ‘(𝐺‘(𝑘 + 1)))))
339	19	ovolfsval 24834	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
340	18, 318, 339	syl2an2r 683	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
341	112	ovolfsval 24834	. . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
344	316, 343	oveq12d 7375	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
345	273, 344	eqtrd 2776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
346	269, 345	eqtrid 2788	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
347		ffvelcdm 7032	. . . . . . . . . . . . . . 15 ⊢ ((𝑈:ℕ⟶(0[,)+∞) ∧ (2 · 𝑘) ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
348	22, 263, 347	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
349	23, 348	sselid 3942	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ)
350	349	recnd 11183	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ)
351	101	ovolfsf 24835	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
352	12, 351	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
353		ffvelcdm 7032	. . . . . . . . . . . . . . 15 ⊢ ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
354	352, 28, 353	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
355	23, 354	sselid 3942	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ)
356	355	recnd 11183	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ)
357	112	ovolfsf 24835	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
358	3, 357	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
359		ffvelcdm 7032	. . . . . . . . . . . . . . 15 ⊢ ((((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
360	358, 28, 359	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
361	23, 360	sselid 3942	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ)
362	361	recnd 11183	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ)
363	350, 356, 362	addassd 11177	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
364	268, 346, 363	3eqtrd 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
365		seqp1 13921	. . . . . . . . . . . . . 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 6843	. . . . . . . . . . . . 13 ⊢ (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1))
368	102	fveq1i 6843	. . . . . . . . . . . . . 14 ⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
369	368	oveq1i 7367	. . . . . . . . . . . . 13 ⊢ ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))
370	366, 367, 369	3eqtr4g 2801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
371		seqp1 13921	. . . . . . . . . . . . . 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 6843	. . . . . . . . . . . . 13 ⊢ (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1))
374	113	fveq1i 6843	. . . . . . . . . . . . . 14 ⊢ (𝑇‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
375	374	oveq1i 7367	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
376	372, 373, 375	3eqtr4g 2801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
377	370, 376	oveq12d 7375	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
378	104	ffvelcdmda 7035	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ (0[,)+∞))
379	23, 378	sselid 3942	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ)
380	379	recnd 11183	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℂ)
381	115	ffvelcdmda 7035	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ (0[,)+∞))
382	23, 381	sselid 3942	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℝ)
383	382	recnd 11183	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℂ)
384	380, 356, 383, 362	add4d 11383	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
385	377, 384	eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
386	364, 385	eqeq12d 2752	. . . . . . . . 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 12171	. . . . 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 11183	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℂ)
395	68	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℝ)
396	395	rehalfcld 12400	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ)
397	396	recnd 11183	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ)
398	65	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℝ)
399	398	recnd 11183	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℂ)
400	394, 397, 399, 397	add4d 11383	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))) = (((vol‘𝐴) + (vol‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))))
401	395	recnd 11183	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
402	401	2halvesd 12399	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
403	402	oveq2d 7373	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))
404	400, 403	eqtr2d 2777	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) = (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))))
405	168, 392, 404	3brtr4d 5137	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))
406	26, 61, 70, 100, 405	letrd 11312	1 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 ifcif 4486 ∪ cuni 4865 class class class wbr 5105 ↦ cmpt 5188 × cxp 5631 dom cdm 5633 ran crn 5634 ∘ ccom 5637 Fn wfn 6491 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 1^st c1st 7919 2^nd c2nd 7920 ↑_m cmap 8765 supcsup 9376 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 · cmul 11056 +∞cpnf 11186 -∞cmnf 11187 ℝ^*cxr 11188 < clt 11189 ≤ cle 11190 − cmin 11385 / cdiv 11812 ℕcn 12153 2c2 12208 ℤcz 12499 ℤ_≥cuz 12763 ℝ⁺crp 12915 (,)cioo 13264 [,)cico 13266 ...cfz 13424 ⌊cfl 13695 seqcseq 13906 abscabs 15119 vol*covol 24826

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 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 2707 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-sup 9378 df-inf 9379 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-n0 12414 df-z 12500 df-uz 12764 df-rp 12916 df-ico 13270 df-fz 13425 df-fl 13697 df-seq 13907 df-exp 13968 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121

This theorem is referenced by: ovolunlem1 24861

W3C validator