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 33061
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 2920 . . . 4 β„²π‘˜ 𝐴 ∈ 𝑉
3 esumcst.2 . . . . 5 β„²π‘˜π΅
43nfel1 2920 . . . 4 β„²π‘˜ 𝐡 ∈ (0[,]+∞)
52, 4nfan 1903 . . 3 β„²π‘˜(𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞))
6 simpl 484 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ 𝐴 ∈ 𝑉)
7 simplr 768 . . 3 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘˜ ∈ 𝐴) β†’ 𝐡 ∈ (0[,]+∞))
8 xrge0tmd 32925 . . . . . . 7 (ℝ*𝑠 β†Ύs (0[,]+∞)) ∈ TopMnd
9 tmdmnd 23579 . . . . . . 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 4230 . . . . . 6 (𝒫 𝐴 ∩ Fin) βŠ† Fin
13 simpr 486 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ π‘₯ ∈ (𝒫 𝐴 ∩ Fin))
1412, 13sselid 3981 . . . . 5 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ π‘₯ ∈ Fin)
15 simplr 768 . . . . 5 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ 𝐡 ∈ (0[,]+∞))
16 xrge0base 32186 . . . . . 6 (0[,]+∞) = (Baseβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
17 eqid 2733 . . . . . 6 (.gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞))) = (.gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
183, 16, 17gsumconstf 19803 . . . . 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 14316 . . . . . 6 (π‘₯ ∈ Fin β†’ (β™―β€˜π‘₯) ∈ β„•0)
2114, 20syl 17 . . . . 5 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ (β™―β€˜π‘₯) ∈ β„•0)
22 xrge0mulgnn0 32190 . . . . 5 (((β™―β€˜π‘₯) ∈ β„•0 ∧ 𝐡 ∈ (0[,]+∞)) β†’ ((β™―β€˜π‘₯)(.gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
2321, 15, 22syl2anc 585 . . . 4 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ ((β™―β€˜π‘₯)(.gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
2419, 23eqtrd 2773 . . 3 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ ((ℝ*𝑠 β†Ύs (0[,]+∞)) Ξ£g (π‘˜ ∈ π‘₯ ↦ 𝐡)) = ((β™―β€˜π‘₯) Β·e 𝐡))
255, 1, 6, 7, 24esumval 33044 . 2 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ Ξ£*π‘˜ ∈ 𝐴𝐡 = sup(ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)), ℝ*, < ))
26 nn0ssre 12476 . . . . . . . . . 10 β„•0 βŠ† ℝ
27 ressxr 11258 . . . . . . . . . 10 ℝ βŠ† ℝ*
2826, 27sstri 3992 . . . . . . . . 9 β„•0 βŠ† ℝ*
29 pnfxr 11268 . . . . . . . . . 10 +∞ ∈ ℝ*
30 snssi 4812 . . . . . . . . . 10 (+∞ ∈ ℝ* β†’ {+∞} βŠ† ℝ*)
3129, 30ax-mp 5 . . . . . . . . 9 {+∞} βŠ† ℝ*
3228, 31unssi 4186 . . . . . . . 8 (β„•0 βˆͺ {+∞}) βŠ† ℝ*
33 hashf 14298 . . . . . . . . 9 β™―:V⟢(β„•0 βˆͺ {+∞})
34 vex 3479 . . . . . . . . 9 π‘₯ ∈ V
35 ffvelcdm 7084 . . . . . . . . 9 ((β™―:V⟢(β„•0 βˆͺ {+∞}) ∧ π‘₯ ∈ V) β†’ (β™―β€˜π‘₯) ∈ (β„•0 βˆͺ {+∞}))
3633, 34, 35mp2an 691 . . . . . . . 8 (β™―β€˜π‘₯) ∈ (β„•0 βˆͺ {+∞})
3732, 36sselii 3980 . . . . . . 7 (β™―β€˜π‘₯) ∈ ℝ*
3837a1i 11 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ (β™―β€˜π‘₯) ∈ ℝ*)
39 iccssxr 13407 . . . . . . . 8 (0[,]+∞) βŠ† ℝ*
40 simpr 486 . . . . . . . 8 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ 𝐡 ∈ (0[,]+∞))
4139, 40sselid 3981 . . . . . . 7 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ 𝐡 ∈ ℝ*)
4241adantr 482 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ 𝐡 ∈ ℝ*)
4338, 42xmulcld 13281 . . . . 5 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ ((β™―β€˜π‘₯) Β·e 𝐡) ∈ ℝ*)
4443fmpttd 7115 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)):(𝒫 𝐴 ∩ Fin)βŸΆβ„*)
4544frnd 6726 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) βŠ† ℝ*)
46 hashxrcl 14317 . . . . 5 (𝐴 ∈ 𝑉 β†’ (β™―β€˜π΄) ∈ ℝ*)
4746adantr 482 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ (β™―β€˜π΄) ∈ ℝ*)
4847, 41xmulcld 13281 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ ((β™―β€˜π΄) Β·e 𝐡) ∈ ℝ*)
49 vex 3479 . . . . . . . 8 𝑦 ∈ V
50 eqid 2733 . . . . . . . . 9 (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) = (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))
5150elrnmpt 5956 . . . . . . . 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 11261 . . . . . . . . . . 11 0 ∈ ℝ*
5655a1i 11 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ 0 ∈ ℝ*)
5729a1i 11 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ +∞ ∈ ℝ*)
58 iccgelb 13380 . . . . . . . . . 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 4229 . . . . . . . . . . . 12 (𝒫 𝐴 ∩ Fin) βŠ† 𝒫 𝐴
6362sseli 3979 . . . . . . . . . . 11 (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) β†’ π‘₯ ∈ 𝒫 𝐴)
64 elpwi 4610 . . . . . . . . . . 11 (π‘₯ ∈ 𝒫 𝐴 β†’ π‘₯ βŠ† 𝐴)
6513, 63, 643syl 18 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ π‘₯ βŠ† 𝐴)
66 ssdomg 8996 . . . . . . . . . 10 (𝐴 ∈ 𝑉 β†’ (π‘₯ βŠ† 𝐴 β†’ π‘₯ β‰Ό 𝐴))
6761, 65, 66sylc 65 . . . . . . . . 9 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ π‘₯ β‰Ό 𝐴)
68 hashdomi 14340 . . . . . . . . 9 (π‘₯ β‰Ό 𝐴 β†’ (β™―β€˜π‘₯) ≀ (β™―β€˜π΄))
6967, 68syl 17 . . . . . . . 8 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ (β™―β€˜π‘₯) ≀ (β™―β€˜π΄))
70 xlemul1a 13267 . . . . . . . 8 ((((β™―β€˜π‘₯) ∈ ℝ* ∧ (β™―β€˜π΄) ∈ ℝ* ∧ (𝐡 ∈ ℝ* ∧ 0 ≀ 𝐡)) ∧ (β™―β€˜π‘₯) ≀ (β™―β€˜π΄)) β†’ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡))
7138, 54, 60, 69, 70syl31anc 1374 . . . . . . 7 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ π‘₯ ∈ (𝒫 𝐴 ∩ Fin)) β†’ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡))
7271ralrimiva 3147 . . . . . 6 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ βˆ€π‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡))
73 r19.29r 3117 . . . . . 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 5171 . . . . . 6 ((𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡) ∧ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡)) β†’ 𝑦 ≀ ((β™―β€˜π΄) Β·e 𝐡))
7877rexlimivw 3152 . . . . 5 (βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((β™―β€˜π‘₯) Β·e 𝐡) ∧ ((β™―β€˜π‘₯) Β·e 𝐡) ≀ ((β™―β€˜π΄) Β·e 𝐡)) β†’ 𝑦 ≀ ((β™―β€˜π΄) Β·e 𝐡))
7974, 78syl 17 . . . 4 (((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))) β†’ 𝑦 ≀ ((β™―β€˜π΄) Β·e 𝐡))
8079ralrimiva 3147 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ βˆ€π‘¦ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 ≀ ((β™―β€˜π΄) Β·e 𝐡))
81 pwidg 4623 . . . . . . . . . . 11 (𝐴 ∈ Fin β†’ 𝐴 ∈ 𝒫 𝐴)
8281ancri 551 . . . . . . . . . 10 (𝐴 ∈ Fin β†’ (𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin))
83 elin 3965 . . . . . . . . . 10 (𝐴 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin))
8482, 83sylibr 233 . . . . . . . . 9 (𝐴 ∈ Fin β†’ 𝐴 ∈ (𝒫 𝐴 ∩ Fin))
85 eqid 2733 . . . . . . . . . . 11 ((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π΄) Β·e 𝐡)
86 fveq2 6892 . . . . . . . . . . . . 13 (π‘₯ = 𝐴 β†’ (β™―β€˜π‘₯) = (β™―β€˜π΄))
8786oveq1d 7424 . . . . . . . . . . . 12 (π‘₯ = 𝐴 β†’ ((β™―β€˜π‘₯) Β·e 𝐡) = ((β™―β€˜π΄) Β·e 𝐡))
8887rspceeqv 3634 . . . . . . . . . . 11 ((𝐴 ∈ (𝒫 𝐴 ∩ Fin) ∧ ((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π΄) Β·e 𝐡)) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
8985, 88mpan2 690 . . . . . . . . . 10 (𝐴 ∈ (𝒫 𝐴 ∩ Fin) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
90 ovex 7442 . . . . . . . . . . 11 ((β™―β€˜π΄) Β·e 𝐡) ∈ V
9150elrnmpt 5956 . . . . . . . . . . 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 5153 . . . . . . . 8 (𝑧 = ((β™―β€˜π΄) Β·e 𝐡) β†’ (𝑦 < 𝑧 ↔ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)))
9897rspcev 3613 . . . . . . 7 ((((β™―β€˜π΄) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
9995, 96, 98syl2anc 585 . . . . . 6 (((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ 𝐴 ∈ Fin) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
100 0elpw 5355 . . . . . . . . . . . 12 βˆ… ∈ 𝒫 𝐴
101 0fin 9171 . . . . . . . . . . . 12 βˆ… ∈ Fin
102 elin 3965 . . . . . . . . . . . 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 7425 . . . . . . . . . . 11 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ ((β™―β€˜βˆ…) Β·e 𝐡) = ((β™―β€˜βˆ…) Β·e 0))
107 hash0 14327 . . . . . . . . . . . . 13 (β™―β€˜βˆ…) = 0
108107, 55eqeltri 2830 . . . . . . . . . . . 12 (β™―β€˜βˆ…) ∈ ℝ*
109 xmul01 13246 . . . . . . . . . . . 12 ((β™―β€˜βˆ…) ∈ ℝ* β†’ ((β™―β€˜βˆ…) Β·e 0) = 0)
110108, 109ax-mp 5 . . . . . . . . . . 11 ((β™―β€˜βˆ…) Β·e 0) = 0
111106, 110eqtr2di 2790 . . . . . . . . . 10 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ 0 = ((β™―β€˜βˆ…) Β·e 𝐡))
112 fveq2 6892 . . . . . . . . . . . 12 (π‘₯ = βˆ… β†’ (β™―β€˜π‘₯) = (β™―β€˜βˆ…))
113112oveq1d 7424 . . . . . . . . . . 11 (π‘₯ = βˆ… β†’ ((β™―β€˜π‘₯) Β·e 𝐡) = ((β™―β€˜βˆ…) Β·e 𝐡))
114113rspceeqv 3634 . . . . . . . . . 10 ((βˆ… ∈ (𝒫 𝐴 ∩ Fin) ∧ 0 = ((β™―β€˜βˆ…) Β·e 𝐡)) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)0 = ((β™―β€˜π‘₯) Β·e 𝐡))
115104, 111, 114syl2anc 585 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)0 = ((β™―β€˜π‘₯) Β·e 𝐡))
116 ovex 7442 . . . . . . . . . 10 ((β™―β€˜π‘₯) Β·e 𝐡) ∈ V
11750, 116elrnmpti 5960 . . . . . . . . 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 7425 . . . . . . . . . 10 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ ((β™―β€˜π΄) Β·e 𝐡) = ((β™―β€˜π΄) Β·e 0))
12147ad4antr 731 . . . . . . . . . . 11 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ (β™―β€˜π΄) ∈ ℝ*)
122 xmul01 13246 . . . . . . . . . . 11 ((β™―β€˜π΄) ∈ ℝ* β†’ ((β™―β€˜π΄) Β·e 0) = 0)
123121, 122syl 17 . . . . . . . . . 10 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ ((β™―β€˜π΄) Β·e 0) = 0)
124120, 123eqtrd 2773 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ ((β™―β€˜π΄) Β·e 𝐡) = 0)
125119, 124breqtrd 5175 . . . . . . . 8 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = 0) β†’ 𝑦 < 0)
126 breq2 5153 . . . . . . . . 9 (𝑧 = 0 β†’ (𝑦 < 𝑧 ↔ 𝑦 < 0))
127126rspcev 3613 . . . . . . . 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 2834 . . . . . . . . . . . . . . 15 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ (β™―β€˜π‘Ž) ∈ β„•)
133 nnnn0 12479 . . . . . . . . . . . . . . . 16 ((β™―β€˜π‘Ž) ∈ β„• β†’ (β™―β€˜π‘Ž) ∈ β„•0)
134 vex 3479 . . . . . . . . . . . . . . . . 17 π‘Ž ∈ V
135 hashclb 14318 . . . . . . . . . . . . . . . . 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 4195 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ π‘Ž ∈ (𝒫 𝐴 ∩ Fin))
140 eqidd 2734 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ ((β™―β€˜π‘Ž) Β·e 𝐡) = ((β™―β€˜π‘Ž) Β·e 𝐡))
141 fveq2 6892 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ž β†’ (β™―β€˜π‘₯) = (β™―β€˜π‘Ž))
142141oveq1d 7424 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ž β†’ ((β™―β€˜π‘₯) Β·e 𝐡) = ((β™―β€˜π‘Ž) Β·e 𝐡))
143142rspceeqv 3634 . . . . . . . . . . . . 13 ((π‘Ž ∈ (𝒫 𝐴 ∩ Fin) ∧ ((β™―β€˜π‘Ž) Β·e 𝐡) = ((β™―β€˜π‘Ž) Β·e 𝐡)) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π‘Ž) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
144139, 140, 143syl2anc 585 . . . . . . . . . . . 12 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ βˆƒπ‘₯ ∈ (𝒫 𝐴 ∩ Fin)((β™―β€˜π‘Ž) Β·e 𝐡) = ((β™―β€˜π‘₯) Β·e 𝐡))
14550, 116elrnmpti 5960 . . . . . . . . . . . 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 12227 . . . . . . . . . . . . . 14 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝑛 ∈ ℝ)
150 simp-5r 785 . . . . . . . . . . . . . 14 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝐡 ∈ ℝ+)
151148, 149, 150ltdivmul2d 13068 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ ((𝑦 / 𝐡) < 𝑛 ↔ 𝑦 < (𝑛 Β· 𝐡)))
152147, 151mpbid 231 . . . . . . . . . . . 12 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝑦 < (𝑛 Β· 𝐡))
153130oveq1d 7424 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ ((β™―β€˜π‘Ž) Β·e 𝐡) = (𝑛 Β·e 𝐡))
154150rpred 13016 . . . . . . . . . . . . . 14 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝐡 ∈ ℝ)
155 rexmul 13250 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝑛 Β·e 𝐡) = (𝑛 Β· 𝐡))
156149, 154, 155syl2anc 585 . . . . . . . . . . . . 13 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ (𝑛 Β·e 𝐡) = (𝑛 Β· 𝐡))
157153, 156eqtrd 2773 . . . . . . . . . . . 12 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ ((β™―β€˜π‘Ž) Β·e 𝐡) = (𝑛 Β· 𝐡))
158152, 157breqtrrd 5177 . . . . . . . . . . 11 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ 𝑦 < ((β™―β€˜π‘Ž) Β·e 𝐡))
159 breq2 5153 . . . . . . . . . . . 12 (𝑧 = ((β™―β€˜π‘Ž) Β·e 𝐡) β†’ (𝑦 < 𝑧 ↔ 𝑦 < ((β™―β€˜π‘Ž) Β·e 𝐡)))
160159rspcev 3613 . . . . . . . . . . 11 ((((β™―β€˜π‘Ž) Β·e 𝐡) ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡)) ∧ 𝑦 < ((β™―β€˜π‘Ž) Β·e 𝐡)) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
161146, 158, 160syl2anc 585 . . . . . . . . . 10 ((((((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) ∧ 𝑛 ∈ β„•) ∧ (𝑦 / 𝐡) < 𝑛) ∧ π‘Ž ∈ 𝒫 𝐴) ∧ (β™―β€˜π‘Ž) = 𝑛) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
162161rexlimdva2 3158 . . . . . . . . 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 13047 . . . . . . . . . 10 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ (𝑦 / 𝐡) ∈ ℝ)
167 arch 12469 . . . . . . . . . 10 ((𝑦 / 𝐡) ∈ ℝ β†’ βˆƒπ‘› ∈ β„• (𝑦 / 𝐡) < 𝑛)
168166, 167syl 17 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ βˆƒπ‘› ∈ β„• (𝑦 / 𝐡) < 𝑛)
169 ishashinf 14424 . . . . . . . . . 10 (Β¬ 𝐴 ∈ Fin β†’ βˆ€π‘› ∈ β„• βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛)
170169ad2antlr 726 . . . . . . . . 9 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ βˆ€π‘› ∈ β„• βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛)
171 r19.29r 3117 . . . . . . . . 9 ((βˆƒπ‘› ∈ β„• (𝑦 / 𝐡) < 𝑛 ∧ βˆ€π‘› ∈ β„• βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛) β†’ βˆƒπ‘› ∈ β„• ((𝑦 / 𝐡) < 𝑛 ∧ βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛))
172168, 170, 171syl2anc 585 . . . . . . . 8 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ βˆƒπ‘› ∈ β„• ((𝑦 / 𝐡) < 𝑛 ∧ βˆƒπ‘Ž ∈ 𝒫 𝐴(β™―β€˜π‘Ž) = 𝑛))
173163, 172r19.29a 3163 . . . . . . 7 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 ∈ ℝ+) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧)
174 nfielex 9273 . . . . . . . . . . . 12 (Β¬ 𝐴 ∈ Fin β†’ βˆƒπ‘™ 𝑙 ∈ 𝐴)
175174adantr 482 . . . . . . . . . . 11 ((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) β†’ βˆƒπ‘™ 𝑙 ∈ 𝐴)
176 snelpwi 5444 . . . . . . . . . . . . . . 15 (𝑙 ∈ 𝐴 β†’ {𝑙} ∈ 𝒫 𝐴)
177 snfi 9044 . . . . . . . . . . . . . . 15 {𝑙} ∈ Fin
178176, 177jctir 522 . . . . . . . . . . . . . 14 (𝑙 ∈ 𝐴 β†’ ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin))
179 elin 3965 . . . . . . . . . . . . . 14 ({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ↔ ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin))
180178, 179sylibr 233 . . . . . . . . . . . . 13 (𝑙 ∈ 𝐴 β†’ {𝑙} ∈ (𝒫 𝐴 ∩ Fin))
181180adantl 483 . . . . . . . . . . . 12 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ {𝑙} ∈ (𝒫 𝐴 ∩ Fin))
182 simplr 768 . . . . . . . . . . . . . 14 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ 𝐡 = +∞)
183182oveq2d 7425 . . . . . . . . . . . . 13 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ ((β™―β€˜{𝑙}) Β·e 𝐡) = ((β™―β€˜{𝑙}) Β·e +∞))
184 hashsng 14329 . . . . . . . . . . . . . . . 16 (𝑙 ∈ 𝐴 β†’ (β™―β€˜{𝑙}) = 1)
185 1re 11214 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
18627, 185sselii 3980 . . . . . . . . . . . . . . . 16 1 ∈ ℝ*
187184, 186eqeltrdi 2842 . . . . . . . . . . . . . . 15 (𝑙 ∈ 𝐴 β†’ (β™―β€˜{𝑙}) ∈ ℝ*)
188 0lt1 11736 . . . . . . . . . . . . . . . 16 0 < 1
189188, 184breqtrrid 5187 . . . . . . . . . . . . . . 15 (𝑙 ∈ 𝐴 β†’ 0 < (β™―β€˜{𝑙}))
190 xmulpnf1 13253 . . . . . . . . . . . . . . 15 (((β™―β€˜{𝑙}) ∈ ℝ* ∧ 0 < (β™―β€˜{𝑙})) β†’ ((β™―β€˜{𝑙}) Β·e +∞) = +∞)
191187, 189, 190syl2anc 585 . . . . . . . . . . . . . 14 (𝑙 ∈ 𝐴 β†’ ((β™―β€˜{𝑙}) Β·e +∞) = +∞)
192191adantl 483 . . . . . . . . . . . . 13 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ ((β™―β€˜{𝑙}) Β·e +∞) = +∞)
193183, 192eqtr2d 2774 . . . . . . . . . . . 12 (((Β¬ 𝐴 ∈ Fin ∧ 𝐡 = +∞) ∧ 𝑙 ∈ 𝐴) β†’ +∞ = ((β™―β€˜{𝑙}) Β·e 𝐡))
194 fveq2 6892 . . . . . . . . . . . . . 14 (π‘₯ = {𝑙} β†’ (β™―β€˜π‘₯) = (β™―β€˜{𝑙}))
195194oveq1d 7424 . . . . . . . . . . . . 13 (π‘₯ = {𝑙} β†’ ((β™―β€˜π‘₯) Β·e 𝐡) = ((β™―β€˜{𝑙}) Β·e 𝐡))
196195rspceeqv 3634 . . . . . . . . . . . 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 5960 . . . . . . . . 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 13100 . . . . . . . . 9 (𝑦 ∈ ℝ β†’ 𝑦 < +∞)
204202, 203syl 17 . . . . . . . 8 ((((((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((β™―β€˜π΄) Β·e 𝐡)) ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝐡 = +∞) β†’ 𝑦 < +∞)
205 breq2 5153 . . . . . . . . 9 (𝑧 = +∞ β†’ (𝑦 < 𝑧 ↔ 𝑦 < +∞))
206205rspcev 3613 . . . . . . . 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 32098 . . . . . . . 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 3147 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ (0[,]+∞)) β†’ βˆ€π‘¦ ∈ ℝ (𝑦 < ((β™―β€˜π΄) Β·e 𝐡) β†’ βˆƒπ‘§ ∈ ran (π‘₯ ∈ (𝒫 𝐴 ∩ Fin) ↦ ((β™―β€˜π‘₯) Β·e 𝐡))𝑦 < 𝑧))
215 supxr2 13293 . . 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 2773 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 2884  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629   class class class wbr 5149   ↦ cmpt 5232  ran crn 5678  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   β‰Ό cdom 8937  Fincfn 8939  supcsup 9435  β„cr 11109  0cc0 11110  1c1 11111   Β· cmul 11115  +∞cpnf 11245  β„*cxr 11247   < clt 11248   ≀ cle 11249   / cdiv 11871  β„•cn 12212  β„•0cn0 12472  β„+crp 12974   Β·e cxmu 13091  [,]cicc 13327  β™―chash 14290   β†Ύs cress 17173   Ξ£g cgsu 17386  β„*𝑠cxrs 17446  Mndcmnd 18625  .gcmg 18950  TopMndctmd 23574  Ξ£*cesum 33025
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 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188  ax-addf 11189  ax-mulf 11190
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-oadd 8470  df-er 8703  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-fi 9406  df-sup 9437  df-inf 9438  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-xnn0 12545  df-z 12559  df-dec 12678  df-uz 12823  df-q 12933  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-ioo 13328  df-ioc 13329  df-ico 13330  df-icc 13331  df-fz 13485  df-fzo 13628  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-fac 14234  df-bc 14263  df-hash 14291  df-shft 15014  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-limsup 15415  df-clim 15432  df-rlim 15433  df-sum 15633  df-ef 16011  df-sin 16013  df-cos 16014  df-pi 16016  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-starv 17212  df-sca 17213  df-vsca 17214  df-ip 17215  df-tset 17216  df-ple 17217  df-ds 17219  df-unif 17220  df-hom 17221  df-cco 17222  df-rest 17368  df-topn 17369  df-0g 17387  df-gsum 17388  df-topgen 17389  df-pt 17390  df-prds 17393  df-ordt 17447  df-xrs 17448  df-qtop 17453  df-imas 17454  df-xps 17456  df-mre 17530  df-mrc 17531  df-acs 17533  df-ps 18519  df-tsr 18520  df-plusf 18560  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-mhm 18671  df-submnd 18672  df-grp 18822  df-minusg 18823  df-sbg 18824  df-mulg 18951  df-subg 19003  df-cntz 19181  df-cmn 19650  df-abl 19651  df-mgp 19988  df-ur 20005  df-ring 20058  df-cring 20059  df-subrg 20317  df-abv 20425  df-lmod 20473  df-scaf 20474  df-sra 20785  df-rgmod 20786  df-psmet 20936  df-xmet 20937  df-met 20938  df-bl 20939  df-mopn 20940  df-fbas 20941  df-fg 20942  df-cnfld 20945  df-top 22396  df-topon 22413  df-topsp 22435  df-bases 22449  df-cld 22523  df-ntr 22524  df-cls 22525  df-nei 22602  df-lp 22640  df-perf 22641  df-cn 22731  df-cnp 22732  df-haus 22819  df-tx 23066  df-hmeo 23259  df-fil 23350  df-fm 23442  df-flim 23443  df-flf 23444  df-tmd 23576  df-tgp 23577  df-tsms 23631  df-trg 23664  df-xms 23826  df-ms 23827  df-tms 23828  df-nm 24091  df-ngp 24092  df-nrg 24094  df-nlm 24095  df-ii 24393  df-cncf 24394  df-limc 25383  df-dv 25384  df-log 26065  df-esum 33026
This theorem is referenced by:  esumpinfval  33071  esumpinfsum  33075
  Copyright terms: Public domain W3C validator