Metamath Proof Explorer

Theorem vonioo

Description: The n-dimensional Lebesgue measure of an open interval. This is the first statement in Proposition 115G (d) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses vonioo.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
vonioo.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
vonioo.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
vonioo.i ⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) )
vonioo.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
Assertion vonioo ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 vonioo.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 vonioo.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
3 vonioo.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
4 vonioo.i ⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) )
5 vonioo.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 : 𝑋 ⟶ ℝ )
7 feq2 ⊢ ( 𝑋 = ∅ → ( 𝐴 : 𝑋 ⟶ ℝ ↔ 𝐴 : ∅ ⟶ ℝ ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 : 𝑋 ⟶ ℝ ↔ 𝐴 : ∅ ⟶ ℝ ) )
9 6 8 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 : ∅ ⟶ ℝ )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐵 : 𝑋 ⟶ ℝ )
11 feq2 ⊢ ( 𝑋 = ∅ → ( 𝐵 : 𝑋 ⟶ ℝ ↔ 𝐵 : ∅ ⟶ ℝ ) )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐵 : 𝑋 ⟶ ℝ ↔ 𝐵 : ∅ ⟶ ℝ ) )
13 10 12 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐵 : ∅ ⟶ ℝ )
14 5 9 13 hoidmv0val ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐵 ) = 0 )
15 14 eqcomd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 0 = ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐵 ) )
16 fveq2 ⊢ ( 𝑋 = ∅ → ( voln ‘ 𝑋 ) = ( voln ‘ ∅ ) )
17 4 a1i ⊢ ( 𝑋 = ∅ → 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) )
18 ixpeq1 ⊢ ( 𝑋 = ∅ → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) = X 𝑘 ∈ ∅ ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) )
19 17 18 eqtrd ⊢ ( 𝑋 = ∅ → 𝐼 = X 𝑘 ∈ ∅ ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) )
20 16 19 fveq12d ⊢ ( 𝑋 = ∅ → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( ( voln ‘ ∅ ) ‘ X 𝑘 ∈ ∅ ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( ( voln ‘ ∅ ) ‘ X 𝑘 ∈ ∅ ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) ) )
22 0fin ⊢ ∅ ∈ Fin
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∅ ∈ Fin )
24 eqid ⊢ dom ( voln ‘ ∅ ) = dom ( voln ‘ ∅ )
25 ressxr ⊢ ℝ ⊆ ℝ*
26 25 a1i ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ℝ ⊆ ℝ* )
27 9 26 fssd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 : ∅ ⟶ ℝ* )
28 13 26 fssd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐵 : ∅ ⟶ ℝ* )
29 23 24 27 28 ioovonmbl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → X 𝑘 ∈ ∅ ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom ( voln ‘ ∅ ) )
30 29 von0val ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ ∅ ) ‘ X 𝑘 ∈ ∅ ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 )
31 21 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = 0 )
32 fveq2 ⊢ ( 𝑋 = ∅ → ( 𝐿 ‘ 𝑋 ) = ( 𝐿 ‘ ∅ ) )
33 32 oveqd ⊢ ( 𝑋 = ∅ → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐵 ) )
34 33 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐵 ) )
35 15 31 34 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
36 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
37 36 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
38 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑋 ≠ ∅ )
39 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 )
40 38 39 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
41 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
42 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
43 volico ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) )
44 41 42 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) )
45 44 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) )
46 rspa ⊢ ( ( ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
47 46 iftrued ⊢ ( ( ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ∧ 𝑘 ∈ 𝑋 ) → if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
48 47 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) ∧ 𝑘 ∈ 𝑋 ) → if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
49 45 48 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
50 49 ex ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ( 𝑘 ∈ 𝑋 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ) )
51 40 50 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
52 51 prodeq2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
53 52 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ∏ 𝑘 ∈ 𝑋 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
54 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑗 ) )
55 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑗 ) )
56 54 55 breq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ↔ ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ) )
57 56 cbvralvw ⊢ ( ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ↔ ∀ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) )
58 57 biimpi ⊢ ( ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) → ∀ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) )
59 58 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ∀ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) )
60 1 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ∈ Fin )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ) → 𝑋 ∈ Fin )
62 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝐴 : 𝑋 ⟶ ℝ )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ) → 𝐴 : 𝑋 ⟶ ℝ )
64 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝐵 : 𝑋 ⟶ ℝ )
65 64 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ) → 𝐵 : 𝑋 ⟶ ℝ )
66 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ≠ ∅ )
67 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ) → 𝑋 ≠ ∅ )
68 57 46 sylanbr ⊢ ( ( ∀ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
69 68 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
70 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐴 ‘ 𝑗 ) = ( 𝐴 ‘ 𝑘 ) )
71 70 oveq1d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) = ( ( 𝐴 ‘ 𝑘 ) + ( 1 / 𝑚 ) ) )
72 71 cbvmptv ⊢ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) = ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑘 ) + ( 1 / 𝑚 ) ) )
73 72 a1i ⊢ ( 𝑚 = 𝑛 → ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) = ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑘 ) + ( 1 / 𝑚 ) ) ) )
74 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 1 / 𝑚 ) = ( 1 / 𝑛 ) )
75 74 oveq2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 ‘ 𝑘 ) + ( 1 / 𝑚 ) ) = ( ( 𝐴 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) )
76 75 mpteq2dv ⊢ ( 𝑚 = 𝑛 → ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑘 ) + ( 1 / 𝑚 ) ) ) = ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) )
77 73 76 eqtrd ⊢ ( 𝑚 = 𝑛 → ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) = ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) )
78 77 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) )
79 nfcv ⊢ Ⅎ 𝑛 X 𝑘 ∈ 𝑋 ( ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑚 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
80 nfcv ⊢ Ⅎ 𝑚 𝑋
81 nffvmpt1 ⊢ Ⅎ 𝑚 ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑛 )
82 nfcv ⊢ Ⅎ 𝑚 𝑘
83 81 82 nffv ⊢ Ⅎ 𝑚 ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑛 ) ‘ 𝑘 )
84 nfcv ⊢ Ⅎ 𝑚 [,)
85 nfcv ⊢ Ⅎ 𝑚 ( 𝐵 ‘ 𝑘 )
86 83 84 85 nfov ⊢ Ⅎ 𝑚 ( ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
87 80 86 nfixpw ⊢ Ⅎ 𝑚 X 𝑘 ∈ 𝑋 ( ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
88 fveq2 ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑚 ) = ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑛 ) )
89 88 fveq1d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑚 ) ‘ 𝑘 ) = ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑛 ) ‘ 𝑘 ) )
90 89 oveq1d ⊢ ( 𝑚 = 𝑛 → ( ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑚 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = ( ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
91 90 ixpeq2dv ⊢ ( 𝑚 = 𝑛 → X 𝑘 ∈ 𝑋 ( ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑚 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = X 𝑘 ∈ 𝑋 ( ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
92 79 87 91 cbvmpt ⊢ ( 𝑚 ∈ ℕ ↦ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑚 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( 𝑛 ∈ ℕ ↦ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑚 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) + ( 1 / 𝑚 ) ) ) ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
93 61 63 65 67 69 4 78 92 vonioolem2 ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ∏ 𝑘 ∈ 𝑋 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
94 59 93 syldan ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ∏ 𝑘 ∈ 𝑋 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
95 5 60 66 62 64 hoidmvn0val ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
96 95 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
97 53 94 96 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
98 rexnal ⊢ ( ∃ 𝑘 ∈ 𝑋 ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ↔ ¬ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
99 98 bicomi ⊢ ( ¬ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ 𝑋 ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
100 99 biimpi ⊢ ( ¬ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) → ∃ 𝑘 ∈ 𝑋 ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
101 100 adantl ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ∃ 𝑘 ∈ 𝑋 ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
102 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
103 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
104 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
105 103 104 lenltd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ( ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ↔ ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) )
106 102 105 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) )
107 106 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) → ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) )
108 107 reximdva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑋 ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) → ∃ 𝑘 ∈ 𝑋 ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) )
109 108 adantr ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ( ∃ 𝑘 ∈ 𝑋 ¬ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) → ∃ 𝑘 ∈ 𝑋 ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) )
110 101 109 mpd ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ∃ 𝑘 ∈ 𝑋 ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) )
111 110 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ¬ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ∃ 𝑘 ∈ 𝑋 ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) )
112 nfcv ⊢ Ⅎ 𝑘 ( voln ‘ 𝑋 )
113 nfixp1 ⊢ Ⅎ 𝑘 X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) )
114 4 113 nfcxfr ⊢ Ⅎ 𝑘 𝐼
115 112 114 nffv ⊢ Ⅎ 𝑘 ( ( voln ‘ 𝑋 ) ‘ 𝐼 )
116 nfcv ⊢ Ⅎ 𝑘 ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 )
117 115 116 nfeq ⊢ Ⅎ 𝑘 ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 )
118 1 vonmea ⊢ ( 𝜑 → ( voln ‘ 𝑋 ) ∈ Meas )
119 118 mea0 ⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ ∅ ) = 0 )
120 119 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( ( voln ‘ 𝑋 ) ‘ ∅ ) = 0 )
121 4 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) )
122 simp2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → 𝑘 ∈ 𝑋 )
123 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) )
124 25 41 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ* )
125 124 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ* )
126 25 42 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
127 126 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
128 ioo0 ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ* ) → ( ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) = ∅ ↔ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) )
129 125 127 128 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) = ∅ ↔ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) )
130 123 129 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) = ∅ )
131 rspe ⊢ ( ( 𝑘 ∈ 𝑋 ∧ ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) = ∅ ) → ∃ 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) = ∅ )
132 122 130 131 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ∃ 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) = ∅ )
133 ixp0 ⊢ ( ∃ 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) = ∅ → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) = ∅ )
134 132 133 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) ) = ∅ )
135 121 134 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → 𝐼 = ∅ )
136 135 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( ( voln ‘ 𝑋 ) ‘ ∅ ) )
137 ne0i ⊢ ( 𝑘 ∈ 𝑋 → 𝑋 ≠ ∅ )
138 137 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑋 ≠ ∅ )
139 138 95 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
140 139 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
141 eleq1w ⊢ ( 𝑗 = 𝑘 → ( 𝑗 ∈ 𝑋 ↔ 𝑘 ∈ 𝑋 ) )
142 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐵 ‘ 𝑗 ) = ( 𝐵 ‘ 𝑘 ) )
143 142 70 breq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ↔ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) )
144 141 143 3anbi23d ⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) ) )
145 144 imbi1d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 ) ) )
146 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) )
147 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → 𝑋 ∈ Fin )
148 volicore ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
149 41 42 148 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
150 149 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℂ )
151 150 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℂ )
152 simp2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → 𝑗 ∈ 𝑋 )
153 54 55 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) )
154 153 fveq2d ⊢ ( 𝑘 = 𝑗 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) )
155 154 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) ∧ 𝑘 = 𝑗 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) )
156 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑗 ) ∈ ℝ )
157 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑗 ) ∈ ℝ )
158 volico ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) = if ( ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , 0 ) )
159 156 157 158 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) = if ( ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , 0 ) )
160 159 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) = if ( ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , 0 ) )
161 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) )
162 157 156 lenltd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ↔ ¬ ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ) )
163 162 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ( ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ↔ ¬ ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ) )
164 161 163 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ¬ ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) )
165 164 iffalsed ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → if ( ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , 0 ) = 0 )
166 160 165 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) = 0 )
167 166 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) ∧ 𝑘 = 𝑗 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) = 0 )
168 155 167 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) ∧ 𝑘 = 𝑗 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 )
169 146 147 151 152 168 fprodeq0g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 )
170 145 169 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 )
171 140 170 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = 0 )
172 120 136 171 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
173 172 3exp ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 → ( ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ) ) )
174 173 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝑘 ∈ 𝑋 → ( ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ) ) )
175 38 117 174 rexlimd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑘 ∈ 𝑋 ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ) )
176 175 imp ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ∃ 𝑘 ∈ 𝑋 ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
177 111 176 syldan ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ ¬ ∀ 𝑘 ∈ 𝑋 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
178 97 177 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
179 37 178 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
180 35 179 pm2.61dan ⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )