Step | Hyp | Ref
| Expression |
1 | | hoidmv1le.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
2 | | hoidmv1le.z |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
3 | | snidg 4153 |
. . . . . . . . . . . 12
⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍}) |
4 | 2, 3 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ {𝑍}) |
5 | | hoidmv1le.x |
. . . . . . . . . . 11
⊢ 𝑋 = {𝑍} |
6 | 4, 5 | syl6eleqr 2699 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ 𝑋) |
7 | 1, 6 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) |
8 | | hoidmv1le.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
9 | 8, 6 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) |
10 | 7, 9 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ) |
11 | 10 | rexrd 9968 |
. . . . . . 7
⊢ (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈
ℝ*) |
12 | | pnfxr 9971 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → +∞ ∈
ℝ*) |
14 | 10 | ltpnfd 11831 |
. . . . . . 7
⊢ (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) < +∞) |
15 | 11, 13, 14 | xrltled 38427 |
. . . . . 6
⊢ (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ +∞) |
16 | 15 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ +∞) |
17 | | id 22 |
. . . . . . 7
⊢
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞ →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) |
18 | 17 | eqcomd 2616 |
. . . . . 6
⊢
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞ → +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))) |
19 | 18 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))) |
20 | 16, 19 | breqtrd 4609 |
. . . 4
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))) |
21 | | simpl 472 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍))) |
22 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) |
23 | | nnex 10903 |
. . . . . . . 8
⊢ ℕ
∈ V |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ℕ ∈
V) |
25 | | hoidmv1le.l |
. . . . . . . . . . . 12
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
26 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 = {𝑍}) |
27 | | snfi 7923 |
. . . . . . . . . . . . . . 15
⊢ {𝑍} ∈ Fin |
28 | 27 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑍} ∈ Fin) |
29 | 26, 28 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ Fin) |
30 | 29 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin) |
31 | | ne0i 3880 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ 𝑋 → 𝑋 ≠ ∅) |
32 | 6, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ≠ ∅) |
33 | 32 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅) |
34 | | hoidmv1le.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶:ℕ⟶(ℝ
↑𝑚 𝑋)) |
35 | 34 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑋)) |
36 | | elmapi 7765 |
. . . . . . . . . . . . 13
⊢ ((𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑋) → (𝐶‘𝑗):𝑋⟶ℝ) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ) |
38 | | hoidmv1le.d |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷:ℕ⟶(ℝ
↑𝑚 𝑋)) |
39 | 38 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑋)) |
40 | | elmapi 7765 |
. . . . . . . . . . . . 13
⊢ ((𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑋) → (𝐷‘𝑗):𝑋⟶ℝ) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) |
42 | 25, 30, 33, 37, 41 | hoidmvn0val 39474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
43 | 5 | prodeq1i 14487 |
. . . . . . . . . . . 12
⊢
∏𝑘 ∈
𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
45 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑉) |
46 | 6 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑋) |
47 | 37, 46 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) |
48 | 41, 46 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
49 | | volicore 39471 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℝ) |
50 | 47, 48, 49 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℝ) |
51 | 50 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℂ) |
52 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑍 → ((𝐶‘𝑗)‘𝑘) = ((𝐶‘𝑗)‘𝑍)) |
53 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑍 → ((𝐷‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝑍)) |
54 | 52, 53 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑍 → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
55 | 54 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑍 → (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
56 | 55 | prodsn 14531 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈ 𝑉 ∧ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
57 | 45, 51, 56 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
58 | 42, 44, 57 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
59 | 58 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) |
60 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑙 → (𝑎‘𝑘) = (𝑎‘𝑙)) |
61 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑙 → (𝑏‘𝑘) = (𝑏‘𝑙)) |
62 | 60, 61 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑙 → ((𝑎‘𝑘)[,)(𝑏‘𝑘)) = ((𝑎‘𝑙)[,)(𝑏‘𝑙))) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑙 → (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))) |
64 | 63 | cbvprodv 14485 |
. . . . . . . . . . . . . . . . 17
⊢
∏𝑘 ∈
𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))) |
65 | | ifeq2 4041 |
. . . . . . . . . . . . . . . . 17
⊢
(∏𝑘 ∈
𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))) → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))) |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))) |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ (ℝ
↑𝑚 𝑥) ∧ 𝑏 ∈ (ℝ ↑𝑚
𝑥)) → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))) |
68 | 67 | mpt2eq3ia 6618 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (ℝ
↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))) |
69 | 68 | mpteq2i 4669 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ
↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))))) |
70 | 25, 69 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))))) |
71 | 70, 30, 37, 41 | hoidmvcl 39472 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞)) |
72 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) |
73 | 71, 72 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,)+∞)) |
74 | | icossicc 12131 |
. . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
75 | 74 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (0[,)+∞) ⊆
(0[,]+∞)) |
76 | 73, 75 | fssd 5970 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,]+∞)) |
77 | 59, 76 | feq1dd 38341 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))):ℕ⟶(0[,]+∞)) |
78 | 77 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))):ℕ⟶(0[,]+∞)) |
79 | 24, 78 | sge0repnf 39279 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞)) |
80 | 22, 79 | mpbird 246 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) |
81 | 9 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐴‘𝑍) ∈ ℝ) |
82 | 7 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐵‘𝑍) ∈ ℝ) |
83 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐴‘𝑍) < (𝐵‘𝑍)) |
84 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) |
85 | 47, 84 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)):ℕ⟶ℝ) |
86 | 85 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)):ℕ⟶ℝ) |
87 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) |
88 | 48, 87 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)):ℕ⟶ℝ) |
89 | 88 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)):ℕ⟶ℝ) |
90 | | hoidmv1le.s |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
91 | 5 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ 𝑋 ↔ 𝑘 ∈ {𝑍}) |
92 | 91 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ 𝑋 → 𝑘 ∈ {𝑍}) |
93 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ {𝑍} → 𝑘 = 𝑍) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ 𝑋 → 𝑘 = 𝑍) |
95 | 94, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝑋 → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
96 | 95 | rgen 2906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
∀𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) |
97 | | ixpeq2 7808 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
100 | 99 | iuneq2i 4475 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
102 | 90, 101 | sseqtrd 3604 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
103 | 102 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
104 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) |
105 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → {〈𝑍, 𝑥〉} = {〈𝑍, 𝑥〉}) |
106 | | opeq2 4341 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑥 → 〈𝑍, 𝑦〉 = 〈𝑍, 𝑥〉) |
107 | 106 | sneqd 4137 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑥 → {〈𝑍, 𝑦〉} = {〈𝑍, 𝑥〉}) |
108 | 107 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → ({〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉} ↔ {〈𝑍, 𝑥〉} = {〈𝑍, 𝑥〉})) |
109 | 108 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ∧ {〈𝑍, 𝑥〉} = {〈𝑍, 𝑥〉}) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) |
110 | 104, 105,
109 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) |
111 | 110 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) |
112 | | elixpsn 7833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑍 ∈ 𝑉 → ({〈𝑍, 𝑥〉} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉})) |
113 | 2, 112 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ({〈𝑍, 𝑥〉} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉})) |
114 | 113 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ({〈𝑍, 𝑥〉} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉})) |
115 | 111, 114 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍))) |
116 | 5 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑍} = 𝑋 |
117 | | ixpeq1 7805 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑍} = 𝑋 → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍))) |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ X𝑘 ∈
{𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) |
119 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍)) |
120 | 94, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ 𝑋 → (𝐴‘𝑘) = (𝐴‘𝑍)) |
121 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑍 → (𝐵‘𝑘) = (𝐵‘𝑍)) |
122 | 94, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ 𝑋 → (𝐵‘𝑘) = (𝐵‘𝑍)) |
123 | 120, 122 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝑋 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍))) |
124 | 123 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝑋 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
125 | 124 | rgen 2906 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∀𝑘 ∈
𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)) |
126 | | ixpeq2 7808 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑘 ∈
𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
127 | 125, 126 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ X𝑘 ∈
𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) |
128 | 118, 127 | eqtri 2632 |
. . . . . . . . . . . . . . . . . 18
⊢ X𝑘 ∈
{𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) |
129 | 128 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → X𝑘 ∈
{𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
130 | 129 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
131 | 115, 130 | eleqtrd 2690 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
132 | 103, 131 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {〈𝑍, 𝑥〉} ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
133 | | eliun 4460 |
. . . . . . . . . . . . . 14
⊢
({〈𝑍, 𝑥〉} ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
134 | 132, 133 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑗 ∈ ℕ {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
135 | | ixpeq1 7805 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑋 = {𝑍} → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
136 | 5, 135 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) |
137 | 136 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈𝑍, 𝑥〉} ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
138 | 137 | biimpi 205 |
. . . . . . . . . . . . . . . . . . 19
⊢
({〈𝑍, 𝑥〉} ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
139 | 138 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
140 | | elixpsn 7833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑍 ∈ 𝑉 → ({〈𝑍, 𝑥〉} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉})) |
141 | 2, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ({〈𝑍, 𝑥〉} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉})) |
142 | 141 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ({〈𝑍, 𝑥〉} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉})) |
143 | 139, 142 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) |
144 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
〈𝑍, 𝑥〉 ∈ V |
145 | 144 | sneqr 4311 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
({〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉} → 〈𝑍, 𝑥〉 = 〈𝑍, 𝑦〉) |
146 | 145 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ {〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) → 〈𝑍, 𝑥〉 = 〈𝑍, 𝑦〉) |
147 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑥 ∈ V |
148 | 147 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑥 ∈ V) |
149 | | opthg 4872 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑥 ∈ V) → (〈𝑍, 𝑥〉 = 〈𝑍, 𝑦〉 ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦))) |
150 | 2, 148, 149 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (〈𝑍, 𝑥〉 = 〈𝑍, 𝑦〉 ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦))) |
151 | 150 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ {〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) → (〈𝑍, 𝑥〉 = 〈𝑍, 𝑦〉 ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦))) |
152 | 146, 151 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ {〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) → (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)) |
153 | 152 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ {〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) → 𝑥 = 𝑦) |
154 | 153 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) → 𝑥 = 𝑦) |
155 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) → 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
156 | 154, 155 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉}) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
157 | 156 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ({〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) |
158 | 157 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ({〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) |
159 | 158 | rexlimdv 3012 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){〈𝑍, 𝑥〉} = {〈𝑍, 𝑦〉} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
160 | 143, 159 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
161 | 160 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ({〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
162 | 161 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∧ 𝑗 ∈ ℕ) → ({〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
163 | 162 | reximdva 3000 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → (∃𝑗 ∈ ℕ {〈𝑍, 𝑥〉} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
164 | 134, 163 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
165 | | eliun 4460 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
166 | 164, 165 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → 𝑥 ∈ ∪
𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
167 | 166 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))𝑥 ∈ ∪
𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
168 | | dfss3 3558 |
. . . . . . . . . 10
⊢ (((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∀𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))𝑥 ∈ ∪
𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
169 | 167, 168 | sylibr 223 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
170 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))) |
171 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖)) |
172 | 171 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍)) |
173 | 172 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍)) |
174 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ) |
175 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ ((𝐶‘𝑖)‘𝑍) ∈ V |
176 | 175 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ V) |
177 | 170, 173,
174, 176 | fvmptd 6197 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖) = ((𝐶‘𝑖)‘𝑍)) |
178 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))) |
179 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖)) |
180 | 179 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍)) |
181 | 180 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍)) |
182 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ ((𝐷‘𝑖)‘𝑍) ∈ V |
183 | 182 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ V) |
184 | 178, 181,
174, 183 | fvmptd 6197 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) = ((𝐷‘𝑖)‘𝑍)) |
185 | 177, 184 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) |
186 | 185 | iuneq2dv 4478 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = ∪
𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) |
187 | 172, 180 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) |
188 | 187 | cbviunv 4495 |
. . . . . . . . . . . 12
⊢ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = ∪
𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) |
189 | 188 | eqcomi 2619 |
. . . . . . . . . . 11
⊢ ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = ∪
𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) |
190 | 189 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = ∪
𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
191 | 186, 190 | eqtr2d 2645 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = ∪
𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))) |
192 | 169, 191 | sseqtrd 3604 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))) |
193 | 192 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))) |
194 | 172, 84, 175 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖) = ((𝐶‘𝑖)‘𝑍)) |
195 | 180, 87, 182 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) = ((𝐷‘𝑖)‘𝑍)) |
196 | 194, 195 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) |
197 | 196 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ →
(vol‘(((𝑗 ∈
ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))) = (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) |
198 | 197 | mpteq2ia 4668 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ ↦
(vol‘(((𝑗 ∈
ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) |
199 | | eqcom 2617 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 ↔ 𝑖 = 𝑗) |
200 | 199 | imbi1i 338 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) |
201 | | eqcom 2617 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) ↔ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
202 | 201 | imbi2i 325 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 = 𝑗 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
203 | 200, 202 | bitri 263 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
204 | 187, 203 | mpbi 219 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
205 | 204 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
206 | 205 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ ↦
(vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
207 | 198, 206 | eqtri 2632 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℕ ↦
(vol‘(((𝑗 ∈
ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
208 | 207 | fveq2i 6106 |
. . . . . . . . 9
⊢
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) |
209 | 208 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) →
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))) |
210 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) |
211 | 209, 210 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) →
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) ∈ ℝ) |
212 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑤 − (𝐴‘𝑍)) = (𝑧 − (𝐴‘𝑍))) |
213 | 195 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧 ↔ ((𝐷‘𝑖)‘𝑍) ≤ 𝑧)) |
214 | 213, 195 | ifbieq1d 4059 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℕ →
if(((𝑗 ∈ ℕ
↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧) = if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)) |
215 | 194, 214 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)) = (((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))) |
216 | 215 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ →
(vol‘(((𝑗 ∈
ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))) = (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))) |
217 | 216 | mpteq2ia 4668 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ ↦
(vol‘(((𝑗 ∈
ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))) |
218 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = ℎ → (𝐶‘𝑖) = (𝐶‘ℎ)) |
219 | 218 | fveq1d 6105 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = ℎ → ((𝐶‘𝑖)‘𝑍) = ((𝐶‘ℎ)‘𝑍)) |
220 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = ℎ → (𝐷‘𝑖) = (𝐷‘ℎ)) |
221 | 220 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = ℎ → ((𝐷‘𝑖)‘𝑍) = ((𝐷‘ℎ)‘𝑍)) |
222 | 221 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = ℎ → (((𝐷‘𝑖)‘𝑍) ≤ 𝑧 ↔ ((𝐷‘ℎ)‘𝑍) ≤ 𝑧)) |
223 | 222, 221 | ifbieq1d 4059 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = ℎ → if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)) |
224 | 219, 223 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ℎ → (((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)) = (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))) |
225 | 224 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = ℎ → (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))) = (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))) |
226 | 225 | cbvmptv 4678 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ ↦
(vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))) |
227 | 217, 226 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ ↦
(vol‘(((𝑗 ∈
ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))) |
228 | 227 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))) |
229 | | breq2 4587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑧 → (((𝐷‘ℎ)‘𝑍) ≤ 𝑤 ↔ ((𝐷‘ℎ)‘𝑍) ≤ 𝑧)) |
230 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) |
231 | 229, 230 | ifbieq2d 4061 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑧 → if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)) |
232 | 231 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)) |
233 | 232 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)) = (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))) |
234 | 233 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))) = (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))) |
235 | 234 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) |
236 | 228, 235 | eqtr2d 2645 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))))) |
237 | 236 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 →
(Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) =
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))) |
238 | 212, 237 | breq12d 4596 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → ((𝑤 − (𝐴‘𝑍)) ≤
(Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) ↔ (𝑧 − (𝐴‘𝑍)) ≤
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))))))) |
239 | 238 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤
(Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))} = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑧 − (𝐴‘𝑍)) ≤
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))} |
240 | | eqid 2610 |
. . . . . . 7
⊢
sup({𝑤 ∈
((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤
(Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤
(Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))}, ℝ, < ) |
241 | 81, 82, 83, 86, 89, 193, 211, 239, 240 | hoidmv1lelem3 39483 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))))) |
242 | 241, 209 | breqtrd 4609 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))) |
243 | 21, 80, 242 | syl2anc 691 |
. . . 4
⊢ (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))) |
244 | 20, 243 | pm2.61dan 828 |
. . 3
⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))) |
245 | 25, 29, 32, 8, 1 | hoidmvn0val 39474 |
. . . . . . 7
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
246 | 26 | prodeq1d 14490 |
. . . . . . 7
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
247 | | volicore 39471 |
. . . . . . . . . 10
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ) |
248 | 9, 7, 247 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ) |
249 | 248 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ) |
250 | 119, 121 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍))) |
251 | 250 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
252 | 251 | prodsn 14531 |
. . . . . . . 8
⊢ ((𝑍 ∈ 𝑉 ∧ (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
253 | 2, 249, 252 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
254 | 245, 246,
253 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
255 | 254 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
256 | | volico 38876 |
. . . . . . 7
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0)) |
257 | 9, 7, 256 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0)) |
258 | 257 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0)) |
259 | | iftrue 4042 |
. . . . . 6
⊢ ((𝐴‘𝑍) < (𝐵‘𝑍) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = ((𝐵‘𝑍) − (𝐴‘𝑍))) |
260 | 259 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = ((𝐵‘𝑍) − (𝐴‘𝑍))) |
261 | 255, 258,
260 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = ((𝐵‘𝑍) − (𝐴‘𝑍))) |
262 | 59 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))) |
263 | 262 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))) |
264 | 261, 263 | breq12d 4596 |
. . 3
⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → ((𝐴(𝐿‘𝑋)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ↔ ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))) |
265 | 244, 264 | mpbird 246 |
. 2
⊢ ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
266 | 245 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
267 | 246 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
268 | 253 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
269 | 257 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0)) |
270 | | iffalse 4045 |
. . . . . 6
⊢ (¬
(𝐴‘𝑍) < (𝐵‘𝑍) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = 0) |
271 | 270 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = 0) |
272 | 268, 269,
271 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) |
273 | 266, 267,
272 | 3eqtrd 2648 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = 0) |
274 | 23 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℕ ∈
V) |
275 | 274, 76 | sge0ge0 39277 |
. . . 4
⊢ (𝜑 → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
276 | 275 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
277 | 273, 276 | eqbrtrd 4605 |
. 2
⊢ ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
278 | 265, 277 | pm2.61dan 828 |
1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |