MPE Home 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