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

Theorem ioombl1lem4 23375
Description: Lemma for ioombl1 23376. (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 3866 . . . . 5 (𝐸𝐵) ⊆ 𝐸
21a1i 11 . . . 4 (𝜑 → (𝐸𝐵) ⊆ 𝐸)
3 ioombl1.e . . . 4 (𝜑𝐸 ⊆ ℝ)
4 ioombl1.v . . . 4 (𝜑 → (vol*‘𝐸) ∈ ℝ)
5 ovolsscl 23300 . . . 4 (((𝐸𝐵) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸𝐵)) ∈ ℝ)
62, 3, 4, 5syl3anc 1366 . . 3 (𝜑 → (vol*‘(𝐸𝐵)) ∈ ℝ)
7 difss 3770 . . . . 5 (𝐸𝐵) ⊆ 𝐸
87a1i 11 . . . 4 (𝜑 → (𝐸𝐵) ⊆ 𝐸)
9 ovolsscl 23300 . . . 4 (((𝐸𝐵) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸𝐵)) ∈ ℝ)
108, 3, 4, 9syl3anc 1366 . . 3 (𝜑 → (vol*‘(𝐸𝐵)) ∈ ℝ)
116, 10readdcld 10107 . 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 23373 . 2 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
2614rpred 11910 . . 3 (𝜑𝐶 ∈ ℝ)
274, 26readdcld 10107 . 2 (𝜑 → ((vol*‘𝐸) + 𝐶) ∈ ℝ)
2812, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24ioombl1lem1 23372 . . . . . . . . 9 (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))))
2928simpld 474 . . . . . . . 8 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
30 eqid 2651 . . . . . . . . 9 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
3130, 16ovolsf 23287 . . . . . . . 8 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
3229, 31syl 17 . . . . . . 7 (𝜑𝑇:ℕ⟶(0[,)+∞))
33 frn 6091 . . . . . . 7 (𝑇:ℕ⟶(0[,)+∞) → ran 𝑇 ⊆ (0[,)+∞))
3432, 33syl 17 . . . . . 6 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
35 rge0ssre 12318 . . . . . 6 (0[,)+∞) ⊆ ℝ
3634, 35syl6ss 3648 . . . . 5 (𝜑 → ran 𝑇 ⊆ ℝ)
37 1nn 11069 . . . . . . . 8 1 ∈ ℕ
38 fdm 6089 . . . . . . . . 9 (𝑇:ℕ⟶(0[,)+∞) → dom 𝑇 = ℕ)
3932, 38syl 17 . . . . . . . 8 (𝜑 → dom 𝑇 = ℕ)
4037, 39syl5eleqr 2737 . . . . . . 7 (𝜑 → 1 ∈ dom 𝑇)
41 ne0i 3954 . . . . . . 7 (1 ∈ dom 𝑇 → dom 𝑇 ≠ ∅)
4240, 41syl 17 . . . . . 6 (𝜑 → dom 𝑇 ≠ ∅)
43 dm0rn0 5374 . . . . . . 7 (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
4443necon3bii 2875 . . . . . 6 (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
4542, 44sylib 208 . . . . 5 (𝜑 → ran 𝑇 ≠ ∅)
4632ffvelrnda 6399 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ (0[,)+∞))
4735, 46sseldi 3634 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ ℝ)
48 eqid 2651 . . . . . . . . . . . . 13 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
4948, 15ovolsf 23287 . . . . . . . . . . . 12 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
5018, 49syl 17 . . . . . . . . . . 11 (𝜑𝑆:ℕ⟶(0[,)+∞))
5150ffvelrnda 6399 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) ∈ (0[,)+∞))
5235, 51sseldi 3634 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) ∈ ℝ)
5325adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
54 simpr 476 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
55 nnuz 11761 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
5654, 55syl6eleq 2740 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
57 simpl 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝜑)
58 elfznn 12408 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
5930ovolfsf 23286 . . . . . . . . . . . . . . 15 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
6029, 59syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
6160ffvelrnda 6399 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞))
6235, 61sseldi 3634 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
6357, 58, 62syl2an 493 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
6448ovolfsf 23286 . . . . . . . . . . . . . . . 16 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
6518, 64syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
6665ffvelrnda 6399 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞))
67 elrege0 12316 . . . . . . . . . . . . . 14 ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
6866, 67sylib 208 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
6968simpld 474 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
7057, 58, 69syl2an 493 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
7128simprd 478 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
72 eqid 2651 . . . . . . . . . . . . . . . . . . 19 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
7372ovolfsf 23286 . . . . . . . . . . . . . . . . . 18 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
7471, 73syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
7574ffvelrnda 6399 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞))
76 elrege0 12316 . . . . . . . . . . . . . . . 16 ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
7775, 76sylib 208 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
7877simprd 478 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛))
7977simpld 474 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
8062, 79addge01d 10653 . . . . . . . . . . . . . 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 23374 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
8381, 82breqtrd 4711 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
8457, 58, 83syl2an 493 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
8556, 63, 70, 84serle 12896 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
8616fveq1i 6230 . . . . . . . . . 10 (𝑇𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗)
8715fveq1i 6230 . . . . . . . . . 10 (𝑆𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗)
8885, 86, 873brtr4g 4719 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ≤ (𝑆𝑗))
89 1zzd 11446 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℤ)
90 eqidd 2652 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
9168simprd 478 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
92 frn 6091 . . . . . . . . . . . . . . . . . . . . 21 (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
9350, 92syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
94 icossxr 12296 . . . . . . . . . . . . . . . . . . . 20 (0[,)+∞) ⊆ ℝ*
9593, 94syl6ss 3648 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran 𝑆 ⊆ ℝ*)
9695adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
97 ffn 6083 . . . . . . . . . . . . . . . . . . . 20 (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
9850, 97syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑆 Fn ℕ)
99 fnfvelrn 6396 . . . . . . . . . . . . . . . . . . 19 ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ran 𝑆)
10098, 99sylan 487 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ran 𝑆)
101 supxrub 12192 . . . . . . . . . . . . . . . . . 18 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆𝑘) ∈ ran 𝑆) → (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
10296, 100, 101syl2anc 694 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
103102ralrimiva 2995 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
104 breq2 4689 . . . . . . . . . . . . . . . . . 18 (𝑥 = sup(ran 𝑆, ℝ*, < ) → ((𝑆𝑘) ≤ 𝑥 ↔ (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < )))
105104ralbidv 3015 . . . . . . . . . . . . . . . . 17 (𝑥 = sup(ran 𝑆, ℝ*, < ) → (∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < )))
106105rspcev 3340 . . . . . . . . . . . . . . . 16 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥)
10725, 103, 106syl2anc 694 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥)
10855, 15, 89, 90, 69, 91, 107isumsup2 14622 . . . . . . . . . . . . . 14 (𝜑𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
10993, 35syl6ss 3648 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝑆 ⊆ ℝ)
110 fdm 6089 . . . . . . . . . . . . . . . . . . 19 (𝑆:ℕ⟶(0[,)+∞) → dom 𝑆 = ℕ)
11150, 110syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom 𝑆 = ℕ)
11237, 111syl5eleqr 2737 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ dom 𝑆)
113 ne0i 3954 . . . . . . . . . . . . . . . . 17 (1 ∈ dom 𝑆 → dom 𝑆 ≠ ∅)
114112, 113syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝑆 ≠ ∅)
115 dm0rn0 5374 . . . . . . . . . . . . . . . . 17 (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
116115necon3bii 2875 . . . . . . . . . . . . . . . 16 (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
117114, 116sylib 208 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝑆 ≠ ∅)
118 breq1 4688 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑆𝑘) → (𝑧𝑥 ↔ (𝑆𝑘) ≤ 𝑥))
119118ralrn 6402 . . . . . . . . . . . . . . . . . 18 (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
12098, 119syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
121120rexbidv 3081 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
122107, 121mpbird 247 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥)
123 supxrre 12195 . . . . . . . . . . . . . . 15 ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
124109, 117, 122, 123syl3anc 1366 . . . . . . . . . . . . . 14 (𝜑 → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
125108, 124breqtrrd 4713 . . . . . . . . . . . . 13 (𝜑𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
126125adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
12715, 126syl5eqbrr 4721 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇝ sup(ran 𝑆, ℝ*, < ))
12869adantlr 751 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
12991adantlr 751 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
13055, 54, 127, 128, 129climserle 14437 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
13187, 130syl5eqbr 4720 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
13247, 52, 53, 88, 131letrd 10232 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
133132ralrimiva 2995 . . . . . . 7 (𝜑 → ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
134 breq2 4689 . . . . . . . . 9 (𝑥 = sup(ran 𝑆, ℝ*, < ) → ((𝑇𝑗) ≤ 𝑥 ↔ (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < )))
135134ralbidv 3015 . . . . . . . 8 (𝑥 = sup(ran 𝑆, ℝ*, < ) → (∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < )))
136135rspcev 3340 . . . . . . 7 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥)
13725, 133, 136syl2anc 694 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥)
138 ffn 6083 . . . . . . . . 9 (𝑇:ℕ⟶(0[,)+∞) → 𝑇 Fn ℕ)
13932, 138syl 17 . . . . . . . 8 (𝜑𝑇 Fn ℕ)
140 breq1 4688 . . . . . . . . 9 (𝑧 = (𝑇𝑗) → (𝑧𝑥 ↔ (𝑇𝑗) ≤ 𝑥))
141140ralrn 6402 . . . . . . . 8 (𝑇 Fn ℕ → (∀𝑧 ∈ ran 𝑇 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥))
142139, 141syl 17 . . . . . . 7 (𝜑 → (∀𝑧 ∈ ran 𝑇 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥))
143142rexbidv 3081 . . . . . 6 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇𝑗) ≤ 𝑥))
144137, 143mpbird 247 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥)
145 suprcl 11021 . . . . 5 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥) → sup(ran 𝑇, ℝ, < ) ∈ ℝ)
14636, 45, 144, 145syl3anc 1366 . . . 4 (𝜑 → sup(ran 𝑇, ℝ, < ) ∈ ℝ)
14772, 17ovolsf 23287 . . . . . . . 8 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
14871, 147syl 17 . . . . . . 7 (𝜑𝑈:ℕ⟶(0[,)+∞))
149 frn 6091 . . . . . . 7 (𝑈:ℕ⟶(0[,)+∞) → ran 𝑈 ⊆ (0[,)+∞))
150148, 149syl 17 . . . . . 6 (𝜑 → ran 𝑈 ⊆ (0[,)+∞))
151150, 35syl6ss 3648 . . . . 5 (𝜑 → ran 𝑈 ⊆ ℝ)
152 fdm 6089 . . . . . . . . 9 (𝑈:ℕ⟶(0[,)+∞) → dom 𝑈 = ℕ)
153148, 152syl 17 . . . . . . . 8 (𝜑 → dom 𝑈 = ℕ)
15437, 153syl5eleqr 2737 . . . . . . 7 (𝜑 → 1 ∈ dom 𝑈)
155 ne0i 3954 . . . . . . 7 (1 ∈ dom 𝑈 → dom 𝑈 ≠ ∅)
156154, 155syl 17 . . . . . 6 (𝜑 → dom 𝑈 ≠ ∅)
157 dm0rn0 5374 . . . . . . 7 (dom 𝑈 = ∅ ↔ ran 𝑈 = ∅)
158157necon3bii 2875 . . . . . 6 (dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅)
159156, 158sylib 208 . . . . 5 (𝜑 → ran 𝑈 ≠ ∅)
160148ffvelrnda 6399 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ∈ (0[,)+∞))
16135, 160sseldi 3634 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ∈ ℝ)
16257, 58, 79syl2an 493 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
163 elrege0 12316 . . . . . . . . . . . . . . . 16 ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
16461, 163sylib 208 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
165164simprd 478 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛))
16679, 62addge02d 10654 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
167165, 166mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
168167, 82breqtrd 4711 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
16957, 58, 168syl2an 493 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
17056, 162, 70, 169serle 12896 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
17117fveq1i 6230 . . . . . . . . . 10 (𝑈𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)
172170, 171, 873brtr4g 4719 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ≤ (𝑆𝑗))
173161, 52, 53, 172, 131letrd 10232 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
174173ralrimiva 2995 . . . . . . 7 (𝜑 → ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
175 breq2 4689 . . . . . . . . 9 (𝑥 = sup(ran 𝑆, ℝ*, < ) → ((𝑈𝑗) ≤ 𝑥 ↔ (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < )))
176175ralbidv 3015 . . . . . . . 8 (𝑥 = sup(ran 𝑆, ℝ*, < ) → (∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < )))
177176rspcev 3340 . . . . . . 7 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥)
17825, 174, 177syl2anc 694 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥)
179 ffn 6083 . . . . . . . . 9 (𝑈:ℕ⟶(0[,)+∞) → 𝑈 Fn ℕ)
180148, 179syl 17 . . . . . . . 8 (𝜑𝑈 Fn ℕ)
181 breq1 4688 . . . . . . . . 9 (𝑧 = (𝑈𝑗) → (𝑧𝑥 ↔ (𝑈𝑗) ≤ 𝑥))
182181ralrn 6402 . . . . . . . 8 (𝑈 Fn ℕ → (∀𝑧 ∈ ran 𝑈 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥))
183180, 182syl 17 . . . . . . 7 (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥))
184183rexbidv 3081 . . . . . 6 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈𝑗) ≤ 𝑥))
185178, 184mpbird 247 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥)
186 suprcl 11021 . . . . 5 ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥) → sup(ran 𝑈, ℝ, < ) ∈ ℝ)
187151, 159, 185, 186syl3anc 1366 . . . 4 (𝜑 → sup(ran 𝑈, ℝ, < ) ∈ ℝ)
188 ssralv 3699 . . . . . . . . . 10 ((𝐸𝐵) ⊆ 𝐸 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
1891, 188ax-mp 5 . . . . . . . . 9 (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
19021breq1i 4692 . . . . . . . . . . . . 13 (𝑃 < 𝑥 ↔ (1st ‘(𝐹𝑛)) < 𝑥)
191 ovolfcl 23281 . . . . . . . . . . . . . . . . . . 19 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
19218, 191sylan 487 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
193192simp1d 1093 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
19421, 193syl5eqel 2734 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
195194adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
1961, 3syl5ss 3647 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸𝐵) ⊆ ℝ)
197196sselda 3636 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐸𝐵)) → 𝑥 ∈ ℝ)
198197adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
199 ltle 10164 . . . . . . . . . . . . . . 15 ((𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑃 < 𝑥𝑃𝑥))
200195, 198, 199syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥𝑃𝑥))
201 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
202 opex 4962 . . . . . . . . . . . . . . . . . . . 20 ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V
20323fvmpt2 6330 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V) → (𝐺𝑛) = ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
204201, 202, 203sylancl 695 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = ⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
205204fveq2d 6233 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = (1st ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
20613adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
207206, 194ifcld 4164 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ)
208192simp2d 1094 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
20922, 208syl5eqel 2734 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
210207, 209ifcld 4164 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
211 op1stg 7222 . . . . . . . . . . . . . . . . . . 19 ((if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (1st ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
212210, 209, 211syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (1st ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
213205, 212eqtrd 2685 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
214213ad2ant2r 798 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (1st ‘(𝐺𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
215210ad2ant2r 798 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
216207ad2ant2r 798 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ)
217196ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (𝐸𝐵) ⊆ ℝ)
218 simplr 807 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑥 ∈ (𝐸𝐵))
219217, 218sseldd 3637 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑥 ∈ ℝ)
220209ad2ant2r 798 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑄 ∈ ℝ)
221 min1 12058 . . . . . . . . . . . . . . . . . 18 ((if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ ∧ 𝑄 ∈ ℝ) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃𝐴, 𝐴, 𝑃))
222216, 220, 221syl2anc 694 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃𝐴, 𝐴, 𝑃))
22313ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝐴 ∈ ℝ)
224 inss2 3867 . . . . . . . . . . . . . . . . . . . . . 22 (𝐸𝐵) ⊆ 𝐵
225224sseli 3632 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐸𝐵) → 𝑥𝐵)
226225ad2antlr 763 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑥𝐵)
22713rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐴 ∈ ℝ*)
228 pnfxr 10130 . . . . . . . . . . . . . . . . . . . . . . . 24 +∞ ∈ ℝ*
229 elioo2 12254 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞)))
230227, 228, 229sylancl 695 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞)))
23112eleq2i 2722 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝐵𝑥 ∈ (𝐴(,)+∞))
232 ltpnf 11992 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ → 𝑥 < +∞)
233232adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝑥 < +∞)
234233pm4.71i 665 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
235 df-3an 1056 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
236234, 235bitr4i 267 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥𝑥 < +∞))
237230, 231, 2363bitr4g 303 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
238 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝐴 < 𝑥)
239237, 238syl6bi 243 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵𝐴 < 𝑥))
240239ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (𝑥𝐵𝐴 < 𝑥))
241226, 240mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝐴 < 𝑥)
242223, 219, 241ltled 10223 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝐴𝑥)
243 simprr 811 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → 𝑃𝑥)
244 breq1 4688 . . . . . . . . . . . . . . . . . . 19 (𝐴 = if(𝑃𝐴, 𝐴, 𝑃) → (𝐴𝑥 ↔ if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥))
245 breq1 4688 . . . . . . . . . . . . . . . . . . 19 (𝑃 = if(𝑃𝐴, 𝐴, 𝑃) → (𝑃𝑥 ↔ if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥))
246244, 245ifboth 4157 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑥𝑃𝑥) → if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥)
247242, 243, 246syl2anc 694 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑥)
248215, 216, 219, 222, 247letrd 10232 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑥)
249214, 248eqbrtrd 4707 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃𝑥)) → (1st ‘(𝐺𝑛)) ≤ 𝑥)
250249expr 642 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃𝑥 → (1st ‘(𝐺𝑛)) ≤ 𝑥))
251200, 250syld 47 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → (1st ‘(𝐺𝑛)) ≤ 𝑥))
252190, 251syl5bir 233 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < 𝑥 → (1st ‘(𝐺𝑛)) ≤ 𝑥))
25322breq2i 4693 . . . . . . . . . . . . . 14 (𝑥 < 𝑄𝑥 < (2nd ‘(𝐹𝑛)))
254209adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
255 ltle 10164 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑄 ∈ ℝ) → (𝑥 < 𝑄𝑥𝑄))
256198, 254, 255syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄𝑥𝑄))
257253, 256syl5bir 233 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹𝑛)) → 𝑥𝑄))
258204fveq2d 6233 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
259 op2ndg 7223 . . . . . . . . . . . . . . . . 17 ((if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (2nd ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
260210, 209, 259syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (2nd ‘⟨if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
261258, 260eqtrd 2685 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = 𝑄)
262261adantlr 751 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = 𝑄)
263262breq2d 4697 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ (2nd ‘(𝐺𝑛)) ↔ 𝑥𝑄))
264257, 263sylibrd 249 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹𝑛)) → 𝑥 ≤ (2nd ‘(𝐺𝑛))))
265252, 264anim12d 585 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
266265reximdva 3046 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐸𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
267266ralimdva 2991 . . . . . . . . 9 (𝜑 → (∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
268189, 267syl5 34 . . . . . . . 8 (𝜑 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
269 ovolfioo 23282 . . . . . . . . 9 ((𝐸 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐸 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
2703, 18, 269syl2anc 694 . . . . . . . 8 (𝜑 → (𝐸 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
271 ovolficc 23283 . . . . . . . . 9 (((𝐸𝐵) ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
272196, 29, 271syl2anc 694 . . . . . . . 8 (𝜑 → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
273268, 270, 2723imtr4d 283 . . . . . . 7 (𝜑 → (𝐸 ran ((,) ∘ 𝐹) → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐺)))
27419, 273mpd 15 . . . . . 6 (𝜑 → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐺))
27516ovollb2 23303 . . . . . 6 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸𝐵) ⊆ ran ([,] ∘ 𝐺)) → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
27629, 274, 275syl2anc 694 . . . . 5 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
277 supxrre 12195 . . . . . 6 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧𝑥) → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
27836, 45, 144, 277syl3anc 1366 . . . . 5 (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
279276, 278breqtrd 4711 . . . 4 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑇, ℝ, < ))
280 ssralv 3699 . . . . . . . . . 10 ((𝐸𝐵) ⊆ 𝐸 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
2817, 280ax-mp 5 . . . . . . . . 9 (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
282194adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
2837, 3syl5ss 3647 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸𝐵) ⊆ ℝ)
284283sselda 3636 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐸𝐵)) → 𝑥 ∈ ℝ)
285284adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
286282, 285, 199syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥𝑃𝑥))
287190, 286syl5bir 233 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < 𝑥𝑃𝑥))
288 opex 4962 . . . . . . . . . . . . . . . . . 18 𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V
28924fvmpt2 6330 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V) → (𝐻𝑛) = ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩)
290201, 288, 289sylancl 695 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐻𝑛) = ⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩)
291290fveq2d 6233 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐻𝑛)) = (1st ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩))
292 op1stg 7222 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℝ ∧ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (1st ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
293194, 210, 292syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (1st ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
294291, 293eqtrd 2685 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐻𝑛)) = 𝑃)
295294adantlr 751 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻𝑛)) = 𝑃)
296295breq1d 4695 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑃𝑥))
297287, 296sylibrd 249 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < 𝑥 → (1st ‘(𝐻𝑛)) ≤ 𝑥))
298209adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
299285, 298, 255syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄𝑥𝑄))
300283ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝐸𝐵) ⊆ ℝ)
301 simplr 807 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ∈ (𝐸𝐵))
302300, 301sseldd 3637 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ∈ ℝ)
30313ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝐴 ∈ ℝ)
304194ad2ant2r 798 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑃 ∈ ℝ)
305303, 304ifcld 4164 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → if(𝑃𝐴, 𝐴, 𝑃) ∈ ℝ)
306 eldifn 3766 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐸𝐵) → ¬ 𝑥𝐵)
307306ad2antlr 763 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → ¬ 𝑥𝐵)
308302biantrurd 528 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝐴 < 𝑥 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
309237ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝑥𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
310308, 309bitr4d 271 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝐴 < 𝑥𝑥𝐵))
311307, 310mtbird 314 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → ¬ 𝐴 < 𝑥)
312302, 303lenltd 10221 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (𝑥𝐴 ↔ ¬ 𝐴 < 𝑥))
313311, 312mpbird 247 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥𝐴)
314 max2 12056 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ if(𝑃𝐴, 𝐴, 𝑃))
315304, 303, 314syl2anc 694 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝐴 ≤ if(𝑃𝐴, 𝐴, 𝑃))
316302, 303, 305, 313, 315letrd 10232 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ≤ if(𝑃𝐴, 𝐴, 𝑃))
317 simprr 811 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥𝑄)
318 breq2 4689 . . . . . . . . . . . . . . . . . 18 (if(𝑃𝐴, 𝐴, 𝑃) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ if(𝑃𝐴, 𝐴, 𝑃) ↔ 𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)))
319 breq2 4689 . . . . . . . . . . . . . . . . . 18 (𝑄 = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) → (𝑥𝑄𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)))
320318, 319ifboth 4157 . . . . . . . . . . . . . . . . 17 ((𝑥 ≤ if(𝑃𝐴, 𝐴, 𝑃) ∧ 𝑥𝑄) → 𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
321316, 317, 320syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → 𝑥 ≤ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
322290fveq2d 6233 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐻𝑛)) = (2nd ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩))
323 op2ndg 7223 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℝ ∧ if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (2nd ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
324194, 210, 323syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (2nd ‘⟨𝑃, if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
325322, 324eqtrd 2685 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐻𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
326325ad2ant2r 798 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐸𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥𝑄)) → (2nd ‘(𝐻𝑛)) = if(if(𝑃𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃𝐴, 𝐴, 𝑃), 𝑄))
327321, 326breqtrrd 4713 . . . . . . . . . . . . . . 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 3046 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐸𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
333332ralimdva 2991 . . . . . . . . 9 (𝜑 → (∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
334281, 333syl5 34 . . . . . . . 8 (𝜑 → (∀𝑥𝐸𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
335 ovolficc 23283 . . . . . . . . 9 (((𝐸𝐵) ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
336283, 71, 335syl2anc 694 . . . . . . . 8 (𝜑 → ((𝐸𝐵) ⊆ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐻𝑛)))))
337334, 270, 3363imtr4d 283 . . . . . . 7 (𝜑 → (𝐸 ran ((,) ∘ 𝐹) → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐻)))
33819, 337mpd 15 . . . . . 6 (𝜑 → (𝐸𝐵) ⊆ ran ([,] ∘ 𝐻))
33917ovollb2 23303 . . . . . 6 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸𝐵) ⊆ ran ([,] ∘ 𝐻)) → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
34071, 338, 339syl2anc 694 . . . . 5 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
341 supxrre 12195 . . . . . 6 ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑥) → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
342151, 159, 185, 341syl3anc 1366 . . . . 5 (𝜑 → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
343340, 342breqtrd 4711 . . . 4 (𝜑 → (vol*‘(𝐸𝐵)) ≤ sup(ran 𝑈, ℝ, < ))
3446, 10, 146, 187, 279, 343le2addd 10684 . . 3 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ≤ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
345 eqidd 2652 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐺)‘𝑛))
34655, 16, 89, 345, 62, 165, 137isumsup2 14622 . . . . 5 (𝜑𝑇 ⇝ sup(ran 𝑇, ℝ, < ))
347 seqex 12843 . . . . . . 7 seq1( + , ((abs ∘ − ) ∘ 𝐹)) ∈ V
34815, 347eqeltri 2726 . . . . . 6 𝑆 ∈ V
349348a1i 11 . . . . 5 (𝜑𝑆 ∈ V)
350 eqidd 2652 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) = (((abs ∘ − ) ∘ 𝐻)‘𝑛))
35155, 17, 89, 350, 79, 78, 178isumsup2 14622 . . . . 5 (𝜑𝑈 ⇝ sup(ran 𝑈, ℝ, < ))
35247recnd 10106 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ ℂ)
353161recnd 10106 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑈𝑗) ∈ ℂ)
35462recnd 10106 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
35557, 58, 354syl2an 493 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
35679recnd 10106 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
35757, 58, 356syl2an 493 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
35882eqcomd 2657 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
35957, 58, 358syl2an 493 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
36056, 355, 357, 359seradd 12883 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)))
36186, 171oveq12i 6702 . . . . . 6 ((𝑇𝑗) + (𝑈𝑗)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗))
362360, 87, 3613eqtr4g 2710 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑆𝑗) = ((𝑇𝑗) + (𝑈𝑗)))
36355, 89, 346, 349, 351, 352, 353, 362climadd 14406 . . . 4 (𝜑𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
364 climuni 14327 . . . 4 ((𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) ∧ 𝑆 ⇝ sup(ran 𝑆, ℝ*, < )) → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
365363, 125, 364syl2anc 694 . . 3 (𝜑 → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
366344, 365breqtrd 4711 . 2 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ≤ sup(ran 𝑆, ℝ*, < ))
36711, 25, 27, 366, 20letrd 10232 1 (𝜑 → ((vol*‘(𝐸𝐵)) + (vol*‘(𝐸𝐵))) ≤ ((vol*‘𝐸) + 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cdif 3604  cin 3606  wss 3607  c0 3948  ifcif 4119  cop 4216   cuni 4468   class class class wbr 4685  cmpt 4762   × cxp 5141  dom cdm 5143  ran crn 5144  ccom 5147   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  supcsup 8387  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977  +∞cpnf 10109  *cxr 10111   < clt 10112  cle 10113  cmin 10304  cn 11058  cuz 11725  +crp 11870  (,)cioo 12213  [,)cico 12215  [,]cicc 12216  ...cfz 12364  seqcseq 12841  abscabs 14018  cli 14259  vol*covol 23277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-ovol 23279
This theorem is referenced by:  ioombl1  23376
  Copyright terms: Public domain W3C validator