Metamath Proof Explorer

Theorem hoidmvlelem5

Description: The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvlelem5.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
hoidmvlelem5.f ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hoidmvlelem5.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
hoidmvlelem5.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) )
hoidmvlelem5.w ⊢ 𝑊 = ( 𝑌 ∪ { 𝑍 } )
hoidmvlelem5.a ⊢ ( 𝜑 → 𝐴 : 𝑊 ⟶ ℝ )
hoidmvlelem5.b ⊢ ( 𝜑 → 𝐵 : 𝑊 ⟶ ℝ )
hoidmvlelem5.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
hoidmvlelem5.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
hoidmvlelem5.i ⊢ ( 𝜑 → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ℎ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘 ∈ 𝑌 ( ( 𝑒 ‘ 𝑘 ) [,) ( 𝑓 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑌 ( ( ( 𝑔 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ℎ ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿 ‘ 𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ℎ ‘ 𝑗 ) ) ) ) ) )
hoidmvlelem5.s ⊢ ( 𝜑 → X 𝑘 ∈ 𝑊 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑊 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
hoidmvlelem5.n ⊢ ( 𝜑 → 𝑌 ≠ ∅ )
Assertion hoidmvlelem5 ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoidmvlelem5.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2 hoidmvlelem5.f ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 hoidmvlelem5.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
4 hoidmvlelem5.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) )
5 hoidmvlelem5.w ⊢ 𝑊 = ( 𝑌 ∪ { 𝑍 } )
6 hoidmvlelem5.a ⊢ ( 𝜑 → 𝐴 : 𝑊 ⟶ ℝ )
7 hoidmvlelem5.b ⊢ ( 𝜑 → 𝐵 : 𝑊 ⟶ ℝ )
8 hoidmvlelem5.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
9 hoidmvlelem5.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
10 hoidmvlelem5.i ⊢ ( 𝜑 → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ℎ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘 ∈ 𝑌 ( ( 𝑒 ‘ 𝑘 ) [,) ( 𝑓 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑌 ( ( ( 𝑔 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ℎ ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿 ‘ 𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ℎ ‘ 𝑗 ) ) ) ) ) )
11 hoidmvlelem5.s ⊢ ( 𝜑 → X 𝑘 ∈ 𝑊 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑊 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
12 hoidmvlelem5.n ⊢ ( 𝜑 → 𝑌 ≠ ∅ )
13 nfv ⊢ Ⅎ 𝑠 𝜑
14 nfre1 ⊢ Ⅎ 𝑠 ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 )
15 13 14 nfan ⊢ Ⅎ 𝑠 ( 𝜑 ∧ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) )
16 ssfi ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 ∈ Fin )
17 2 3 16 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ Fin )
18 snfi ⊢ { 𝑍 } ∈ Fin
19 18 a1i ⊢ ( 𝜑 → { 𝑍 } ∈ Fin )
20 unfi ⊢ ( ( 𝑌 ∈ Fin ∧ { 𝑍 } ∈ Fin ) → ( 𝑌 ∪ { 𝑍 } ) ∈ Fin )
21 17 19 20 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) ∈ Fin )
22 5 21 eqeltrid ⊢ ( 𝜑 → 𝑊 ∈ Fin )
23 22 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → 𝑊 ∈ Fin )
24 6 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → 𝐴 : 𝑊 ⟶ ℝ )
25 7 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → 𝐵 : 𝑊 ⟶ ℝ )
26 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) )
27 15 1 23 24 25 26 hoidmvval0 ⊢ ( ( 𝜑 ∧ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) = 0 )
28 nnex ⊢ ℕ ∈ V
29 28 a1i ⊢ ( 𝜑 → ℕ ∈ V )
30 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
31 22 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑊 ∈ Fin )
32 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
33 elmapi ⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
34 32 33 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
35 9 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
36 elmapi ⊢ ( ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
38 1 31 34 37 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) )
39 30 38 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
40 39 fmpttd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
41 29 40 sge0ge0 ⊢ ( 𝜑 → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
43 27 42 eqbrtrd ⊢ ( ( 𝜑 ∧ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
44 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
45 1 22 6 7 hoidmvcl ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ( 0 [,) +∞ ) )
46 44 45 sselid ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ* )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ* )
48 29 40 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
49 48 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
50 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
51 50 45 sselid ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ )
52 ltpnf ⊢ ( ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) < +∞ )
53 51 52 syl ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) < +∞ )
54 53 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) < +∞ )
55 id ⊢ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ )
56 55 eqcomd ⊢ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ → +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
57 56 adantl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
58 54 57 breqtrd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) < ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
59 47 49 58 xrltled ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
60 59 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
61 simpll ⊢ ( ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → 𝜑 )
62 simpr ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) )
63 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑠 ) ∈ ℝ )
64 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑊 ) → ( 𝐵 ‘ 𝑠 ) ∈ ℝ )
65 63 64 ltnled ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑊 ) → ( ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ↔ ¬ ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) )
66 65 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝑊 ¬ ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) )
67 ralnex ⊢ ( ∀ 𝑠 ∈ 𝑊 ¬ ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ↔ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) )
68 67 a1i ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝑊 ¬ ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ↔ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) )
69 66 68 bitrd ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ↔ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ↔ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) )
71 62 70 mpbird ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) )
72 71 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) )
73 simpr ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ )
74 28 a1i ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ℕ ∈ V )
75 40 adantr ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
76 74 75 sge0repnf ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) )
77 73 76 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
78 77 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
79 simpll ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) )
80 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐶 ‘ 𝑗 ) = ( 𝐶 ‘ 𝑖 ) )
81 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑖 ) )
82 80 81 oveq12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) )
83 82 cbvmptv ⊢ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) = ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) )
84 83 fveq2i ⊢ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) )
85 84 eleq1i ⊢ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ↔ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ )
86 85 biimpi ⊢ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ )
87 86 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ )
88 simpr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
89 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑋 ∈ Fin )
90 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑌 ⊆ 𝑋 )
91 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑌 ≠ ∅ )
92 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) )
93 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝐴 : 𝑊 ⟶ ℝ )
94 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝐵 : 𝑊 ⟶ ℝ )
95 fveq2 ⊢ ( 𝑠 = 𝑘 → ( 𝐴 ‘ 𝑠 ) = ( 𝐴 ‘ 𝑘 ) )
96 fveq2 ⊢ ( 𝑠 = 𝑘 → ( 𝐵 ‘ 𝑠 ) = ( 𝐵 ‘ 𝑘 ) )
97 95 96 breq12d ⊢ ( 𝑠 = 𝑘 → ( ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ↔ ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) )
98 97 cbvralvw ⊢ ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ↔ ∀ 𝑘 ∈ 𝑊 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
99 98 birani ⊢ ( ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ∧ 𝑘 ∈ 𝑊 ) → ∀ 𝑘 ∈ 𝑊 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
100 simpr ⊢ ( ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ 𝑊 )
101 rspa ⊢ ( ( ∀ 𝑘 ∈ 𝑊 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
102 99 100 101 syl2anc ⊢ ( ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
103 102 ad5ant25 ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
104 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
105 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
106 85 biimpri ⊢ ( ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
107 106 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
108 fveq1 ⊢ ( 𝑑 = 𝑐 → ( 𝑑 ‘ 𝑖 ) = ( 𝑐 ‘ 𝑖 ) )
109 108 breq1d ⊢ ( 𝑑 = 𝑐 → ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 ) )
110 109 108 ifbieq1d ⊢ ( 𝑑 = 𝑐 → if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) = if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) )
111 108 110 ifeq12d ⊢ ( 𝑑 = 𝑐 → if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) = if ( 𝑖 ∈ 𝑌 , ( 𝑐 ‘ 𝑖 ) , if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) ) )
112 111 mpteq2dv ⊢ ( 𝑑 = 𝑐 → ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) = ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑐 ‘ 𝑖 ) , if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) ) ) )
113 eleq1w ⊢ ( 𝑖 = 𝑗 → ( 𝑖 ∈ 𝑌 ↔ 𝑗 ∈ 𝑌 ) )
114 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 𝑗 ) )
115 114 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 ) )
116 115 114 ifbieq1d ⊢ ( 𝑖 = 𝑗 → if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) = if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) )
117 113 114 116 ifbieq12d ⊢ ( 𝑖 = 𝑗 → if ( 𝑖 ∈ 𝑌 , ( 𝑐 ‘ 𝑖 ) , if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) ) = if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) )
118 117 cbvmptv ⊢ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑐 ‘ 𝑖 ) , if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) ) ) = ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) )
119 118 a1i ⊢ ( 𝑑 = 𝑐 → ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑐 ‘ 𝑖 ) , if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) ) ) = ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) )
120 112 119 eqtrd ⊢ ( 𝑑 = 𝑐 → ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) = ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) )
121 120 cbvmptv ⊢ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) )
122 121 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) )
123 eqid ⊢ ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) = ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) )
124 simpr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
125 oveq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) = ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) )
126 125 oveq2d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ) = ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) )
127 breq2 ⊢ ( 𝑤 = 𝑥 → ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 ↔ ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 ) )
128 eqidd ⊢ ( 𝑤 = 𝑥 → ( 𝑑 ‘ 𝑖 ) = ( 𝑑 ‘ 𝑖 ) )
129 id ⊢ ( 𝑤 = 𝑥 → 𝑤 = 𝑥 )
130 127 128 129 ifbieq12d ⊢ ( 𝑤 = 𝑥 → if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) = if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) )
131 130 ifeq2d ⊢ ( 𝑤 = 𝑥 → if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) = if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) )
132 131 mpteq2dv ⊢ ( 𝑤 = 𝑥 → ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) = ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) )
133 132 mpteq2dv ⊢ ( 𝑤 = 𝑥 → ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) = ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) )
134 133 cbvmptv ⊢ ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) )
135 134 a1i ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) )
136 id ⊢ ( 𝑤 = 𝑧 → 𝑤 = 𝑧 )
137 135 136 fveq12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) = ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) )
138 137 fveq1d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) = ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) )
139 138 oveq2d ⊢ ( 𝑤 = 𝑧 → ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) = ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) )
140 139 mpteq2dv ⊢ ( 𝑤 = 𝑧 → ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) = ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) )
141 fveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐶 ‘ 𝑙 ) = ( 𝐶 ‘ 𝑗 ) )
142 2fveq3 ⊢ ( 𝑙 = 𝑗 → ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) = ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
143 141 142 oveq12d ⊢ ( 𝑙 = 𝑗 → ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
144 143 cbvmptv ⊢ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
145 144 a1i ⊢ ( 𝑤 = 𝑧 → ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
146 140 145 eqtrd ⊢ ( 𝑤 = 𝑧 → ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
147 146 fveq2d ⊢ ( 𝑤 = 𝑧 → ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
148 147 oveq2d ⊢ ( 𝑤 = 𝑧 → ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) ) = ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
149 126 148 breq12d ⊢ ( 𝑤 = 𝑧 → ( ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) ) ↔ ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
150 149 cbvrabv ⊢ { 𝑤 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) ) } = { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) }
151 eqid ⊢ sup ( { 𝑤 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) ) } , ℝ , < ) = sup ( { 𝑤 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) ) } , ℝ , < )
152 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ℎ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘 ∈ 𝑌 ( ( 𝑒 ‘ 𝑘 ) [,) ( 𝑓 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑌 ( ( ( 𝑔 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ℎ ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿 ‘ 𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ℎ ‘ 𝑗 ) ) ) ) ) )
153 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → X 𝑘 ∈ 𝑊 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑊 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
154 1 89 90 91 92 5 93 94 103 104 105 107 122 123 124 150 151 152 153 hoidmvlelem4 ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
155 79 87 88 154 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
156 155 ralrimiva ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ∀ 𝑟 ∈ ℝ+ ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
157 nfv ⊢ Ⅎ 𝑟 ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
158 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ* )
159 0xr ⊢ 0 ∈ ℝ*
160 159 a1i ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → 0 ∈ ℝ* )
161 pnfxr ⊢ +∞ ∈ ℝ*
162 161 a1i ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → +∞ ∈ ℝ* )
163 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
164 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
165 ltpnf ⊢ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) < +∞ )
166 165 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) < +∞ )
167 160 162 163 164 166 elicod ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ( 0 [,) +∞ ) )
168 157 158 167 xralrple2 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ↔ ∀ 𝑟 ∈ ℝ+ ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
169 156 168 mpbird ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
170 61 72 78 169 syl21anc ⊢ ( ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
171 60 170 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
172 43 171 pm2.61dan ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )