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

Theorem ovolunlem1a 22988
Description: Lemma for ovolun 22991. (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 9883 . . . . . . . . . . . . 13 ℝ ∈ V
32, 2xpex 6837 . . . . . . . . . . . 12 (ℝ × ℝ) ∈ V
43inex2 4723 . . . . . . . . . . 11 ( ≤ ∩ (ℝ × ℝ)) ∈ V
5 nnex 10873 . . . . . . . . . . 11 ℕ ∈ V
64, 5elmap 7749 . . . . . . . . . 10 (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
71, 6sylib 206 . . . . . . . . 9 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
87adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
98ffvelrnda 6252 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
10 nneo 11293 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
1110adantl 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
1211con2bid 342 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈ ℕ))
1312biimpar 500 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → ((𝑛 + 1) / 2) ∈ ℕ)
14 ovolun.f1 . . . . . . . . . . 11 (𝜑𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
154, 5elmap 7749 . . . . . . . . . . 11 (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1614, 15sylib 206 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1716adantr 479 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1817ffvelrnda 6252 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
1913, 18syldan 485 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
209, 19ifclda 4069 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
21 ovolun.h . . . . . 6 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
2220, 21fmptd 6277 . . . . 5 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
23 eqid 2609 . . . . . 6 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
24 ovolun.u . . . . . 6 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
2523, 24ovolsf 22965 . . . . 5 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
2622, 25syl 17 . . . 4 (𝜑𝑈:ℕ⟶(0[,)+∞))
27 rge0ssre 12107 . . . 4 (0[,)+∞) ⊆ ℝ
28 fss 5955 . . . 4 ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
2926, 27, 28sylancl 692 . . 3 (𝜑𝑈:ℕ⟶ℝ)
3029ffvelrnda 6252 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ∈ ℝ)
31 2nn 11032 . . . 4 2 ∈ ℕ
32 peano2nn 10879 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
3332adantl 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
3433nnred 10882 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
3534rehalfcld 11126 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ)
3635flcld 12416 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℤ)
37 ax-1cn 9850 . . . . . . . . 9 1 ∈ ℂ
38372timesi 10994 . . . . . . . 8 (2 · 1) = (1 + 1)
39 nnge1 10893 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
4039adantl 480 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 1 ≤ 𝑘)
41 nnre 10874 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
4241adantl 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
43 1re 9895 . . . . . . . . . . 11 1 ∈ ℝ
44 leadd1 10345 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4543, 43, 44mp3an13 1406 . . . . . . . . . 10 (𝑘 ∈ ℝ → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4642, 45syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4740, 46mpbid 220 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (1 + 1) ≤ (𝑘 + 1))
4838, 47syl5eqbr 4612 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (2 · 1) ≤ (𝑘 + 1))
49 2re 10937 . . . . . . . . . 10 2 ∈ ℝ
50 2pos 10959 . . . . . . . . . 10 0 < 2
5149, 50pm3.2i 469 . . . . . . . . 9 (2 ∈ ℝ ∧ 0 < 2)
52 lemuldiv2 10753 . . . . . . . . 9 ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5343, 51, 52mp3an13 1406 . . . . . . . 8 ((𝑘 + 1) ∈ ℝ → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5434, 53syl 17 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5548, 54mpbid 220 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 1 ≤ ((𝑘 + 1) / 2))
56 1z 11240 . . . . . . 7 1 ∈ ℤ
57 flge 12423 . . . . . . 7 ((((𝑘 + 1) / 2) ∈ ℝ ∧ 1 ∈ ℤ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5835, 56, 57sylancl 692 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5955, 58mpbid 220 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 1 ≤ (⌊‘((𝑘 + 1) / 2)))
60 elnnz1 11236 . . . . 5 ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
6136, 59, 60sylanbrc 694 . . . 4 ((𝜑𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
62 nnmulcl 10890 . . . 4 ((2 ∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
6331, 61, 62sylancr 693 . . 3 ((𝜑𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
6429ffvelrnda 6252 . . 3 ((𝜑 ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
6563, 64syldan 485 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
66 ovolun.a . . . . . 6 (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
6766simprd 477 . . . . 5 (𝜑 → (vol*‘𝐴) ∈ ℝ)
68 ovolun.b . . . . . 6 (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
6968simprd 477 . . . . 5 (𝜑 → (vol*‘𝐵) ∈ ℝ)
7067, 69readdcld 9925 . . . 4 (𝜑 → ((vol*‘𝐴) + (vol*‘𝐵)) ∈ ℝ)
71 ovolun.c . . . . 5 (𝜑𝐶 ∈ ℝ+)
7271rpred 11704 . . . 4 (𝜑𝐶 ∈ ℝ)
7370, 72readdcld 9925 . . 3 (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
7473adantr 479 . 2 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
75 simpr 475 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
76 nnuz 11555 . . . . 5 ℕ = (ℤ‘1)
7775, 76syl6eleq 2697 . . . 4 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
78 nnz 11232 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
7978adantl 480 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
80 flhalf 12448 . . . . . 6 (𝑘 ∈ ℤ → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
8179, 80syl 17 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
82 nnz 11232 . . . . . . 7 ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ)
83 eluz 11533 . . . . . . 7 ((𝑘 ∈ ℤ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8478, 82, 83syl2an 492 . . . . . 6 ((𝑘 ∈ ℕ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8575, 63, 84syl2anc 690 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8681, 85mpbird 245 . . . 4 ((𝜑𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘))
87 elfznn 12196 . . . . 5 (𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ ℕ)
8823ovolfsf 22964 . . . . . . . . . 10 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8922, 88syl 17 . . . . . . . . 9 (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
9089adantr 479 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
9190ffvelrnda 6252 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞))
92 elrege0 12105 . . . . . . 7 ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
9391, 92sylib 206 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
9493simpld 473 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
9587, 94sylan2 489 . . . 4 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2))))) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
96 elfzuz 12164 . . . . . 6 (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ (ℤ‘(𝑘 + 1)))
97 eluznn 11590 . . . . . 6 (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
9833, 96, 97syl2an 492 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 𝑗 ∈ ℕ)
9993simprd 477 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
10098, 99syldan 485 . . . 4 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
10177, 86, 95, 100sermono 12650 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))))
10224fveq1i 6089 . . 3 (𝑈𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘)
10324fveq1i 6089 . . 3 (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2))))
104101, 102, 1033brtr4g 4611 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
105 eqid 2609 . . . . . . . . . 10 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
106 ovolun.s . . . . . . . . . 10 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
107105, 106ovolsf 22965 . . . . . . . . 9 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
10816, 107syl 17 . . . . . . . 8 (𝜑𝑆:ℕ⟶(0[,)+∞))
109 frn 5952 . . . . . . . 8 (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
110108, 109syl 17 . . . . . . 7 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
111110, 27syl6ss 3579 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
112111adantr 479 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ)
113 ffn 5944 . . . . . . . 8 (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
114108, 113syl 17 . . . . . . 7 (𝜑𝑆 Fn ℕ)
115114adantr 479 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑆 Fn ℕ)
116 fnfvelrn 6249 . . . . . 6 ((𝑆 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
117115, 61, 116syl2anc 690 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
118112, 117sseldd 3568 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
119 eqid 2609 . . . . . . . . . 10 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
120 ovolun.t . . . . . . . . . 10 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
121119, 120ovolsf 22965 . . . . . . . . 9 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
1227, 121syl 17 . . . . . . . 8 (𝜑𝑇:ℕ⟶(0[,)+∞))
123 frn 5952 . . . . . . . 8 (𝑇:ℕ⟶(0[,)+∞) → ran 𝑇 ⊆ (0[,)+∞))
124122, 123syl 17 . . . . . . 7 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
125124, 27syl6ss 3579 . . . . . 6 (𝜑 → ran 𝑇 ⊆ ℝ)
126125adantr 479 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ)
127 ffn 5944 . . . . . . . 8 (𝑇:ℕ⟶(0[,)+∞) → 𝑇 Fn ℕ)
128122, 127syl 17 . . . . . . 7 (𝜑𝑇 Fn ℕ)
129128adantr 479 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑇 Fn ℕ)
130 fnfvelrn 6249 . . . . . 6 ((𝑇 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
131129, 61, 130syl2anc 690 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
132126, 131sseldd 3568 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
13372rehalfcld 11126 . . . . . 6 (𝜑 → (𝐶 / 2) ∈ ℝ)
13467, 133readdcld 9925 . . . . 5 (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
135134adantr 479 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
13669, 133readdcld 9925 . . . . 5 (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
137136adantr 479 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
138 ressxr 9939 . . . . . . . . 9 ℝ ⊆ ℝ*
139111, 138syl6ss 3579 . . . . . . . 8 (𝜑 → ran 𝑆 ⊆ ℝ*)
140 supxrcl 11973 . . . . . . . 8 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
141139, 140syl 17 . . . . . . 7 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
142 1nn 10878 . . . . . . . . . . 11 1 ∈ ℕ
143 fdm 5950 . . . . . . . . . . . 12 (𝑆:ℕ⟶(0[,)+∞) → dom 𝑆 = ℕ)
144108, 143syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝑆 = ℕ)
145142, 144syl5eleqr 2694 . . . . . . . . . 10 (𝜑 → 1 ∈ dom 𝑆)
146 ne0i 3879 . . . . . . . . . 10 (1 ∈ dom 𝑆 → dom 𝑆 ≠ ∅)
147145, 146syl 17 . . . . . . . . 9 (𝜑 → dom 𝑆 ≠ ∅)
148 dm0rn0 5250 . . . . . . . . . 10 (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
149148necon3bii 2833 . . . . . . . . 9 (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
150147, 149sylib 206 . . . . . . . 8 (𝜑 → ran 𝑆 ≠ ∅)
151 supxrgtmnf 11987 . . . . . . . 8 ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → -∞ < sup(ran 𝑆, ℝ*, < ))
152111, 150, 151syl2anc 690 . . . . . . 7 (𝜑 → -∞ < sup(ran 𝑆, ℝ*, < ))
153 ovolun.f3 . . . . . . 7 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
154 xrre 11833 . . . . . . 7 (((sup(ran 𝑆, ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
155141, 134, 152, 153, 154syl22anc 1318 . . . . . 6 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
156155adantr 479 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
157139adantr 479 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
158 supxrub 11982 . . . . . 6 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, < ))
159157, 117, 158syl2anc 690 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, < ))
160153adantr 479 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
161118, 156, 135, 159, 160letrd 10045 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
162125, 138syl6ss 3579 . . . . . . . 8 (𝜑 → ran 𝑇 ⊆ ℝ*)
163 supxrcl 11973 . . . . . . . 8 (ran 𝑇 ⊆ ℝ* → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
164162, 163syl 17 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
165 fdm 5950 . . . . . . . . . . . 12 (𝑇:ℕ⟶(0[,)+∞) → dom 𝑇 = ℕ)
166122, 165syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝑇 = ℕ)
167142, 166syl5eleqr 2694 . . . . . . . . . 10 (𝜑 → 1 ∈ dom 𝑇)
168 ne0i 3879 . . . . . . . . . 10 (1 ∈ dom 𝑇 → dom 𝑇 ≠ ∅)
169167, 168syl 17 . . . . . . . . 9 (𝜑 → dom 𝑇 ≠ ∅)
170 dm0rn0 5250 . . . . . . . . . 10 (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
171170necon3bii 2833 . . . . . . . . 9 (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
172169, 171sylib 206 . . . . . . . 8 (𝜑 → ran 𝑇 ≠ ∅)
173 supxrgtmnf 11987 . . . . . . . 8 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅) → -∞ < sup(ran 𝑇, ℝ*, < ))
174125, 172, 173syl2anc 690 . . . . . . 7 (𝜑 → -∞ < sup(ran 𝑇, ℝ*, < ))
175 ovolun.g3 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
176 xrre 11833 . . . . . . 7 (((sup(ran 𝑇, ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
177164, 136, 174, 175, 176syl22anc 1318 . . . . . 6 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
178177adantr 479 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
179162adantr 479 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ*)
180 supxrub 11982 . . . . . 6 ((ran 𝑇 ⊆ ℝ* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, < ))
181179, 131, 180syl2anc 690 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, < ))
182175adantr 479 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
183132, 178, 137, 181, 182letrd 10045 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
184118, 132, 135, 137, 161, 183le2addd 10495 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))))
185 oveq2 6535 . . . . . . . . 9 (𝑧 = 1 → (2 · 𝑧) = (2 · 1))
186185fveq2d 6092 . . . . . . . 8 (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1)))
187 fveq2 6088 . . . . . . . . 9 (𝑧 = 1 → (𝑆𝑧) = (𝑆‘1))
188 fveq2 6088 . . . . . . . . 9 (𝑧 = 1 → (𝑇𝑧) = (𝑇‘1))
189187, 188oveq12d 6545 . . . . . . . 8 (𝑧 = 1 → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘1) + (𝑇‘1)))
190186, 189eqeq12d 2624 . . . . . . 7 (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))
191190imbi2d 328 . . . . . 6 (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))))
192 oveq2 6535 . . . . . . . . 9 (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘))
193192fveq2d 6092 . . . . . . . 8 (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘)))
194 fveq2 6088 . . . . . . . . 9 (𝑧 = 𝑘 → (𝑆𝑧) = (𝑆𝑘))
195 fveq2 6088 . . . . . . . . 9 (𝑧 = 𝑘 → (𝑇𝑧) = (𝑇𝑘))
196194, 195oveq12d 6545 . . . . . . . 8 (𝑧 = 𝑘 → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆𝑘) + (𝑇𝑘)))
197193, 196eqeq12d 2624 . . . . . . 7 (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘))))
198197imbi2d 328 . . . . . 6 (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)))))
199 oveq2 6535 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1)))
200199fveq2d 6092 . . . . . . . 8 (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1))))
201 fveq2 6088 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (𝑆𝑧) = (𝑆‘(𝑘 + 1)))
202 fveq2 6088 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (𝑇𝑧) = (𝑇‘(𝑘 + 1)))
203201, 202oveq12d 6545 . . . . . . . 8 (𝑧 = (𝑘 + 1) → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))
204200, 203eqeq12d 2624 . . . . . . 7 (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
205204imbi2d 328 . . . . . 6 (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
206 oveq2 6535 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 · 𝑧) = (2 · (⌊‘((𝑘 + 1) / 2))))
207206fveq2d 6092 . . . . . . . 8 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
208 fveq2 6088 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2))))
209 fveq2 6088 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2))))
210208, 209oveq12d 6545 . . . . . . . 8 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
211207, 210eqeq12d 2624 . . . . . . 7 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
212211imbi2d 328 . . . . . 6 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))))
21324fveq1i 6089 . . . . . . . 8 (𝑈‘(2 · 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1))
21423ovolfsval 22963 . . . . . . . . . . . 12 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))))
21522, 142, 214sylancl 692 . . . . . . . . . . 11 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))))
216 halfnz 11287 . . . . . . . . . . . . . . . . . 18 ¬ (1 / 2) ∈ ℤ
217 nnz 11232 . . . . . . . . . . . . . . . . . . 19 ((𝑛 / 2) ∈ ℕ → (𝑛 / 2) ∈ ℤ)
218 oveq1 6534 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 / 2) = (1 / 2))
219218eleq1d 2671 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → ((𝑛 / 2) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
220217, 219syl5ib 232 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → ((𝑛 / 2) ∈ ℕ → (1 / 2) ∈ ℤ))
221216, 220mtoi 188 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ¬ (𝑛 / 2) ∈ ℕ)
222221iffalsed 4046 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2)))
223 oveq1 6534 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
224 df-2 10926 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
225223, 224syl6eqr 2661 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 + 1) = 2)
226225oveq1d 6542 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2))
227 2div2e1 10997 . . . . . . . . . . . . . . . . . 18 (2 / 2) = 1
228226, 227syl6eq 2659 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ((𝑛 + 1) / 2) = 1)
229228fveq2d 6092 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1))
230222, 229eqtrd 2643 . . . . . . . . . . . . . . 15 (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1))
231 fvex 6098 . . . . . . . . . . . . . . 15 (𝐹‘1) ∈ V
232230, 21, 231fvmpt 6176 . . . . . . . . . . . . . 14 (1 ∈ ℕ → (𝐻‘1) = (𝐹‘1))
233142, 232ax-mp 5 . . . . . . . . . . . . 13 (𝐻‘1) = (𝐹‘1)
234233fveq2i 6091 . . . . . . . . . . . 12 (2nd ‘(𝐻‘1)) = (2nd ‘(𝐹‘1))
235233fveq2i 6091 . . . . . . . . . . . 12 (1st ‘(𝐻‘1)) = (1st ‘(𝐹‘1))
236234, 235oveq12i 6539 . . . . . . . . . . 11 ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1)))
237215, 236syl6eq 2659 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
23856, 237seq1i 12632 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
239 2t1e2 11023 . . . . . . . . . . 11 (2 · 1) = 2
240239fveq2i 6091 . . . . . . . . . 10 (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘ − ) ∘ 𝐻)‘2)
24123ovolfsval 22963 . . . . . . . . . . . 12 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 2 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))))
24222, 31, 241sylancl 692 . . . . . . . . . . 11 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))))
243 oveq1 6534 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 2 → (𝑛 / 2) = (2 / 2))
244243, 227syl6eq 2659 . . . . . . . . . . . . . . . . . 18 (𝑛 = 2 → (𝑛 / 2) = 1)
245244, 142syl6eqel 2695 . . . . . . . . . . . . . . . . 17 (𝑛 = 2 → (𝑛 / 2) ∈ ℕ)
246245iftrued 4043 . . . . . . . . . . . . . . . 16 (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2)))
247244fveq2d 6092 . . . . . . . . . . . . . . . 16 (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1))
248246, 247eqtrd 2643 . . . . . . . . . . . . . . 15 (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1))
249 fvex 6098 . . . . . . . . . . . . . . 15 (𝐺‘1) ∈ V
250248, 21, 249fvmpt 6176 . . . . . . . . . . . . . 14 (2 ∈ ℕ → (𝐻‘2) = (𝐺‘1))
25131, 250ax-mp 5 . . . . . . . . . . . . 13 (𝐻‘2) = (𝐺‘1)
252251fveq2i 6091 . . . . . . . . . . . 12 (2nd ‘(𝐻‘2)) = (2nd ‘(𝐺‘1))
253251fveq2i 6091 . . . . . . . . . . . 12 (1st ‘(𝐻‘2)) = (1st ‘(𝐺‘1))
254252, 253oveq12i 6539 . . . . . . . . . . 11 ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))
255242, 254syl6eq 2659 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
256240, 255syl5eq 2655 . . . . . . . . 9 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
25776, 142, 38, 238, 256seqp1i 12634 . . . . . . . 8 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
258213, 257syl5eq 2655 . . . . . . 7 (𝜑 → (𝑈‘(2 · 1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
259106fveq1i 6089 . . . . . . . . 9 (𝑆‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1)
260105ovolfsval 22963 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
26116, 142, 260sylancl 692 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
26256, 261seq1i 12632 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
263259, 262syl5eq 2655 . . . . . . . 8 (𝜑 → (𝑆‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
264120fveq1i 6089 . . . . . . . . 9 (𝑇‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1)
265119ovolfsval 22963 . . . . . . . . . . 11 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
2667, 142, 265sylancl 692 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
26756, 266seq1i 12632 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
268264, 267syl5eq 2655 . . . . . . . 8 (𝜑 → (𝑇‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
269263, 268oveq12d 6545 . . . . . . 7 (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
270258, 269eqtr4d 2646 . . . . . 6 (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))
271 oveq1 6534 . . . . . . . . 9 ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
27238oveq2i 6538 . . . . . . . . . . . . 13 ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
273 2cnd 10940 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 2 ∈ ℂ)
27442recnd 9924 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
275 1cnd 9912 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 1 ∈ ℂ)
276273, 274, 275adddid 9920 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
277 nnmulcl 10890 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
27831, 277mpan 701 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
279278adantl 480 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
280279nncnd 10883 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
281280, 275, 275addassd 9918 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
282272, 276, 2813eqtr4a 2669 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1))
283282fveq2d 6092 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1)))
28424fveq1i 6089 . . . . . . . . . . . 12 (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1))
285279peano2nnd 10884 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
286285, 76syl6eleq 2697 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ (ℤ‘1))
287 seqp1 12633 . . . . . . . . . . . . . 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 2697 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ (ℤ‘1))
290 seqp1 12633 . . . . . . . . . . . . . . . 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 6089 . . . . . . . . . . . . . . . . 17 (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘))
293292a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)))
294 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2))
295294eleq1d 2671 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
296294fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2)))
297 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1))
298297oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 + 1) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
299298fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
300295, 296, 299ifbieq12d 4062 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
301 fvex 6098 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈ V
302 fvex 6098 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈ V
303301, 302ifex 4105 . . . . . . . . . . . . . . . . . . . . . 22 if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V
304300, 21, 303fvmpt 6176 . . . . . . . . . . . . . . . . . . . . 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 10960 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ≠ 0
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ) → 2 ≠ 0)
308274, 273, 307divcan3d 10655 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘)
309308, 75eqeltrd 2687 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈ ℕ)
310 nneo 11293 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 · 𝑘) ∈ ℕ → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
311279, 310syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
312309, 311mpbid 220 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ)
313312iffalsed 4046 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
314282oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
31533nncnd 10883 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
316 2cn 10938 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℂ
317 divcan3 10560 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
318316, 306, 317mp3an23 1407 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 + 1) ∈ ℂ → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
319315, 318syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
320314, 319eqtr3d 2645 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1))
321320fveq2d 6092 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1)))
322305, 313, 3213eqtrd 2647 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1)))
323322fveq2d 6092 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐻‘((2 · 𝑘) + 1))) = (2nd ‘(𝐹‘(𝑘 + 1))))
324322fveq2d 6092 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐻‘((2 · 𝑘) + 1))) = (1st ‘(𝐹‘(𝑘 + 1))))
325323, 324oveq12d 6545 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
32622adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
32723ovolfsval 22963 . . . . . . . . . . . . . . . . . 18 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))))
328326, 285, 327syl2anc 690 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))))
329105ovolfsval 22963 . . . . . . . . . . . . . . . . . 18 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
33016, 32, 329syl2an 492 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
331325, 328, 3303eqtr4rd 2654 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))
332293, 331oveq12d 6545 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
333291, 332eqtr4d 2646 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
334282fveq2d 6092 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1)))
335285peano2nnd 10884 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈ ℕ)
336282, 335eqeltrd 2687 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈ ℕ)
337 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2))
338337eleq1d 2671 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · (𝑘 + 1)) / 2) ∈ ℕ))
339337fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
340 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1))
341340oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 + 1) / 2) = (((2 · (𝑘 + 1)) + 1) / 2))
342341fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))
343338, 339, 342ifbieq12d 4062 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
344 fvex 6098 . . . . . . . . . . . . . . . . . . . . . 22 (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈ V
345 fvex 6098 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈ V
346344, 345ifex 4105 . . . . . . . . . . . . . . . . . . . . 21 if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V
347343, 21, 346fvmpt 6176 . . . . . . . . . . . . . . . . . . . 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 2687 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈ ℕ)
350349iftrued 4043 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
351319fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1)))
352348, 350, 3513eqtrd 2647 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1)))
353334, 352eqtr3d 2645 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1)))
354353fveq2d 6092 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (2nd ‘(𝐺‘(𝑘 + 1))))
355353fveq2d 6092 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (1st ‘(𝐺‘(𝑘 + 1))))
356354, 355oveq12d 6545 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
35723ovolfsval 22963 . . . . . . . . . . . . . . . 16 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
358326, 335, 357syl2anc 690 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
359119ovolfsval 22963 . . . . . . . . . . . . . . . 16 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
3607, 32, 359syl2an 492 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
361356, 358, 3603eqtr4d 2653 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
362333, 361oveq12d 6545 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
363288, 362eqtrd 2643 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
364284, 363syl5eq 2655 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
365 ffvelrn 6250 . . . . . . . . . . . . . . 15 ((𝑈:ℕ⟶(0[,)+∞) ∧ (2 · 𝑘) ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
36626, 278, 365syl2an 492 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
36727, 366sseldi 3565 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ)
368367recnd 9924 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ)
369105ovolfsf 22964 . . . . . . . . . . . . . . . 16 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
37016, 369syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
371 ffvelrn 6250 . . . . . . . . . . . . . . 15 ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
372370, 32, 371syl2an 492 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
37327, 372sseldi 3565 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ)
374373recnd 9924 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ)
375119ovolfsf 22964 . . . . . . . . . . . . . . . 16 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
3767, 375syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
377 ffvelrn 6250 . . . . . . . . . . . . . . 15 ((((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
378376, 32, 377syl2an 492 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
37927, 378sseldi 3565 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ)
380379recnd 9924 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ)
381368, 374, 380addassd 9918 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
382283, 364, 3813eqtrd 2647 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
383 seqp1 12633 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
38477, 383syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
385106fveq1i 6089 . . . . . . . . . . . . 13 (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1))
386106fveq1i 6089 . . . . . . . . . . . . . 14 (𝑆𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
387386oveq1i 6537 . . . . . . . . . . . . 13 ((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))
388384, 385, 3873eqtr4g 2668 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
389 seqp1 12633 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
39077, 389syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
391120fveq1i 6089 . . . . . . . . . . . . 13 (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1))
392120fveq1i 6089 . . . . . . . . . . . . . 14 (𝑇𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
393392oveq1i 6537 . . . . . . . . . . . . 13 ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
394390, 391, 3933eqtr4g 2668 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
395388, 394oveq12d 6545 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
396108ffvelrnda 6252 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ (0[,)+∞))
39727, 396sseldi 3565 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
398397recnd 9924 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℂ)
399122ffvelrnda 6252 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ (0[,)+∞))
40027, 399sseldi 3565 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ ℝ)
401400recnd 9924 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ ℂ)
402398, 374, 401, 380add4d 10115 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
403395, 402eqtrd 2643 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
404382, 403eqeq12d 2624 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) ↔ ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))))
405271, 404syl5ibr 234 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
406405expcom 449 . . . . . . 7 (𝑘 ∈ ℕ → (𝜑 → ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
407406a2d 29 . . . . . 6 (𝑘 ∈ ℕ → ((𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘))) → (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
408191, 198, 205, 212, 270, 407nnind 10885 . . . . 5 ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ → (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
409408impcom 444 . . . 4 ((𝜑 ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
41061, 409syldan 485 . . 3 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
41167adantr 479 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
412411recnd 9924 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℂ)
41372adantr 479 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℝ)
414413rehalfcld 11126 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ)
415414recnd 9924 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ)
41669adantr 479 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℝ)
417416recnd 9924 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℂ)
418412, 415, 417, 415add4d 10115 . . . 4 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))))
419413recnd 9924 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
4204192halvesd 11125 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
421420oveq2d 6543 . . . 4 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
422418, 421eqtr2d 2644 . . 3 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) = (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))))
423184, 410, 4223brtr4d 4609 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
42430, 65, 74, 104, 423letrd 10045 1 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wne 2779  cin 3538  wss 3539  c0 3873  ifcif 4035   cuni 4366   class class class wbr 4577  cmpt 4637   × cxp 5026  dom cdm 5028  ran crn 5029  ccom 5032   Fn wfn 5785  wf 5786  cfv 5790  (class class class)co 6527  1st c1st 7034  2nd c2nd 7035  𝑚 cmap 7721  supcsup 8206  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797  +∞cpnf 9927  -∞cmnf 9928  *cxr 9929   < clt 9930  cle 9931  cmin 10117   / cdiv 10533  cn 10867  2c2 10917  cz 11210  cuz 11519  +crp 11664  (,)cioo 12002  [,)cico 12004  ...cfz 12152  cfl 12408  seqcseq 12618  abscabs 13768  vol*covol 22955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-map 7723  df-en 7819  df-dom 7820  df-sdom 7821  df-sup 8208  df-inf 8209  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-n0 11140  df-z 11211  df-uz 11520  df-rp 11665  df-ico 12008  df-fz 12153  df-fl 12410  df-seq 12619  df-exp 12678  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770
This theorem is referenced by:  ovolunlem1  22989
  Copyright terms: Public domain W3C validator