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 23264

Description: Lemma for ovolun 23267. (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	⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_𝑚 ℕ))
ovolun.f2	⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))
ovolun.f3	⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
ovolun.g1	⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_𝑚 ℕ))
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 ⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_𝑚 ℕ))
2		reex 10027	. . . . . . . . . . . . 13 ⊢ ℝ ∈ V
3	2, 2	xpex 6962	. . . . . . . . . . . 12 ⊢ (ℝ × ℝ) ∈ V
4	3	inex2 4800	. . . . . . . . . . 11 ⊢ ( ≤ ∩ (ℝ × ℝ)) ∈ V
5		nnex 11026	. . . . . . . . . . 11 ⊢ ℕ ∈ V
6	4, 5	elmap 7886	. . . . . . . . . 10 ⊢ (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_𝑚 ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
7	1, 6	sylib 208	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
8	7	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
9	8	ffvelrnda 6359	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
10		nneo 11461	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
11	10	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
12	11	con2bid 344	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈ ℕ))
13	12	biimpar 502	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → ((𝑛 + 1) / 2) ∈ ℕ)
14		ovolun.f1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_𝑚 ℕ))
15	4, 5	elmap 7886	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑_𝑚 ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
16	14, 15	sylib 208	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
17	16	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
18	17	ffvelrnda 6359	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
19	13, 18	syldan 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
20	9, 19	ifclda 4120	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
21		ovolun.h	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
22	20, 21	fmptd 6385	. . . . 5 ⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
23		eqid 2622	. . . . . 6 ⊢ ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
24		ovolun.u	. . . . . 6 ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
25	23, 24	ovolsf 23241	. . . . 5 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
26	22, 25	syl 17	. . . 4 ⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞))
27		rge0ssre 12280	. . . 4 ⊢ (0[,)+∞) ⊆ ℝ
28		fss 6056	. . . 4 ⊢ ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
29	26, 27, 28	sylancl 694	. . 3 ⊢ (𝜑 → 𝑈:ℕ⟶ℝ)
30	29	ffvelrnda 6359	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ∈ ℝ)
31		2nn 11185	. . . 4 ⊢ 2 ∈ ℕ
32		peano2nn 11032	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
33	32	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
34	33	nnred 11035	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
35	34	rehalfcld 11279	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ)
36	35	flcld 12599	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℤ)
37		ax-1cn 9994	. . . . . . . . 9 ⊢ 1 ∈ ℂ
38	37	2timesi 11147	. . . . . . . 8 ⊢ (2 · 1) = (1 + 1)
39		nnge1 11046	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ≤ 𝑘)
40	39	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
41		nnre 11027	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
42	41	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
43		1re 10039	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
44		leadd1 10496	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
45	43, 43, 44	mp3an13 1415	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℝ → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
46	42, 45	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
47	40, 46	mpbid 222	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 + 1) ≤ (𝑘 + 1))
48	38, 47	syl5eqbr 4688	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 1) ≤ (𝑘 + 1))
49		2re 11090	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
50		2pos 11112	. . . . . . . . . 10 ⊢ 0 < 2
51	49, 50	pm3.2i 471	. . . . . . . . 9 ⊢ (2 ∈ ℝ ∧ 0 < 2)
52		lemuldiv2 10904	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
53	43, 51, 52	mp3an13 1415	. . . . . . . 8 ⊢ ((𝑘 + 1) ∈ ℝ → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
54	34, 53	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
55	48, 54	mpbid 222	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ ((𝑘 + 1) / 2))
56		1z 11407	. . . . . . 7 ⊢ 1 ∈ ℤ
57		flge 12606	. . . . . . 7 ⊢ ((((𝑘 + 1) / 2) ∈ ℝ ∧ 1 ∈ ℤ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
58	35, 56, 57	sylancl 694	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
59	55, 58	mpbid 222	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ (⌊‘((𝑘 + 1) / 2)))
60		elnnz1 11403	. . . . 5 ⊢ ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
61	36, 59, 60	sylanbrc 698	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
62		nnmulcl 11043	. . . 4 ⊢ ((2 ∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
63	31, 61, 62	sylancr 695	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
64	29	ffvelrnda 6359	. . 3 ⊢ ((𝜑 ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
65	63, 64	syldan 487	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
66		ovolun.a	. . . . . 6 ⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
67	66	simprd 479	. . . . 5 ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)
68		ovolun.b	. . . . . 6 ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
69	68	simprd 479	. . . . 5 ⊢ (𝜑 → (vol*‘𝐵) ∈ ℝ)
70	67, 69	readdcld 10069	. . . 4 ⊢ (𝜑 → ((vol‘𝐴) + (vol‘𝐵)) ∈ ℝ)
71		ovolun.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
72	71	rpred 11872	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
73	70, 72	readdcld 10069	. . 3 ⊢ (𝜑 → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) ∈ ℝ)
74	73	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) ∈ ℝ)
75		simpr 477	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
76		nnuz 11723	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
77	75, 76	syl6eleq 2711	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
78		nnz 11399	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
79	78	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
80		flhalf 12631	. . . . . 6 ⊢ (𝑘 ∈ ℤ → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
81	79, 80	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
82		nnz 11399	. . . . . . 7 ⊢ ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ)
83		eluz 11701	. . . . . . 7 ⊢ ((𝑘 ∈ ℤ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
84	78, 82, 83	syl2an 494	. . . . . 6 ⊢ ((𝑘 ∈ ℕ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
85	75, 63, 84	syl2anc 693	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
86	81, 85	mpbird 247	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ_≥‘𝑘))
87		elfznn 12370	. . . . 5 ⊢ (𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ ℕ)
88	23	ovolfsf 23240	. . . . . . . . . 10 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
89	22, 88	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
90	89	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
91	90	ffvelrnda 6359	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞))
92		elrege0 12278	. . . . . . 7 ⊢ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
93	91, 92	sylib 208	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
94	93	simpld 475	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
95	87, 94	sylan2 491	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2))))) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
96		elfzuz 12338	. . . . . 6 ⊢ (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ (ℤ_≥‘(𝑘 + 1)))
97		eluznn 11758	. . . . . 6 ⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
98	33, 96, 97	syl2an 494	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 𝑗 ∈ ℕ)
99	93	simprd 479	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
100	98, 99	syldan 487	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
101	77, 86, 95, 100	sermono 12833	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))))
102	24	fveq1i 6192	. . 3 ⊢ (𝑈‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘)
103	24	fveq1i 6192	. . 3 ⊢ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2))))
104	101, 102, 103	3brtr4g 4687	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
105		eqid 2622	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
106		ovolun.s	. . . . . . . . . 10 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
107	105, 106	ovolsf 23241	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
108	16, 107	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
109		frn 6053	. . . . . . . 8 ⊢ (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
110	108, 109	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
111	110, 27	syl6ss 3615	. . . . . 6 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
112	111	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ)
113		ffn 6045	. . . . . . . 8 ⊢ (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
114	108, 113	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆 Fn ℕ)
115	114	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑆 Fn ℕ)
116		fnfvelrn 6356	. . . . . 6 ⊢ ((𝑆 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
117	115, 61, 116	syl2anc 693	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
118	112, 117	sseldd 3604	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
119		eqid 2622	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
120		ovolun.t	. . . . . . . . . 10 ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
121	119, 120	ovolsf 23241	. . . . . . . . 9 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
122	7, 121	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
123		frn 6053	. . . . . . . 8 ⊢ (𝑇:ℕ⟶(0[,)+∞) → ran 𝑇 ⊆ (0[,)+∞))
124	122, 123	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
125	124, 27	syl6ss 3615	. . . . . 6 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ)
126	125	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ)
127		ffn 6045	. . . . . . . 8 ⊢ (𝑇:ℕ⟶(0[,)+∞) → 𝑇 Fn ℕ)
128	122, 127	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑇 Fn ℕ)
129	128	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 Fn ℕ)
130		fnfvelrn 6356	. . . . . 6 ⊢ ((𝑇 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
131	129, 61, 130	syl2anc 693	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
132	126, 131	sseldd 3604	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
133	72	rehalfcld 11279	. . . . . 6 ⊢ (𝜑 → (𝐶 / 2) ∈ ℝ)
134	67, 133	readdcld 10069	. . . . 5 ⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
135	134	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
136	69, 133	readdcld 10069	. . . . 5 ⊢ (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
137	136	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
138		ressxr 10083	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ^*
139	111, 138	syl6ss 3615	. . . . . . . 8 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ^*)
140		supxrcl 12145	. . . . . . . 8 ⊢ (ran 𝑆 ⊆ ℝ^* → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
141	139, 140	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
142		1nn 11031	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
143		fdm 6051	. . . . . . . . . . . 12 ⊢ (𝑆:ℕ⟶(0[,)+∞) → dom 𝑆 = ℕ)
144	108, 143	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑆 = ℕ)
145	142, 144	syl5eleqr 2708	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ dom 𝑆)
146		ne0i 3921	. . . . . . . . . 10 ⊢ (1 ∈ dom 𝑆 → dom 𝑆 ≠ ∅)
147	145, 146	syl 17	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑆 ≠ ∅)
148		dm0rn0 5342	. . . . . . . . . 10 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
149	148	necon3bii 2846	. . . . . . . . 9 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
150	147, 149	sylib 208	. . . . . . . 8 ⊢ (𝜑 → ran 𝑆 ≠ ∅)
151		supxrgtmnf 12159	. . . . . . . 8 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → -∞ < sup(ran 𝑆, ℝ^*, < ))
152	111, 150, 151	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → -∞ < sup(ran 𝑆, ℝ^*, < ))
153		ovolun.f3	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
154		xrre 12000	. . . . . . 7 ⊢ (((sup(ran 𝑆, ℝ^, < ) ∈ ℝ^ ∧ ((vol‘𝐴) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ^, < ) ∧ sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))) → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
155	141, 134, 152, 153, 154	syl22anc 1327	. . . . . 6 ⊢ (𝜑 → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
156	155	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
157	139	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ^*)
158		supxrub 12154	. . . . . 6 ⊢ ((ran 𝑆 ⊆ ℝ^* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ^*, < ))
159	157, 117, 158	syl2anc 693	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ^*, < ))
160	153	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ^, < ) ≤ ((vol‘𝐴) + (𝐶 / 2)))
161	118, 156, 135, 159, 160	letrd 10194	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
162	125, 138	syl6ss 3615	. . . . . . . 8 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ^*)
163		supxrcl 12145	. . . . . . . 8 ⊢ (ran 𝑇 ⊆ ℝ^* → sup(ran 𝑇, ℝ^, < ) ∈ ℝ^)
164	162, 163	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ∈ ℝ^)
165		fdm 6051	. . . . . . . . . . . 12 ⊢ (𝑇:ℕ⟶(0[,)+∞) → dom 𝑇 = ℕ)
166	122, 165	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑇 = ℕ)
167	142, 166	syl5eleqr 2708	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ dom 𝑇)
168		ne0i 3921	. . . . . . . . . 10 ⊢ (1 ∈ dom 𝑇 → dom 𝑇 ≠ ∅)
169	167, 168	syl 17	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑇 ≠ ∅)
170		dm0rn0 5342	. . . . . . . . . 10 ⊢ (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
171	170	necon3bii 2846	. . . . . . . . 9 ⊢ (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
172	169, 171	sylib 208	. . . . . . . 8 ⊢ (𝜑 → ran 𝑇 ≠ ∅)
173		supxrgtmnf 12159	. . . . . . . 8 ⊢ ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅) → -∞ < sup(ran 𝑇, ℝ^*, < ))
174	125, 172, 173	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → -∞ < sup(ran 𝑇, ℝ^*, < ))
175		ovolun.g3	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
176		xrre 12000	. . . . . . 7 ⊢ (((sup(ran 𝑇, ℝ^, < ) ∈ ℝ^ ∧ ((vol‘𝐵) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑇, ℝ^, < ) ∧ sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
177	164, 136, 174, 175, 176	syl22anc 1327	. . . . . 6 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
178	177	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
179	162	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ^*)
180		supxrub 12154	. . . . . 6 ⊢ ((ran 𝑇 ⊆ ℝ^* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ^*, < ))
181	179, 131, 180	syl2anc 693	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ^*, < ))
182	175	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐵) + (𝐶 / 2)))
183	132, 178, 137, 181, 182	letrd 10194	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
184	118, 132, 135, 137, 161, 183	le2addd 10646	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))))
185		oveq2 6658	. . . . . . . . 9 ⊢ (𝑧 = 1 → (2 · 𝑧) = (2 · 1))
186	185	fveq2d 6195	. . . . . . . 8 ⊢ (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1)))
187		fveq2 6191	. . . . . . . . 9 ⊢ (𝑧 = 1 → (𝑆‘𝑧) = (𝑆‘1))
188		fveq2 6191	. . . . . . . . 9 ⊢ (𝑧 = 1 → (𝑇‘𝑧) = (𝑇‘1))
189	187, 188	oveq12d 6668	. . . . . . . 8 ⊢ (𝑧 = 1 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘1) + (𝑇‘1)))
190	186, 189	eqeq12d 2637	. . . . . . 7 ⊢ (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))
191	190	imbi2d 330	. . . . . 6 ⊢ (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))))
192		oveq2 6658	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘))
193	192	fveq2d 6195	. . . . . . . 8 ⊢ (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘)))
194		fveq2 6191	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (𝑆‘𝑧) = (𝑆‘𝑘))
195		fveq2 6191	. . . . . . . . 9 ⊢ (𝑧 = 𝑘 → (𝑇‘𝑧) = (𝑇‘𝑘))
196	194, 195	oveq12d 6668	. . . . . . . 8 ⊢ (𝑧 = 𝑘 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))
197	193, 196	eqeq12d 2637	. . . . . . 7 ⊢ (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))))
198	197	imbi2d 330	. . . . . 6 ⊢ (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))))
199		oveq2 6658	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1)))
200	199	fveq2d 6195	. . . . . . . 8 ⊢ (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1))))
201		fveq2 6191	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (𝑆‘𝑧) = (𝑆‘(𝑘 + 1)))
202		fveq2 6191	. . . . . . . . 9 ⊢ (𝑧 = (𝑘 + 1) → (𝑇‘𝑧) = (𝑇‘(𝑘 + 1)))
203	201, 202	oveq12d 6668	. . . . . . . 8 ⊢ (𝑧 = (𝑘 + 1) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))
204	200, 203	eqeq12d 2637	. . . . . . 7 ⊢ (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
205	204	imbi2d 330	. . . . . 6 ⊢ (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
206		oveq2 6658	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 · 𝑧) = (2 · (⌊‘((𝑘 + 1) / 2))))
207	206	fveq2d 6195	. . . . . . . 8 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
208		fveq2 6191	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆‘𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2))))
209		fveq2 6191	. . . . . . . . 9 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇‘𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2))))
210	208, 209	oveq12d 6668	. . . . . . . 8 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
211	207, 210	eqeq12d 2637	. . . . . . 7 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
212	211	imbi2d 330	. . . . . 6 ⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))))
213	24	fveq1i 6192	. . . . . . . 8 ⊢ (𝑈‘(2 · 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1))
214	23	ovolfsval 23239	. . . . . . . . . . . 12 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))))
215	22, 142, 214	sylancl 694	. . . . . . . . . . 11 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))))
216		halfnz 11455	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ (1 / 2) ∈ ℤ
217		nnz 11399	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 / 2) ∈ ℕ → (𝑛 / 2) ∈ ℤ)
218		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 / 2) = (1 / 2))
219	218	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → ((𝑛 / 2) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
220	217, 219	syl5ib 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → ((𝑛 / 2) ∈ ℕ → (1 / 2) ∈ ℤ))
221	216, 220	mtoi 190	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → ¬ (𝑛 / 2) ∈ ℕ)
222	221	iffalsed 4097	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2)))
223		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
224		df-2 11079	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
225	223, 224	syl6eqr 2674	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑛 + 1) = 2)
226	225	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2))
227		2div2e1 11150	. . . . . . . . . . . . . . . . . 18 ⊢ (2 / 2) = 1
228	226, 227	syl6eq 2672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = 1)
229	228	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1))
230	222, 229	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1))
231		fvex 6201	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘1) ∈ V
232	230, 21, 231	fvmpt 6282	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → (𝐻‘1) = (𝐹‘1))
233	142, 232	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐻‘1) = (𝐹‘1)
234	233	fveq2i 6194	. . . . . . . . . . . 12 ⊢ (2^nd ‘(𝐻‘1)) = (2^nd ‘(𝐹‘1))
235	233	fveq2i 6194	. . . . . . . . . . . 12 ⊢ (1^st ‘(𝐻‘1)) = (1^st ‘(𝐹‘1))
236	234, 235	oveq12i 6662	. . . . . . . . . . 11 ⊢ ((2^nd ‘(𝐻‘1)) − (1^st ‘(𝐻‘1))) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1)))
237	215, 236	syl6eq 2672	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
238	56, 237	seq1i 12815	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
239		2t1e2 11176	. . . . . . . . . . 11 ⊢ (2 · 1) = 2
240	239	fveq2i 6194	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘ − ) ∘ 𝐻)‘2)
241	23	ovolfsval 23239	. . . . . . . . . . . 12 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 2 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))))
242	22, 31, 241	sylancl 694	. . . . . . . . . . 11 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))))
243		oveq1 6657	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 2 → (𝑛 / 2) = (2 / 2))
244	243, 227	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 2 → (𝑛 / 2) = 1)
245	244, 142	syl6eqel 2709	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 2 → (𝑛 / 2) ∈ ℕ)
246	245	iftrued 4094	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2)))
247	244	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1))
248	246, 247	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1))
249		fvex 6201	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘1) ∈ V
250	248, 21, 249	fvmpt 6282	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℕ → (𝐻‘2) = (𝐺‘1))
251	31, 250	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐻‘2) = (𝐺‘1)
252	251	fveq2i 6194	. . . . . . . . . . . 12 ⊢ (2^nd ‘(𝐻‘2)) = (2^nd ‘(𝐺‘1))
253	251	fveq2i 6194	. . . . . . . . . . . 12 ⊢ (1^st ‘(𝐻‘2)) = (1^st ‘(𝐺‘1))
254	252, 253	oveq12i 6662	. . . . . . . . . . 11 ⊢ ((2^nd ‘(𝐻‘2)) − (1^st ‘(𝐻‘2))) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))
255	242, 254	syl6eq 2672	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
256	240, 255	syl5eq 2668	. . . . . . . . 9 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
257	76, 142, 38, 238, 256	seqp1i 12817	. . . . . . . 8 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
258	213, 257	syl5eq 2668	. . . . . . 7 ⊢ (𝜑 → (𝑈‘(2 · 1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
259	106	fveq1i 6192	. . . . . . . . 9 ⊢ (𝑆‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1)
260	105	ovolfsval 23239	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
261	16, 142, 260	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
262	56, 261	seq1i 12815	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
263	259, 262	syl5eq 2668	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘1) = ((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))))
264	120	fveq1i 6192	. . . . . . . . 9 ⊢ (𝑇‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1)
265	119	ovolfsval 23239	. . . . . . . . . . 11 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
266	7, 142, 265	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
267	56, 266	seq1i 12815	. . . . . . . . 9 ⊢ (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
268	264, 267	syl5eq 2668	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘1) = ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1))))
269	263, 268	oveq12d 6668	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2^nd ‘(𝐹‘1)) − (1^st ‘(𝐹‘1))) + ((2^nd ‘(𝐺‘1)) − (1^st ‘(𝐺‘1)))))
270	258, 269	eqtr4d 2659	. . . . . 6 ⊢ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))
271		oveq1 6657	. . . . . . . . 9 ⊢ ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
272	38	oveq2i 6661	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
273		2cnd 11093	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
274	42	recnd 10068	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
275		1cnd 10056	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
276	273, 274, 275	adddid 10064	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
277		nnmulcl 11043	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
278	31, 277	mpan 706	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
279	278	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
280	279	nncnd 11036	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
281	280, 275, 275	addassd 10062	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
282	272, 276, 281	3eqtr4a 2682	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1))
283	282	fveq2d 6195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1)))
284	24	fveq1i 6192	. . . . . . . . . . . 12 ⊢ (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1))
285	279	peano2nnd 11037	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
286	285, 76	syl6eleq 2711	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ (ℤ_≥‘1))
287		seqp1 12816	. . . . . . . . . . . . . 14 ⊢ (((2 · 𝑘) + 1) ∈ (ℤ_≥‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))))
288	286, 287	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))))
289	279, 76	syl6eleq 2711	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ (ℤ_≥‘1))
290		seqp1 12816	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑘) ∈ (ℤ_≥‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
291	289, 290	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
292	24	fveq1i 6192	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘))
293	292	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)))
294		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2))
295	294	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
296	294	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2)))
297		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1))
298	297	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 + 1) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
299	298	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
300	295, 296, 299	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
301		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈ V
302		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈ V
303	301, 302	ifex 4156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V
304	300, 21, 303	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 · 𝑘) + 1) ∈ ℕ → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
305	285, 304	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
306		2ne0 11113	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ≠ 0
307	306	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ≠ 0)
308	274, 273, 307	divcan3d 10806	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘)
309	308, 75	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈ ℕ)
310		nneo 11461	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 · 𝑘) ∈ ℕ → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
311	279, 310	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
312	309, 311	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ)
313	312	iffalsed 4097	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
314	282	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
315	33	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
316		2cn 11091	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℂ
317		divcan3 10711	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
318	316, 306, 317	mp3an23 1416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 + 1) ∈ ℂ → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
319	315, 318	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
320	314, 319	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1))
321	320	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1)))
322	305, 313, 321	3eqtrd 2660	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1)))
323	322	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐻‘((2 · 𝑘) + 1))) = (2^nd ‘(𝐹‘(𝑘 + 1))))
324	322	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐻‘((2 · 𝑘) + 1))) = (1^st ‘(𝐹‘(𝑘 + 1))))
325	323, 324	oveq12d 6668	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2^nd ‘(𝐹‘(𝑘 + 1))) − (1^st ‘(𝐹‘(𝑘 + 1)))))
326	22	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
327	23	ovolfsval 23239	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))))
328	326, 285, 327	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2^nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1^st ‘(𝐻‘((2 · 𝑘) + 1)))))
329	105	ovolfsval 23239	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2^nd ‘(𝐹‘(𝑘 + 1))) − (1^st ‘(𝐹‘(𝑘 + 1)))))
330	16, 32, 329	syl2an 494	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2^nd ‘(𝐹‘(𝑘 + 1))) − (1^st ‘(𝐹‘(𝑘 + 1)))))
331	325, 328, 330	3eqtr4rd 2667	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))
332	293, 331	oveq12d 6668	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
333	291, 332	eqtr4d 2659	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
334	282	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1)))
335	285	peano2nnd 11037	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈ ℕ)
336	282, 335	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈ ℕ)
337		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2))
338	337	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · (𝑘 + 1)) / 2) ∈ ℕ))
339	337	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
340		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1))
341	340	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 + 1) / 2) = (((2 · (𝑘 + 1)) + 1) / 2))
342	341	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))
343	338, 339, 342	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
344		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈ V
345		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈ V
346	344, 345	ifex 4156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V
347	343, 21, 346	fvmpt 6282	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · (𝑘 + 1)) ∈ ℕ → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
348	336, 347	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
349	319, 33	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈ ℕ)
350	349	iftrued 4094	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
351	319	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1)))
352	348, 350, 351	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1)))
353	334, 352	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1)))
354	353	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (2^nd ‘(𝐺‘(𝑘 + 1))))
355	353	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (1^st ‘(𝐺‘(𝑘 + 1))))
356	354, 355	oveq12d 6668	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2^nd ‘(𝐺‘(𝑘 + 1))) − (1^st ‘(𝐺‘(𝑘 + 1)))))
357	23	ovolfsval 23239	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
358	326, 335, 357	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2^nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1^st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
359	119	ovolfsval 23239	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2^nd ‘(𝐺‘(𝑘 + 1))) − (1^st ‘(𝐺‘(𝑘 + 1)))))
360	7, 32, 359	syl2an 494	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2^nd ‘(𝐺‘(𝑘 + 1))) − (1^st ‘(𝐺‘(𝑘 + 1)))))
361	356, 358, 360	3eqtr4d 2666	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
362	333, 361	oveq12d 6668	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
363	288, 362	eqtrd 2656	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
364	284, 363	syl5eq 2668	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
365		ffvelrn 6357	. . . . . . . . . . . . . . 15 ⊢ ((𝑈:ℕ⟶(0[,)+∞) ∧ (2 · 𝑘) ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
366	26, 278, 365	syl2an 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
367	27, 366	sseldi 3601	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ)
368	367	recnd 10068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ)
369	105	ovolfsf 23240	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
370	16, 369	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
371		ffvelrn 6357	. . . . . . . . . . . . . . 15 ⊢ ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
372	370, 32, 371	syl2an 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
373	27, 372	sseldi 3601	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ)
374	373	recnd 10068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ)
375	119	ovolfsf 23240	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
376	7, 375	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
377		ffvelrn 6357	. . . . . . . . . . . . . . 15 ⊢ ((((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
378	376, 32, 377	syl2an 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
379	27, 378	sseldi 3601	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ)
380	379	recnd 10068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ)
381	368, 374, 380	addassd 10062	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
382	283, 364, 381	3eqtrd 2660	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
383		seqp1 12816	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
384	77, 383	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
385	106	fveq1i 6192	. . . . . . . . . . . . 13 ⊢ (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1))
386	106	fveq1i 6192	. . . . . . . . . . . . . 14 ⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
387	386	oveq1i 6660	. . . . . . . . . . . . 13 ⊢ ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))
388	384, 385, 387	3eqtr4g 2681	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
389		seqp1 12816	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
390	77, 389	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
391	120	fveq1i 6192	. . . . . . . . . . . . 13 ⊢ (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1))
392	120	fveq1i 6192	. . . . . . . . . . . . . 14 ⊢ (𝑇‘𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
393	392	oveq1i 6660	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
394	390, 391, 393	3eqtr4g 2681	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
395	388, 394	oveq12d 6668	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
396	108	ffvelrnda 6359	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ (0[,)+∞))
397	27, 396	sseldi 3601	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ)
398	397	recnd 10068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℂ)
399	122	ffvelrnda 6359	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ (0[,)+∞))
400	27, 399	sseldi 3601	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℝ)
401	400	recnd 10068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℂ)
402	398, 374, 401, 380	add4d 10264	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
403	395, 402	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
404	382, 403	eqeq12d 2637	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) ↔ ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))))
405	271, 404	syl5ibr 236	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
406	405	expcom 451	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝜑 → ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
407	406	a2d 29	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))) → (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
408	191, 198, 205, 212, 270, 407	nnind 11038	. . . . 5 ⊢ ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ → (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
409	408	impcom 446	. . . 4 ⊢ ((𝜑 ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
410	61, 409	syldan 487	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
411	67	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
412	411	recnd 10068	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℂ)
413	72	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℝ)
414	413	rehalfcld 11279	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ)
415	414	recnd 10068	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ)
416	69	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℝ)
417	416	recnd 10068	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℂ)
418	412, 415, 417, 415	add4d 10264	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))) = (((vol‘𝐴) + (vol‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))))
419	413	recnd 10068	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
420	419	2halvesd 11278	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
421	420	oveq2d 6666	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))
422	418, 421	eqtr2d 2657	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol‘𝐴) + (vol‘𝐵)) + 𝐶) = (((vol‘𝐴) + (𝐶 / 2)) + ((vol‘𝐵) + (𝐶 / 2))))
423	184, 410, 422	3brtr4d 4685	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))
424	30, 65, 74, 104, 423	letrd 10194	1 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol‘𝐴) + (vol‘𝐵)) + 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 ifcif 4086 ∪ cuni 4436 class class class wbr 4653 ↦ cmpt 4729 × cxp 5112 dom cdm 5114 ran crn 5115 ∘ ccom 5118 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 1^st c1st 7166 2^nd c2nd 7167 ↑_𝑚 cmap 7857 supcsup 8346 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 +∞cpnf 10071 -∞cmnf 10072 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 ℕcn 11020 2c2 11070 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 (,)cioo 12175 [,)cico 12177 ...cfz 12326 ⌊cfl 12591 seqcseq 12801 abscabs 13974 vol*covol 23231

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-ico 12181 df-fz 12327 df-fl 12593 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976

This theorem is referenced by: ovolunlem1 23265

W3C validator