Metamath Proof Explorer

Theorem esumcst

Description: The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017) (Revised by Thierry Arnoux, 5-Jul-2017)

Ref Expression
Hypotheses esumcst.1 ⊢ Ⅎ 𝑘 𝐴
esumcst.2 ⊢ Ⅎ 𝑘 𝐵
Assertion esumcst ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 = ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )

Proof

Step Hyp Ref Expression
1 esumcst.1 ⊢ Ⅎ 𝑘 𝐴
2 esumcst.2 ⊢ Ⅎ 𝑘 𝐵
3 1 nfel1 ⊢ Ⅎ 𝑘 𝐴 ∈ 𝑉
4 2 nfel1 ⊢ Ⅎ 𝑘 𝐵 ∈ ( 0 [,] +∞ )
5 3 4 nfan ⊢ Ⅎ 𝑘 ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) )
6 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → 𝐴 ∈ 𝑉 )
7 simplr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
8 xrge0tmd ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd
9 tmdmnd ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
10 8 9 ax-mp ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd
11 10 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
12 inss2 ⊢ ( 𝒫 𝐴 ∩ Fin ) ⊆ Fin
13 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
14 12 13 sselid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ Fin )
15 simplr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
16 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
17 eqid ⊢ ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
18 2 16 17 gsumconstf ⊢ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd ∧ 𝑥 ∈ Fin ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) = ( ( ♯ ‘ 𝑥 ) ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) 𝐵 ) )
19 11 14 15 18 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) = ( ( ♯ ‘ 𝑥 ) ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) 𝐵 ) )
20 hashcl ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
21 14 20 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
22 xrge0mulgnn0 ⊢ ( ( ( ♯ ‘ 𝑥 ) ∈ ℕ0 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ( ♯ ‘ 𝑥 ) ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) 𝐵 ) = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
23 21 15 22 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ♯ ‘ 𝑥 ) ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) 𝐵 ) = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
24 19 23 eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
25 5 1 6 7 24 esumval ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) , ℝ* , < ) )
26 nn0ssre ⊢ ℕ0 ⊆ ℝ
27 ressxr ⊢ ℝ ⊆ ℝ*
28 26 27 sstri ⊢ ℕ0 ⊆ ℝ*
29 pnfxr ⊢ +∞ ∈ ℝ*
30 snssi ⊢ ( +∞ ∈ ℝ* → { +∞ } ⊆ ℝ* )
31 29 30 ax-mp ⊢ { +∞ } ⊆ ℝ*
32 28 31 unssi ⊢ ( ℕ0 ∪ { +∞ } ) ⊆ ℝ*
33 hashf ⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
34 vex ⊢ 𝑥 ∈ V
35 ffvelrn ⊢ ( ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) ∧ 𝑥 ∈ V ) → ( ♯ ‘ 𝑥 ) ∈ ( ℕ0 ∪ { +∞ } ) )
36 33 34 35 mp2an ⊢ ( ♯ ‘ 𝑥 ) ∈ ( ℕ0 ∪ { +∞ } )
37 32 36 sselii ⊢ ( ♯ ‘ 𝑥 ) ∈ ℝ*
38 37 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ♯ ‘ 𝑥 ) ∈ ℝ* )
39 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
40 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
41 39 40 sselid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → 𝐵 ∈ ℝ* )
42 41 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐵 ∈ ℝ* )
43 38 42 xmulcld ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ∈ ℝ* )
44 43 fmpttd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ ℝ* )
45 44 frnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ⊆ ℝ* )
46 hashxrcl ⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
47 46 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
48 47 41 xmulcld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∈ ℝ* )
49 vex ⊢ 𝑦 ∈ V
50 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
51 50 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) )
52 49 51 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
53 52 biimpi ⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
54 47 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
55 0xr ⊢ 0 ∈ ℝ*
56 55 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 0 ∈ ℝ* )
57 29 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → +∞ ∈ ℝ* )
58 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐵 )
59 56 57 15 58 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 0 ≤ 𝐵 )
60 42 59 jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) )
61 6 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐴 ∈ 𝑉 )
62 inss1 ⊢ ( 𝒫 𝐴 ∩ Fin ) ⊆ 𝒫 𝐴
63 62 sseli ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ 𝒫 𝐴 )
64 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
65 13 63 64 3syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ⊆ 𝐴 )
66 ssdomg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ⊆ 𝐴 → 𝑥 ≼ 𝐴 ) )
67 61 65 66 sylc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ≼ 𝐴 )
68 hashdomi ⊢ ( 𝑥 ≼ 𝐴 → ( ♯ ‘ 𝑥 ) ≤ ( ♯ ‘ 𝐴 ) )
69 67 68 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ♯ ‘ 𝑥 ) ≤ ( ♯ ‘ 𝐴 ) )
70 xlemul1a ⊢ ( ( ( ( ♯ ‘ 𝑥 ) ∈ ℝ* ∧ ( ♯ ‘ 𝐴 ) ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ ( ♯ ‘ 𝑥 ) ≤ ( ♯ ‘ 𝐴 ) ) → ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
71 38 54 60 69 70 syl31anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
72 71 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
73 r19.29r ⊢ ( ( ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ∧ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ∧ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) )
74 53 72 73 syl2anr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ∧ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) )
75 simpl ⊢ ( ( 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ∧ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) → 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
76 simpr ⊢ ( ( 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ∧ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) → ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
77 75 76 eqbrtrd ⊢ ( ( 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ∧ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) → 𝑦 ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
78 77 rexlimivw ⊢ ( ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ∧ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) → 𝑦 ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
79 74 78 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ) → 𝑦 ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
80 79 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ∀ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
81 pwidg ⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ 𝒫 𝐴 )
82 81 ancri ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin ) )
83 elin ⊢ ( 𝐴 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin ) )
84 82 83 sylibr ⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ ( 𝒫 𝐴 ∩ Fin ) )
85 eqid ⊢ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ·e 𝐵 )
86 fveq2 ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) )
87 86 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
88 87 rspceeqv ⊢ ( ( 𝐴 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
89 85 88 mpan2 ⊢ ( 𝐴 ∈ ( 𝒫 𝐴 ∩ Fin ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
90 ovex ⊢ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∈ V
91 50 elrnmpt ⊢ ( ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∈ V → ( ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) )
92 90 91 ax-mp ⊢ ( ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
93 89 92 sylibr ⊢ ( 𝐴 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) )
94 84 93 syl ⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) )
95 94 adantl ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ 𝐴 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) )
96 simplr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ 𝐴 ∈ Fin ) → 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
97 breq2 ⊢ ( 𝑧 = ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) → ( 𝑦 < 𝑧 ↔ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) )
98 97 rspcev ⊢ ( ( ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
99 95 96 98 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ 𝐴 ∈ Fin ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
100 0elpw ⊢ ∅ ∈ 𝒫 𝐴
101 0fin ⊢ ∅ ∈ Fin
102 elin ⊢ ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ∅ ∈ 𝒫 𝐴 ∧ ∅ ∈ Fin ) )
103 100 101 102 mpbir2an ⊢ ∅ ∈ ( 𝒫 𝐴 ∩ Fin )
104 103 a1i ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) )
105 simpr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → 𝐵 = 0 )
106 105 oveq2d ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → ( ( ♯ ‘ ∅ ) ·e 𝐵 ) = ( ( ♯ ‘ ∅ ) ·e 0 ) )
107 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
108 107 55 eqeltri ⊢ ( ♯ ‘ ∅ ) ∈ ℝ*
109 xmul01 ⊢ ( ( ♯ ‘ ∅ ) ∈ ℝ* → ( ( ♯ ‘ ∅ ) ·e 0 ) = 0 )
110 108 109 ax-mp ⊢ ( ( ♯ ‘ ∅ ) ·e 0 ) = 0
111 106 110 eqtr2di ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → 0 = ( ( ♯ ‘ ∅ ) ·e 𝐵 ) )
112 fveq2 ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ∅ ) )
113 112 oveq1d ⊢ ( 𝑥 = ∅ → ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) = ( ( ♯ ‘ ∅ ) ·e 𝐵 ) )
114 113 rspceeqv ⊢ ( ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 0 = ( ( ♯ ‘ ∅ ) ·e 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 0 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
115 104 111 114 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 0 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
116 ovex ⊢ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ∈ V
117 50 116 elrnmpti ⊢ ( 0 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 0 = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
118 115 117 sylibr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → 0 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) )
119 simpllr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
120 105 oveq2d ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ·e 0 ) )
121 47 ad4antr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
122 xmul01 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℝ* → ( ( ♯ ‘ 𝐴 ) ·e 0 ) = 0 )
123 121 122 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → ( ( ♯ ‘ 𝐴 ) ·e 0 ) = 0 )
124 120 123 eqtrd ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) = 0 )
125 119 124 breqtrd ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → 𝑦 < 0 )
126 breq2 ⊢ ( 𝑧 = 0 → ( 𝑦 < 𝑧 ↔ 𝑦 < 0 ) )
127 126 rspcev ⊢ ( ( 0 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ∧ 𝑦 < 0 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
128 118 125 127 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = 0 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
129 simplr ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → 𝑎 ∈ 𝒫 𝐴 )
130 simpr ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ( ♯ ‘ 𝑎 ) = 𝑛 )
131 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → 𝑛 ∈ ℕ )
132 130 131 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ( ♯ ‘ 𝑎 ) ∈ ℕ )
133 nnnn0 ⊢ ( ( ♯ ‘ 𝑎 ) ∈ ℕ → ( ♯ ‘ 𝑎 ) ∈ ℕ0 )
134 vex ⊢ 𝑎 ∈ V
135 hashclb ⊢ ( 𝑎 ∈ V → ( 𝑎 ∈ Fin ↔ ( ♯ ‘ 𝑎 ) ∈ ℕ0 ) )
136 134 135 ax-mp ⊢ ( 𝑎 ∈ Fin ↔ ( ♯ ‘ 𝑎 ) ∈ ℕ0 )
137 133 136 sylibr ⊢ ( ( ♯ ‘ 𝑎 ) ∈ ℕ → 𝑎 ∈ Fin )
138 132 137 syl ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → 𝑎 ∈ Fin )
139 129 138 elind ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) )
140 eqidd ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) )
141 fveq2 ⊢ ( 𝑥 = 𝑎 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑎 ) )
142 141 oveq1d ⊢ ( 𝑥 = 𝑎 → ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) )
143 142 rspceeqv ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
144 139 140 143 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
145 50 116 elrnmpti ⊢ ( ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
146 144 145 sylibr ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) )
147 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ( 𝑦 / 𝐵 ) < 𝑛 )
148 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → 𝑦 ∈ ℝ )
149 131 nnred ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → 𝑛 ∈ ℝ )
150 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → 𝐵 ∈ ℝ+ )
151 148 149 150 ltdivmul2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ( ( 𝑦 / 𝐵 ) < 𝑛 ↔ 𝑦 < ( 𝑛 · 𝐵 ) ) )
152 147 151 mpbid ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → 𝑦 < ( 𝑛 · 𝐵 ) )
153 130 oveq1d ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) = ( 𝑛 ·e 𝐵 ) )
154 150 rpred ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → 𝐵 ∈ ℝ )
155 rexmul ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑛 ·e 𝐵 ) = ( 𝑛 · 𝐵 ) )
156 149 154 155 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ( 𝑛 ·e 𝐵 ) = ( 𝑛 · 𝐵 ) )
157 153 156 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) = ( 𝑛 · 𝐵 ) )
158 152 157 breqtrrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → 𝑦 < ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) )
159 breq2 ⊢ ( 𝑧 = ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) → ( 𝑦 < 𝑧 ↔ 𝑦 < ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) ) )
160 159 rspcev ⊢ ( ( ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ∧ 𝑦 < ( ( ♯ ‘ 𝑎 ) ·e 𝐵 ) ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
161 146 158 160 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( ♯ ‘ 𝑎 ) = 𝑛 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
162 161 rexlimdva2 ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 / 𝐵 ) < 𝑛 ) → ( ∃ 𝑎 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑎 ) = 𝑛 → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 ) )
163 162 impr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑦 / 𝐵 ) < 𝑛 ∧ ∃ 𝑎 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑎 ) = 𝑛 ) ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
164 simp-4r ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) → 𝑦 ∈ ℝ )
165 simpr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
166 164 165 rerpdivcld ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) → ( 𝑦 / 𝐵 ) ∈ ℝ )
167 arch ⊢ ( ( 𝑦 / 𝐵 ) ∈ ℝ → ∃ 𝑛 ∈ ℕ ( 𝑦 / 𝐵 ) < 𝑛 )
168 166 167 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑛 ∈ ℕ ( 𝑦 / 𝐵 ) < 𝑛 )
169 ishashinf ⊢ ( ¬ 𝐴 ∈ Fin → ∀ 𝑛 ∈ ℕ ∃ 𝑎 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑎 ) = 𝑛 )
170 169 ad2antlr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) → ∀ 𝑛 ∈ ℕ ∃ 𝑎 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑎 ) = 𝑛 )
171 r19.29r ⊢ ( ( ∃ 𝑛 ∈ ℕ ( 𝑦 / 𝐵 ) < 𝑛 ∧ ∀ 𝑛 ∈ ℕ ∃ 𝑎 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑎 ) = 𝑛 ) → ∃ 𝑛 ∈ ℕ ( ( 𝑦 / 𝐵 ) < 𝑛 ∧ ∃ 𝑎 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑎 ) = 𝑛 ) )
172 168 170 171 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑛 ∈ ℕ ( ( 𝑦 / 𝐵 ) < 𝑛 ∧ ∃ 𝑎 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑎 ) = 𝑛 ) )
173 163 172 r19.29a ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
174 nfielex ⊢ ( ¬ 𝐴 ∈ Fin → ∃ 𝑙 𝑙 ∈ 𝐴 )
175 174 adantr ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞ ) → ∃ 𝑙 𝑙 ∈ 𝐴 )
176 snelpwi ⊢ ( 𝑙 ∈ 𝐴 → { 𝑙 } ∈ 𝒫 𝐴 )
177 snfi ⊢ { 𝑙 } ∈ Fin
178 176 177 jctir ⊢ ( 𝑙 ∈ 𝐴 → ( { 𝑙 } ∈ 𝒫 𝐴 ∧ { 𝑙 } ∈ Fin ) )
179 elin ⊢ ( { 𝑙 } ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( { 𝑙 } ∈ 𝒫 𝐴 ∧ { 𝑙 } ∈ Fin ) )
180 178 179 sylibr ⊢ ( 𝑙 ∈ 𝐴 → { 𝑙 } ∈ ( 𝒫 𝐴 ∩ Fin ) )
181 180 adantl ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞ ) ∧ 𝑙 ∈ 𝐴 ) → { 𝑙 } ∈ ( 𝒫 𝐴 ∩ Fin ) )
182 simplr ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞ ) ∧ 𝑙 ∈ 𝐴 ) → 𝐵 = +∞ )
183 182 oveq2d ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞ ) ∧ 𝑙 ∈ 𝐴 ) → ( ( ♯ ‘ { 𝑙 } ) ·e 𝐵 ) = ( ( ♯ ‘ { 𝑙 } ) ·e +∞ ) )
184 hashsng ⊢ ( 𝑙 ∈ 𝐴 → ( ♯ ‘ { 𝑙 } ) = 1 )
185 1re ⊢ 1 ∈ ℝ
186 27 185 sselii ⊢ 1 ∈ ℝ*
187 184 186 eqeltrdi ⊢ ( 𝑙 ∈ 𝐴 → ( ♯ ‘ { 𝑙 } ) ∈ ℝ* )
188 0lt1 ⊢ 0 < 1
189 188 184 breqtrrid ⊢ ( 𝑙 ∈ 𝐴 → 0 < ( ♯ ‘ { 𝑙 } ) )
190 xmulpnf1 ⊢ ( ( ( ♯ ‘ { 𝑙 } ) ∈ ℝ* ∧ 0 < ( ♯ ‘ { 𝑙 } ) ) → ( ( ♯ ‘ { 𝑙 } ) ·e +∞ ) = +∞ )
191 187 189 190 syl2anc ⊢ ( 𝑙 ∈ 𝐴 → ( ( ♯ ‘ { 𝑙 } ) ·e +∞ ) = +∞ )
192 191 adantl ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞ ) ∧ 𝑙 ∈ 𝐴 ) → ( ( ♯ ‘ { 𝑙 } ) ·e +∞ ) = +∞ )
193 183 192 eqtr2d ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞ ) ∧ 𝑙 ∈ 𝐴 ) → +∞ = ( ( ♯ ‘ { 𝑙 } ) ·e 𝐵 ) )
194 fveq2 ⊢ ( 𝑥 = { 𝑙 } → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ { 𝑙 } ) )
195 194 oveq1d ⊢ ( 𝑥 = { 𝑙 } → ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) = ( ( ♯ ‘ { 𝑙 } ) ·e 𝐵 ) )
196 195 rspceeqv ⊢ ( ( { 𝑙 } ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ +∞ = ( ( ♯ ‘ { 𝑙 } ) ·e 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) +∞ = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
197 181 193 196 syl2anc ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞ ) ∧ 𝑙 ∈ 𝐴 ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) +∞ = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
198 175 197 exlimddv ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞ ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) +∞ = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
199 198 adantll ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = +∞ ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) +∞ = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
200 50 116 elrnmpti ⊢ ( +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) +∞ = ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) )
201 199 200 sylibr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = +∞ ) → +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) )
202 simp-4r ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = +∞ ) → 𝑦 ∈ ℝ )
203 ltpnf ⊢ ( 𝑦 ∈ ℝ → 𝑦 < +∞ )
204 202 203 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = +∞ ) → 𝑦 < +∞ )
205 breq2 ⊢ ( 𝑧 = +∞ → ( 𝑦 < 𝑧 ↔ 𝑦 < +∞ ) )
206 205 rspcev ⊢ ( ( +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ∧ 𝑦 < +∞ ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
207 201 204 206 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = +∞ ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
208 simp-4r ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) → 𝐵 ∈ ( 0 [,] +∞ ) )
209 elxrge02 ⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( 𝐵 = 0 ∨ 𝐵 ∈ ℝ+ ∨ 𝐵 = +∞ ) )
210 208 209 sylib ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐵 = 0 ∨ 𝐵 ∈ ℝ+ ∨ 𝐵 = +∞ ) )
211 128 173 207 210 mpjao3dan ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) ∧ ¬ 𝐴 ∈ Fin ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
212 99 211 pm2.61dan ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 )
213 212 ex ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 ∈ ℝ ) → ( 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 ) )
214 213 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ∀ 𝑦 ∈ ℝ ( 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 ) )
215 supxr2 ⊢ ( ( ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) ⊆ ℝ* ∧ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 ≤ ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) 𝑦 < 𝑧 ) ) ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) , ℝ* , < ) = ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
216 45 48 80 214 215 syl22anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ♯ ‘ 𝑥 ) ·e 𝐵 ) ) , ℝ* , < ) = ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )
217 25 216 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 = ( ( ♯ ‘ 𝐴 ) ·e 𝐵 ) )