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