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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
33 elmapi ⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
34 32 33 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
35 9 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
36 elmapi ⊢ ( ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
38 1 31 34 37 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) )
39 30 38 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 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 sseldi ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ* )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ* )
48 29 40 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
49 48 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
50 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
51 50 45 sseldi ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ )
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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑠 ) ∈ ℝ )
64 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑊 ) → ( 𝐵 ‘ 𝑠 ) ∈ ℝ )
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 biimpi ⊢ ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) → ∀ 𝑘 ∈ 𝑊 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
100 99 adantr ⊢ ( ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ∧ 𝑘 ∈ 𝑊 ) → ∀ 𝑘 ∈ 𝑊 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
101 simpr ⊢ ( ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ 𝑊 )
102 rspa ⊢ ( ( ∀ 𝑘 ∈ 𝑊 ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
103 100 101 102 syl2anc ⊢ ( ( ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
104 103 ad5ant25 ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
105 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
106 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
107 85 biimpri ⊢ ( ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
108 107 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
109 fveq1 ⊢ ( 𝑑 = 𝑐 → ( 𝑑 ‘ 𝑖 ) = ( 𝑐 ‘ 𝑖 ) )
110 109 breq1d ⊢ ( 𝑑 = 𝑐 → ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 ) )
111 110 109 ifbieq1d ⊢ ( 𝑑 = 𝑐 → if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) = if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) )
112 109 111 ifeq12d ⊢ ( 𝑑 = 𝑐 → if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) = if ( 𝑖 ∈ 𝑌 , ( 𝑐 ‘ 𝑖 ) , if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) ) )
113 112 mpteq2dv ⊢ ( 𝑑 = 𝑐 → ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) = ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑐 ‘ 𝑖 ) , if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) ) ) )
114 eleq1w ⊢ ( 𝑖 = 𝑗 → ( 𝑖 ∈ 𝑌 ↔ 𝑗 ∈ 𝑌 ) )
115 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 𝑗 ) )
116 115 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 ) )
117 116 115 ifbieq1d ⊢ ( 𝑖 = 𝑗 → if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) = if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) )
118 114 115 117 ifbieq12d ⊢ ( 𝑖 = 𝑗 → if ( 𝑖 ∈ 𝑌 , ( 𝑐 ‘ 𝑖 ) , if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) ) = if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) )
119 118 cbvmptv ⊢ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑐 ‘ 𝑖 ) , if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) ) ) = ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) )
120 119 a1i ⊢ ( 𝑑 = 𝑐 → ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑐 ‘ 𝑖 ) , if ( ( 𝑐 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑖 ) , 𝑥 ) ) ) = ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) )
121 113 120 eqtrd ⊢ ( 𝑑 = 𝑐 → ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) = ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) )
122 121 cbvmptv ⊢ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) )
123 122 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) )
124 eqid ⊢ ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) = ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) )
125 simpr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
126 oveq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) = ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) )
127 126 oveq2d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ) = ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) )
128 breq2 ⊢ ( 𝑤 = 𝑥 → ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 ↔ ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 ) )
129 eqidd ⊢ ( 𝑤 = 𝑥 → ( 𝑑 ‘ 𝑖 ) = ( 𝑑 ‘ 𝑖 ) )
130 id ⊢ ( 𝑤 = 𝑥 → 𝑤 = 𝑥 )
131 128 129 130 ifbieq12d ⊢ ( 𝑤 = 𝑥 → if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) = if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) )
132 131 ifeq2d ⊢ ( 𝑤 = 𝑥 → if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) = if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) )
133 132 mpteq2dv ⊢ ( 𝑤 = 𝑥 → ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) = ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) )
134 133 mpteq2dv ⊢ ( 𝑤 = 𝑥 → ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) = ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) )
135 134 cbvmptv ⊢ ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) )
136 135 a1i ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) )
137 id ⊢ ( 𝑤 = 𝑧 → 𝑤 = 𝑧 )
138 136 137 fveq12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) = ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) )
139 138 fveq1d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) = ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) )
140 139 oveq2d ⊢ ( 𝑤 = 𝑧 → ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) = ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) )
141 140 mpteq2dv ⊢ ( 𝑤 = 𝑧 → ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) = ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) )
142 fveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐶 ‘ 𝑙 ) = ( 𝐶 ‘ 𝑗 ) )
143 2fveq3 ⊢ ( 𝑙 = 𝑗 → ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) = ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
144 142 143 oveq12d ⊢ ( 𝑙 = 𝑗 → ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
145 144 cbvmptv ⊢ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
146 145 a1i ⊢ ( 𝑤 = 𝑧 → ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
147 141 146 eqtrd ⊢ ( 𝑤 = 𝑧 → ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
148 147 fveq2d ⊢ ( 𝑤 = 𝑧 → ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
149 148 oveq2d ⊢ ( 𝑤 = 𝑧 → ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) ) = ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
150 127 149 breq12d ⊢ ( 𝑤 = 𝑧 → ( ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) ) ↔ ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
151 150 cbvrabv ⊢ { 𝑤 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) ) } = { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑥 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑥 , ( 𝑑 ‘ 𝑖 ) , 𝑥 ) ) ) ) ) ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) }
152 eqid ⊢ sup ( { 𝑤 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) ) } , ℝ , < ) = sup ( { 𝑤 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) · ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑙 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑙 ) ( 𝐿 ‘ 𝑊 ) ( ( ( 𝑤 ∈ ℝ ↦ ( 𝑑 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖 ∈ 𝑊 ↦ if ( 𝑖 ∈ 𝑌 , ( 𝑑 ‘ 𝑖 ) , if ( ( 𝑑 ‘ 𝑖 ) ≤ 𝑤 , ( 𝑑 ‘ 𝑖 ) , 𝑤 ) ) ) ) ) ‘ 𝑤 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ) ) ) } , ℝ , < )
153 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ℎ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘 ∈ 𝑌 ( ( 𝑒 ‘ 𝑘 ) [,) ( 𝑓 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑌 ( ( ( 𝑔 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ℎ ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿 ‘ 𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ℎ ‘ 𝑗 ) ) ) ) ) )
154 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → X 𝑘 ∈ 𝑊 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑊 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
155 1 89 90 91 92 5 93 94 104 105 106 108 123 124 125 151 152 153 154 hoidmvlelem4 ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑖 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑖 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
156 79 87 88 155 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
157 156 ralrimiva ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ∀ 𝑟 ∈ ℝ+ ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
158 nfv ⊢ Ⅎ 𝑟 ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
159 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ* )
160 0xr ⊢ 0 ∈ ℝ*
161 160 a1i ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → 0 ∈ ℝ* )
162 pnfxr ⊢ +∞ ∈ ℝ*
163 162 a1i ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → +∞ ∈ ℝ* )
164 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
165 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
166 ltpnf ⊢ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) < +∞ )
167 166 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) < +∞ )
168 161 163 164 165 167 elicod ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ( 0 [,) +∞ ) )
169 158 159 168 xralrple2 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ↔ ∀ 𝑟 ∈ ℝ+ ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝑟 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
170 157 169 mpbird ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ 𝑊 ( 𝐴 ‘ 𝑠 ) < ( 𝐵 ‘ 𝑠 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
171 61 72 78 170 syl21anc ⊢ ( ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = +∞ ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
172 60 171 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑠 ∈ 𝑊 ( 𝐵 ‘ 𝑠 ) ≤ ( 𝐴 ‘ 𝑠 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
173 43 172 pm2.61dan ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )