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

Theorem ioombl1lem4 23242
 Description: Lemma for ioombl1 23243. (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 3813 . . . . 5 (𝐸𝐵) ⊆ 𝐸
21a1i 11 . . . 4 (𝜑 → (𝐸𝐵) ⊆ 𝐸)
3 ioombl1.e . . . 4 (𝜑𝐸 ⊆ ℝ)
4 ioombl1.v . . . 4 (𝜑 → (vol*‘𝐸) ∈ ℝ)
5 ovolsscl 23167 . . . 4 (((𝐸𝐵) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸𝐵)) ∈ ℝ)
62, 3, 4, 5syl3anc 1323 . . 3 (𝜑 → (vol*‘(𝐸𝐵)) ∈ ℝ)
7 difss 3717 . . . . 5 (𝐸𝐵) ⊆ 𝐸
87a1i 11 . . . 4 (𝜑 → (𝐸𝐵) ⊆ 𝐸)
9 ovolsscl 23167 . . . 4 (((𝐸𝐵) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸𝐵)) ∈ ℝ)
108, 3, 4, 9syl3anc 1323 . . 3 (𝜑 → (vol*‘(𝐸𝐵)) ∈ ℝ)
116, 10readdcld 10016 . 2 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ∈ ℝ)
12 ioombl1.b . . 3 𝐵 = (𝐴(,)+∞)
13 ioombl1.a . . 3 (𝜑𝐴 ∈ ℝ)
14 ioombl1.c . . 3 (𝜑𝐶 ∈ ℝ+)
15 ioombl1.s . . 3 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
16 ioombl1.t . . 3 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
17 ioombl1.u . . 3 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
18 ioombl1.f1 . . 3 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
19 ioombl1.f2 . . 3 (𝜑𝐸 ran ((,) ∘ 𝐹))
20 ioombl1.f3 . . 3 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
21 ioombl1.p . . 3 𝑃 = (1st ‘(𝐹𝑛))
22 ioombl1.q . . 3 𝑄 = (2nd ‘(𝐹𝑛))
23 ioombl1.g . . 3 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
24 ioombl1.h . . 3 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩)
2512, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24ioombl1lem2 23240 . 2 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
2614rpred 11819 . . 3 (𝜑𝐶 ∈ ℝ)
274, 26readdcld 10016 . 2 (𝜑 → ((vol*‘𝐸) + 𝐶) ∈ ℝ)
2812, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24ioombl1lem1 23239 . . . . . . . . 9 (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))))
2928simpld 475 . . . . . . . 8 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
30 eqid 2621 . . . . . . . . 9 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
3130, 16ovolsf 23154 . . . . . . . 8 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
3229, 31syl 17 . . . . . . 7 (𝜑𝑇:ℕ⟶(0[,)+∞))
33 frn 6012 . . . . . . 7 (𝑇:ℕ⟶(0[,)+∞) → ran 𝑇 ⊆ (0[,)+∞))
3432, 33syl 17 . . . . . 6 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
35 rge0ssre 12225 . . . . . 6 (0[,)+∞) ⊆ ℝ
3634, 35syl6ss 3596 . . . . 5 (𝜑 → ran 𝑇 ⊆ ℝ)
37 1nn 10978 . . . . . . . 8 1 ∈ ℕ
38 fdm 6010 . . . . . . . . 9 (𝑇:ℕ⟶(0[,)+∞) → dom 𝑇 = ℕ)
3932, 38syl 17 . . . . . . . 8 (𝜑 → dom 𝑇 = ℕ)
4037, 39syl5eleqr 2705 . . . . . . 7 (𝜑 → 1 ∈ dom 𝑇)
41 ne0i 3899 . . . . . . 7 (1 ∈ dom 𝑇 → dom 𝑇 ≠ ∅)
4240, 41syl 17 . . . . . 6 (𝜑 → dom 𝑇 ≠ ∅)
43 dm0rn0 5304 . . . . . . 7 (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
4443necon3bii 2842 . . . . . 6 (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
4542, 44sylib 208 . . . . 5 (𝜑 → ran 𝑇 ≠ ∅)
4632ffvelrnda 6317 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ (0[,)+∞))
4735, 46sseldi 3582 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ ℝ)
48 eqid 2621 . . . . . . . . . . . . 13 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
4948, 15ovolsf 23154 . . . . . . . . . . . 12 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
5018, 49syl 17 . . . . . . . . . . 11 (𝜑𝑆:ℕ⟶(0[,)+∞))
5150ffvelrnda 6317 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) ∈ (0[,)+∞))
5235, 51sseldi 3582 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) ∈ ℝ)
5325adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
54 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
55 nnuz 11670 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
5654, 55syl6eleq 2708 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
57 simpl 473 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝜑)
58 elfznn 12315 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
5930ovolfsf 23153 . . . . . . . . . . . . . . 15 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
6029, 59syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
6160ffvelrnda 6317 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞))
6235, 61sseldi 3582 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
6357, 58, 62syl2an 494 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
6448ovolfsf 23153 . . . . . . . . . . . . . . . 16 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
6518, 64syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
6665ffvelrnda 6317 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞))
67 elrege0 12223 . . . . . . . . . . . . . 14 ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
6866, 67sylib 208 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
6968simpld 475 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
7057, 58, 69syl2an 494 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
7128simprd 479 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
72 eqid 2621 . . . . . . . . . . . . . . . . . . 19 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
7372ovolfsf 23153 . . . . . . . . . . . . . . . . . 18 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
7471, 73syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
7574ffvelrnda 6317 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞))
76 elrege0 12223 . . . . . . . . . . . . . . . 16 ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
7775, 76sylib 208 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
7877simprd 479 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛))
7977simpld 475 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
8062, 79addge01d 10562 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
8178, 80mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
8212, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24ioombl1lem3 23241 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
8381, 82breqtrd 4641 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
8457, 58, 83syl2an 494 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
8556, 63, 70, 84serle 12799 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
8616fveq1i 6151 . . . . . . . . . 10 (𝑇𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗)
8715fveq1i 6151 . . . . . . . . . 10 (𝑆𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗)
8885, 86, 873brtr4g 4649 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ≤ (𝑆𝑗))
89 1zzd 11355 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℤ)
90 eqidd 2622 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
9168simprd 479 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
92 frn 6012 . . . . . . . . . . . . . . . . . . . . 21 (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
9350, 92syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
94 icossxr 12203 . . . . . . . . . . . . . . . . . . . 20 (0[,)+∞) ⊆ ℝ*
9593, 94syl6ss 3596 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran 𝑆 ⊆ ℝ*)
9695adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
97 ffn 6004 . . . . . . . . . . . . . . . . . . . 20 (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
9850, 97syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑆 Fn ℕ)
99 fnfvelrn 6314 . . . . . . . . . . . . . . . . . . 19 ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ran 𝑆)
10098, 99sylan 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ran 𝑆)
101 supxrub 12100 . . . . . . . . . . . . . . . . . 18 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆𝑘) ∈ ran 𝑆) → (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
10296, 100, 101syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
103102ralrimiva 2960 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
104 breq2 4619 . . . . . . . . . . . . . . . . . 18 (𝑥 = sup(ran 𝑆, ℝ*, < ) → ((𝑆𝑘) ≤ 𝑥 ↔ (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < )))
105104ralbidv 2980 . . . . . . . . . . . . . . . . 17 (𝑥 = sup(ran 𝑆, ℝ*, < ) → (∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < )))
106105rspcev 3295 . . . . . . . . . . . . . . . 16 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥)
10725, 103, 106syl2anc 692 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥)
10855, 15, 89, 90, 69, 91, 107isumsup2 14506 . . . . . . . . . . . . . 14 (𝜑𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
10993, 35syl6ss 3596 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝑆 ⊆ ℝ)
110 fdm 6010 . . . . . . . . . . . . . . . . . . 19 (𝑆:ℕ⟶(0[,)+∞) → dom 𝑆 = ℕ)
11150, 110syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom 𝑆 = ℕ)
11237, 111syl5eleqr 2705 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ dom 𝑆)
113 ne0i 3899 . . . . . . . . . . . . . . . . 17 (1 ∈ dom 𝑆 → dom 𝑆 ≠ ∅)
114112, 113syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝑆 ≠ ∅)
115 dm0rn0 5304 . . . . . . . . . . . . . . . . 17 (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
116115necon3bii 2842 . . . . . . . . . . . . . . . 16 (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
117114, 116sylib 208 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝑆 ≠ ∅)
118 breq1 4618 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑆𝑘) → (𝑧𝑥 ↔ (𝑆𝑘) ≤ 𝑥))
119118ralrn 6320 . . . . . . . . . . . . . . . . . 18 (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
12098, 119syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
121120rexbidv 3045 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
122107, 121mpbird 247 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥)
123 supxrre 12103 . . . . . . . . . . . . . . 15 ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
124109, 117, 122, 123syl3anc 1323 . . . . . . . . . . . . . 14 (𝜑 → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
125108, 124breqtrrd 4643 . . . . . . . . . . . . 13 (𝜑𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
126125adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
12715, 126syl5eqbrr 4651 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇝ sup(ran 𝑆, ℝ*, < ))
12869adantlr 750 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
12991adantlr 750 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
13055, 54, 127, 128, 129climserle 14330 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
13187, 130syl5eqbr 4650 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
13247, 52, 53, 88, 131letrd 10141 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
133132ralrimiva 2960 . . . . . . 7 (𝜑 → ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
134 breq2 4619 . . . . . . . . 9 (𝑥 = sup(ran 𝑆, ℝ*, < ) → ((𝑇𝑗) ≤ 𝑥 ↔ (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < )))
135134ralbidv 2980 . . . . . . . 8 (𝑥 = sup(ran 𝑆, ℝ*, < ) → (∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < )))
136135rspcev 3295 . . . . . . 7 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥)
13725, 133, 136syl2anc 692 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥)
138 ffn 6004 . . . . . . . . 9 (𝑇:ℕ⟶(0[,)+∞) → 𝑇 Fn ℕ)
13932, 138syl 17 . . . . . . . 8 (𝜑𝑇 Fn ℕ)
140 breq1 4618 . . . . . . . . 9 (𝑧 = (𝑇𝑗) → (𝑧𝑥 ↔ (𝑇𝑗) ≤ 𝑥))
141140ralrn 6320 . . . . . . . 8 (𝑇 Fn ℕ → (∀𝑧 ∈ ran 𝑇 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥))
142139, 141syl 17 . . . . . . 7 (𝜑 → (∀𝑧 ∈ ran 𝑇 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥))
143142rexbidv 3045 . . . . . 6 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥))
144137, 143mpbird 247 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥)
145 suprcl 10930 . . . . 5 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥) → sup(ran 𝑇, ℝ, < ) ∈ ℝ)
14636, 45, 144, 145syl3anc 1323 . . . 4 (𝜑 → sup(ran 𝑇, ℝ, < ) ∈ ℝ)
14772, 17ovolsf 23154 . . . . . . . 8 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
14871, 147syl 17 . . . . . . 7 (𝜑𝑈:ℕ⟶(0[,)+∞))
149 frn 6012 . . . . . . 7 (𝑈:ℕ⟶(0[,)+∞) → ran 𝑈 ⊆ (0[,)+∞))
150148, 149syl 17 . . . . . 6 (𝜑 → ran 𝑈 ⊆ (0[,)+∞))
151150, 35syl6ss 3596 . . . . 5 (𝜑 → ran 𝑈 ⊆ ℝ)
152 fdm 6010 . . . . . . . . 9 (𝑈:ℕ⟶(0[,)+∞) → dom 𝑈 = ℕ)
153148, 152syl 17 . . . . . . . 8 (𝜑 → dom 𝑈 = ℕ)
15437, 153syl5eleqr 2705 . . . . . . 7 (𝜑 → 1 ∈ dom 𝑈)
155 ne0i 3899 . . . . . . 7 (1 ∈ dom 𝑈 → dom 𝑈 ≠ ∅)
156154, 155syl 17 . . . . . 6 (𝜑 → dom 𝑈 ≠ ∅)
157 dm0rn0 5304 . . . . . . 7 (dom 𝑈 = ∅ ↔ ran 𝑈 = ∅)
158157necon3bii 2842 . . . . . 6 (dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅)
159156, 158sylib 208 . . . . 5 (𝜑 → ran 𝑈 ≠ ∅)
160148ffvelrnda 6317 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ∈ (0[,)+∞))
16135, 160sseldi 3582 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ∈ ℝ)
16257, 58, 79syl2an 494 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
163 elrege0 12223 . . . . . . . . . . . . . . . 16 ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
16461, 163sylib 208 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
165164simprd 479 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛))
16679, 62addge02d 10563 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
167165, 166mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
168167, 82breqtrd 4641 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
16957, 58, 168syl2an 494 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
17056, 162, 70, 169serle 12799 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
17117fveq1i 6151 . . . . . . . . . 10 (𝑈𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)
172170, 171, 873brtr4g 4649 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ≤ (𝑆𝑗))
173161, 52, 53, 172, 131letrd 10141 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
174173ralrimiva 2960 . . . . . . 7 (𝜑 → ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
175 breq2 4619 . . . . . . . . 9 (𝑥 = sup(ran 𝑆, ℝ*, < ) → ((𝑈𝑗) ≤ 𝑥 ↔ (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < )))
176175ralbidv 2980 . . . . . . . 8 (𝑥 = sup(ran 𝑆, ℝ*, < ) → (∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < )))
177176rspcev 3295 . . . . . . 7 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥)
17825, 174, 177syl2anc 692 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥)
179 ffn 6004 . . . . . . . . 9 (𝑈:ℕ⟶(0[,)+∞) → 𝑈 Fn ℕ)
180148, 179syl 17 . . . . . . . 8 (𝜑𝑈 Fn ℕ)
181 breq1 4618 . . . . . . . . 9 (𝑧 = (𝑈𝑗) → (𝑧𝑥 ↔ (𝑈𝑗) ≤ 𝑥))
182181ralrn 6320 . . . . . . . 8 (𝑈 Fn ℕ → (∀𝑧 ∈ ran 𝑈 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥))
183180, 182syl 17 . . . . . . 7 (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥))
184183rexbidv 3045 . . . . . 6 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥))
185178, 184mpbird 247 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥)
186 suprcl 10930 . . . . 5 ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥) → sup(ran 𝑈, ℝ, < ) ∈ ℝ)
187151, 159, 185, 186syl3anc 1323 . . . 4 (𝜑 → sup(ran 𝑈, ℝ, < ) ∈ ℝ)
188 ssralv 3647 . . . . . . . . . 10 ((𝐸𝐵) ⊆ 𝐸 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
1891, 188ax-mp 5 . . . . . . . . 9 (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
19021breq1i 4622 . . . . . . . . . . . . 13 (𝑃 < 𝑥 ↔ (1st ‘(𝐹𝑛)) < 𝑥)
191 ovolfcl 23148 . . . . . . . . . . . . . . . . . . 19 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
19218, 191sylan 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
193192simp1d 1071 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
19421, 193syl5eqel 2702 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
195194adantlr 750 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
1961, 3syl5ss 3595 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸𝐵) ⊆ ℝ)
197196sselda 3584 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐸𝐵)) → 𝑥 ∈ ℝ)
198197adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
199 ltle 10073 . . . . . . . . . . . . . . 15 ((𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑃 < 𝑥𝑃𝑥))
200195, 198, 199syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥𝑃𝑥))
201 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
202 opex 4895 . . . . . . . . . . . . . . . . . . . 20 ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V
20323fvmpt2 6250 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V) → (𝐺𝑛) = ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
204201, 202, 203sylancl 693 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
205204fveq2d 6154 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = (1st ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
20613adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
207206, 194ifcld 4105 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ)
208192simp2d 1072 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
20922, 208syl5eqel 2702 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
210207, 209ifcld 4105 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
211 op1stg 7128 . . . . . . . . . . . . . . . . . . 19 ((if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (1st ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
212210, 209, 211syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (1st ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
213205, 212eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
214213ad2ant2r 782 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (1st ‘(𝐺𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
215210ad2ant2r 782 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
216207ad2ant2r 782 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ)
217196ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (𝐸𝐵) ⊆ ℝ)
218 simplr 791 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑥 ∈ (𝐸𝐵))
219217, 218sseldd 3585 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑥 ∈ ℝ)
220209ad2ant2r 782 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑄 ∈ ℝ)
221 min1 11966 . . . . . . . . . . . . . . . . . 18 ((if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ ∧ 𝑄 ∈ ℝ) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃𝐴, 𝐴, 𝑃))
222216, 220, 221syl2anc 692 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃𝐴, 𝐴, 𝑃))
22313ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝐴 ∈ ℝ)
224 inss2 3814 . . . . . . . . . . . . . . . . . . . . . 22 (𝐸𝐵) ⊆ 𝐵
225224sseli 3580 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐸𝐵) → 𝑥𝐵)
226225ad2antlr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑥𝐵)
22713rexrd 10036 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐴 ∈ ℝ*)
228 pnfxr 10039 . . . . . . . . . . . . . . . . . . . . . . . 24 +∞ ∈ ℝ*
229 elioo2 12161 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞)))
230227, 228, 229sylancl 693 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞)))
23112eleq2i 2690 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝐵𝑥 ∈ (𝐴(,)+∞))
232 ltpnf 11901 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ → 𝑥 < +∞)
233232adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝑥 < +∞)
234233pm4.71i 663 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
235 df-3an 1038 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
236234, 235bitr4i 267 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞))
237230, 231, 2363bitr4g 303 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
238 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝐴 < 𝑥)
239237, 238syl6bi 243 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵𝐴 < 𝑥))
240239ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (𝑥𝐵𝐴 < 𝑥))
241226, 240mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝐴 < 𝑥)
242223, 219, 241ltled 10132 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝐴𝑥)
243 simprr 795 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑃𝑥)
244 breq1 4618 . . . . . . . . . . . . . . . . . . 19 (𝐴 = if(𝑃𝐴, 𝐴, 𝑃) → (𝐴𝑥 ↔ if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥))
245 breq1 4618 . . . . . . . . . . . . . . . . . . 19 (𝑃 = if(𝑃𝐴, 𝐴, 𝑃) → (𝑃𝑥 ↔ if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥))
246244, 245ifboth 4098 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑥𝑃𝑥) → if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥)
247242, 243, 246syl2anc 692 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥)
248215, 216, 219, 222, 247letrd 10141 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑥)
249214, 248eqbrtrd 4637 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (1st ‘(𝐺𝑛)) ≤ 𝑥)
250249expr 642 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃𝑥 → (1st ‘(𝐺𝑛)) ≤ 𝑥))
251200, 250syld 47 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → (1st ‘(𝐺𝑛)) ≤ 𝑥))
252190, 251syl5bir 233 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < 𝑥 → (1st ‘(𝐺𝑛)) ≤ 𝑥))
25322breq2i 4623 . . . . . . . . . . . . . 14 (𝑥 < 𝑄𝑥 < (2nd ‘(𝐹𝑛)))
254209adantlr 750 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
255 ltle 10073 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑄 ∈ ℝ) → (𝑥 < 𝑄𝑥𝑄))
256198, 254, 255syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄𝑥𝑄))
257253, 256syl5bir 233 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹𝑛)) → 𝑥𝑄))
258204fveq2d 6154 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
259 op2ndg 7129 . . . . . . . . . . . . . . . . 17 ((if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (2nd ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
260210, 209, 259syl2anc 692 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (2nd ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
261258, 260eqtrd 2655 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = 𝑄)
262261adantlr 750 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = 𝑄)
263262breq2d 4627 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ (2nd ‘(𝐺𝑛)) ↔ 𝑥𝑄))
264257, 263sylibrd 249 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹𝑛)) → 𝑥 ≤ (2nd ‘(𝐺𝑛))))
265252, 264anim12d 585 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
266265reximdva 3011 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐸𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
267266ralimdva 2956 . . . . . . . . 9 (𝜑 → (∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
268189, 267syl5 34 . . . . . . . 8 (𝜑 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
269 ovolfioo 23149 . . . . . . . . 9 ((𝐸 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐸 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
2703, 18, 269syl2anc 692 . . . . . . . 8 (𝜑 → (𝐸 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
271 ovolficc 23150 . . . . . . . . 9 (((𝐸𝐵) ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
272196, 29, 271syl2anc 692 . . . . . . . 8 (𝜑 → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
273268, 270, 2723imtr4d 283 . . . . . . 7 (𝜑 → (𝐸 ran ((,) ∘ 𝐹) → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐺)))
27419, 273mpd 15 . . . . . 6 (𝜑 → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐺))
27516ovollb2 23170 . . . . . 6 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸𝐵) ⊆ ran ([,] ∘ 𝐺)) → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
27629, 274, 275syl2anc 692 . . . . 5 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
277 supxrre 12103 . . . . . 6 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥) → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
27836, 45, 144, 277syl3anc 1323 . . . . 5 (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
279276, 278breqtrd 4641 . . . 4 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑇, ℝ, < ))
280 ssralv 3647 . . . . . . . . . 10 ((𝐸𝐵) ⊆ 𝐸 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
2817, 280ax-mp 5 . . . . . . . . 9 (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
282194adantlr 750 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
2837, 3syl5ss 3595 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸𝐵) ⊆ ℝ)
284283sselda 3584 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐸𝐵)) → 𝑥 ∈ ℝ)
285284adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
286282, 285, 199syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥𝑃𝑥))
287190, 286syl5bir 233 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < 𝑥𝑃𝑥))
288 opex 4895 . . . . . . . . . . . . . . . . . 18 𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V
28924fvmpt2 6250 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V) → (𝐻𝑛) = ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩)
290201, 288, 289sylancl 693 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐻𝑛) = ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩)
291290fveq2d 6154 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐻𝑛)) = (1st ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩))
292 op1stg 7128 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℝ ∧ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (1st ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
293194, 210, 292syl2anc 692 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (1st ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
294291, 293eqtrd 2655 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐻𝑛)) = 𝑃)
295294adantlr 750 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻𝑛)) = 𝑃)
296295breq1d 4625 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑃𝑥))
297287, 296sylibrd 249 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < 𝑥 → (1st ‘(𝐻𝑛)) ≤ 𝑥))
298209adantlr 750 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
299285, 298, 255syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄𝑥𝑄))
300283ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝐸𝐵) ⊆ ℝ)
301 simplr 791 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ∈ (𝐸𝐵))
302300, 301sseldd 3585 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ∈ ℝ)
30313ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝐴 ∈ ℝ)
304194ad2ant2r 782 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑃 ∈ ℝ)
305303, 304ifcld 4105 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ)
306 eldifn 3713 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐸𝐵) → ¬ 𝑥𝐵)
307306ad2antlr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → ¬ 𝑥𝐵)
308302biantrurd 529 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝐴 < 𝑥 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
309237ad2antrr 761 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝑥𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
310308, 309bitr4d 271 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝐴 < 𝑥𝑥𝐵))
311307, 310mtbird 315 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → ¬ 𝐴 < 𝑥)
312302, 303lenltd 10130 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝑥𝐴 ↔ ¬ 𝐴 < 𝑥))
313311, 312mpbird 247 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥𝐴)
314 max2 11964 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ if(𝑃𝐴, 𝐴, 𝑃))
315304, 303, 314syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝐴 ≤ if(𝑃𝐴, 𝐴, 𝑃))
316302, 303, 305, 313, 315letrd 10141 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ≤ if(𝑃𝐴, 𝐴, 𝑃))
317 simprr 795 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥𝑄)
318 breq2 4619 . . . . . . . . . . . . . . . . . 18 (if(𝑃𝐴, 𝐴, 𝑃) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ if(𝑃𝐴, 𝐴, 𝑃) ↔ 𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)))
319 breq2 4619 . . . . . . . . . . . . . . . . . 18 (𝑄 = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) → (𝑥𝑄𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)))
320318, 319ifboth 4098 . . . . . . . . . . . . . . . . 17 ((𝑥 ≤ if(𝑃𝐴, 𝐴, 𝑃) ∧ 𝑥𝑄) → 𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
321316, 317, 320syl2anc 692 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
322290fveq2d 6154 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐻𝑛)) = (2nd ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩))
323 op2ndg 7129 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℝ ∧ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (2nd ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
324194, 210, 323syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (2nd ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
325322, 324eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐻𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
326325ad2ant2r 782 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (2nd ‘(𝐻𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
327321, 326breqtrrd 4643 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ≤ (2nd ‘(𝐻𝑛)))
328327expr 642 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥𝑄𝑥 ≤ (2nd ‘(𝐻𝑛))))
329299, 328syld 47 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄𝑥 ≤ (2nd ‘(𝐻𝑛))))
330253, 329syl5bir 233 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹𝑛)) → 𝑥 ≤ (2nd ‘(𝐻𝑛))))
331297, 330anim12d 585 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
332331reximdva 3011 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐸𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
333332ralimdva 2956 . . . . . . . . 9 (𝜑 → (∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
334281, 333syl5 34 . . . . . . . 8 (𝜑 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
335 ovolficc 23150 . . . . . . . . 9 (((𝐸𝐵) ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
336283, 71, 335syl2anc 692 . . . . . . . 8 (𝜑 → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
337334, 270, 3363imtr4d 283 . . . . . . 7 (𝜑 → (𝐸 ran ((,) ∘ 𝐹) → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐻)))
33819, 337mpd 15 . . . . . 6 (𝜑 → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐻))
33917ovollb2 23170 . . . . . 6 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸𝐵) ⊆ ran ([,] ∘ 𝐻)) → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
34071, 338, 339syl2anc 692 . . . . 5 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
341 supxrre 12103 . . . . . 6 ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥) → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
342151, 159, 185, 341syl3anc 1323 . . . . 5 (𝜑 → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
343340, 342breqtrd 4641 . . . 4 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑈, ℝ, < ))
3446, 10, 146, 187, 279, 343le2addd 10593 . . 3 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ≤ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
345 eqidd 2622 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐺)‘𝑛))
34655, 16, 89, 345, 62, 165, 137isumsup2 14506 . . . . 5 (𝜑𝑇 ⇝ sup(ran 𝑇, ℝ, < ))
347 seqex 12746 . . . . . . 7 seq1( + , ((abs ∘ − ) ∘ 𝐹)) ∈ V
34815, 347eqeltri 2694 . . . . . 6 𝑆 ∈ V
349348a1i 11 . . . . 5 (𝜑𝑆 ∈ V)
350 eqidd 2622 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) = (((abs ∘ − ) ∘ 𝐻)‘𝑛))
35155, 17, 89, 350, 79, 78, 178isumsup2 14506 . . . . 5 (𝜑𝑈 ⇝ sup(ran 𝑈, ℝ, < ))
35247recnd 10015 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ ℂ)
353161recnd 10015 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ∈ ℂ)
35462recnd 10015 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
35557, 58, 354syl2an 494 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
35679recnd 10015 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
35757, 58, 356syl2an 494 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
35882eqcomd 2627 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
35957, 58, 358syl2an 494 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
36056, 355, 357, 359seradd 12786 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)))
36186, 171oveq12i 6619 . . . . . 6 ((𝑇𝑗) + (𝑈𝑗)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗))
362360, 87, 3613eqtr4g 2680 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) = ((𝑇𝑗) + (𝑈𝑗)))
36355, 89, 346, 349, 351, 352, 353, 362climadd 14299 . . . 4 (𝜑𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
364 climuni 14220 . . . 4 ((𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) ∧ 𝑆 ⇝ sup(ran 𝑆, ℝ*, < )) → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
365363, 125, 364syl2anc 692 . . 3 (𝜑 → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
366344, 365breqtrd 4641 . 2 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ≤ sup(ran 𝑆, ℝ*, < ))
36711, 25, 27, 366, 20letrd 10141 1 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ≤ ((vol*‘𝐸) + 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  ∃wrex 2908  Vcvv 3186   ∖ cdif 3553   ∩ cin 3555   ⊆ wss 3556  ∅c0 3893  ifcif 4060  ⟨cop 4156  ∪ cuni 4404   class class class wbr 4615   ↦ cmpt 4675   × cxp 5074  dom cdm 5076  ran crn 5077   ∘ ccom 5080   Fn wfn 5844  ⟶wf 5845  ‘cfv 5849  (class class class)co 6607  1st c1st 7114  2nd c2nd 7115  supcsup 8293  ℂcc 9881  ℝcr 9882  0cc0 9883  1c1 9884   + caddc 9886  +∞cpnf 10018  ℝ*cxr 10020   < clt 10021   ≤ cle 10022   − cmin 10213  ℕcn 10967  ℤ≥cuz 11634  ℝ+crp 11779  (,)cioo 12120  [,)cico 12122  [,]cicc 12123  ...cfz 12271  seqcseq 12744  abscabs 13911   ⇝ cli 14152  vol*covol 23144 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-inf2 8485  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-pre-sup 9961 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-se 5036  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-isom 5858  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-oadd 7512  df-er 7690  df-map 7807  df-pm 7808  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-sup 8295  df-inf 8296  df-oi 8362  df-card 8712  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-nn 10968  df-2 11026  df-3 11027  df-n0 11240  df-z 11325  df-uz 11635  df-q 11736  df-rp 11780  df-ioo 12124  df-ico 12126  df-icc 12127  df-fz 12272  df-fzo 12410  df-fl 12536  df-seq 12745  df-exp 12804  df-hash 13061  df-cj 13776  df-re 13777  df-im 13778  df-sqrt 13912  df-abs 13913  df-clim 14156  df-rlim 14157  df-sum 14354  df-ovol 23146 This theorem is referenced by:  ioombl1  23243
 Copyright terms: Public domain W3C validator