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 ⊢ Ⅎ _ k A
esumcst.2 ⊢ Ⅎ _ k B
Assertion esumcst ⊢ A ∈ V ∧ B ∈ 0 +∞ → ∑ * k ∈ A B = A ⋅ 𝑒 B

Proof

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