Metamath Proof Explorer

Theorem vonicc

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

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

Proof

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