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 29452
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 2765 . . . 4 𝑘 𝐴𝑉
3 esumcst.2 . . . . 5 𝑘𝐵
43nfel1 2765 . . . 4 𝑘 𝐵 ∈ (0[,]+∞)
52, 4nfan 1816 . . 3 𝑘(𝐴𝑉𝐵 ∈ (0[,]+∞))
6 simpl 472 . . 3 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → 𝐴𝑉)
7 simplr 788 . . 3 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑘𝐴) → 𝐵 ∈ (0[,]+∞))
8 xrge0tmd 29320 . . . . . . 7 (ℝ*𝑠s (0[,]+∞)) ∈ TopMnd
9 tmdmnd 21689 . . . . . . 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 3796 . . . . . 6 (𝒫 𝐴 ∩ Fin) ⊆ Fin
13 simpr 476 . . . . . 6 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ (𝒫 𝐴 ∩ Fin))
1412, 13sseldi 3566 . . . . 5 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin)
15 simplr 788 . . . . 5 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐵 ∈ (0[,]+∞))
16 xrge0base 29016 . . . . . 6 (0[,]+∞) = (Base‘(ℝ*𝑠s (0[,]+∞)))
17 eqid 2610 . . . . . 6 (.g‘(ℝ*𝑠s (0[,]+∞))) = (.g‘(ℝ*𝑠s (0[,]+∞)))
183, 16, 17gsumconstf 18158 . . . . 5 (((ℝ*𝑠s (0[,]+∞)) ∈ Mnd ∧ 𝑥 ∈ Fin ∧ 𝐵 ∈ (0[,]+∞)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) = ((#‘𝑥)(.g‘(ℝ*𝑠s (0[,]+∞)))𝐵))
1911, 14, 15, 18syl3anc 1318 . . . 4 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) = ((#‘𝑥)(.g‘(ℝ*𝑠s (0[,]+∞)))𝐵))
20 hashcl 13009 . . . . . 6 (𝑥 ∈ Fin → (#‘𝑥) ∈ ℕ0)
2114, 20syl 17 . . . . 5 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (#‘𝑥) ∈ ℕ0)
22 xrge0mulgnn0 29020 . . . . 5 (((#‘𝑥) ∈ ℕ0𝐵 ∈ (0[,]+∞)) → ((#‘𝑥)(.g‘(ℝ*𝑠s (0[,]+∞)))𝐵) = ((#‘𝑥) ·e 𝐵))
2321, 15, 22syl2anc 691 . . . 4 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((#‘𝑥)(.g‘(ℝ*𝑠s (0[,]+∞)))𝐵) = ((#‘𝑥) ·e 𝐵))
2419, 23eqtrd 2644 . . 3 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) = ((#‘𝑥) ·e 𝐵))
255, 1, 6, 7, 24esumval 29435 . 2 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → Σ*𝑘𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)), ℝ*, < ))
26 nn0ssre 11173 . . . . . . . . . 10 0 ⊆ ℝ
27 ressxr 9962 . . . . . . . . . 10 ℝ ⊆ ℝ*
2826, 27sstri 3577 . . . . . . . . 9 0 ⊆ ℝ*
29 pnfxr 9971 . . . . . . . . . 10 +∞ ∈ ℝ*
30 snssi 4280 . . . . . . . . . 10 (+∞ ∈ ℝ* → {+∞} ⊆ ℝ*)
3129, 30ax-mp 5 . . . . . . . . 9 {+∞} ⊆ ℝ*
3228, 31unssi 3750 . . . . . . . 8 (ℕ0 ∪ {+∞}) ⊆ ℝ*
33 hashf 12987 . . . . . . . . 9 #:V⟶(ℕ0 ∪ {+∞})
34 vex 3176 . . . . . . . . 9 𝑥 ∈ V
35 ffvelrn 6265 . . . . . . . . 9 ((#:V⟶(ℕ0 ∪ {+∞}) ∧ 𝑥 ∈ V) → (#‘𝑥) ∈ (ℕ0 ∪ {+∞}))
3633, 34, 35mp2an 704 . . . . . . . 8 (#‘𝑥) ∈ (ℕ0 ∪ {+∞})
3732, 36sselii 3565 . . . . . . 7 (#‘𝑥) ∈ ℝ*
3837a1i 11 . . . . . 6 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (#‘𝑥) ∈ ℝ*)
39 iccssxr 12127 . . . . . . . 8 (0[,]+∞) ⊆ ℝ*
40 simpr 476 . . . . . . . 8 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → 𝐵 ∈ (0[,]+∞))
4139, 40sseldi 3566 . . . . . . 7 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → 𝐵 ∈ ℝ*)
4241adantr 480 . . . . . 6 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐵 ∈ ℝ*)
4338, 42xmulcld 12004 . . . . 5 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((#‘𝑥) ·e 𝐵) ∈ ℝ*)
44 eqid 2610 . . . . 5 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) = (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))
4543, 44fmptd 6292 . . . 4 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)):(𝒫 𝐴 ∩ Fin)⟶ℝ*)
46 frn 5966 . . . 4 ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)):(𝒫 𝐴 ∩ Fin)⟶ℝ* → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ⊆ ℝ*)
4745, 46syl 17 . . 3 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ⊆ ℝ*)
48 hashxrcl 13010 . . . . 5 (𝐴𝑉 → (#‘𝐴) ∈ ℝ*)
4948adantr 480 . . . 4 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → (#‘𝐴) ∈ ℝ*)
5049, 41xmulcld 12004 . . 3 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → ((#‘𝐴) ·e 𝐵) ∈ ℝ*)
51 vex 3176 . . . . . . . 8 𝑦 ∈ V
5244elrnmpt 5293 . . . . . . . 8 (𝑦 ∈ V → (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((#‘𝑥) ·e 𝐵)))
5351, 52ax-mp 5 . . . . . . 7 (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((#‘𝑥) ·e 𝐵))
5453biimpi 205 . . . . . 6 (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((#‘𝑥) ·e 𝐵))
5549adantr 480 . . . . . . . 8 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (#‘𝐴) ∈ ℝ*)
56 0xr 9965 . . . . . . . . . . 11 0 ∈ ℝ*
5756a1i 11 . . . . . . . . . 10 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈ ℝ*)
5829a1i 11 . . . . . . . . . 10 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → +∞ ∈ ℝ*)
59 iccgelb 12101 . . . . . . . . . 10 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐵 ∈ (0[,]+∞)) → 0 ≤ 𝐵)
6057, 58, 15, 59syl3anc 1318 . . . . . . . . 9 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ≤ 𝐵)
6142, 60jca 553 . . . . . . . 8 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵))
626adantr 480 . . . . . . . . . 10 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐴𝑉)
63 inss1 3795 . . . . . . . . . . . 12 (𝒫 𝐴 ∩ Fin) ⊆ 𝒫 𝐴
6463sseli 3564 . . . . . . . . . . 11 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴)
65 elpwi 4117 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
6613, 64, 653syl 18 . . . . . . . . . 10 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝐴)
67 ssdomg 7887 . . . . . . . . . 10 (𝐴𝑉 → (𝑥𝐴𝑥𝐴))
6862, 66, 67sylc 63 . . . . . . . . 9 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝐴)
69 hashdomi 13030 . . . . . . . . 9 (𝑥𝐴 → (#‘𝑥) ≤ (#‘𝐴))
7068, 69syl 17 . . . . . . . 8 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (#‘𝑥) ≤ (#‘𝐴))
71 xlemul1a 11990 . . . . . . . 8 ((((#‘𝑥) ∈ ℝ* ∧ (#‘𝐴) ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵)) ∧ (#‘𝑥) ≤ (#‘𝐴)) → ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵))
7238, 55, 61, 70, 71syl31anc 1321 . . . . . . 7 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵))
7372ralrimiva 2949 . . . . . 6 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → ∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵))
74 r19.29r 3055 . . . . . 6 ((∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)))
7554, 73, 74syl2anr 494 . . . . 5 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)))
76 simpl 472 . . . . . . 7 ((𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)) → 𝑦 = ((#‘𝑥) ·e 𝐵))
77 simpr 476 . . . . . . 7 ((𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)) → ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵))
7876, 77eqbrtrd 4605 . . . . . 6 ((𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)) → 𝑦 ≤ ((#‘𝐴) ·e 𝐵))
7978rexlimivw 3011 . . . . 5 (∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)) → 𝑦 ≤ ((#‘𝐴) ·e 𝐵))
8075, 79syl 17 . . . 4 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))) → 𝑦 ≤ ((#‘𝐴) ·e 𝐵))
8180ralrimiva 2949 . . 3 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → ∀𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 ≤ ((#‘𝐴) ·e 𝐵))
82 pwidg 4121 . . . . . . . . . . 11 (𝐴 ∈ Fin → 𝐴 ∈ 𝒫 𝐴)
8382ancri 573 . . . . . . . . . 10 (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐴𝐴 ∈ Fin))
84 elin 3758 . . . . . . . . . 10 (𝐴 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐴𝐴 ∈ Fin))
8583, 84sylibr 223 . . . . . . . . 9 (𝐴 ∈ Fin → 𝐴 ∈ (𝒫 𝐴 ∩ Fin))
86 eqid 2610 . . . . . . . . . . 11 ((#‘𝐴) ·e 𝐵) = ((#‘𝐴) ·e 𝐵)
87 fveq2 6103 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (#‘𝑥) = (#‘𝐴))
8887oveq1d 6564 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → ((#‘𝑥) ·e 𝐵) = ((#‘𝐴) ·e 𝐵))
8988eqeq2d 2620 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (((#‘𝐴) ·e 𝐵) = ((#‘𝑥) ·e 𝐵) ↔ ((#‘𝐴) ·e 𝐵) = ((#‘𝐴) ·e 𝐵)))
9089rspcev 3282 . . . . . . . . . . 11 ((𝐴 ∈ (𝒫 𝐴 ∩ Fin) ∧ ((#‘𝐴) ·e 𝐵) = ((#‘𝐴) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝐴) ·e 𝐵) = ((#‘𝑥) ·e 𝐵))
9186, 90mpan2 703 . . . . . . . . . 10 (𝐴 ∈ (𝒫 𝐴 ∩ Fin) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝐴) ·e 𝐵) = ((#‘𝑥) ·e 𝐵))
92 ovex 6577 . . . . . . . . . . 11 ((#‘𝐴) ·e 𝐵) ∈ V
9344elrnmpt 5293 . . . . . . . . . . 11 (((#‘𝐴) ·e 𝐵) ∈ V → (((#‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝐴) ·e 𝐵) = ((#‘𝑥) ·e 𝐵)))
9492, 93ax-mp 5 . . . . . . . . . 10 (((#‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝐴) ·e 𝐵) = ((#‘𝑥) ·e 𝐵))
9591, 94sylibr 223 . . . . . . . . 9 (𝐴 ∈ (𝒫 𝐴 ∩ Fin) → ((#‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)))
9685, 95syl 17 . . . . . . . 8 (𝐴 ∈ Fin → ((#‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)))
9796adantl 481 . . . . . . 7 (((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → ((#‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)))
98 simplr 788 . . . . . . 7 (((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → 𝑦 < ((#‘𝐴) ·e 𝐵))
99 breq2 4587 . . . . . . . 8 (𝑧 = ((#‘𝐴) ·e 𝐵) → (𝑦 < 𝑧𝑦 < ((#‘𝐴) ·e 𝐵)))
10099rspcev 3282 . . . . . . 7 ((((#‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
10197, 98, 100syl2anc 691 . . . . . 6 (((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
102 0elpw 4760 . . . . . . . . . . . 12 ∅ ∈ 𝒫 𝐴
103 0fin 8073 . . . . . . . . . . . 12 ∅ ∈ Fin
104 elin 3758 . . . . . . . . . . . 12 (∅ ∈ (𝒫 𝐴 ∩ Fin) ↔ (∅ ∈ 𝒫 𝐴 ∧ ∅ ∈ Fin))
105102, 103, 104mpbir2an 957 . . . . . . . . . . 11 ∅ ∈ (𝒫 𝐴 ∩ Fin)
106105a1i 11 . . . . . . . . . 10 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∅ ∈ (𝒫 𝐴 ∩ Fin))
107 simpr 476 . . . . . . . . . . . 12 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝐵 = 0)
108107oveq2d 6565 . . . . . . . . . . 11 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((#‘∅) ·e 𝐵) = ((#‘∅) ·e 0))
109 hash0 13019 . . . . . . . . . . . . 13 (#‘∅) = 0
110109, 56eqeltri 2684 . . . . . . . . . . . 12 (#‘∅) ∈ ℝ*
111 xmul01 11969 . . . . . . . . . . . 12 ((#‘∅) ∈ ℝ* → ((#‘∅) ·e 0) = 0)
112110, 111ax-mp 5 . . . . . . . . . . 11 ((#‘∅) ·e 0) = 0
113108, 112syl6req 2661 . . . . . . . . . 10 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 0 = ((#‘∅) ·e 𝐵))
114 fveq2 6103 . . . . . . . . . . . . 13 (𝑥 = ∅ → (#‘𝑥) = (#‘∅))
115114oveq1d 6564 . . . . . . . . . . . 12 (𝑥 = ∅ → ((#‘𝑥) ·e 𝐵) = ((#‘∅) ·e 𝐵))
116115eqeq2d 2620 . . . . . . . . . . 11 (𝑥 = ∅ → (0 = ((#‘𝑥) ·e 𝐵) ↔ 0 = ((#‘∅) ·e 𝐵)))
117116rspcev 3282 . . . . . . . . . 10 ((∅ ∈ (𝒫 𝐴 ∩ Fin) ∧ 0 = ((#‘∅) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)0 = ((#‘𝑥) ·e 𝐵))
118106, 113, 117syl2anc 691 . . . . . . . . 9 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)0 = ((#‘𝑥) ·e 𝐵))
119 ovex 6577 . . . . . . . . . 10 ((#‘𝑥) ·e 𝐵) ∈ V
12044, 119elrnmpti 5297 . . . . . . . . 9 (0 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)0 = ((#‘𝑥) ·e 𝐵))
121118, 120sylibr 223 . . . . . . . 8 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 0 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)))
122 simpllr 795 . . . . . . . . 9 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝑦 < ((#‘𝐴) ·e 𝐵))
123107oveq2d 6565 . . . . . . . . . 10 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((#‘𝐴) ·e 𝐵) = ((#‘𝐴) ·e 0))
12449ad4antr 764 . . . . . . . . . . 11 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → (#‘𝐴) ∈ ℝ*)
125 xmul01 11969 . . . . . . . . . . 11 ((#‘𝐴) ∈ ℝ* → ((#‘𝐴) ·e 0) = 0)
126124, 125syl 17 . . . . . . . . . 10 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((#‘𝐴) ·e 0) = 0)
127123, 126eqtrd 2644 . . . . . . . . 9 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((#‘𝐴) ·e 𝐵) = 0)
128122, 127breqtrd 4609 . . . . . . . 8 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝑦 < 0)
129 breq2 4587 . . . . . . . . 9 (𝑧 = 0 → (𝑦 < 𝑧𝑦 < 0))
130129rspcev 3282 . . . . . . . 8 ((0 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ∧ 𝑦 < 0) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
131121, 128, 130syl2anc 691 . . . . . . 7 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
132 simplr 788 . . . . . . . . . . . . . . 15 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑎 ∈ 𝒫 𝐴)
133 simpr 476 . . . . . . . . . . . . . . . . 17 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → (#‘𝑎) = 𝑛)
134 simp-4r 803 . . . . . . . . . . . . . . . . 17 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑛 ∈ ℕ)
135133, 134eqeltrd 2688 . . . . . . . . . . . . . . . 16 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → (#‘𝑎) ∈ ℕ)
136 nnnn0 11176 . . . . . . . . . . . . . . . . 17 ((#‘𝑎) ∈ ℕ → (#‘𝑎) ∈ ℕ0)
137 vex 3176 . . . . . . . . . . . . . . . . . 18 𝑎 ∈ V
138 hashclb 13011 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ V → (𝑎 ∈ Fin ↔ (#‘𝑎) ∈ ℕ0))
139137, 138ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ Fin ↔ (#‘𝑎) ∈ ℕ0)
140136, 139sylibr 223 . . . . . . . . . . . . . . . 16 ((#‘𝑎) ∈ ℕ → 𝑎 ∈ Fin)
141135, 140syl 17 . . . . . . . . . . . . . . 15 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑎 ∈ Fin)
142132, 141elind 3760 . . . . . . . . . . . . . 14 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin))
143 eqidd 2611 . . . . . . . . . . . . . 14 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ((#‘𝑎) ·e 𝐵) = ((#‘𝑎) ·e 𝐵))
144 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (#‘𝑥) = (#‘𝑎))
145144oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → ((#‘𝑥) ·e 𝐵) = ((#‘𝑎) ·e 𝐵))
146145eqeq2d 2620 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (((#‘𝑎) ·e 𝐵) = ((#‘𝑥) ·e 𝐵) ↔ ((#‘𝑎) ·e 𝐵) = ((#‘𝑎) ·e 𝐵)))
147146rspcev 3282 . . . . . . . . . . . . . 14 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ ((#‘𝑎) ·e 𝐵) = ((#‘𝑎) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝑎) ·e 𝐵) = ((#‘𝑥) ·e 𝐵))
148142, 143, 147syl2anc 691 . . . . . . . . . . . . 13 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝑎) ·e 𝐵) = ((#‘𝑥) ·e 𝐵))
14944, 119elrnmpti 5297 . . . . . . . . . . . . 13 (((#‘𝑎) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝑎) ·e 𝐵) = ((#‘𝑥) ·e 𝐵))
150148, 149sylibr 223 . . . . . . . . . . . 12 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ((#‘𝑎) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)))
151 simpllr 795 . . . . . . . . . . . . . 14 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → (𝑦 / 𝐵) < 𝑛)
152 simp-8r 811 . . . . . . . . . . . . . . 15 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑦 ∈ ℝ)
153134nnred 10912 . . . . . . . . . . . . . . 15 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑛 ∈ ℝ)
154 simp-5r 805 . . . . . . . . . . . . . . 15 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝐵 ∈ ℝ+)
155152, 153, 154ltdivmul2d 11800 . . . . . . . . . . . . . 14 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ((𝑦 / 𝐵) < 𝑛𝑦 < (𝑛 · 𝐵)))
156151, 155mpbid 221 . . . . . . . . . . . . 13 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑦 < (𝑛 · 𝐵))
157133oveq1d 6564 . . . . . . . . . . . . . 14 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ((#‘𝑎) ·e 𝐵) = (𝑛 ·e 𝐵))
158154rpred 11748 . . . . . . . . . . . . . . 15 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝐵 ∈ ℝ)
159 rexmul 11973 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑛 ·e 𝐵) = (𝑛 · 𝐵))
160153, 158, 159syl2anc 691 . . . . . . . . . . . . . 14 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → (𝑛 ·e 𝐵) = (𝑛 · 𝐵))
161157, 160eqtrd 2644 . . . . . . . . . . . . 13 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ((#‘𝑎) ·e 𝐵) = (𝑛 · 𝐵))
162156, 161breqtrrd 4611 . . . . . . . . . . . 12 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑦 < ((#‘𝑎) ·e 𝐵))
163 breq2 4587 . . . . . . . . . . . . 13 (𝑧 = ((#‘𝑎) ·e 𝐵) → (𝑦 < 𝑧𝑦 < ((#‘𝑎) ·e 𝐵)))
164163rspcev 3282 . . . . . . . . . . . 12 ((((#‘𝑎) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ∧ 𝑦 < ((#‘𝑎) ·e 𝐵)) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
165150, 162, 164syl2anc 691 . . . . . . . . . . 11 ((((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
166165ex 449 . . . . . . . . . 10 (((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) → ((#‘𝑎) = 𝑛 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧))
167166rexlimdva 3013 . . . . . . . . 9 ((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) → (∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧))
168167impr 647 . . . . . . . 8 ((((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ ((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛)) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
169 simp-4r 803 . . . . . . . . . . 11 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → 𝑦 ∈ ℝ)
170 simpr 476 . . . . . . . . . . 11 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → 𝐵 ∈ ℝ+)
171169, 170rerpdivcld 11779 . . . . . . . . . 10 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → (𝑦 / 𝐵) ∈ ℝ)
172 arch 11166 . . . . . . . . . 10 ((𝑦 / 𝐵) ∈ ℝ → ∃𝑛 ∈ ℕ (𝑦 / 𝐵) < 𝑛)
173171, 172syl 17 . . . . . . . . 9 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → ∃𝑛 ∈ ℕ (𝑦 / 𝐵) < 𝑛)
174 ishashinf 13104 . . . . . . . . . 10 𝐴 ∈ Fin → ∀𝑛 ∈ ℕ ∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛)
175174ad2antlr 759 . . . . . . . . 9 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → ∀𝑛 ∈ ℕ ∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛)
176 r19.29r 3055 . . . . . . . . 9 ((∃𝑛 ∈ ℕ (𝑦 / 𝐵) < 𝑛 ∧ ∀𝑛 ∈ ℕ ∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛) → ∃𝑛 ∈ ℕ ((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛))
177173, 175, 176syl2anc 691 . . . . . . . 8 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → ∃𝑛 ∈ ℕ ((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛))
178168, 177r19.29a 3060 . . . . . . 7 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
179 nfielex 8074 . . . . . . . . . . . 12 𝐴 ∈ Fin → ∃𝑙 𝑙𝐴)
180179adantr 480 . . . . . . . . . . 11 ((¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞) → ∃𝑙 𝑙𝐴)
181 snelpwi 4839 . . . . . . . . . . . . . . 15 (𝑙𝐴 → {𝑙} ∈ 𝒫 𝐴)
182 snfi 7923 . . . . . . . . . . . . . . 15 {𝑙} ∈ Fin
183181, 182jctir 559 . . . . . . . . . . . . . 14 (𝑙𝐴 → ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin))
184 elin 3758 . . . . . . . . . . . . . 14 ({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ↔ ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin))
185183, 184sylibr 223 . . . . . . . . . . . . 13 (𝑙𝐴 → {𝑙} ∈ (𝒫 𝐴 ∩ Fin))
186185adantl 481 . . . . . . . . . . . 12 (((¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙𝐴) → {𝑙} ∈ (𝒫 𝐴 ∩ Fin))
187 simplr 788 . . . . . . . . . . . . . 14 (((¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙𝐴) → 𝐵 = +∞)
188187oveq2d 6565 . . . . . . . . . . . . 13 (((¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙𝐴) → ((#‘{𝑙}) ·e 𝐵) = ((#‘{𝑙}) ·e +∞))
189 hashsng 13020 . . . . . . . . . . . . . . . 16 (𝑙𝐴 → (#‘{𝑙}) = 1)
190 1re 9918 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
19127, 190sselii 3565 . . . . . . . . . . . . . . . 16 1 ∈ ℝ*
192189, 191syl6eqel 2696 . . . . . . . . . . . . . . 15 (𝑙𝐴 → (#‘{𝑙}) ∈ ℝ*)
193 0lt1 10429 . . . . . . . . . . . . . . . 16 0 < 1
194193, 189syl5breqr 4621 . . . . . . . . . . . . . . 15 (𝑙𝐴 → 0 < (#‘{𝑙}))
195 xmulpnf1 11976 . . . . . . . . . . . . . . 15 (((#‘{𝑙}) ∈ ℝ* ∧ 0 < (#‘{𝑙})) → ((#‘{𝑙}) ·e +∞) = +∞)
196192, 194, 195syl2anc 691 . . . . . . . . . . . . . 14 (𝑙𝐴 → ((#‘{𝑙}) ·e +∞) = +∞)
197196adantl 481 . . . . . . . . . . . . 13 (((¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙𝐴) → ((#‘{𝑙}) ·e +∞) = +∞)
198188, 197eqtr2d 2645 . . . . . . . . . . . 12 (((¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙𝐴) → +∞ = ((#‘{𝑙}) ·e 𝐵))
199 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑥 = {𝑙} → (#‘𝑥) = (#‘{𝑙}))
200199oveq1d 6564 . . . . . . . . . . . . . 14 (𝑥 = {𝑙} → ((#‘𝑥) ·e 𝐵) = ((#‘{𝑙}) ·e 𝐵))
201200eqeq2d 2620 . . . . . . . . . . . . 13 (𝑥 = {𝑙} → (+∞ = ((#‘𝑥) ·e 𝐵) ↔ +∞ = ((#‘{𝑙}) ·e 𝐵)))
202201rspcev 3282 . . . . . . . . . . . 12 (({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ∧ +∞ = ((#‘{𝑙}) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((#‘𝑥) ·e 𝐵))
203186, 198, 202syl2anc 691 . . . . . . . . . . 11 (((¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙𝐴) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((#‘𝑥) ·e 𝐵))
204180, 203exlimddv 1850 . . . . . . . . . 10 ((¬ 𝐴 ∈ Fin ∧ 𝐵 = +∞) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((#‘𝑥) ·e 𝐵))
205204adantll 746 . . . . . . . . 9 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((#‘𝑥) ·e 𝐵))
20644, 119elrnmpti 5297 . . . . . . . . 9 (+∞ ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((#‘𝑥) ·e 𝐵))
207205, 206sylibr 223 . . . . . . . 8 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → +∞ ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)))
208 simp-4r 803 . . . . . . . . 9 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → 𝑦 ∈ ℝ)
209 ltpnf 11830 . . . . . . . . 9 (𝑦 ∈ ℝ → 𝑦 < +∞)
210208, 209syl 17 . . . . . . . 8 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → 𝑦 < +∞)
211 breq2 4587 . . . . . . . . 9 (𝑧 = +∞ → (𝑦 < 𝑧𝑦 < +∞))
212211rspcev 3282 . . . . . . . 8 ((+∞ ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ∧ 𝑦 < +∞) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
213207, 210, 212syl2anc 691 . . . . . . 7 ((((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
214 simp-4r 803 . . . . . . . 8 (((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → 𝐵 ∈ (0[,]+∞))
215 elxrge02 28971 . . . . . . . 8 (𝐵 ∈ (0[,]+∞) ↔ (𝐵 = 0 ∨ 𝐵 ∈ ℝ+𝐵 = +∞))
216214, 215sylib 207 . . . . . . 7 (((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → (𝐵 = 0 ∨ 𝐵 ∈ ℝ+𝐵 = +∞))
217131, 178, 213, 216mpjao3dan 1387 . . . . . 6 (((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
218101, 217pm2.61dan 828 . . . . 5 ((((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)
219218ex 449 . . . 4 (((𝐴𝑉𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) → (𝑦 < ((#‘𝐴) ·e 𝐵) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧))
220219ralrimiva 2949 . . 3 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → ∀𝑦 ∈ ℝ (𝑦 < ((#‘𝐴) ·e 𝐵) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧))
221 supxr2 12016 . . 3 (((ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ⊆ ℝ* ∧ ((#‘𝐴) ·e 𝐵) ∈ ℝ*) ∧ (∀𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 ≤ ((#‘𝐴) ·e 𝐵) ∧ ∀𝑦 ∈ ℝ (𝑦 < ((#‘𝐴) ·e 𝐵) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧))) → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)), ℝ*, < ) = ((#‘𝐴) ·e 𝐵))
22247, 50, 81, 220, 221syl22anc 1319 . 2 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)), ℝ*, < ) = ((#‘𝐴) ·e 𝐵))
22325, 222eqtrd 2644 1 ((𝐴𝑉𝐵 ∈ (0[,]+∞)) → Σ*𝑘𝐴𝐵 = ((#‘𝐴) ·e 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3o 1030   = wceq 1475  wex 1695  wcel 1977  wnfc 2738  wral 2896  wrex 2897  Vcvv 3173  cun 3538  cin 3539  wss 3540  c0 3874  𝒫 cpw 4108  {csn 4125   class class class wbr 4583  cmpt 4643  ran crn 5039  wf 5800  cfv 5804  (class class class)co 6549  cdom 7839  Fincfn 7841  supcsup 8229  cr 9814  0cc0 9815  1c1 9816   · cmul 9820  +∞cpnf 9950  *cxr 9952   < clt 9953  cle 9954   / cdiv 10563  cn 10897  0cn0 11169  +crp 11708   ·e cxmu 11821  [,]cicc 12049  #chash 12979  s cress 15696   Σg cgsu 15924  *𝑠cxrs 15983  Mndcmnd 17117  .gcmg 17363  TopMndctmd 21684  Σ*cesum 29416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-xnn0 11241  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-sin 14639  df-cos 14640  df-pi 14642  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-ordt 15984  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-ps 17023  df-tsr 17024  df-plusf 17064  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mhm 17158  df-submnd 17159  df-grp 17248  df-minusg 17249  df-sbg 17250  df-mulg 17364  df-subg 17414  df-cntz 17573  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-cring 18373  df-subrg 18601  df-abv 18640  df-lmod 18688  df-scaf 18689  df-sra 18993  df-rgmod 18994  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-tmd 21686  df-tgp 21687  df-tsms 21740  df-trg 21773  df-xms 21935  df-ms 21936  df-tms 21937  df-nm 22197  df-ngp 22198  df-nrg 22200  df-nlm 22201  df-ii 22488  df-cncf 22489  df-limc 23436  df-dv 23437  df-log 24107  df-esum 29417
This theorem is referenced by:  esumpinfval  29462  esumpinfsum  29466
  Copyright terms: Public domain W3C validator