Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  esumcst Structured version   Visualization version   GIF version

Theorem esumcst 32702
Description: The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017.) (Revised by Thierry Arnoux, 5-Jul-2017.)
Hypotheses
Ref Expression
esumcst.1 β„²π‘˜π΄
esumcst.2 β„²π‘˜π΅
Assertion
Ref Expression
esumcst ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ Ξ£*π‘˜ ∈ 𝐴𝐡 = ((β™―β€˜π΄) Β·e 𝐡))
Distinct variable group:   π‘˜,𝑉
Allowed substitution hints:   𝐴(π‘˜)   𝐡(π‘˜)

Proof of Theorem esumcst
Dummy variables π‘Ž 𝑙 𝑛 π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 esumcst.1 . . . . 5 β„²π‘˜π΄
21nfel1 2924 . . . 4 β„²π‘˜ 𝐴 ∈ 𝑉
3 esumcst.2 . . . . 5 β„²π‘˜π΅
43nfel1 2924 . . . 4 β„²π‘˜ 𝐡 ∈ (0[,]+∞)
52, 4nfan 1903 . . 3 β„²π‘˜(𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞))
6 simpl 484 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ 𝐴 ∈ 𝑉)
7 simplr 768 . . 3 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘˜ ∈ 𝐴) β†’ 𝐡 ∈ (0[,]+∞))
8 xrge0tmd 32566 . . . . . . 7 (ℝ*𝑠 β†Ύs (0[,]+∞)) ∈ TopMnd
9 tmdmnd 23442 . . . . . . 7 ((ℝ*𝑠 β†Ύs (0[,]+∞)) ∈ TopMnd β†’ (ℝ*𝑠 β†Ύs (0[,]+∞)) ∈ Mnd)
108, 9ax-mp 5 . . . . . 6 (ℝ*𝑠 β†Ύs (0[,]+∞)) ∈ Mnd
1110a1i 11 . . . . 5 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ (ℝ*𝑠 β†Ύs (0[,]+∞)) ∈ Mnd)
12 inss2 4194 . . . . . 6 (𝒫 𝐴 ∩ Fin) βŠ† Fin
13 simpr 486 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ π‘₯ ∈ (𝒫 𝐴 ∩ Fin))
1412, 13sselid 3947 . . . . 5 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ π‘₯ ∈ Fin)
15 simplr 768 . . . . 5 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ 𝐡 ∈ (0[,]+∞))
16 xrge0base 31918 . . . . . 6 (0[,]+∞) = (Baseβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
17 eqid 2737 . . . . . 6 (.gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞))) = (.gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
183, 16, 17gsumconstf 19719 . . . . 5 (((ℝ*𝑠 β†Ύs (0[,]+∞)) ∈ Mnd ∧ π‘₯ ∈ Fin ∧ 𝐡 ∈ (0[,]+∞)) β†’ ((ℝ*𝑠 β†Ύs (0[,]+∞)) Ξ£g (π‘˜ ∈ π‘₯ ↦ 𝐡)) = ((β™―β€˜π‘₯)(.gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))𝐡))
1911, 14, 15, 18syl3anc 1372 . . . 4 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ ((ℝ*𝑠 β†Ύs (0[,]+∞)) Ξ£g (π‘˜ ∈ π‘₯ ↦ 𝐡)) = ((β™―β€˜π‘₯)(.gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))𝐡))
20 hashcl 14263 . . . . . 6 (π‘₯ ∈ Fin β†’ (β™―β€˜π‘₯) ∈ β„•0)
2114, 20syl 17 . . . . 5 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ (β™―β€˜π‘₯) ∈ β„•0)
22 xrge0mulgnn0 31922 . . . . 5 (((β™―β€˜π‘₯) ∈ β„•0 ∧ 𝐡 ∈ (0[,]+∞)) β†’ ((β™―β€˜π‘₯)(.gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
2321, 15, 22syl2anc 585 . . . 4 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ ((β™―β€˜π‘₯)(.gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
2419, 23eqtrd 2777 . . 3 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ ((ℝ*𝑠 β†Ύs (0[,]+∞)) Ξ£g (π‘˜ ∈ π‘₯ ↦ 𝐡)) = ((β™―β€˜π‘₯) Β·e 𝐡))
255, 1, 6, 7, 24esumval 32685 . 2 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ Ξ£*π‘˜ ∈ 𝐴𝐡 = sup(ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)), ℝ*, < ))
26 nn0ssre 12424 . . . . . . . . . 10 β„•0 βŠ† ℝ
27 ressxr 11206 . . . . . . . . . 10 ℝ βŠ† ℝ*
2826, 27sstri 3958 . . . . . . . . 9 β„•0 βŠ† ℝ*
29 pnfxr 11216 . . . . . . . . . 10 +∞ ∈ ℝ*
30 snssi 4773 . . . . . . . . . 10 (+∞ ∈ ℝ* β†’ {+∞} βŠ† ℝ*)
3129, 30ax-mp 5 . . . . . . . . 9 {+∞} βŠ† ℝ*
3228, 31unssi 4150 . . . . . . . 8 (β„•0 βˆͺ {+∞}) βŠ† ℝ*
33 hashf 14245 . . . . . . . . 9 β™―:V⟢(β„•0 βˆͺ {+∞})
34 vex 3452 . . . . . . . . 9 π‘₯ ∈ V
35 ffvelcdm 7037 . . . . . . . . 9 ((β™―:V⟢(β„•0 βˆͺ {+∞}) ∧ π‘₯ ∈ V) β†’ (β™―β€˜π‘₯) ∈ (β„•0 βˆͺ {+∞}))
3633, 34, 35mp2an 691 . . . . . . . 8 (β™―β€˜π‘₯) ∈ (β„•0 βˆͺ {+∞})
3732, 36sselii 3946 . . . . . . 7 (β™―β€˜π‘₯) ∈ ℝ*
3837a1i 11 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ (β™―β€˜π‘₯) ∈ ℝ*)
39 iccssxr 13354 . . . . . . . 8 (0[,]+∞) βŠ† ℝ*
40 simpr 486 . . . . . . . 8 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ 𝐡 ∈ (0[,]+∞))
4139, 40sselid 3947 . . . . . . 7 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ 𝐡 ∈ ℝ*)
4241adantr 482 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ 𝐡 ∈ ℝ*)
4338, 42xmulcld 13228 . . . . 5 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ ((β™―β€˜π‘₯) Β·e 𝐡) ∈ ℝ*)
4443fmpttd 7068 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)):(𝒫 𝐴 ∩ Fin)βŸΆβ„*)
4544frnd 6681 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) βŠ† ℝ*)
46 hashxrcl 14264 . . . . 5 (𝐴 ∈ 𝑉 β†’ (β™―β€˜π΄) ∈ ℝ*)
4746adantr 482 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ (β™―β€˜π΄) ∈ ℝ*)
4847, 41xmulcld 13228 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ ((β™―β€˜π΄) Β·e 𝐡) ∈ ℝ*)
49 vex 3452 . . . . . . . 8 𝑦 ∈ V
50 eqid 2737 . . . . . . . . 9 (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) = (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))
5150elrnmpt 5916 . . . . . . . 8 (𝑦 ∈ V β†’ (𝑦 ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ↔ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡)))
5249, 51ax-mp 5 . . . . . . 7 (𝑦 ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ↔ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡))
5352biimpi 215 . . . . . 6 (𝑦 ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡))
5447adantr 482 . . . . . . . 8 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ (β™―β€˜π΄) ∈ ℝ*)
55 0xr 11209 . . . . . . . . . . 11 0 ∈ ℝ*
5655a1i 11 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ 0 ∈ ℝ*)
5729a1i 11 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ +∞ ∈ ℝ*)
58 iccgelb 13327 . . . . . . . . . 10 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐡 ∈ (0[,]+∞)) β†’ 0 ≀ 𝐡)
5956, 57, 15, 58syl3anc 1372 . . . . . . . . 9 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ 0 ≀ 𝐡)
6042, 59jca 513 . . . . . . . 8 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ (𝐡 ∈ ℝ* ∧ 0 ≀ 𝐡))
616adantr 482 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ 𝐴 ∈ 𝑉)
62 inss1 4193 . . . . . . . . . . . 12 (𝒫 𝐴 ∩ Fin) βŠ† 𝒫 𝐴
6362sseli 3945 . . . . . . . . . . 11 (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) β†’ π‘₯ ∈ 𝒫 𝐴)
64 elpwi 4572 . . . . . . . . . . 11 (π‘₯ ∈ 𝒫 𝐴 β†’ π‘₯ βŠ† 𝐴)
6513, 63, 643syl 18 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ π‘₯ βŠ† 𝐴)
66 ssdomg 8947 . . . . . . . . . 10 (𝐴 ∈ 𝑉 β†’ (π‘₯ βŠ† 𝐴 β†’ π‘₯ β‰Ό 𝐴))
6761, 65, 66sylc 65 . . . . . . . . 9 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ π‘₯ β‰Ό 𝐴)
68 hashdomi 14287 . . . . . . . . 9 (π‘₯ β‰Ό 𝐴 β†’ (β™―β€˜π‘₯) ≀ (β™―β€˜π΄))
6967, 68syl 17 . . . . . . . 8 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ (β™―β€˜π‘₯) ≀ (β™―β€˜π΄))
70 xlemul1a 13214 . . . . . . . 8 ((((β™―β€˜π‘₯) ∈ ℝ* ∧ (β™―β€˜π΄) ∈ ℝ* ∧ (𝐡 ∈ ℝ* ∧ 0 ≀ 𝐡)) ∧ (β™―β€˜π‘₯) ≀ (β™―β€˜π΄)) β†’ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡))
7138, 54, 60, 69, 70syl31anc 1374 . . . . . . 7 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡))
7271ralrimiva 3144 . . . . . 6 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ βˆ€π‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡))
73 r19.29r 3120 . . . . . 6 ((βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡) ∧ βˆ€π‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡)) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡) ∧ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡)))
7453, 72, 73syl2anr 598 . . . . 5 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡) ∧ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡)))
75 simpl 484 . . . . . . 7 ((𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡) ∧ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡)) β†’ 𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡))
76 simpr 486 . . . . . . 7 ((𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡) ∧ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡)) β†’ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡))
7775, 76eqbrtrd 5132 . . . . . 6 ((𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡) ∧ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡)) β†’ 𝑦 ≀ ((β™―β€˜π΄) Β·e 𝐡))
7877rexlimivw 3149 . . . . 5 (βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡) ∧ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡)) β†’ 𝑦 ≀ ((β™―β€˜π΄) Β·e 𝐡))
7974, 78syl 17 . . . 4 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))) β†’ 𝑦 ≀ ((β™―β€˜π΄) Β·e 𝐡))
8079ralrimiva 3144 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ βˆ€π‘¦ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 ≀ ((β™―β€˜π΄) Β·e 𝐡))
81 pwidg 4585 . . . . . . . . . . 11 (𝐴 ∈ Fin β†’ 𝐴 ∈ 𝒫 𝐴)
8281ancri 551 . . . . . . . . . 10 (𝐴 ∈ Fin β†’ (𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin))
83 elin 3931 . . . . . . . . . 10 (𝐴 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin))
8482, 83sylibr 233 . . . . . . . . 9 (𝐴 ∈ Fin β†’ 𝐴 ∈ (𝒫 𝐴 ∩ Fin))
85 eqid 2737 . . . . . . . . . . 11 ((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π΄) Β·e 𝐡)
86 fveq2 6847 . . . . . . . . . . . . 13 (π‘₯ = 𝐴 β†’ (β™―β€˜π‘₯) = (β™―β€˜π΄))
8786oveq1d 7377 . . . . . . . . . . . 12 (π‘₯ = 𝐴 β†’ ((β™―β€˜π‘₯) Β·e 𝐡) = ((β™―β€˜π΄) Β·e 𝐡))
8887rspceeqv 3600 . . . . . . . . . . 11 ((𝐴 ∈ (𝒫 𝐴 ∩ Fin) ∧ ((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π΄) Β·e 𝐡)) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
8985, 88mpan2 690 . . . . . . . . . 10 (𝐴 ∈ (𝒫 𝐴 ∩ Fin) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
90 ovex 7395 . . . . . . . . . . 11 ((β™―β€˜π΄) Β·e 𝐡) ∈ V
9150elrnmpt 5916 . . . . . . . . . . 11 (((β™―β€˜π΄) Β·e 𝐡) ∈ V β†’ (((β™―β€˜π΄) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ↔ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡)))
9290, 91ax-mp 5 . . . . . . . . . 10 (((β™―β€˜π΄) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ↔ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
9389, 92sylibr 233 . . . . . . . . 9 (𝐴 ∈ (𝒫 𝐴 ∩ Fin) β†’ ((β™―β€˜π΄) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)))
9484, 93syl 17 . . . . . . . 8 (𝐴 ∈ Fin β†’ ((β™―β€˜π΄) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)))
9594adantl 483 . . . . . . 7 (((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ 𝐴 ∈ Fin) β†’ ((β™―β€˜π΄) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)))
96 simplr 768 . . . . . . 7 (((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ 𝐴 ∈ Fin) β†’ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡))
97 breq2 5114 . . . . . . . 8 (𝑧 = ((β™―β€˜π΄) Β·e 𝐡) β†’ (𝑦 < 𝑧 ↔ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)))
9897rspcev 3584 . . . . . . 7 ((((β™―β€˜π΄) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
9995, 96, 98syl2anc 585 . . . . . 6 (((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ 𝐴 ∈ Fin) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
100 0elpw 5316 . . . . . . . . . . . 12 βˆ… ∈ 𝒫 𝐴
101 0fin 9122 . . . . . . . . . . . 12 βˆ… ∈ Fin
102 elin 3931 . . . . . . . . . . . 12 (βˆ… ∈ (𝒫 𝐴 ∩ Fin) ↔ (βˆ… ∈ 𝒫 𝐴 ∧ βˆ… ∈ Fin))
103100, 101, 102mpbir2an 710 . . . . . . . . . . 11 βˆ… ∈ (𝒫 𝐴 ∩ Fin)
104103a1i 11 . . . . . . . . . 10 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ βˆ… ∈ (𝒫 𝐴 ∩ Fin))
105 simpr 486 . . . . . . . . . . . 12 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ 𝐡 = 0)
106105oveq2d 7378 . . . . . . . . . . 11 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ ((β™―β€˜βˆ…) Β·e 𝐡) = ((β™―β€˜βˆ…) Β·e 0))
107 hash0 14274 . . . . . . . . . . . . 13 (β™―β€˜βˆ…) = 0
108107, 55eqeltri 2834 . . . . . . . . . . . 12 (β™―β€˜βˆ…) ∈ ℝ*
109 xmul01 13193 . . . . . . . . . . . 12 ((β™―β€˜βˆ…) ∈ ℝ* β†’ ((β™―β€˜βˆ…) Β·e 0) = 0)
110108, 109ax-mp 5 . . . . . . . . . . 11 ((β™―β€˜βˆ…) Β·e 0) = 0
111106, 110eqtr2di 2794 . . . . . . . . . 10 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ 0 = ((β™―β€˜βˆ…) Β·e 𝐡))
112 fveq2 6847 . . . . . . . . . . . 12 (π‘₯ = βˆ… β†’ (β™―β€˜π‘₯) = (β™―β€˜βˆ…))
113112oveq1d 7377 . . . . . . . . . . 11 (π‘₯ = βˆ… β†’ ((β™―β€˜π‘₯) Β·e 𝐡) = ((β™―β€˜βˆ…) Β·e 𝐡))
114113rspceeqv 3600 . . . . . . . . . 10 ((βˆ… ∈ (𝒫 𝐴 ∩ Fin) ∧ 0 = ((β™―β€˜βˆ…) Β·e 𝐡)) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)0 = ((β™―β€˜π‘₯) Β·e 𝐡))
115104, 111, 114syl2anc 585 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)0 = ((β™―β€˜π‘₯) Β·e 𝐡))
116 ovex 7395 . . . . . . . . . 10 ((β™―β€˜π‘₯) Β·e 𝐡) ∈ V
11750, 116elrnmpti 5920 . . . . . . . . 9 (0 ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ↔ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)0 = ((β™―β€˜π‘₯) Β·e 𝐡))
118115, 117sylibr 233 . . . . . . . 8 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ 0 ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)))
119 simpllr 775 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡))
120105oveq2d 7378 . . . . . . . . . 10 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ ((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π΄) Β·e 0))
12147ad4antr 731 . . . . . . . . . . 11 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ (β™―β€˜π΄) ∈ ℝ*)
122 xmul01 13193 . . . . . . . . . . 11 ((β™―β€˜π΄) ∈ ℝ* β†’ ((β™―β€˜π΄) Β·e 0) = 0)
123121, 122syl 17 . . . . . . . . . 10 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ ((β™―β€˜π΄) Β·e 0) = 0)
124120, 123eqtrd 2777 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ ((β™―β€˜π΄) Β·e 𝐡) = 0)
125119, 124breqtrd 5136 . . . . . . . 8 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ 𝑦 < 0)
126 breq2 5114 . . . . . . . . 9 (𝑧 = 0 β†’ (𝑦 < 𝑧 ↔ 𝑦 < 0))
127126rspcev 3584 . . . . . . . 8 ((0 ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ∧ 𝑦 < 0) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
128118, 125, 127syl2anc 585 . . . . . . 7 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
129 simplr 768 . . . . . . . . . . . . . 14 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ π‘Ž ∈ 𝒫 𝐴)
130 simpr 486 . . . . . . . . . . . . . . . 16 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ (β™―β€˜π‘Ž) = 𝑛)
131 simp-4r 783 . . . . . . . . . . . . . . . 16 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝑛 ∈ β„•)
132130, 131eqeltrd 2838 . . . . . . . . . . . . . . 15 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ (β™―β€˜π‘Ž) ∈ β„•)
133 nnnn0 12427 . . . . . . . . . . . . . . . 16 ((β™―β€˜π‘Ž) ∈ β„• β†’ (β™―β€˜π‘Ž) ∈ β„•0)
134 vex 3452 . . . . . . . . . . . . . . . . 17 π‘Ž ∈ V
135 hashclb 14265 . . . . . . . . . . . . . . . . 17 (π‘Ž ∈ V β†’ (π‘Ž ∈ Fin ↔ (β™―β€˜π‘Ž) ∈ β„•0))
136134, 135ax-mp 5 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ Fin ↔ (β™―β€˜π‘Ž) ∈ β„•0)
137133, 136sylibr 233 . . . . . . . . . . . . . . 15 ((β™―β€˜π‘Ž) ∈ β„• β†’ π‘Ž ∈ Fin)
138132, 137syl 17 . . . . . . . . . . . . . 14 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ π‘Ž ∈ Fin)
139129, 138elind 4159 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ π‘Ž ∈ (𝒫 𝐴 ∩ Fin))
140 eqidd 2738 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ ((β™―β€˜π‘Ž) Β·e 𝐡) = ((β™―β€˜π‘Ž) Β·e 𝐡))
141 fveq2 6847 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ž β†’ (β™―β€˜π‘₯) = (β™―β€˜π‘Ž))
142141oveq1d 7377 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ž β†’ ((β™―β€˜π‘₯) Β·e 𝐡) = ((β™―β€˜π‘Ž) Β·e 𝐡))
143142rspceeqv 3600 . . . . . . . . . . . . 13 ((π‘Ž ∈ (𝒫 𝐴 ∩ Fin) ∧ ((β™―β€˜π‘Ž) Β·e 𝐡) = ((β™―β€˜π‘Ž) Β·e 𝐡)) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π‘Ž) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
144139, 140, 143syl2anc 585 . . . . . . . . . . . 12 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π‘Ž) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
14550, 116elrnmpti 5920 . . . . . . . . . . . 12 (((β™―β€˜π‘Ž) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ↔ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π‘Ž) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
146144, 145sylibr 233 . . . . . . . . . . 11 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ ((β™―β€˜π‘Ž) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)))
147 simpllr 775 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ (𝑦 / 𝐡) < 𝑛)
148 simp-8r 791 . . . . . . . . . . . . . 14 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝑦 ∈ ℝ)
149131nnred 12175 . . . . . . . . . . . . . 14 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝑛 ∈ ℝ)
150 simp-5r 785 . . . . . . . . . . . . . 14 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝐡 ∈ ℝ+)
151148, 149, 150ltdivmul2d 13016 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ ((𝑦 / 𝐡) < 𝑛 ↔ 𝑦 < (𝑛 Β· 𝐡)))
152147, 151mpbid 231 . . . . . . . . . . . 12 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝑦 < (𝑛 Β· 𝐡))
153130oveq1d 7377 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ ((β™―β€˜π‘Ž) Β·e 𝐡) = (𝑛 Β·e 𝐡))
154150rpred 12964 . . . . . . . . . . . . . 14 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝐡 ∈ ℝ)
155 rexmul 13197 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝑛 Β·e 𝐡) = (𝑛 Β· 𝐡))
156149, 154, 155syl2anc 585 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ (𝑛 Β·e 𝐡) = (𝑛 Β· 𝐡))
157153, 156eqtrd 2777 . . . . . . . . . . . 12 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ ((β™―β€˜π‘Ž) Β·e 𝐡) = (𝑛 Β· 𝐡))
158152, 157breqtrrd 5138 . . . . . . . . . . 11 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝑦 < ((β™―β€˜π‘Ž) Β·e 𝐡))
159 breq2 5114 . . . . . . . . . . . 12 (𝑧 = ((β™―β€˜π‘Ž) Β·e 𝐡) β†’ (𝑦 < 𝑧 ↔ 𝑦 < ((β™―β€˜π‘Ž) Β·e 𝐡)))
160159rspcev 3584 . . . . . . . . . . 11 ((((β™―β€˜π‘Ž) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ∧ 𝑦 < ((β™―β€˜π‘Ž) Β·e 𝐡)) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
161146, 158, 160syl2anc 585 . . . . . . . . . 10 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
162161rexlimdva2 3155 . . . . . . . . 9 ((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) β†’ (βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛 β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧))
163162impr 456 . . . . . . . 8 ((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ ((𝑦 / 𝐡) < 𝑛 ∧ βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛)) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
164 simp-4r 783 . . . . . . . . . . 11 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ 𝑦 ∈ ℝ)
165 simpr 486 . . . . . . . . . . 11 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ 𝐡 ∈ ℝ+)
166164, 165rerpdivcld 12995 . . . . . . . . . 10 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ (𝑦 / 𝐡) ∈ ℝ)
167 arch 12417 . . . . . . . . . 10 ((𝑦 / 𝐡) ∈ ℝ β†’ βˆƒπ‘› ∈ β„• (𝑦 / 𝐡) < 𝑛)
168166, 167syl 17 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ βˆƒπ‘› ∈ β„• (𝑦 / 𝐡) < 𝑛)
169 ishashinf 14369 . . . . . . . . . 10 (Β¬ 𝐴 ∈ Fin β†’ βˆ€π‘› ∈ β„• βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛)
170169ad2antlr 726 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ βˆ€π‘› ∈ β„• βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛)
171 r19.29r 3120 . . . . . . . . 9 ((βˆƒπ‘› ∈ β„• (𝑦 / 𝐡) < 𝑛 ∧ βˆ€π‘› ∈ β„• βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛) β†’ βˆƒπ‘› ∈ β„• ((𝑦 / 𝐡) < 𝑛 ∧ βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛))
172168, 170, 171syl2anc 585 . . . . . . . 8 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ βˆƒπ‘› ∈ β„• ((𝑦 / 𝐡) < 𝑛 ∧ βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛))
173163, 172r19.29a 3160 . . . . . . 7 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
174 nfielex 9224 . . . . . . . . . . . 12 (Β¬ 𝐴 ∈ Fin β†’ βˆƒπ‘™ 𝑙 ∈ 𝐴)
175174adantr 482 . . . . . . . . . . 11 ((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) β†’ βˆƒπ‘™ 𝑙 ∈ 𝐴)
176 snelpwi 5405 . . . . . . . . . . . . . . 15 (𝑙 ∈ 𝐴 β†’ {𝑙} ∈ 𝒫 𝐴)
177 snfi 8995 . . . . . . . . . . . . . . 15 {𝑙} ∈ Fin
178176, 177jctir 522 . . . . . . . . . . . . . 14 (𝑙 ∈ 𝐴 β†’ ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin))
179 elin 3931 . . . . . . . . . . . . . 14 ({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ↔ ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin))
180178, 179sylibr 233 . . . . . . . . . . . . 13 (𝑙 ∈ 𝐴 β†’ {𝑙} ∈ (𝒫 𝐴 ∩ Fin))
181180adantl 483 . . . . . . . . . . . 12 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ {𝑙} ∈ (𝒫 𝐴 ∩ Fin))
182 simplr 768 . . . . . . . . . . . . . 14 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ 𝐡 = +∞)
183182oveq2d 7378 . . . . . . . . . . . . 13 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ ((β™―β€˜{𝑙}) Β·e 𝐡) = ((β™―β€˜{𝑙}) Β·e +∞))
184 hashsng 14276 . . . . . . . . . . . . . . . 16 (𝑙 ∈ 𝐴 β†’ (β™―β€˜{𝑙}) = 1)
185 1re 11162 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
18627, 185sselii 3946 . . . . . . . . . . . . . . . 16 1 ∈ ℝ*
187184, 186eqeltrdi 2846 . . . . . . . . . . . . . . 15 (𝑙 ∈ 𝐴 β†’ (β™―β€˜{𝑙}) ∈ ℝ*)
188 0lt1 11684 . . . . . . . . . . . . . . . 16 0 < 1
189188, 184breqtrrid 5148 . . . . . . . . . . . . . . 15 (𝑙 ∈ 𝐴 β†’ 0 < (β™―β€˜{𝑙}))
190 xmulpnf1 13200 . . . . . . . . . . . . . . 15 (((β™―β€˜{𝑙}) ∈ ℝ* ∧ 0 < (β™―β€˜{𝑙})) β†’ ((β™―β€˜{𝑙}) Β·e +∞) = +∞)
191187, 189, 190syl2anc 585 . . . . . . . . . . . . . 14 (𝑙 ∈ 𝐴 β†’ ((β™―β€˜{𝑙}) Β·e +∞) = +∞)
192191adantl 483 . . . . . . . . . . . . 13 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ ((β™―β€˜{𝑙}) Β·e +∞) = +∞)
193183, 192eqtr2d 2778 . . . . . . . . . . . 12 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ +∞ = ((β™―β€˜{𝑙}) Β·e 𝐡))
194 fveq2 6847 . . . . . . . . . . . . . 14 (π‘₯ = {𝑙} β†’ (β™―β€˜π‘₯) = (β™―β€˜{𝑙}))
195194oveq1d 7377 . . . . . . . . . . . . 13 (π‘₯ = {𝑙} β†’ ((β™―β€˜π‘₯) Β·e 𝐡) = ((β™―β€˜{𝑙}) Β·e 𝐡))
196195rspceeqv 3600 . . . . . . . . . . . 12 (({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ∧ +∞ = ((β™―β€˜{𝑙}) Β·e 𝐡)) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((β™―β€˜π‘₯) Β·e 𝐡))
197181, 193, 196syl2anc 585 . . . . . . . . . . 11 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((β™―β€˜π‘₯) Β·e 𝐡))
198175, 197exlimddv 1939 . . . . . . . . . 10 ((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((β™―β€˜π‘₯) Β·e 𝐡))
199198adantll 713 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = +∞) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((β™―β€˜π‘₯) Β·e 𝐡))
20050, 116elrnmpti 5920 . . . . . . . . 9 (+∞ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ↔ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((β™―β€˜π‘₯) Β·e 𝐡))
201199, 200sylibr 233 . . . . . . . 8 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = +∞) β†’ +∞ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)))
202 simp-4r 783 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = +∞) β†’ 𝑦 ∈ ℝ)
203 ltpnf 13048 . . . . . . . . 9 (𝑦 ∈ ℝ β†’ 𝑦 < +∞)
204202, 203syl 17 . . . . . . . 8 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = +∞) β†’ 𝑦 < +∞)
205 breq2 5114 . . . . . . . . 9 (𝑧 = +∞ β†’ (𝑦 < 𝑧 ↔ 𝑦 < +∞))
206205rspcev 3584 . . . . . . . 8 ((+∞ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ∧ 𝑦 < +∞) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
207201, 204, 206syl2anc 585 . . . . . . 7 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = +∞) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
208 simp-4r 783 . . . . . . . 8 (((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) β†’ 𝐡 ∈ (0[,]+∞))
209 elxrge02 31830 . . . . . . . 8 (𝐡 ∈ (0[,]+∞) ↔ (𝐡 = 0 ∨ 𝐡 ∈ ℝ+ ∨ 𝐡 = +∞))
210208, 209sylib 217 . . . . . . 7 (((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) β†’ (𝐡 = 0 ∨ 𝐡 ∈ ℝ+ ∨ 𝐡 = +∞))
211128, 173, 207, 210mpjao3dan 1432 . . . . . 6 (((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
21299, 211pm2.61dan 812 . . . . 5 ((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
213212ex 414 . . . 4 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) β†’ (𝑦 < ((β™―β€˜π΄) Β·e 𝐡) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧))
214213ralrimiva 3144 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ βˆ€π‘¦ ∈ ℝ (𝑦 < ((β™―β€˜π΄) Β·e 𝐡) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧))
215 supxr2 13240 . . 3 (((ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) βŠ† ℝ* ∧ ((β™―β€˜π΄) Β·e 𝐡) ∈ ℝ*) ∧ (βˆ€π‘¦ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 ≀ ((β™―β€˜π΄) Β·e 𝐡) ∧ βˆ€π‘¦ ∈ ℝ (𝑦 < ((β™―β€˜π΄) Β·e 𝐡) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧))) β†’ sup(ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)), ℝ*, < ) = ((β™―β€˜π΄) Β·e 𝐡))
21645, 48, 80, 214, 215syl22anc 838 . 2 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ sup(ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)), ℝ*, < ) = ((β™―β€˜π΄) Β·e 𝐡))
21725, 216eqtrd 2777 1 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ Ξ£*π‘˜ ∈ 𝐴𝐡 = ((β™―β€˜π΄) Β·e 𝐡))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ w3o 1087   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  β„²wnfc 2888  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3448   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  π’« cpw 4565  {csn 4591   class class class wbr 5110   ↦ cmpt 5193  ran crn 5639  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   β‰Ό cdom 8888  Fincfn 8890  supcsup 9383  β„cr 11057  0cc0 11058  1c1 11059   Β· cmul 11063  +∞cpnf 11193  β„*cxr 11195   < clt 11196   ≀ cle 11197   / cdiv 11819  β„•cn 12160  β„•0cn0 12420  β„+crp 12922   Β·e cxmu 13039  [,]cicc 13274  β™―chash 14237   β†Ύs cress 17119   Ξ£g cgsu 17329  β„*𝑠cxrs 17389  Mndcmnd 18563  .gcmg 18879  TopMndctmd 23437  Ξ£*cesum 32666
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-xnn0 12493  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-sin 15959  df-cos 15960  df-pi 15962  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-ordt 17390  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-ps 18462  df-tsr 18463  df-plusf 18503  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-mhm 18608  df-submnd 18609  df-grp 18758  df-minusg 18759  df-sbg 18760  df-mulg 18880  df-subg 18932  df-cntz 19104  df-cmn 19571  df-abl 19572  df-mgp 19904  df-ur 19921  df-ring 19973  df-cring 19974  df-subrg 20236  df-abv 20292  df-lmod 20340  df-scaf 20341  df-sra 20649  df-rgmod 20650  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-tmd 23439  df-tgp 23440  df-tsms 23494  df-trg 23527  df-xms 23689  df-ms 23690  df-tms 23691  df-nm 23954  df-ngp 23955  df-nrg 23957  df-nlm 23958  df-ii 24256  df-cncf 24257  df-limc 25246  df-dv 25247  df-log 25928  df-esum 32667
This theorem is referenced by:  esumpinfval  32712  esumpinfsum  32716
  Copyright terms: Public domain W3C validator