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

Theorem uniioombllem3 23272
Description: Lemma for uniioombl 23276. (Contributed by Mario Carneiro, 26-Mar-2015.)
Hypotheses
Ref Expression
uniioombl.1 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.2 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
uniioombl.3 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
uniioombl.a 𝐴 = ran ((,) ∘ 𝐹)
uniioombl.e (𝜑 → (vol*‘𝐸) ∈ ℝ)
uniioombl.c (𝜑𝐶 ∈ ℝ+)
uniioombl.g (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.s (𝜑𝐸 ran ((,) ∘ 𝐺))
uniioombl.t 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
uniioombl.v (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
uniioombl.m (𝜑𝑀 ∈ ℕ)
uniioombl.m2 (𝜑 → (abs‘((𝑇𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)
uniioombl.k 𝐾 = (((,) ∘ 𝐺) “ (1...𝑀))
Assertion
Ref Expression
uniioombllem3 (𝜑 → ((vol*‘(𝐸𝐴)) + (vol*‘(𝐸𝐴))) < (((vol*‘(𝐾𝐴)) + (vol*‘(𝐾𝐴))) + (𝐶 + 𝐶)))
Distinct variable groups:   𝑥,𝐹   𝑥,𝐺   𝑥,𝐾   𝑥,𝐴   𝑥,𝐶   𝑥,𝑀   𝜑,𝑥   𝑥,𝑇
Allowed substitution hints:   𝑆(𝑥)   𝐸(𝑥)

Proof of Theorem uniioombllem3
Dummy variables 𝑗 𝑘 𝑛 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 3816 . . . . 5 (𝐸𝐴) ⊆ 𝐸
21a1i 11 . . . 4 (𝜑 → (𝐸𝐴) ⊆ 𝐸)
3 uniioombl.s . . . . 5 (𝜑𝐸 ran ((,) ∘ 𝐺))
4 uniioombl.g . . . . . . . 8 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
54uniiccdif 23265 . . . . . . 7 (𝜑 → ( ran ((,) ∘ 𝐺) ⊆ ran ([,] ∘ 𝐺) ∧ (vol*‘( ran ([,] ∘ 𝐺) ∖ ran ((,) ∘ 𝐺))) = 0))
65simpld 475 . . . . . 6 (𝜑 ran ((,) ∘ 𝐺) ⊆ ran ([,] ∘ 𝐺))
7 ovolficcss 23157 . . . . . . 7 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐺) ⊆ ℝ)
84, 7syl 17 . . . . . 6 (𝜑 ran ([,] ∘ 𝐺) ⊆ ℝ)
96, 8sstrd 3597 . . . . 5 (𝜑 ran ((,) ∘ 𝐺) ⊆ ℝ)
103, 9sstrd 3597 . . . 4 (𝜑𝐸 ⊆ ℝ)
11 uniioombl.e . . . 4 (𝜑 → (vol*‘𝐸) ∈ ℝ)
12 ovolsscl 23173 . . . 4 (((𝐸𝐴) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸𝐴)) ∈ ℝ)
132, 10, 11, 12syl3anc 1323 . . 3 (𝜑 → (vol*‘(𝐸𝐴)) ∈ ℝ)
14 difssd 3721 . . . 4 (𝜑 → (𝐸𝐴) ⊆ 𝐸)
15 ovolsscl 23173 . . . 4 (((𝐸𝐴) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸𝐴)) ∈ ℝ)
1614, 10, 11, 15syl3anc 1323 . . 3 (𝜑 → (vol*‘(𝐸𝐴)) ∈ ℝ)
17 inss1 3816 . . . . . 6 (𝐾𝐴) ⊆ 𝐾
1817a1i 11 . . . . 5 (𝜑 → (𝐾𝐴) ⊆ 𝐾)
19 uniioombl.1 . . . . . . . 8 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
20 uniioombl.2 . . . . . . . 8 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
21 uniioombl.3 . . . . . . . 8 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
22 uniioombl.a . . . . . . . 8 𝐴 = ran ((,) ∘ 𝐹)
23 uniioombl.c . . . . . . . 8 (𝜑𝐶 ∈ ℝ+)
24 uniioombl.t . . . . . . . 8 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
25 uniioombl.v . . . . . . . 8 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
26 uniioombl.m . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
27 uniioombl.m2 . . . . . . . 8 (𝜑 → (abs‘((𝑇𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)
28 uniioombl.k . . . . . . . 8 𝐾 = (((,) ∘ 𝐺) “ (1...𝑀))
2919, 20, 21, 22, 11, 23, 4, 3, 24, 25, 26, 27, 28uniioombllem3a 23271 . . . . . . 7 (𝜑 → (𝐾 = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)) ∧ (vol*‘𝐾) ∈ ℝ))
3029simpld 475 . . . . . 6 (𝜑𝐾 = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
31 inss2 3817 . . . . . . . . . . . . 13 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
32 elfznn 12319 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
33 ffvelrn 6318 . . . . . . . . . . . . . 14 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
344, 32, 33syl2an 494 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
3531, 34sseldi 3585 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) ∈ (ℝ × ℝ))
36 1st2nd2 7157 . . . . . . . . . . . 12 ((𝐺𝑗) ∈ (ℝ × ℝ) → (𝐺𝑗) = ⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
3735, 36syl 17 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) = ⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
3837fveq2d 6157 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) = ((,)‘⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩))
39 df-ov 6613 . . . . . . . . . 10 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) = ((,)‘⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
4038, 39syl6eqr 2673 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) = ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))))
41 ioossre 12184 . . . . . . . . 9 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) ⊆ ℝ
4240, 41syl6eqss 3639 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) ⊆ ℝ)
4342ralrimiva 2961 . . . . . . 7 (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)) ⊆ ℝ)
44 iunss 4532 . . . . . . 7 ( 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)) ⊆ ℝ)
4543, 44sylibr 224 . . . . . 6 (𝜑 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)) ⊆ ℝ)
4630, 45eqsstrd 3623 . . . . 5 (𝜑𝐾 ⊆ ℝ)
4729simprd 479 . . . . 5 (𝜑 → (vol*‘𝐾) ∈ ℝ)
48 ovolsscl 23173 . . . . 5 (((𝐾𝐴) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘(𝐾𝐴)) ∈ ℝ)
4918, 46, 47, 48syl3anc 1323 . . . 4 (𝜑 → (vol*‘(𝐾𝐴)) ∈ ℝ)
5023rpred 11823 . . . 4 (𝜑𝐶 ∈ ℝ)
5149, 50readdcld 10020 . . 3 (𝜑 → ((vol*‘(𝐾𝐴)) + 𝐶) ∈ ℝ)
52 difssd 3721 . . . . 5 (𝜑 → (𝐾𝐴) ⊆ 𝐾)
53 ovolsscl 23173 . . . . 5 (((𝐾𝐴) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘(𝐾𝐴)) ∈ ℝ)
5452, 46, 47, 53syl3anc 1323 . . . 4 (𝜑 → (vol*‘(𝐾𝐴)) ∈ ℝ)
5554, 50readdcld 10020 . . 3 (𝜑 → ((vol*‘(𝐾𝐴)) + 𝐶) ∈ ℝ)
56 ssun2 3760 . . . . . . 7 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ⊆ (𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))
57 ioof 12220 . . . . . . . . . . . . . . 15 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
58 rexpssxrxp 10035 . . . . . . . . . . . . . . . . 17 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
5931, 58sstri 3596 . . . . . . . . . . . . . . . 16 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
60 fss 6018 . . . . . . . . . . . . . . . 16 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
614, 59, 60sylancl 693 . . . . . . . . . . . . . . 15 (𝜑𝐺:ℕ⟶(ℝ* × ℝ*))
62 fco 6020 . . . . . . . . . . . . . . 15 (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
6357, 61, 62sylancr 694 . . . . . . . . . . . . . 14 (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
64 ffn 6007 . . . . . . . . . . . . . 14 (((,) ∘ 𝐺):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐺) Fn ℕ)
6563, 64syl 17 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
66 fnima 5972 . . . . . . . . . . . . 13 (((,) ∘ 𝐺) Fn ℕ → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
6765, 66syl 17 . . . . . . . . . . . 12 (𝜑 → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
68 nnuz 11674 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
6926peano2nnd 10988 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 + 1) ∈ ℕ)
7069, 68syl6eleq 2708 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 + 1) ∈ (ℤ‘1))
71 uzsplit 12360 . . . . . . . . . . . . . . . 16 ((𝑀 + 1) ∈ (ℤ‘1) → (ℤ‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ‘(𝑀 + 1))))
7270, 71syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (ℤ‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ‘(𝑀 + 1))))
7368, 72syl5eq 2667 . . . . . . . . . . . . . 14 (𝜑 → ℕ = ((1...((𝑀 + 1) − 1)) ∪ (ℤ‘(𝑀 + 1))))
7426nncnd 10987 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℂ)
75 ax-1cn 9945 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
76 pncan 10238 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
7774, 75, 76sylancl 693 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
7877oveq2d 6626 . . . . . . . . . . . . . . 15 (𝜑 → (1...((𝑀 + 1) − 1)) = (1...𝑀))
7978uneq1d 3749 . . . . . . . . . . . . . 14 (𝜑 → ((1...((𝑀 + 1) − 1)) ∪ (ℤ‘(𝑀 + 1))) = ((1...𝑀) ∪ (ℤ‘(𝑀 + 1))))
8073, 79eqtrd 2655 . . . . . . . . . . . . 13 (𝜑 → ℕ = ((1...𝑀) ∪ (ℤ‘(𝑀 + 1))))
8180imaeq2d 5430 . . . . . . . . . . . 12 (𝜑 → (((,) ∘ 𝐺) “ ℕ) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ‘(𝑀 + 1)))))
8267, 81eqtr3d 2657 . . . . . . . . . . 11 (𝜑 → ran ((,) ∘ 𝐺) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ‘(𝑀 + 1)))))
83 imaundi 5509 . . . . . . . . . . 11 (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ‘(𝑀 + 1)))) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))
8482, 83syl6eq 2671 . . . . . . . . . 10 (𝜑 → ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
8584unieqd 4417 . . . . . . . . 9 (𝜑 ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
86 uniun 4427 . . . . . . . . 9 ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) = ( (((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))
8785, 86syl6eq 2671 . . . . . . . 8 (𝜑 ran ((,) ∘ 𝐺) = ( (((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
8828uneq1i 3746 . . . . . . . 8 (𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) = ( (((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))
8987, 88syl6eqr 2673 . . . . . . 7 (𝜑 ran ((,) ∘ 𝐺) = (𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
9056, 89syl5sseqr 3638 . . . . . 6 (𝜑 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ⊆ ran ((,) ∘ 𝐺))
9119, 20, 21, 22, 11, 23, 4, 3, 24, 25uniioombllem1 23268 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
92 ssid 3608 . . . . . . . 8 ran ((,) ∘ 𝐺) ⊆ ran ((,) ∘ 𝐺)
9324ovollb 23166 . . . . . . . 8 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ran ((,) ∘ 𝐺) ⊆ ran ((,) ∘ 𝐺)) → (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
944, 92, 93sylancl 693 . . . . . . 7 (𝜑 → (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
95 ovollecl 23170 . . . . . . 7 (( ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ ∧ (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < )) → (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ)
969, 91, 94, 95syl3anc 1323 . . . . . 6 (𝜑 → (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ)
97 ovolsscl 23173 . . . . . 6 (( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ⊆ ran ((,) ∘ 𝐺) ∧ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∈ ℝ)
9890, 9, 96, 97syl3anc 1323 . . . . 5 (𝜑 → (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∈ ℝ)
9949, 98readdcld 10020 . . . 4 (𝜑 → ((vol*‘(𝐾𝐴)) + (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) ∈ ℝ)
100 unss1 3765 . . . . . . . 8 ((𝐾𝐴) ⊆ 𝐾 → ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ (𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
10117, 100ax-mp 5 . . . . . . 7 ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ (𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))
102101, 89syl5sseqr 3638 . . . . . 6 (𝜑 → ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ ran ((,) ∘ 𝐺))
103 ovolsscl 23173 . . . . . 6 ((((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ ran ((,) ∘ 𝐺) ∧ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) ∈ ℝ)
104102, 9, 96, 103syl3anc 1323 . . . . 5 (𝜑 → (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) ∈ ℝ)
1053, 89sseqtrd 3625 . . . . . . . 8 (𝜑𝐸 ⊆ (𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
106 ssrin 3821 . . . . . . . 8 (𝐸 ⊆ (𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) → (𝐸𝐴) ⊆ ((𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∩ 𝐴))
107105, 106syl 17 . . . . . . 7 (𝜑 → (𝐸𝐴) ⊆ ((𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∩ 𝐴))
108 indir 3856 . . . . . . . 8 ((𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∩ 𝐴) = ((𝐾𝐴) ∪ ( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ∩ 𝐴))
109 inss1 3816 . . . . . . . . 9 ( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ∩ 𝐴) ⊆ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))
110 unss2 3767 . . . . . . . . 9 (( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ∩ 𝐴) ⊆ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) → ((𝐾𝐴) ∪ ( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
111109, 110ax-mp 5 . . . . . . . 8 ((𝐾𝐴) ∪ ( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))
112108, 111eqsstri 3619 . . . . . . 7 ((𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∩ 𝐴) ⊆ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))
113107, 112syl6ss 3599 . . . . . 6 (𝜑 → (𝐸𝐴) ⊆ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
114102, 9sstrd 3597 . . . . . 6 (𝜑 → ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ ℝ)
115 ovolss 23172 . . . . . 6 (((𝐸𝐴) ⊆ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∧ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ ℝ) → (vol*‘(𝐸𝐴)) ≤ (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))))
116113, 114, 115syl2anc 692 . . . . 5 (𝜑 → (vol*‘(𝐸𝐴)) ≤ (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))))
11718, 46sstrd 3597 . . . . . 6 (𝜑 → (𝐾𝐴) ⊆ ℝ)
11890, 9sstrd 3597 . . . . . 6 (𝜑 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ⊆ ℝ)
119 ovolun 23186 . . . . . 6 ((((𝐾𝐴) ⊆ ℝ ∧ (vol*‘(𝐾𝐴)) ∈ ℝ) ∧ ( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ⊆ ℝ ∧ (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∈ ℝ)) → (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾𝐴)) + (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))))
120117, 49, 118, 98, 119syl22anc 1324 . . . . 5 (𝜑 → (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾𝐴)) + (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))))
12113, 104, 99, 116, 120letrd 10145 . . . 4 (𝜑 → (vol*‘(𝐸𝐴)) ≤ ((vol*‘(𝐾𝐴)) + (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))))
122 rge0ssre 12229 . . . . . . . 8 (0[,)+∞) ⊆ ℝ
123 eqid 2621 . . . . . . . . . . 11 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
124123, 24ovolsf 23160 . . . . . . . . . 10 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
1254, 124syl 17 . . . . . . . . 9 (𝜑𝑇:ℕ⟶(0[,)+∞))
126125, 26ffvelrnd 6321 . . . . . . . 8 (𝜑 → (𝑇𝑀) ∈ (0[,)+∞))
127122, 126sseldi 3585 . . . . . . 7 (𝜑 → (𝑇𝑀) ∈ ℝ)
12891, 127resubcld 10409 . . . . . 6 (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)) ∈ ℝ)
12998rexrd 10040 . . . . . . 7 (𝜑 → (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∈ ℝ*)
130 id 22 . . . . . . . . . . . . . 14 (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
131 nnaddcl 10993 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
132130, 26, 131syl2anr 495 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
1334ffvelrnda 6320 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧 + 𝑀) ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
134132, 133syldan 487 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
135 eqid 2621 . . . . . . . . . . . 12 (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))
136134, 135fmptd 6346 . . . . . . . . . . 11 (𝜑 → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
137 eqid 2621 . . . . . . . . . . . 12 ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
138 eqid 2621 . . . . . . . . . . . 12 seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) = seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
139137, 138ovolsf 23160 . . . . . . . . . . 11 ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
140136, 139syl 17 . . . . . . . . . 10 (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
141 frn 6015 . . . . . . . . . 10 (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞) → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ (0[,)+∞))
142140, 141syl 17 . . . . . . . . 9 (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ (0[,)+∞))
143 icossxr 12207 . . . . . . . . 9 (0[,)+∞) ⊆ ℝ*
144142, 143syl6ss 3599 . . . . . . . 8 (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ*)
145 supxrcl 12095 . . . . . . . 8 (ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈ ℝ*)
146144, 145syl 17 . . . . . . 7 (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈ ℝ*)
147128rexrd 10040 . . . . . . 7 (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)) ∈ ℝ*)
148 1zzd 11359 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → 1 ∈ ℤ)
14926nnzd 11432 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℤ)
150149adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → 𝑀 ∈ ℤ)
151 addcom 10173 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑀 + 1) = (1 + 𝑀))
15274, 75, 151sylancl 693 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 + 1) = (1 + 𝑀))
153152fveq2d 6157 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (ℤ‘(𝑀 + 1)) = (ℤ‘(1 + 𝑀)))
154153eleq2d 2684 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥 ∈ (ℤ‘(𝑀 + 1)) ↔ 𝑥 ∈ (ℤ‘(1 + 𝑀))))
155154biimpa 501 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → 𝑥 ∈ (ℤ‘(1 + 𝑀)))
156 eluzsub 11668 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ (ℤ‘(1 + 𝑀))) → (𝑥𝑀) ∈ (ℤ‘1))
157148, 150, 155, 156syl3anc 1323 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → (𝑥𝑀) ∈ (ℤ‘1))
158157, 68syl6eleqr 2709 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → (𝑥𝑀) ∈ ℕ)
159 eluzelz 11648 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (ℤ‘(𝑀 + 1)) → 𝑥 ∈ ℤ)
160159adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → 𝑥 ∈ ℤ)
161160zcnd 11434 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → 𝑥 ∈ ℂ)
16274adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → 𝑀 ∈ ℂ)
163161, 162npcand 10347 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → ((𝑥𝑀) + 𝑀) = 𝑥)
164163eqcomd 2627 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → 𝑥 = ((𝑥𝑀) + 𝑀))
165 oveq1 6617 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑥𝑀) → (𝑧 + 𝑀) = ((𝑥𝑀) + 𝑀))
166165eqeq2d 2631 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑥𝑀) → (𝑥 = (𝑧 + 𝑀) ↔ 𝑥 = ((𝑥𝑀) + 𝑀)))
167166rspcev 3298 . . . . . . . . . . . . . . . . 17 (((𝑥𝑀) ∈ ℕ ∧ 𝑥 = ((𝑥𝑀) + 𝑀)) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
168158, 164, 167syl2anc 692 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
169 vex 3192 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
170 eqid 2621 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))
171170elrnmpt 5337 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)))
172169, 171ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
173168, 172sylibr 224 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 1))) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
174173ex 450 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ (ℤ‘(𝑀 + 1)) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
175174ssrdv 3593 . . . . . . . . . . . . 13 (𝜑 → (ℤ‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
176 imass2 5465 . . . . . . . . . . . . 13 ((ℤ‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) → (𝐺 “ (ℤ‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
177175, 176syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐺 “ (ℤ‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
178 rnco2 5606 . . . . . . . . . . . . 13 ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
179 eqidd 2622 . . . . . . . . . . . . . . 15 (𝜑 → (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
1804feqmptd 6211 . . . . . . . . . . . . . . 15 (𝜑𝐺 = (𝑤 ∈ ℕ ↦ (𝐺𝑤)))
181 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑤 = (𝑧 + 𝑀) → (𝐺𝑤) = (𝐺‘(𝑧 + 𝑀)))
182132, 179, 180, 181fmptco 6357 . . . . . . . . . . . . . 14 (𝜑 → (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
183182rneqd 5318 . . . . . . . . . . . . 13 (𝜑 → ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
184178, 183syl5eqr 2669 . . . . . . . . . . . 12 (𝜑 → (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
185177, 184sseqtrd 3625 . . . . . . . . . . 11 (𝜑 → (𝐺 “ (ℤ‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
186 imass2 5465 . . . . . . . . . . 11 ((𝐺 “ (ℤ‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) → ((,) “ (𝐺 “ (ℤ‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
187185, 186syl 17 . . . . . . . . . 10 (𝜑 → ((,) “ (𝐺 “ (ℤ‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
188 imaco 5604 . . . . . . . . . 10 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) = ((,) “ (𝐺 “ (ℤ‘(𝑀 + 1))))
189 rnco2 5606 . . . . . . . . . 10 ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
190187, 188, 1893sstr4g 3630 . . . . . . . . 9 (𝜑 → (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
191190unissd 4433 . . . . . . . 8 (𝜑 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
192138ovollb 23166 . . . . . . . 8 (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) → (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ))
193136, 191, 192syl2anc 692 . . . . . . 7 (𝜑 → (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ))
194 frn 6015 . . . . . . . . . . . . . . 15 (𝑇:ℕ⟶(0[,)+∞) → ran 𝑇 ⊆ (0[,)+∞))
195125, 194syl 17 . . . . . . . . . . . . . 14 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
196195, 143syl6ss 3599 . . . . . . . . . . . . 13 (𝜑 → ran 𝑇 ⊆ ℝ*)
197196adantr 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ran 𝑇 ⊆ ℝ*)
19824fveq1i 6154 . . . . . . . . . . . . . 14 (𝑇‘(𝑀 + 𝑛)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛))
19926nnred 10986 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℝ)
200199ltp1d 10905 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 < (𝑀 + 1))
201 fzdisj 12317 . . . . . . . . . . . . . . . . . 18 (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
202200, 201syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
203202adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
204 nnnn0 11250 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
205 nn0addge1 11290 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ0) → 𝑀 ≤ (𝑀 + 𝑛))
206199, 204, 205syl2an 494 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → 𝑀 ≤ (𝑀 + 𝑛))
20726adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑀 ∈ ℕ)
208207, 68syl6eleq 2708 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝑀 ∈ (ℤ‘1))
209 nnaddcl 10993 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
21026, 209sylan 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
211210nnzd 11432 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℤ)
212 elfz5 12283 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ (ℤ‘1) ∧ (𝑀 + 𝑛) ∈ ℤ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
213208, 211, 212syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
214206, 213mpbird 247 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → 𝑀 ∈ (1...(𝑀 + 𝑛)))
215 fzsplit 12316 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (1...(𝑀 + 𝑛)) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
216214, 215syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
217 fzfid 12719 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) ∈ Fin)
2184adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
219 elfznn 12319 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...(𝑀 + 𝑛)) → 𝑗 ∈ ℕ)
220 ovolfcl 23154 . . . . . . . . . . . . . . . . . . . 20 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
221218, 219, 220syl2an 494 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
222221simp2d 1072 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (2nd ‘(𝐺𝑗)) ∈ ℝ)
223221simp1d 1071 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (1st ‘(𝐺𝑗)) ∈ ℝ)
224222, 223resubcld 10409 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℝ)
225224recnd 10019 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℂ)
226203, 216, 217, 225fsumsplit 14411 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) = (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗)))))
227123ovolfsval 23158 . . . . . . . . . . . . . . . . 17 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
228218, 219, 227syl2an 494 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
229210, 68syl6eleq 2708 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ (ℤ‘1))
230228, 229, 225fsumser 14401 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)))
2314ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
23232adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
233231, 232, 227syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
2344, 32, 220syl2an 494 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
235234simp2d 1072 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺𝑗)) ∈ ℝ)
236234simp1d 1071 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺𝑗)) ∈ ℝ)
237235, 236resubcld 10409 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℝ)
238237adantlr 750 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℝ)
239238recnd 10019 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℂ)
240233, 208, 239fsumser 14401 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀))
24124fveq1i 6154 . . . . . . . . . . . . . . . . 17 (𝑇𝑀) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀)
242240, 241syl6eqr 2673 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) = (𝑇𝑀))
243207nnzd 11432 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → 𝑀 ∈ ℤ)
244243peano2zd 11436 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℤ)
2454ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
246207peano2nnd 10988 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℕ)
247 elfzuz 12287 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛)) → 𝑗 ∈ (ℤ‘(𝑀 + 1)))
248 eluznn 11709 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ‘(𝑀 + 1))) → 𝑗 ∈ ℕ)
249246, 247, 248syl2an 494 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝑗 ∈ ℕ)
250245, 249, 220syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
251250simp2d 1072 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (2nd ‘(𝐺𝑗)) ∈ ℝ)
252250simp1d 1071 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (1st ‘(𝐺𝑗)) ∈ ℝ)
253251, 252resubcld 10409 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℝ)
254253recnd 10019 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℂ)
255 fveq2 6153 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑘 + 𝑀) → (𝐺𝑗) = (𝐺‘(𝑘 + 𝑀)))
256255fveq2d 6157 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑘 + 𝑀) → (2nd ‘(𝐺𝑗)) = (2nd ‘(𝐺‘(𝑘 + 𝑀))))
257255fveq2d 6157 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑘 + 𝑀) → (1st ‘(𝐺𝑗)) = (1st ‘(𝐺‘(𝑘 + 𝑀))))
258256, 257oveq12d 6628 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑘 + 𝑀) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))))
259243, 244, 211, 254, 258fsumshftm 14448 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) = Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))))
260207nncnd 10987 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑀 ∈ ℂ)
261 pncan2 10239 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 𝑀) = 1)
262260, 75, 261sylancl 693 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ((𝑀 + 1) − 𝑀) = 1)
263 nncn 10979 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
264263adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
265260, 264pncan2d 10345 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ((𝑀 + 𝑛) − 𝑀) = 𝑛)
266262, 265oveq12d 6628 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀)) = (1...𝑛))
267266sumeq1d 14372 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))))
268136adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
269 elfznn 12319 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
270137ovolfsval 23158 . . . . . . . . . . . . . . . . . . . 20 (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
271268, 269, 270syl2an 494 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
272269adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
273 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑘 → (𝑧 + 𝑀) = (𝑘 + 𝑀))
274273fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑘 → (𝐺‘(𝑧 + 𝑀)) = (𝐺‘(𝑘 + 𝑀)))
275 fvex 6163 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺‘(𝑘 + 𝑀)) ∈ V
276274, 135, 275fvmpt 6244 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
277272, 276syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
278277fveq2d 6157 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (2nd ‘(𝐺‘(𝑘 + 𝑀))))
279277fveq2d 6157 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (1st ‘(𝐺‘(𝑘 + 𝑀))))
280278, 279oveq12d 6628 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))))
281271, 280eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))))
282 simpr 477 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
283282, 68syl6eleq 2708 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
2844ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
285 nnaddcl 10993 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 + 𝑀) ∈ ℕ)
286269, 207, 285syl2anr 495 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 𝑀) ∈ ℕ)
287 ovolfcl 23154 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 𝑀) ∈ ℕ) → ((1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st ‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀)))))
288284, 286, 287syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st ‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀)))))
289288simp2d 1072 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ)
290288simp1d 1071 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ)
291289, 290resubcld 10409 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℝ)
292291recnd 10019 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℂ)
293281, 283, 292fsumser 14401 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
294259, 267, 2933eqtrd 2659 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
295242, 294oveq12d 6628 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗)))) = ((𝑇𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
296226, 230, 2953eqtr3d 2663 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)) = ((𝑇𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
297198, 296syl5eq 2667 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) = ((𝑇𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
298 ffn 6007 . . . . . . . . . . . . . . . 16 (𝑇:ℕ⟶(0[,)+∞) → 𝑇 Fn ℕ)
299125, 298syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑇 Fn ℕ)
300299adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 𝑇 Fn ℕ)
301 fnfvelrn 6317 . . . . . . . . . . . . . 14 ((𝑇 Fn ℕ ∧ (𝑀 + 𝑛) ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
302300, 210, 301syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
303297, 302eqeltrrd 2699 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((𝑇𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇)
304 supxrub 12104 . . . . . . . . . . . 12 ((ran 𝑇 ⊆ ℝ* ∧ ((𝑇𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) → ((𝑇𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, < ))
305197, 303, 304syl2anc 692 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((𝑇𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, < ))
306127adantr 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑇𝑀) ∈ ℝ)
307140ffvelrnda 6320 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ (0[,)+∞))
308122, 307sseldi 3585 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ ℝ)
30991adantr 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
310306, 308, 309leaddsub2d 10580 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (((𝑇𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, < ) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀))))
311305, 310mpbid 222 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)))
312311ralrimiva 2961 . . . . . . . . 9 (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)))
313 ffn 6007 . . . . . . . . . . 11 (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ)
314140, 313syl 17 . . . . . . . . . 10 (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ)
315 breq1 4621 . . . . . . . . . . 11 (𝑥 = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) → (𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀))))
316315ralrn 6323 . . . . . . . . . 10 (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ → (∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀))))
317314, 316syl 17 . . . . . . . . 9 (𝜑 → (∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀))))
318312, 317mpbird 247 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)))
319 supxrleub 12106 . . . . . . . . 9 ((ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* ∧ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)) ∈ ℝ*) → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀))))
320144, 147, 319syl2anc 692 . . . . . . . 8 (𝜑 → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀))))
321318, 320mpbird 247 . . . . . . 7 (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)))
322129, 146, 147, 193, 321xrletrd 11944 . . . . . 6 (𝜑 → (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)))
323127, 91, 50absdifltd 14113 . . . . . . . . 9 (𝜑 → ((abs‘((𝑇𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶 ↔ ((sup(ran 𝑇, ℝ*, < ) − 𝐶) < (𝑇𝑀) ∧ (𝑇𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶))))
32427, 323mpbid 222 . . . . . . . 8 (𝜑 → ((sup(ran 𝑇, ℝ*, < ) − 𝐶) < (𝑇𝑀) ∧ (𝑇𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶)))
325324simpld 475 . . . . . . 7 (𝜑 → (sup(ran 𝑇, ℝ*, < ) − 𝐶) < (𝑇𝑀))
32691, 50, 127, 325ltsub23d 10583 . . . . . 6 (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇𝑀)) < 𝐶)
32798, 128, 50, 322, 326lelttrd 10146 . . . . 5 (𝜑 → (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) < 𝐶)
32898, 50, 49, 327ltadd2dd 10147 . . . 4 (𝜑 → ((vol*‘(𝐾𝐴)) + (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) < ((vol*‘(𝐾𝐴)) + 𝐶))
32913, 99, 51, 121, 328lelttrd 10146 . . 3 (𝜑 → (vol*‘(𝐸𝐴)) < ((vol*‘(𝐾𝐴)) + 𝐶))
33054, 98readdcld 10020 . . . 4 (𝜑 → ((vol*‘(𝐾𝐴)) + (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) ∈ ℝ)
331 difss 3720 . . . . . . . 8 (𝐾𝐴) ⊆ 𝐾
332 unss1 3765 . . . . . . . 8 ((𝐾𝐴) ⊆ 𝐾 → ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ (𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
333331, 332ax-mp 5 . . . . . . 7 ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ (𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))
334333, 89syl5sseqr 3638 . . . . . 6 (𝜑 → ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ ran ((,) ∘ 𝐺))
335 ovolsscl 23173 . . . . . 6 ((((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ ran ((,) ∘ 𝐺) ∧ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) ∈ ℝ)
336334, 9, 96, 335syl3anc 1323 . . . . 5 (𝜑 → (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) ∈ ℝ)
337105ssdifd 3729 . . . . . . 7 (𝜑 → (𝐸𝐴) ⊆ ((𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∖ 𝐴))
338 difundir 3861 . . . . . . . 8 ((𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∖ 𝐴) = ((𝐾𝐴) ∪ ( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ∖ 𝐴))
339 difss 3720 . . . . . . . . 9 ( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ∖ 𝐴) ⊆ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))
340 unss2 3767 . . . . . . . . 9 (( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ∖ 𝐴) ⊆ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) → ((𝐾𝐴) ∪ ( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
341339, 340ax-mp 5 . . . . . . . 8 ((𝐾𝐴) ∪ ( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))
342338, 341eqsstri 3619 . . . . . . 7 ((𝐾 (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∖ 𝐴) ⊆ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))
343337, 342syl6ss 3599 . . . . . 6 (𝜑 → (𝐸𝐴) ⊆ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))))
344334, 9sstrd 3597 . . . . . 6 (𝜑 → ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ ℝ)
345 ovolss 23172 . . . . . 6 (((𝐸𝐴) ⊆ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∧ ((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ⊆ ℝ) → (vol*‘(𝐸𝐴)) ≤ (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))))
346343, 344, 345syl2anc 692 . . . . 5 (𝜑 → (vol*‘(𝐸𝐴)) ≤ (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))))
34752, 46sstrd 3597 . . . . . 6 (𝜑 → (𝐾𝐴) ⊆ ℝ)
348 ovolun 23186 . . . . . 6 ((((𝐾𝐴) ⊆ ℝ ∧ (vol*‘(𝐾𝐴)) ∈ ℝ) ∧ ( (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))) ⊆ ℝ ∧ (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1)))) ∈ ℝ)) → (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾𝐴)) + (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))))
349347, 54, 118, 98, 348syl22anc 1324 . . . . 5 (𝜑 → (vol*‘((𝐾𝐴) ∪ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾𝐴)) + (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))))
35016, 336, 330, 346, 349letrd 10145 . . . 4 (𝜑 → (vol*‘(𝐸𝐴)) ≤ ((vol*‘(𝐾𝐴)) + (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))))
35198, 50, 54, 327ltadd2dd 10147 . . . 4 (𝜑 → ((vol*‘(𝐾𝐴)) + (vol*‘ (((,) ∘ 𝐺) “ (ℤ‘(𝑀 + 1))))) < ((vol*‘(𝐾𝐴)) + 𝐶))
35216, 330, 55, 350, 351lelttrd 10146 . . 3 (𝜑 → (vol*‘(𝐸𝐴)) < ((vol*‘(𝐾𝐴)) + 𝐶))
35313, 16, 51, 55, 329, 352lt2addd 10601 . 2 (𝜑 → ((vol*‘(𝐸𝐴)) + (vol*‘(𝐸𝐴))) < (((vol*‘(𝐾𝐴)) + 𝐶) + ((vol*‘(𝐾𝐴)) + 𝐶)))
35449recnd 10019 . . 3 (𝜑 → (vol*‘(𝐾𝐴)) ∈ ℂ)
35550recnd 10019 . . 3 (𝜑𝐶 ∈ ℂ)
35654recnd 10019 . . 3 (𝜑 → (vol*‘(𝐾𝐴)) ∈ ℂ)
357354, 355, 356, 355add4d 10215 . 2 (𝜑 → (((vol*‘(𝐾𝐴)) + 𝐶) + ((vol*‘(𝐾𝐴)) + 𝐶)) = (((vol*‘(𝐾𝐴)) + (vol*‘(𝐾𝐴))) + (𝐶 + 𝐶)))
358353, 357breqtrd 4644 1 (𝜑 → ((vol*‘(𝐸𝐴)) + (vol*‘(𝐸𝐴))) < (((vol*‘(𝐾𝐴)) + (vol*‘(𝐾𝐴))) + (𝐶 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  Vcvv 3189  cdif 3556  cun 3557  cin 3558  wss 3559  c0 3896  𝒫 cpw 4135  cop 4159   cuni 4407   ciun 4490  Disj wdisj 4588   class class class wbr 4618  cmpt 4678   × cxp 5077  ran crn 5080  cima 5082  ccom 5083   Fn wfn 5847  wf 5848  cfv 5852  (class class class)co 6610  1st c1st 7118  2nd c2nd 7119  supcsup 8297  cc 9885  cr 9886  0cc0 9887  1c1 9888   + caddc 9890  +∞cpnf 10022  *cxr 10024   < clt 10025  cle 10026  cmin 10217  cn 10971  0cn0 11243  cz 11328  cuz 11638  +crp 11783  (,)cioo 12124  [,)cico 12126  [,]cicc 12127  ...cfz 12275  seqcseq 12748  abscabs 13915  Σcsu 14357  vol*covol 23150
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 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965
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 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fi 8268  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-acn 8719  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-n0 11244  df-z 11329  df-uz 11639  df-q 11740  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ioo 12128  df-ico 12130  df-icc 12131  df-fz 12276  df-fzo 12414  df-fl 12540  df-seq 12749  df-exp 12808  df-hash 13065  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-clim 14160  df-rlim 14161  df-sum 14358  df-rest 16011  df-topgen 16032  df-psmet 19666  df-xmet 19667  df-met 19668  df-bl 19669  df-mopn 19670  df-top 20627  df-topon 20644  df-bases 20670  df-cmp 21109  df-ovol 23152  df-vol 23153
This theorem is referenced by:  uniioombllem5  23274
  Copyright terms: Public domain W3C validator