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

Theorem ioombl1lem4 24096
 Description: Lemma for ioombl1 24097. (Contributed by Mario Carneiro, 16-Jun-2014.)
Hypotheses
Ref Expression
ioombl1.b 𝐵 = (𝐴(,)+∞)
ioombl1.a (𝜑𝐴 ∈ ℝ)
ioombl1.e (𝜑𝐸 ⊆ ℝ)
ioombl1.v (𝜑 → (vol*‘𝐸) ∈ ℝ)
ioombl1.c (𝜑𝐶 ∈ ℝ+)
ioombl1.s 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ioombl1.t 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
ioombl1.u 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
ioombl1.f1 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
ioombl1.f2 (𝜑𝐸 ran ((,) ∘ 𝐹))
ioombl1.f3 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
ioombl1.p 𝑃 = (1st ‘(𝐹𝑛))
ioombl1.q 𝑄 = (2nd ‘(𝐹𝑛))
ioombl1.g 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
ioombl1.h 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩)
Assertion
Ref Expression
ioombl1lem4 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ≤ ((vol*‘𝐸) + 𝐶))
Distinct variable groups:   𝐵,𝑛   𝐶,𝑛   𝑛,𝐸   𝑛,𝐹   𝑛,𝐺   𝑛,𝐻   𝜑,𝑛   𝑆,𝑛
Allowed substitution hints:   𝐴(𝑛)   𝑃(𝑛)   𝑄(𝑛)   𝑇(𝑛)   𝑈(𝑛)

Proof of Theorem ioombl1lem4
Dummy variables 𝑥 𝑗 𝑘 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 4209 . . . 4 (𝐸𝐵) ⊆ 𝐸
2 ioombl1.e . . . 4 (𝜑𝐸 ⊆ ℝ)
3 ioombl1.v . . . 4 (𝜑 → (vol*‘𝐸) ∈ ℝ)
4 ovolsscl 24021 . . . 4 (((𝐸𝐵) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸𝐵)) ∈ ℝ)
51, 2, 3, 4mp3an2i 1459 . . 3 (𝜑 → (vol*‘(𝐸𝐵)) ∈ ℝ)
6 difss 4112 . . . 4 (𝐸𝐵) ⊆ 𝐸
7 ovolsscl 24021 . . . 4 (((𝐸𝐵) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸𝐵)) ∈ ℝ)
86, 2, 3, 7mp3an2i 1459 . . 3 (𝜑 → (vol*‘(𝐸𝐵)) ∈ ℝ)
95, 8readdcld 10664 . 2 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ∈ ℝ)
10 ioombl1.b . . 3 𝐵 = (𝐴(,)+∞)
11 ioombl1.a . . 3 (𝜑𝐴 ∈ ℝ)
12 ioombl1.c . . 3 (𝜑𝐶 ∈ ℝ+)
13 ioombl1.s . . 3 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
14 ioombl1.t . . 3 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
15 ioombl1.u . . 3 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
16 ioombl1.f1 . . 3 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
17 ioombl1.f2 . . 3 (𝜑𝐸 ran ((,) ∘ 𝐹))
18 ioombl1.f3 . . 3 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
19 ioombl1.p . . 3 𝑃 = (1st ‘(𝐹𝑛))
20 ioombl1.q . . 3 𝑄 = (2nd ‘(𝐹𝑛))
21 ioombl1.g . . 3 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
22 ioombl1.h . . 3 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩)
2310, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22ioombl1lem2 24094 . 2 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
2412rpred 12426 . . 3 (𝜑𝐶 ∈ ℝ)
253, 24readdcld 10664 . 2 (𝜑 → ((vol*‘𝐸) + 𝐶) ∈ ℝ)
2610, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22ioombl1lem1 24093 . . . . . . . . 9 (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))))
2726simpld 495 . . . . . . . 8 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
28 eqid 2826 . . . . . . . . 9 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
2928, 14ovolsf 24007 . . . . . . . 8 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
3027, 29syl 17 . . . . . . 7 (𝜑𝑇:ℕ⟶(0[,)+∞))
3130frnd 6520 . . . . . 6 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
32 rge0ssre 12839 . . . . . 6 (0[,)+∞) ⊆ ℝ
3331, 32sstrdi 3983 . . . . 5 (𝜑 → ran 𝑇 ⊆ ℝ)
34 1nn 11643 . . . . . . . 8 1 ∈ ℕ
3530fdmd 6522 . . . . . . . 8 (𝜑 → dom 𝑇 = ℕ)
3634, 35eleqtrrid 2925 . . . . . . 7 (𝜑 → 1 ∈ dom 𝑇)
3736ne0d 4305 . . . . . 6 (𝜑 → dom 𝑇 ≠ ∅)
38 dm0rn0 5794 . . . . . . 7 (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
3938necon3bii 3073 . . . . . 6 (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
4037, 39sylib 219 . . . . 5 (𝜑 → ran 𝑇 ≠ ∅)
4130ffvelrnda 6849 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ (0[,)+∞))
4232, 41sseldi 3969 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ ℝ)
43 eqid 2826 . . . . . . . . . . . . 13 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
4443, 13ovolsf 24007 . . . . . . . . . . . 12 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
4516, 44syl 17 . . . . . . . . . . 11 (𝜑𝑆:ℕ⟶(0[,)+∞))
4645ffvelrnda 6849 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) ∈ (0[,)+∞))
4732, 46sseldi 3969 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) ∈ ℝ)
4823adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
49 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
50 nnuz 12275 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
5149, 50syl6eleq 2928 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
52 simpl 483 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝜑)
53 elfznn 12931 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
5428ovolfsf 24006 . . . . . . . . . . . . . . 15 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
5527, 54syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
5655ffvelrnda 6849 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞))
5732, 56sseldi 3969 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
5852, 53, 57syl2an 595 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
5943ovolfsf 24006 . . . . . . . . . . . . . . . 16 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
6016, 59syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
6160ffvelrnda 6849 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞))
62 elrege0 12837 . . . . . . . . . . . . . 14 ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
6361, 62sylib 219 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
6463simpld 495 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
6552, 53, 64syl2an 595 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
6626simprd 496 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
67 eqid 2826 . . . . . . . . . . . . . . . . . . 19 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
6867ovolfsf 24006 . . . . . . . . . . . . . . . . . 18 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
6966, 68syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
7069ffvelrnda 6849 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞))
71 elrege0 12837 . . . . . . . . . . . . . . . 16 ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
7270, 71sylib 219 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
7372simprd 496 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛))
7472simpld 495 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
7557, 74addge01d 11222 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
7673, 75mpbid 233 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
7710, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22ioombl1lem3 24095 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
7876, 77breqtrd 5089 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
7952, 53, 78syl2an 595 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
8051, 58, 65, 79serle 13420 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
8114fveq1i 6670 . . . . . . . . . 10 (𝑇𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗)
8213fveq1i 6670 . . . . . . . . . 10 (𝑆𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗)
8380, 81, 823brtr4g 5097 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ≤ (𝑆𝑗))
84 1zzd 12007 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℤ)
85 eqidd 2827 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
8663simprd 496 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
8745frnd 6520 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
88 icossxr 12816 . . . . . . . . . . . . . . . . . . . 20 (0[,)+∞) ⊆ ℝ*
8987, 88sstrdi 3983 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran 𝑆 ⊆ ℝ*)
9089adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
9145ffnd 6514 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑆 Fn ℕ)
92 fnfvelrn 6846 . . . . . . . . . . . . . . . . . . 19 ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ran 𝑆)
9391, 92sylan 580 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ran 𝑆)
94 supxrub 12712 . . . . . . . . . . . . . . . . . 18 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆𝑘) ∈ ran 𝑆) → (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
9590, 93, 94syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
9695ralrimiva 3187 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
97 brralrspcev 5123 . . . . . . . . . . . . . . . 16 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥)
9823, 96, 97syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥)
9950, 13, 84, 85, 64, 86, 98isumsup2 15196 . . . . . . . . . . . . . 14 (𝜑𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
10087, 32sstrdi 3983 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝑆 ⊆ ℝ)
10145fdmd 6522 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom 𝑆 = ℕ)
10234, 101eleqtrrid 2925 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ dom 𝑆)
103102ne0d 4305 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝑆 ≠ ∅)
104 dm0rn0 5794 . . . . . . . . . . . . . . . . 17 (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
105104necon3bii 3073 . . . . . . . . . . . . . . . 16 (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
106103, 105sylib 219 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝑆 ≠ ∅)
107 breq1 5066 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑆𝑘) → (𝑧𝑥 ↔ (𝑆𝑘) ≤ 𝑥))
108107ralrn 6852 . . . . . . . . . . . . . . . . . 18 (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
10991, 108syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
110109rexbidv 3302 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
11198, 110mpbird 258 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥)
112 supxrre 12715 . . . . . . . . . . . . . . 15 ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
113100, 106, 111, 112syl3anc 1365 . . . . . . . . . . . . . 14 (𝜑 → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
11499, 113breqtrrd 5091 . . . . . . . . . . . . 13 (𝜑𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
115114adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
11613, 115eqbrtrrid 5099 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇝ sup(ran 𝑆, ℝ*, < ))
11764adantlr 711 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
11886adantlr 711 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
11950, 49, 116, 117, 118climserle 15014 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
12082, 119eqbrtrid 5098 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
12142, 47, 48, 83, 120letrd 10791 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
122121ralrimiva 3187 . . . . . . 7 (𝜑 → ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
123 brralrspcev 5123 . . . . . . 7 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥)
12423, 122, 123syl2anc 584 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥)
12530ffnd 6514 . . . . . . . 8 (𝜑𝑇 Fn ℕ)
126 breq1 5066 . . . . . . . . 9 (𝑧 = (𝑇𝑗) → (𝑧𝑥 ↔ (𝑇𝑗) ≤ 𝑥))
127126ralrn 6852 . . . . . . . 8 (𝑇 Fn ℕ → (∀𝑧 ∈ ran 𝑇 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥))
128125, 127syl 17 . . . . . . 7 (𝜑 → (∀𝑧 ∈ ran 𝑇 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥))
129128rexbidv 3302 . . . . . 6 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥))
130124, 129mpbird 258 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥)
13133, 40, 130suprcld 11598 . . . 4 (𝜑 → sup(ran 𝑇, ℝ, < ) ∈ ℝ)
13267, 15ovolsf 24007 . . . . . . . 8 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
13366, 132syl 17 . . . . . . 7 (𝜑𝑈:ℕ⟶(0[,)+∞))
134133frnd 6520 . . . . . 6 (𝜑 → ran 𝑈 ⊆ (0[,)+∞))
135134, 32sstrdi 3983 . . . . 5 (𝜑 → ran 𝑈 ⊆ ℝ)
136133fdmd 6522 . . . . . . . 8 (𝜑 → dom 𝑈 = ℕ)
13734, 136eleqtrrid 2925 . . . . . . 7 (𝜑 → 1 ∈ dom 𝑈)
138137ne0d 4305 . . . . . 6 (𝜑 → dom 𝑈 ≠ ∅)
139 dm0rn0 5794 . . . . . . 7 (dom 𝑈 = ∅ ↔ ran 𝑈 = ∅)
140139necon3bii 3073 . . . . . 6 (dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅)
141138, 140sylib 219 . . . . 5 (𝜑 → ran 𝑈 ≠ ∅)
142133ffvelrnda 6849 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ∈ (0[,)+∞))
14332, 142sseldi 3969 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ∈ ℝ)
14452, 53, 74syl2an 595 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
145 elrege0 12837 . . . . . . . . . . . . . . . 16 ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
14656, 145sylib 219 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
147146simprd 496 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛))
14874, 57addge02d 11223 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
149147, 148mpbid 233 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
150149, 77breqtrd 5089 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
15152, 53, 150syl2an 595 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
15251, 144, 65, 151serle 13420 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
15315fveq1i 6670 . . . . . . . . . 10 (𝑈𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)
154152, 153, 823brtr4g 5097 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ≤ (𝑆𝑗))
155143, 47, 48, 154, 120letrd 10791 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
156155ralrimiva 3187 . . . . . . 7 (𝜑 → ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
157 brralrspcev 5123 . . . . . . 7 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥)
15823, 156, 157syl2anc 584 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥)
159133ffnd 6514 . . . . . . . 8 (𝜑𝑈 Fn ℕ)
160 breq1 5066 . . . . . . . . 9 (𝑧 = (𝑈𝑗) → (𝑧𝑥 ↔ (𝑈𝑗) ≤ 𝑥))
161160ralrn 6852 . . . . . . . 8 (𝑈 Fn ℕ → (∀𝑧 ∈ ran 𝑈 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥))
162159, 161syl 17 . . . . . . 7 (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥))
163162rexbidv 3302 . . . . . 6 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥))
164158, 163mpbird 258 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥)
165135, 141, 164suprcld 11598 . . . 4 (𝜑 → sup(ran 𝑈, ℝ, < ) ∈ ℝ)
166 ssralv 4037 . . . . . . . . . 10 ((𝐸𝐵) ⊆ 𝐸 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
1671, 166ax-mp 5 . . . . . . . . 9 (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
16819breq1i 5070 . . . . . . . . . . . . 13 (𝑃 < 𝑥 ↔ (1st ‘(𝐹𝑛)) < 𝑥)
169 ovolfcl 24001 . . . . . . . . . . . . . . . . . . 19 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
17016, 169sylan 580 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
171170simp1d 1136 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
17219, 171eqeltrid 2922 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
173172adantlr 711 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
1741, 2sstrid 3982 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸𝐵) ⊆ ℝ)
175174sselda 3971 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐸𝐵)) → 𝑥 ∈ ℝ)
176175adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
177 ltle 10723 . . . . . . . . . . . . . . 15 ((𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑃 < 𝑥𝑃𝑥))
178173, 176, 177syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥𝑃𝑥))
179 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
180 opex 5353 . . . . . . . . . . . . . . . . . . . 20 ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V
18121fvmpt2 6777 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V) → (𝐺𝑛) = ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
182179, 180, 181sylancl 586 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
183182fveq2d 6673 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = (1st ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
18411adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
185184, 172ifcld 4515 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ)
186170simp2d 1137 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
18720, 186eqeltrid 2922 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
188185, 187ifcld 4515 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
189 op1stg 7697 . . . . . . . . . . . . . . . . . . 19 ((if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (1st ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
190188, 187, 189syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (1st ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
191183, 190eqtrd 2861 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
192191ad2ant2r 743 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (1st ‘(𝐺𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
193188ad2ant2r 743 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
194185ad2ant2r 743 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ)
195174ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (𝐸𝐵) ⊆ ℝ)
196 simplr 765 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑥 ∈ (𝐸𝐵))
197195, 196sseldd 3972 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑥 ∈ ℝ)
198187ad2ant2r 743 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑄 ∈ ℝ)
199 min1 12577 . . . . . . . . . . . . . . . . . 18 ((if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ ∧ 𝑄 ∈ ℝ) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃𝐴, 𝐴, 𝑃))
200194, 198, 199syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃𝐴, 𝐴, 𝑃))
20111ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝐴 ∈ ℝ)
202 elinel2 4177 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐸𝐵) → 𝑥𝐵)
203202ad2antlr 723 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑥𝐵)
20411rexrd 10685 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐴 ∈ ℝ*)
205 pnfxr 10689 . . . . . . . . . . . . . . . . . . . . . . . 24 +∞ ∈ ℝ*
206 elioo2 12774 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞)))
207204, 205, 206sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞)))
20810eleq2i 2909 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝐵𝑥 ∈ (𝐴(,)+∞))
209 ltpnf 12510 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ → 𝑥 < +∞)
210209adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝑥 < +∞)
211210pm4.71i 560 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
212 df-3an 1083 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
213211, 212bitr4i 279 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞))
214207, 208, 2133bitr4g 315 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
215 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝐴 < 𝑥)
216214, 215syl6bi 254 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵𝐴 < 𝑥))
217216ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (𝑥𝐵𝐴 < 𝑥))
218203, 217mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝐴 < 𝑥)
219201, 197, 218ltled 10782 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝐴𝑥)
220 simprr 769 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑃𝑥)
221 breq1 5066 . . . . . . . . . . . . . . . . . . 19 (𝐴 = if(𝑃𝐴, 𝐴, 𝑃) → (𝐴𝑥 ↔ if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥))
222 breq1 5066 . . . . . . . . . . . . . . . . . . 19 (𝑃 = if(𝑃𝐴, 𝐴, 𝑃) → (𝑃𝑥 ↔ if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥))
223221, 222ifboth 4508 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑥𝑃𝑥) → if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥)
224219, 220, 223syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥)
225193, 194, 197, 200, 224letrd 10791 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑥)
226192, 225eqbrtrd 5085 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (1st ‘(𝐺𝑛)) ≤ 𝑥)
227226expr 457 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃𝑥 → (1st ‘(𝐺𝑛)) ≤ 𝑥))
228178, 227syld 47 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → (1st ‘(𝐺𝑛)) ≤ 𝑥))
229168, 228syl5bir 244 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < 𝑥 → (1st ‘(𝐺𝑛)) ≤ 𝑥))
23020breq2i 5071 . . . . . . . . . . . . . 14 (𝑥 < 𝑄𝑥 < (2nd ‘(𝐹𝑛)))
231187adantlr 711 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
232 ltle 10723 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑄 ∈ ℝ) → (𝑥 < 𝑄𝑥𝑄))
233176, 231, 232syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄𝑥𝑄))
234230, 233syl5bir 244 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹𝑛)) → 𝑥𝑄))
235182fveq2d 6673 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
236 op2ndg 7698 . . . . . . . . . . . . . . . . 17 ((if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (2nd ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
237188, 187, 236syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (2nd ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
238235, 237eqtrd 2861 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = 𝑄)
239238adantlr 711 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = 𝑄)
240239breq2d 5075 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ (2nd ‘(𝐺𝑛)) ↔ 𝑥𝑄))
241234, 240sylibrd 260 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹𝑛)) → 𝑥 ≤ (2nd ‘(𝐺𝑛))))
242229, 241anim12d 608 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
243242reximdva 3279 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐸𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
244243ralimdva 3182 . . . . . . . . 9 (𝜑 → (∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
245167, 244syl5 34 . . . . . . . 8 (𝜑 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
246 ovolfioo 24002 . . . . . . . . 9 ((𝐸 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐸 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
2472, 16, 246syl2anc 584 . . . . . . . 8 (𝜑 → (𝐸 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
248 ovolficc 24003 . . . . . . . . 9 (((𝐸𝐵) ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
249174, 27, 248syl2anc 584 . . . . . . . 8 (𝜑 → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
250245, 247, 2493imtr4d 295 . . . . . . 7 (𝜑 → (𝐸 ran ((,) ∘ 𝐹) → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐺)))
25117, 250mpd 15 . . . . . 6 (𝜑 → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐺))
25214ovollb2 24024 . . . . . 6 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸𝐵) ⊆ ran ([,] ∘ 𝐺)) → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
25327, 251, 252syl2anc 584 . . . . 5 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
254 supxrre 12715 . . . . . 6 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥) → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
25533, 40, 130, 254syl3anc 1365 . . . . 5 (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
256253, 255breqtrd 5089 . . . 4 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑇, ℝ, < ))
257 ssralv 4037 . . . . . . . . . 10 ((𝐸𝐵) ⊆ 𝐸 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
2586, 257ax-mp 5 . . . . . . . . 9 (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
259172adantlr 711 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
2606, 2sstrid 3982 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸𝐵) ⊆ ℝ)
261260sselda 3971 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐸𝐵)) → 𝑥 ∈ ℝ)
262261adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
263259, 262, 177syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥𝑃𝑥))
264168, 263syl5bir 244 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < 𝑥𝑃𝑥))
265 opex 5353 . . . . . . . . . . . . . . . . . 18 𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V
26622fvmpt2 6777 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V) → (𝐻𝑛) = ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩)
267179, 265, 266sylancl 586 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐻𝑛) = ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩)
268267fveq2d 6673 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐻𝑛)) = (1st ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩))
269 op1stg 7697 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℝ ∧ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (1st ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
270172, 188, 269syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (1st ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
271268, 270eqtrd 2861 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐻𝑛)) = 𝑃)
272271adantlr 711 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻𝑛)) = 𝑃)
273272breq1d 5073 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑃𝑥))
274264, 273sylibrd 260 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < 𝑥 → (1st ‘(𝐻𝑛)) ≤ 𝑥))
275187adantlr 711 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
276262, 275, 232syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄𝑥𝑄))
277260ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝐸𝐵) ⊆ ℝ)
278 simplr 765 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ∈ (𝐸𝐵))
279277, 278sseldd 3972 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ∈ ℝ)
28011ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝐴 ∈ ℝ)
281172ad2ant2r 743 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑃 ∈ ℝ)
282280, 281ifcld 4515 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ)
283 eldifn 4108 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐸𝐵) → ¬ 𝑥𝐵)
284283ad2antlr 723 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → ¬ 𝑥𝐵)
285279biantrurd 533 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝐴 < 𝑥 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
286214ad2antrr 722 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝑥𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
287285, 286bitr4d 283 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝐴 < 𝑥𝑥𝐵))
288284, 287mtbird 326 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → ¬ 𝐴 < 𝑥)
289279, 280, 288nltled 10784 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥𝐴)
290 max2 12575 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ if(𝑃𝐴, 𝐴, 𝑃))
291281, 280, 290syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝐴 ≤ if(𝑃𝐴, 𝐴, 𝑃))
292279, 280, 282, 289, 291letrd 10791 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ≤ if(𝑃𝐴, 𝐴, 𝑃))
293 simprr 769 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥𝑄)
294 breq2 5067 . . . . . . . . . . . . . . . . . 18 (if(𝑃𝐴, 𝐴, 𝑃) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ if(𝑃𝐴, 𝐴, 𝑃) ↔ 𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)))
295 breq2 5067 . . . . . . . . . . . . . . . . . 18 (𝑄 = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) → (𝑥𝑄𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)))
296294, 295ifboth 4508 . . . . . . . . . . . . . . . . 17 ((𝑥 ≤ if(𝑃𝐴, 𝐴, 𝑃) ∧ 𝑥𝑄) → 𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
297292, 293, 296syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
298267fveq2d 6673 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐻𝑛)) = (2nd ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩))
299 op2ndg 7698 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℝ ∧ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (2nd ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
300172, 188, 299syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (2nd ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
301298, 300eqtrd 2861 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐻𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
302301ad2ant2r 743 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (2nd ‘(𝐻𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
303297, 302breqtrrd 5091 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ≤ (2nd ‘(𝐻𝑛)))
304303expr 457 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥𝑄𝑥 ≤ (2nd ‘(𝐻𝑛))))
305276, 304syld 47 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄𝑥 ≤ (2nd ‘(𝐻𝑛))))
306230, 305syl5bir 244 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹𝑛)) → 𝑥 ≤ (2nd ‘(𝐻𝑛))))
307274, 306anim12d 608 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
308307reximdva 3279 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐸𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
309308ralimdva 3182 . . . . . . . . 9 (𝜑 → (∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
310258, 309syl5 34 . . . . . . . 8 (𝜑 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
311 ovolficc 24003 . . . . . . . . 9 (((𝐸𝐵) ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
312260, 66, 311syl2anc 584 . . . . . . . 8 (𝜑 → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
313310, 247, 3123imtr4d 295 . . . . . . 7 (𝜑 → (𝐸 ran ((,) ∘ 𝐹) → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐻)))
31417, 313mpd 15 . . . . . 6 (𝜑 → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐻))
31515ovollb2 24024 . . . . . 6 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸𝐵) ⊆ ran ([,] ∘ 𝐻)) → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
31666, 314, 315syl2anc 584 . . . . 5 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
317 supxrre 12715 . . . . . 6 ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥) → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
318135, 141, 164, 317syl3anc 1365 . . . . 5 (𝜑 → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
319316, 318breqtrd 5089 . . . 4 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑈, ℝ, < ))
3205, 8, 131, 165, 256, 319le2addd 11253 . . 3 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ≤ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
321 eqidd 2827 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐺)‘𝑛))
32250, 14, 84, 321, 57, 147, 124isumsup2 15196 . . . . 5 (𝜑𝑇 ⇝ sup(ran 𝑇, ℝ, < ))
323 seqex 13366 . . . . . . 7 seq1( + , ((abs ∘ − ) ∘ 𝐹)) ∈ V
32413, 323eqeltri 2914 . . . . . 6 𝑆 ∈ V
325324a1i 11 . . . . 5 (𝜑𝑆 ∈ V)
326 eqidd 2827 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) = (((abs ∘ − ) ∘ 𝐻)‘𝑛))
32750, 15, 84, 326, 74, 73, 158isumsup2 15196 . . . . 5 (𝜑𝑈 ⇝ sup(ran 𝑈, ℝ, < ))
32842recnd 10663 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ ℂ)
329143recnd 10663 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ∈ ℂ)
33057recnd 10663 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
33152, 53, 330syl2an 595 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
33274recnd 10663 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
33352, 53, 332syl2an 595 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
33477eqcomd 2832 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
33552, 53, 334syl2an 595 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
33651, 331, 333, 335seradd 13407 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)))
33781, 153oveq12i 7162 . . . . . 6 ((𝑇𝑗) + (𝑈𝑗)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗))
338336, 82, 3373eqtr4g 2886 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) = ((𝑇𝑗) + (𝑈𝑗)))
33950, 84, 322, 325, 327, 328, 329, 338climadd 14983 . . . 4 (𝜑𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
340 climuni 14904 . . . 4 ((𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) ∧ 𝑆 ⇝ sup(ran 𝑆, ℝ*, < )) → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
341339, 114, 340syl2anc 584 . . 3 (𝜑 → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
342320, 341breqtrd 5089 . 2 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ≤ sup(ran 𝑆, ℝ*, < ))
3439, 23, 25, 342, 18letrd 10791 1 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ≤ ((vol*‘𝐸) + 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107   ≠ wne 3021  ∀wral 3143  ∃wrex 3144  Vcvv 3500   ∖ cdif 3937   ∩ cin 3939   ⊆ wss 3940  ∅c0 4295  ifcif 4470  ⟨cop 4570  ∪ cuni 4837   class class class wbr 5063   ↦ cmpt 5143   × cxp 5552  dom cdm 5554  ran crn 5555   ∘ ccom 5558   Fn wfn 6349  ⟶wf 6350  ‘cfv 6354  (class class class)co 7150  1st c1st 7683  2nd c2nd 7684  supcsup 8898  ℂcc 10529  ℝcr 10530  0cc0 10531  1c1 10532   + caddc 10534  +∞cpnf 10666  ℝ*cxr 10668   < clt 10669   ≤ cle 10670   − cmin 10864  ℕcn 11632  ℤ≥cuz 12237  ℝ+crp 12384  (,)cioo 12733  [,)cico 12735  [,]cicc 12736  ...cfz 12887  seqcseq 13364  abscabs 14588   ⇝ cli 14836  vol*covol 23997 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-oadd 8102  df-er 8284  df-map 8403  df-pm 8404  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-inf 8901  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-q 12343  df-rp 12385  df-ioo 12737  df-ico 12739  df-icc 12740  df-fz 12888  df-fzo 13029  df-fl 13157  df-seq 13365  df-exp 13425  df-hash 13686  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-rlim 14841  df-sum 15038  df-ovol 23999 This theorem is referenced by:  ioombl1  24097
 Copyright terms: Public domain W3C validator