Proof of Theorem ovn0lem
Step | Hyp | Ref
| Expression |
1 | | iccssxr 12127 |
. . 3
⊢
(0[,]+∞) ⊆ ℝ* |
2 | | ovn0lem.infm |
. . 3
⊢ (𝜑 → inf(𝑀, ℝ*, < ) ∈
(0[,]+∞)) |
3 | 1, 2 | sseldi 3566 |
. 2
⊢ (𝜑 → inf(𝑀, ℝ*, < ) ∈
ℝ*) |
4 | | 0xr 9965 |
. . 3
⊢ 0 ∈
ℝ* |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → 0 ∈
ℝ*) |
6 | | ovn0lem.m |
. . . . 5
⊢ 𝑀 = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))} |
7 | | ssrab2 3650 |
. . . . 5
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))} ⊆
ℝ* |
8 | 6, 7 | eqsstri 3598 |
. . . 4
⊢ 𝑀 ⊆
ℝ* |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑀 ⊆
ℝ*) |
10 | | 1re 9918 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
11 | | 0re 9919 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
12 | 10, 11 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℝ ∧ 0 ∈ ℝ) |
13 | | opelxp 5070 |
. . . . . . . . . . . . 13
⊢ (〈1,
0〉 ∈ (ℝ × ℝ) ↔ (1 ∈ ℝ ∧ 0
∈ ℝ)) |
14 | 12, 13 | mpbir 220 |
. . . . . . . . . . . 12
⊢ 〈1,
0〉 ∈ (ℝ × ℝ) |
15 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑙 ∈ 𝑋) → 〈1, 0〉 ∈ (ℝ
× ℝ)) |
16 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ 𝑋 ↦ 〈1, 0〉) = (𝑙 ∈ 𝑋 ↦ 〈1, 0〉) |
17 | 15, 16 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑙 ∈ 𝑋 ↦ 〈1, 0〉):𝑋⟶(ℝ ×
ℝ)) |
18 | | reex 9906 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
19 | 18, 18 | xpex 6860 |
. . . . . . . . . . . 12
⊢ (ℝ
× ℝ) ∈ V |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ × ℝ)
∈ V) |
21 | | ovn0lem.x |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ Fin) |
22 | | elmapg 7757 |
. . . . . . . . . . 11
⊢
(((ℝ × ℝ) ∈ V ∧ 𝑋 ∈ Fin) → ((𝑙 ∈ 𝑋 ↦ 〈1, 0〉) ∈ ((ℝ
× ℝ) ↑𝑚 𝑋) ↔ (𝑙 ∈ 𝑋 ↦ 〈1, 0〉):𝑋⟶(ℝ ×
ℝ))) |
23 | 20, 21, 22 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑙 ∈ 𝑋 ↦ 〈1, 0〉) ∈ ((ℝ
× ℝ) ↑𝑚 𝑋) ↔ (𝑙 ∈ 𝑋 ↦ 〈1, 0〉):𝑋⟶(ℝ ×
ℝ))) |
24 | 17, 23 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → (𝑙 ∈ 𝑋 ↦ 〈1, 0〉) ∈ ((ℝ
× ℝ) ↑𝑚 𝑋)) |
25 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑙 ∈ 𝑋 ↦ 〈1, 0〉) ∈ ((ℝ
× ℝ) ↑𝑚 𝑋)) |
26 | | ovn0lem.i |
. . . . . . . 8
⊢ 𝐼 = (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈1, 0〉)) |
27 | 25, 26 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ)
↑𝑚 𝑋)) |
28 | | ovex 6577 |
. . . . . . . . 9
⊢ ((ℝ
× ℝ) ↑𝑚 𝑋) ∈ V |
29 | 28 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ × ℝ)
↑𝑚 𝑋) ∈ V) |
30 | | nnex 10903 |
. . . . . . . . 9
⊢ ℕ
∈ V |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℕ ∈
V) |
32 | | elmapg 7757 |
. . . . . . . 8
⊢
((((ℝ × ℝ) ↑𝑚 𝑋) ∈ V ∧ ℕ ∈
V) → (𝐼 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ↔
𝐼:ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋))) |
33 | 29, 31, 32 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐼 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ↔
𝐼:ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋))) |
34 | 27, 33 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
35 | | ovn0lem.n0 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ≠ ∅) |
36 | | n0 3890 |
. . . . . . . . . . . 12
⊢ (𝑋 ≠ ∅ ↔
∃𝑙 𝑙 ∈ 𝑋) |
37 | 35, 36 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑙 𝑙 ∈ 𝑋) |
38 | 37 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∃𝑙 𝑙 ∈ 𝑋) |
39 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) |
40 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘(vol‘(([,) ∘ (𝐼‘𝑗))‘𝑙)) |
41 | 21 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → 𝑋 ∈ Fin) |
42 | 27 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
43 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋) → (𝐼‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐼‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
46 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
47 | 45, 46 | fvovco 38376 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ((1st ‘((𝐼‘𝑗)‘𝑘))[,)(2nd ‘((𝐼‘𝑗)‘𝑘)))) |
48 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
49 | 25 | elexd 3187 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑙 ∈ 𝑋 ↦ 〈1, 0〉) ∈
V) |
50 | 26 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑗 ∈ ℕ ∧ (𝑙 ∈ 𝑋 ↦ 〈1, 0〉) ∈ V) →
(𝐼‘𝑗) = (𝑙 ∈ 𝑋 ↦ 〈1, 0〉)) |
51 | 48, 49, 50 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) = (𝑙 ∈ 𝑋 ↦ 〈1, 0〉)) |
52 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐼‘𝑗) = (𝑙 ∈ 𝑋 ↦ 〈1, 0〉)) |
53 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑙 = 𝑘) → 〈1, 0〉 = 〈1,
0〉) |
54 | 14 | elexi 3186 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 〈1,
0〉 ∈ V |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 〈1, 0〉 ∈
V) |
56 | 52, 53, 46, 55 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐼‘𝑗)‘𝑘) = 〈1, 0〉) |
57 | 56 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝐼‘𝑗)‘𝑘)) = (1st ‘〈1,
0〉)) |
58 | 10 | elexi 3186 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
V |
59 | 4 | elexi 3186 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
V |
60 | 58, 59 | op1st 7067 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1st ‘〈1, 0〉) = 1 |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1st ‘〈1,
0〉) = 1) |
62 | 57, 61 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝐼‘𝑗)‘𝑘)) = 1) |
63 | 56 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝐼‘𝑗)‘𝑘)) = (2nd ‘〈1,
0〉)) |
64 | 58, 59 | op2nd 7068 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(2nd ‘〈1, 0〉) = 0 |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (2nd ‘〈1,
0〉) = 0) |
66 | 63, 65 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝐼‘𝑗)‘𝑘)) = 0) |
67 | 62, 66 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((1st ‘((𝐼‘𝑗)‘𝑘))[,)(2nd ‘((𝐼‘𝑗)‘𝑘))) = (1[,)0)) |
68 | | 0le1 10430 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≤
1 |
69 | 10 | rexri 9976 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ* |
70 | | ico0 12092 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ* ∧ 0 ∈ ℝ*) → ((1[,)0)
= ∅ ↔ 0 ≤ 1)) |
71 | 69, 4, 70 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1[,)0)
= ∅ ↔ 0 ≤ 1) |
72 | 68, 71 | mpbir 220 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1[,)0) =
∅ |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1[,)0) = ∅) |
74 | 47, 67, 73 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ∅) |
75 | 74 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘∅)) |
76 | | vol0 38851 |
. . . . . . . . . . . . . . . . 17
⊢
(vol‘∅) = 0 |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘∅) =
0) |
78 | 75, 77 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = 0) |
79 | | 0cn 9911 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℂ |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 0 ∈ ℂ) |
81 | 78, 80 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) ∈ ℂ) |
82 | 81 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) ∈ ℂ) |
83 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑙)) |
84 | 83 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑙 → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑙))) |
85 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → 𝑙 ∈ 𝑋) |
86 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑙 → (𝑘 ∈ 𝑋 ↔ 𝑙 ∈ 𝑋)) |
87 | 86 | anbi2d 736 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑙 → (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ↔ ((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑙 ∈ 𝑋))) |
88 | 84 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑙 → ((vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = 0 ↔ (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑙)) = 0)) |
89 | 87, 88 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = 0) ↔ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑙)) = 0))) |
90 | 89, 78 | chvarv 2251 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑙)) = 0) |
91 | 39, 40, 41, 82, 84, 85, 90 | fprod0 38663 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = 0) |
92 | 91 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑙 ∈ 𝑋 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = 0)) |
93 | 92 | exlimdv 1848 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∃𝑙 𝑙 ∈ 𝑋 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = 0)) |
94 | 38, 93 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = 0) |
95 | 94 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ 0)) |
96 | 95 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ 0))) |
97 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑗𝜑 |
98 | 97, 31 | sge0z 39268 |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ 0)) =
0) |
99 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → 0 = 0) |
100 | 96, 98, 99 | 3eqtrrd 2649 |
. . . . . 6
⊢ (𝜑 → 0 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) |
101 | | fveq1 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝐼 → (𝑖‘𝑗) = (𝐼‘𝑗)) |
102 | 101 | coeq2d 5206 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝐼 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗))) |
103 | 102 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝐼 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
104 | 103 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
105 | 104 | ralrimivw 2950 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → ∀𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
106 | 105 | prodeq2d 14491 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
107 | 106 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))) |
108 | 107 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) |
109 | 108 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (0 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 0 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) |
110 | 109 | rspcev 3282 |
. . . . . 6
⊢ ((𝐼 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
0 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)0 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
111 | 34, 100, 110 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)0 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
112 | 5, 111 | jca 553 |
. . . 4
⊢ (𝜑 → (0 ∈
ℝ* ∧ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)0 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
113 | | eqeq1 2614 |
. . . . . 6
⊢ (𝑧 = 0 → (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 0 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
114 | 113 | rexbidv 3034 |
. . . . 5
⊢ (𝑧 = 0 → (∃𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)0 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
115 | 114, 6 | elrab2 3333 |
. . . 4
⊢ (0 ∈
𝑀 ↔ (0 ∈
ℝ* ∧ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)0 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
116 | 112, 115 | sylibr 223 |
. . 3
⊢ (𝜑 → 0 ∈ 𝑀) |
117 | | infxrlb 12036 |
. . 3
⊢ ((𝑀 ⊆ ℝ*
∧ 0 ∈ 𝑀) →
inf(𝑀, ℝ*,
< ) ≤ 0) |
118 | 9, 116, 117 | syl2anc 691 |
. 2
⊢ (𝜑 → inf(𝑀, ℝ*, < ) ≤
0) |
119 | | pnfxr 9971 |
. . . 4
⊢ +∞
∈ ℝ* |
120 | 119 | a1i 11 |
. . 3
⊢ (𝜑 → +∞ ∈
ℝ*) |
121 | | iccgelb 12101 |
. . 3
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
inf(𝑀, ℝ*,
< ) ∈ (0[,]+∞)) → 0 ≤ inf(𝑀, ℝ*, <
)) |
122 | 5, 120, 2, 121 | syl3anc 1318 |
. 2
⊢ (𝜑 → 0 ≤ inf(𝑀, ℝ*, <
)) |
123 | 3, 5, 118, 122 | xrletrid 11862 |
1
⊢ (𝜑 → inf(𝑀, ℝ*, < ) =
0) |