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