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

Theorem ovolunlem1a 23071
 Description: Lemma for ovolun 23074. (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.
StepHypRef Expression
1 ovolun.g1 . . . . . . . . . 10 (𝜑𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
2 reex 9906 . . . . . . . . . . . . 13 ℝ ∈ V
32, 2xpex 6860 . . . . . . . . . . . 12 (ℝ × ℝ) ∈ V
43inex2 4728 . . . . . . . . . . 11 ( ≤ ∩ (ℝ × ℝ)) ∈ V
5 nnex 10903 . . . . . . . . . . 11 ℕ ∈ V
64, 5elmap 7772 . . . . . . . . . 10 (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
71, 6sylib 207 . . . . . . . . 9 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
87adantr 480 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
98ffvelrnda 6267 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
10 nneo 11337 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
1110adantl 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
1211con2bid 343 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈ ℕ))
1312biimpar 501 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → ((𝑛 + 1) / 2) ∈ ℕ)
14 ovolun.f1 . . . . . . . . . . 11 (𝜑𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
154, 5elmap 7772 . . . . . . . . . . 11 (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1614, 15sylib 207 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1716adantr 480 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1817ffvelrnda 6267 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
1913, 18syldan 486 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
209, 19ifclda 4070 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
21 ovolun.h . . . . . 6 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
2220, 21fmptd 6292 . . . . 5 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
23 eqid 2610 . . . . . 6 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
24 ovolun.u . . . . . 6 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
2523, 24ovolsf 23048 . . . . 5 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
2622, 25syl 17 . . . 4 (𝜑𝑈:ℕ⟶(0[,)+∞))
27 rge0ssre 12151 . . . 4 (0[,)+∞) ⊆ ℝ
28 fss 5969 . . . 4 ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
2926, 27, 28sylancl 693 . . 3 (𝜑𝑈:ℕ⟶ℝ)
3029ffvelrnda 6267 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ∈ ℝ)
31 2nn 11062 . . . 4 2 ∈ ℕ
32 peano2nn 10909 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
3332adantl 481 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
3433nnred 10912 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
3534rehalfcld 11156 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ)
3635flcld 12461 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℤ)
37 ax-1cn 9873 . . . . . . . . 9 1 ∈ ℂ
38372timesi 11024 . . . . . . . 8 (2 · 1) = (1 + 1)
39 nnge1 10923 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
4039adantl 481 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 1 ≤ 𝑘)
41 nnre 10904 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
4241adantl 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
43 1re 9918 . . . . . . . . . . 11 1 ∈ ℝ
44 leadd1 10375 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4543, 43, 44mp3an13 1407 . . . . . . . . . 10 (𝑘 ∈ ℝ → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4642, 45syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4740, 46mpbid 221 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (1 + 1) ≤ (𝑘 + 1))
4838, 47syl5eqbr 4618 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (2 · 1) ≤ (𝑘 + 1))
49 2re 10967 . . . . . . . . . 10 2 ∈ ℝ
50 2pos 10989 . . . . . . . . . 10 0 < 2
5149, 50pm3.2i 470 . . . . . . . . 9 (2 ∈ ℝ ∧ 0 < 2)
52 lemuldiv2 10783 . . . . . . . . 9 ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5343, 51, 52mp3an13 1407 . . . . . . . 8 ((𝑘 + 1) ∈ ℝ → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5434, 53syl 17 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5548, 54mpbid 221 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 1 ≤ ((𝑘 + 1) / 2))
56 1z 11284 . . . . . . 7 1 ∈ ℤ
57 flge 12468 . . . . . . 7 ((((𝑘 + 1) / 2) ∈ ℝ ∧ 1 ∈ ℤ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5835, 56, 57sylancl 693 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5955, 58mpbid 221 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 1 ≤ (⌊‘((𝑘 + 1) / 2)))
60 elnnz1 11280 . . . . 5 ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
6136, 59, 60sylanbrc 695 . . . 4 ((𝜑𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
62 nnmulcl 10920 . . . 4 ((2 ∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
6331, 61, 62sylancr 694 . . 3 ((𝜑𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
6429ffvelrnda 6267 . . 3 ((𝜑 ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
6563, 64syldan 486 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
66 ovolun.a . . . . . 6 (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
6766simprd 478 . . . . 5 (𝜑 → (vol*‘𝐴) ∈ ℝ)
68 ovolun.b . . . . . 6 (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
6968simprd 478 . . . . 5 (𝜑 → (vol*‘𝐵) ∈ ℝ)
7067, 69readdcld 9948 . . . 4 (𝜑 → ((vol*‘𝐴) + (vol*‘𝐵)) ∈ ℝ)
71 ovolun.c . . . . 5 (𝜑𝐶 ∈ ℝ+)
7271rpred 11748 . . . 4 (𝜑𝐶 ∈ ℝ)
7370, 72readdcld 9948 . . 3 (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
7473adantr 480 . 2 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
75 simpr 476 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
76 nnuz 11599 . . . . 5 ℕ = (ℤ‘1)
7775, 76syl6eleq 2698 . . . 4 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
78 nnz 11276 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
7978adantl 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
80 flhalf 12493 . . . . . 6 (𝑘 ∈ ℤ → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
8179, 80syl 17 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
82 nnz 11276 . . . . . . 7 ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ)
83 eluz 11577 . . . . . . 7 ((𝑘 ∈ ℤ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8478, 82, 83syl2an 493 . . . . . 6 ((𝑘 ∈ ℕ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8575, 63, 84syl2anc 691 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8681, 85mpbird 246 . . . 4 ((𝜑𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘))
87 elfznn 12241 . . . . 5 (𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ ℕ)
8823ovolfsf 23047 . . . . . . . . . 10 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8922, 88syl 17 . . . . . . . . 9 (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
9089adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
9190ffvelrnda 6267 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞))
92 elrege0 12149 . . . . . . 7 ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
9391, 92sylib 207 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
9493simpld 474 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
9587, 94sylan2 490 . . . 4 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2))))) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
96 elfzuz 12209 . . . . . 6 (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ (ℤ‘(𝑘 + 1)))
97 eluznn 11634 . . . . . 6 (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
9833, 96, 97syl2an 493 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 𝑗 ∈ ℕ)
9993simprd 478 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
10098, 99syldan 486 . . . 4 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
10177, 86, 95, 100sermono 12695 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))))
10224fveq1i 6104 . . 3 (𝑈𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘)
10324fveq1i 6104 . . 3 (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2))))
104101, 102, 1033brtr4g 4617 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
105 eqid 2610 . . . . . . . . . 10 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
106 ovolun.s . . . . . . . . . 10 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
107105, 106ovolsf 23048 . . . . . . . . 9 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
10816, 107syl 17 . . . . . . . 8 (𝜑𝑆:ℕ⟶(0[,)+∞))
109 frn 5966 . . . . . . . 8 (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
110108, 109syl 17 . . . . . . 7 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
111110, 27syl6ss 3580 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
112111adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ)
113 ffn 5958 . . . . . . . 8 (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
114108, 113syl 17 . . . . . . 7 (𝜑𝑆 Fn ℕ)
115114adantr 480 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑆 Fn ℕ)
116 fnfvelrn 6264 . . . . . 6 ((𝑆 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
117115, 61, 116syl2anc 691 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
118112, 117sseldd 3569 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
119 eqid 2610 . . . . . . . . . 10 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
120 ovolun.t . . . . . . . . . 10 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
121119, 120ovolsf 23048 . . . . . . . . 9 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
1227, 121syl 17 . . . . . . . 8 (𝜑𝑇:ℕ⟶(0[,)+∞))
123 frn 5966 . . . . . . . 8 (𝑇:ℕ⟶(0[,)+∞) → ran 𝑇 ⊆ (0[,)+∞))
124122, 123syl 17 . . . . . . 7 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
125124, 27syl6ss 3580 . . . . . 6 (𝜑 → ran 𝑇 ⊆ ℝ)
126125adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ)
127 ffn 5958 . . . . . . . 8 (𝑇:ℕ⟶(0[,)+∞) → 𝑇 Fn ℕ)
128122, 127syl 17 . . . . . . 7 (𝜑𝑇 Fn ℕ)
129128adantr 480 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑇 Fn ℕ)
130 fnfvelrn 6264 . . . . . 6 ((𝑇 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
131129, 61, 130syl2anc 691 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
132126, 131sseldd 3569 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
13372rehalfcld 11156 . . . . . 6 (𝜑 → (𝐶 / 2) ∈ ℝ)
13467, 133readdcld 9948 . . . . 5 (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
135134adantr 480 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
13669, 133readdcld 9948 . . . . 5 (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
137136adantr 480 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
138 ressxr 9962 . . . . . . . . 9 ℝ ⊆ ℝ*
139111, 138syl6ss 3580 . . . . . . . 8 (𝜑 → ran 𝑆 ⊆ ℝ*)
140 supxrcl 12017 . . . . . . . 8 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
141139, 140syl 17 . . . . . . 7 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
142 1nn 10908 . . . . . . . . . . 11 1 ∈ ℕ
143 fdm 5964 . . . . . . . . . . . 12 (𝑆:ℕ⟶(0[,)+∞) → dom 𝑆 = ℕ)
144108, 143syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝑆 = ℕ)
145142, 144syl5eleqr 2695 . . . . . . . . . 10 (𝜑 → 1 ∈ dom 𝑆)
146 ne0i 3880 . . . . . . . . . 10 (1 ∈ dom 𝑆 → dom 𝑆 ≠ ∅)
147145, 146syl 17 . . . . . . . . 9 (𝜑 → dom 𝑆 ≠ ∅)
148 dm0rn0 5263 . . . . . . . . . 10 (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
149148necon3bii 2834 . . . . . . . . 9 (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
150147, 149sylib 207 . . . . . . . 8 (𝜑 → ran 𝑆 ≠ ∅)
151 supxrgtmnf 12031 . . . . . . . 8 ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → -∞ < sup(ran 𝑆, ℝ*, < ))
152111, 150, 151syl2anc 691 . . . . . . 7 (𝜑 → -∞ < sup(ran 𝑆, ℝ*, < ))
153 ovolun.f3 . . . . . . 7 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
154 xrre 11874 . . . . . . 7 (((sup(ran 𝑆, ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
155141, 134, 152, 153, 154syl22anc 1319 . . . . . 6 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
156155adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
157139adantr 480 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
158 supxrub 12026 . . . . . 6 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, < ))
159157, 117, 158syl2anc 691 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, < ))
160153adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
161118, 156, 135, 159, 160letrd 10073 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
162125, 138syl6ss 3580 . . . . . . . 8 (𝜑 → ran 𝑇 ⊆ ℝ*)
163 supxrcl 12017 . . . . . . . 8 (ran 𝑇 ⊆ ℝ* → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
164162, 163syl 17 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
165 fdm 5964 . . . . . . . . . . . 12 (𝑇:ℕ⟶(0[,)+∞) → dom 𝑇 = ℕ)
166122, 165syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝑇 = ℕ)
167142, 166syl5eleqr 2695 . . . . . . . . . 10 (𝜑 → 1 ∈ dom 𝑇)
168 ne0i 3880 . . . . . . . . . 10 (1 ∈ dom 𝑇 → dom 𝑇 ≠ ∅)
169167, 168syl 17 . . . . . . . . 9 (𝜑 → dom 𝑇 ≠ ∅)
170 dm0rn0 5263 . . . . . . . . . 10 (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
171170necon3bii 2834 . . . . . . . . 9 (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
172169, 171sylib 207 . . . . . . . 8 (𝜑 → ran 𝑇 ≠ ∅)
173 supxrgtmnf 12031 . . . . . . . 8 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅) → -∞ < sup(ran 𝑇, ℝ*, < ))
174125, 172, 173syl2anc 691 . . . . . . 7 (𝜑 → -∞ < sup(ran 𝑇, ℝ*, < ))
175 ovolun.g3 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
176 xrre 11874 . . . . . . 7 (((sup(ran 𝑇, ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
177164, 136, 174, 175, 176syl22anc 1319 . . . . . 6 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
178177adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
179162adantr 480 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ*)
180 supxrub 12026 . . . . . 6 ((ran 𝑇 ⊆ ℝ* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, < ))
181179, 131, 180syl2anc 691 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, < ))
182175adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
183132, 178, 137, 181, 182letrd 10073 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
184118, 132, 135, 137, 161, 183le2addd 10525 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))))
185 oveq2 6557 . . . . . . . . 9 (𝑧 = 1 → (2 · 𝑧) = (2 · 1))
186185fveq2d 6107 . . . . . . . 8 (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1)))
187 fveq2 6103 . . . . . . . . 9 (𝑧 = 1 → (𝑆𝑧) = (𝑆‘1))
188 fveq2 6103 . . . . . . . . 9 (𝑧 = 1 → (𝑇𝑧) = (𝑇‘1))
189187, 188oveq12d 6567 . . . . . . . 8 (𝑧 = 1 → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘1) + (𝑇‘1)))
190186, 189eqeq12d 2625 . . . . . . 7 (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))
191190imbi2d 329 . . . . . 6 (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))))
192 oveq2 6557 . . . . . . . . 9 (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘))
193192fveq2d 6107 . . . . . . . 8 (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘)))
194 fveq2 6103 . . . . . . . . 9 (𝑧 = 𝑘 → (𝑆𝑧) = (𝑆𝑘))
195 fveq2 6103 . . . . . . . . 9 (𝑧 = 𝑘 → (𝑇𝑧) = (𝑇𝑘))
196194, 195oveq12d 6567 . . . . . . . 8 (𝑧 = 𝑘 → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆𝑘) + (𝑇𝑘)))
197193, 196eqeq12d 2625 . . . . . . 7 (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘))))
198197imbi2d 329 . . . . . 6 (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)))))
199 oveq2 6557 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1)))
200199fveq2d 6107 . . . . . . . 8 (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1))))
201 fveq2 6103 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (𝑆𝑧) = (𝑆‘(𝑘 + 1)))
202 fveq2 6103 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (𝑇𝑧) = (𝑇‘(𝑘 + 1)))
203201, 202oveq12d 6567 . . . . . . . 8 (𝑧 = (𝑘 + 1) → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))
204200, 203eqeq12d 2625 . . . . . . 7 (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
205204imbi2d 329 . . . . . 6 (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
206 oveq2 6557 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 · 𝑧) = (2 · (⌊‘((𝑘 + 1) / 2))))
207206fveq2d 6107 . . . . . . . 8 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
208 fveq2 6103 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2))))
209 fveq2 6103 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2))))
210208, 209oveq12d 6567 . . . . . . . 8 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
211207, 210eqeq12d 2625 . . . . . . 7 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
212211imbi2d 329 . . . . . 6 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))))
21324fveq1i 6104 . . . . . . . 8 (𝑈‘(2 · 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1))
21423ovolfsval 23046 . . . . . . . . . . . 12 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))))
21522, 142, 214sylancl 693 . . . . . . . . . . 11 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))))
216 halfnz 11331 . . . . . . . . . . . . . . . . . 18 ¬ (1 / 2) ∈ ℤ
217 nnz 11276 . . . . . . . . . . . . . . . . . . 19 ((𝑛 / 2) ∈ ℕ → (𝑛 / 2) ∈ ℤ)
218 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 / 2) = (1 / 2))
219218eleq1d 2672 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → ((𝑛 / 2) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
220217, 219syl5ib 233 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → ((𝑛 / 2) ∈ ℕ → (1 / 2) ∈ ℤ))
221216, 220mtoi 189 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ¬ (𝑛 / 2) ∈ ℕ)
222221iffalsed 4047 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2)))
223 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
224 df-2 10956 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
225223, 224syl6eqr 2662 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 + 1) = 2)
226225oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2))
227 2div2e1 11027 . . . . . . . . . . . . . . . . . 18 (2 / 2) = 1
228226, 227syl6eq 2660 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ((𝑛 + 1) / 2) = 1)
229228fveq2d 6107 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1))
230222, 229eqtrd 2644 . . . . . . . . . . . . . . 15 (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1))
231 fvex 6113 . . . . . . . . . . . . . . 15 (𝐹‘1) ∈ V
232230, 21, 231fvmpt 6191 . . . . . . . . . . . . . 14 (1 ∈ ℕ → (𝐻‘1) = (𝐹‘1))
233142, 232ax-mp 5 . . . . . . . . . . . . 13 (𝐻‘1) = (𝐹‘1)
234233fveq2i 6106 . . . . . . . . . . . 12 (2nd ‘(𝐻‘1)) = (2nd ‘(𝐹‘1))
235233fveq2i 6106 . . . . . . . . . . . 12 (1st ‘(𝐻‘1)) = (1st ‘(𝐹‘1))
236234, 235oveq12i 6561 . . . . . . . . . . 11 ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1)))
237215, 236syl6eq 2660 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
23856, 237seq1i 12677 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
239 2t1e2 11053 . . . . . . . . . . 11 (2 · 1) = 2
240239fveq2i 6106 . . . . . . . . . 10 (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘ − ) ∘ 𝐻)‘2)
24123ovolfsval 23046 . . . . . . . . . . . 12 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 2 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))))
24222, 31, 241sylancl 693 . . . . . . . . . . 11 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))))
243 oveq1 6556 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 2 → (𝑛 / 2) = (2 / 2))
244243, 227syl6eq 2660 . . . . . . . . . . . . . . . . . 18 (𝑛 = 2 → (𝑛 / 2) = 1)
245244, 142syl6eqel 2696 . . . . . . . . . . . . . . . . 17 (𝑛 = 2 → (𝑛 / 2) ∈ ℕ)
246245iftrued 4044 . . . . . . . . . . . . . . . 16 (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2)))
247244fveq2d 6107 . . . . . . . . . . . . . . . 16 (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1))
248246, 247eqtrd 2644 . . . . . . . . . . . . . . 15 (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1))
249 fvex 6113 . . . . . . . . . . . . . . 15 (𝐺‘1) ∈ V
250248, 21, 249fvmpt 6191 . . . . . . . . . . . . . 14 (2 ∈ ℕ → (𝐻‘2) = (𝐺‘1))
25131, 250ax-mp 5 . . . . . . . . . . . . 13 (𝐻‘2) = (𝐺‘1)
252251fveq2i 6106 . . . . . . . . . . . 12 (2nd ‘(𝐻‘2)) = (2nd ‘(𝐺‘1))
253251fveq2i 6106 . . . . . . . . . . . 12 (1st ‘(𝐻‘2)) = (1st ‘(𝐺‘1))
254252, 253oveq12i 6561 . . . . . . . . . . 11 ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))
255242, 254syl6eq 2660 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
256240, 255syl5eq 2656 . . . . . . . . 9 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
25776, 142, 38, 238, 256seqp1i 12679 . . . . . . . 8 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
258213, 257syl5eq 2656 . . . . . . 7 (𝜑 → (𝑈‘(2 · 1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
259106fveq1i 6104 . . . . . . . . 9 (𝑆‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1)
260105ovolfsval 23046 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
26116, 142, 260sylancl 693 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
26256, 261seq1i 12677 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
263259, 262syl5eq 2656 . . . . . . . 8 (𝜑 → (𝑆‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
264120fveq1i 6104 . . . . . . . . 9 (𝑇‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1)
265119ovolfsval 23046 . . . . . . . . . . 11 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
2667, 142, 265sylancl 693 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
26756, 266seq1i 12677 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
268264, 267syl5eq 2656 . . . . . . . 8 (𝜑 → (𝑇‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
269263, 268oveq12d 6567 . . . . . . 7 (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
270258, 269eqtr4d 2647 . . . . . 6 (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))
271 oveq1 6556 . . . . . . . . 9 ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
27238oveq2i 6560 . . . . . . . . . . . . 13 ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
273 2cnd 10970 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 2 ∈ ℂ)
27442recnd 9947 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
275 1cnd 9935 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 1 ∈ ℂ)
276273, 274, 275adddid 9943 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
277 nnmulcl 10920 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
27831, 277mpan 702 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
279278adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
280279nncnd 10913 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
281280, 275, 275addassd 9941 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
282272, 276, 2813eqtr4a 2670 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1))
283282fveq2d 6107 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1)))
28424fveq1i 6104 . . . . . . . . . . . 12 (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1))
285279peano2nnd 10914 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
286285, 76syl6eleq 2698 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ (ℤ‘1))
287 seqp1 12678 . . . . . . . . . . . . . 14 (((2 · 𝑘) + 1) ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))))
288286, 287syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))))
289279, 76syl6eleq 2698 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ (ℤ‘1))
290 seqp1 12678 . . . . . . . . . . . . . . . 16 ((2 · 𝑘) ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
291289, 290syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
29224fveq1i 6104 . . . . . . . . . . . . . . . . 17 (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘))
293292a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)))
294 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2))
295294eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
296294fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2)))
297 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1))
298297oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 + 1) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
299298fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
300295, 296, 299ifbieq12d 4063 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
301 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈ V
302 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈ V
303301, 302ifex 4106 . . . . . . . . . . . . . . . . . . . . . 22 if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V
304300, 21, 303fvmpt 6191 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑘) + 1) ∈ ℕ → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
305285, 304syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
306 2ne0 10990 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ≠ 0
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ) → 2 ≠ 0)
308274, 273, 307divcan3d 10685 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘)
309308, 75eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈ ℕ)
310 nneo 11337 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 · 𝑘) ∈ ℕ → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
311279, 310syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
312309, 311mpbid 221 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ)
313312iffalsed 4047 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
314282oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
31533nncnd 10913 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
316 2cn 10968 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℂ
317 divcan3 10590 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
318316, 306, 317mp3an23 1408 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 + 1) ∈ ℂ → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
319315, 318syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
320314, 319eqtr3d 2646 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1))
321320fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1)))
322305, 313, 3213eqtrd 2648 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1)))
323322fveq2d 6107 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐻‘((2 · 𝑘) + 1))) = (2nd ‘(𝐹‘(𝑘 + 1))))
324322fveq2d 6107 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐻‘((2 · 𝑘) + 1))) = (1st ‘(𝐹‘(𝑘 + 1))))
325323, 324oveq12d 6567 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
32622adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
32723ovolfsval 23046 . . . . . . . . . . . . . . . . . 18 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))))
328326, 285, 327syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))))
329105ovolfsval 23046 . . . . . . . . . . . . . . . . . 18 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
33016, 32, 329syl2an 493 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
331325, 328, 3303eqtr4rd 2655 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))
332293, 331oveq12d 6567 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
333291, 332eqtr4d 2647 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
334282fveq2d 6107 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1)))
335285peano2nnd 10914 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈ ℕ)
336282, 335eqeltrd 2688 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈ ℕ)
337 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2))
338337eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · (𝑘 + 1)) / 2) ∈ ℕ))
339337fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
340 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1))
341340oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 + 1) / 2) = (((2 · (𝑘 + 1)) + 1) / 2))
342341fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))
343338, 339, 342ifbieq12d 4063 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
344 fvex 6113 . . . . . . . . . . . . . . . . . . . . . 22 (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈ V
345 fvex 6113 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈ V
346344, 345ifex 4106 . . . . . . . . . . . . . . . . . . . . 21 if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V
347343, 21, 346fvmpt 6191 . . . . . . . . . . . . . . . . . . . 20 ((2 · (𝑘 + 1)) ∈ ℕ → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
348336, 347syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
349319, 33eqeltrd 2688 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈ ℕ)
350349iftrued 4044 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
351319fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1)))
352348, 350, 3513eqtrd 2648 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1)))
353334, 352eqtr3d 2646 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1)))
354353fveq2d 6107 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (2nd ‘(𝐺‘(𝑘 + 1))))
355353fveq2d 6107 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (1st ‘(𝐺‘(𝑘 + 1))))
356354, 355oveq12d 6567 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
35723ovolfsval 23046 . . . . . . . . . . . . . . . 16 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
358326, 335, 357syl2anc 691 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
359119ovolfsval 23046 . . . . . . . . . . . . . . . 16 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
3607, 32, 359syl2an 493 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
361356, 358, 3603eqtr4d 2654 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
362333, 361oveq12d 6567 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
363288, 362eqtrd 2644 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
364284, 363syl5eq 2656 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
365 ffvelrn 6265 . . . . . . . . . . . . . . 15 ((𝑈:ℕ⟶(0[,)+∞) ∧ (2 · 𝑘) ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
36626, 278, 365syl2an 493 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
36727, 366sseldi 3566 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ)
368367recnd 9947 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ)
369105ovolfsf 23047 . . . . . . . . . . . . . . . 16 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
37016, 369syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
371 ffvelrn 6265 . . . . . . . . . . . . . . 15 ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
372370, 32, 371syl2an 493 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
37327, 372sseldi 3566 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ)
374373recnd 9947 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ)
375119ovolfsf 23047 . . . . . . . . . . . . . . . 16 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
3767, 375syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
377 ffvelrn 6265 . . . . . . . . . . . . . . 15 ((((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
378376, 32, 377syl2an 493 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
37927, 378sseldi 3566 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ)
380379recnd 9947 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ)
381368, 374, 380addassd 9941 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
382283, 364, 3813eqtrd 2648 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
383 seqp1 12678 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
38477, 383syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
385106fveq1i 6104 . . . . . . . . . . . . 13 (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1))
386106fveq1i 6104 . . . . . . . . . . . . . 14 (𝑆𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
387386oveq1i 6559 . . . . . . . . . . . . 13 ((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))
388384, 385, 3873eqtr4g 2669 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
389 seqp1 12678 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
39077, 389syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
391120fveq1i 6104 . . . . . . . . . . . . 13 (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1))
392120fveq1i 6104 . . . . . . . . . . . . . 14 (𝑇𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
393392oveq1i 6559 . . . . . . . . . . . . 13 ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
394390, 391, 3933eqtr4g 2669 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
395388, 394oveq12d 6567 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
396108ffvelrnda 6267 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ (0[,)+∞))
39727, 396sseldi 3566 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
398397recnd 9947 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℂ)
399122ffvelrnda 6267 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ (0[,)+∞))
40027, 399sseldi 3566 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ ℝ)
401400recnd 9947 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ ℂ)
402398, 374, 401, 380add4d 10143 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
403395, 402eqtrd 2644 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
404382, 403eqeq12d 2625 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) ↔ ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))))
405271, 404syl5ibr 235 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
406405expcom 450 . . . . . . 7 (𝑘 ∈ ℕ → (𝜑 → ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
407406a2d 29 . . . . . 6 (𝑘 ∈ ℕ → ((𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘))) → (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
408191, 198, 205, 212, 270, 407nnind 10915 . . . . 5 ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ → (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
409408impcom 445 . . . 4 ((𝜑 ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
41061, 409syldan 486 . . 3 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
41167adantr 480 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
412411recnd 9947 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℂ)
41372adantr 480 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℝ)
414413rehalfcld 11156 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ)
415414recnd 9947 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ)
41669adantr 480 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℝ)
417416recnd 9947 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℂ)
418412, 415, 417, 415add4d 10143 . . . 4 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))))
419413recnd 9947 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
4204192halvesd 11155 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
421420oveq2d 6565 . . . 4 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
422418, 421eqtr2d 2645 . . 3 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) = (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))))
423184, 410, 4223brtr4d 4615 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
42430, 65, 74, 104, 423letrd 10073 1 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  ∪ cuni 4372   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  dom cdm 5038  ran crn 5039   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  1st c1st 7057  2nd c2nd 7058   ↑𝑚 cmap 7744  supcsup 8229  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950  -∞cmnf 9951  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  ℤcz 11254  ℤ≥cuz 11563  ℝ+crp 11708  (,)cioo 12046  [,)cico 12048  ...cfz 12197  ⌊cfl 12453  seqcseq 12663  abscabs 13822  vol*covol 23038 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-ico 12052  df-fz 12198  df-fl 12455  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824 This theorem is referenced by:  ovolunlem1  23072
 Copyright terms: Public domain W3C validator