Step | Hyp | Ref
| Expression |
1 | | esumcst.1 |
. . . . 5
⊢
Ⅎ𝑘𝐴 |
2 | 1 | nfel1 2915 |
. . . 4
⊢
Ⅎ𝑘 𝐴 ∈ 𝑉 |
3 | | esumcst.2 |
. . . . 5
⊢
Ⅎ𝑘𝐵 |
4 | 3 | nfel1 2915 |
. . . 4
⊢
Ⅎ𝑘 𝐵 ∈
(0[,]+∞) |
5 | 2, 4 | nfan 1905 |
. . 3
⊢
Ⅎ𝑘(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) |
6 | | simpl 486 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → 𝐴 ∈ 𝑉) |
7 | | simplr 769 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
8 | | xrge0tmd 31467 |
. . . . . . 7
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ TopMnd |
9 | | tmdmnd 22827 |
. . . . . . 7
⊢
((ℝ*𝑠 ↾s
(0[,]+∞)) ∈ TopMnd → (ℝ*𝑠
↾s (0[,]+∞)) ∈ Mnd) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ Mnd |
11 | 10 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ Mnd) |
12 | | inss2 4121 |
. . . . . 6
⊢
(𝒫 𝐴 ∩
Fin) ⊆ Fin |
13 | | simpr 488 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) |
14 | 12, 13 | sseldi 3876 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin) |
15 | | simplr 769 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐵 ∈
(0[,]+∞)) |
16 | | xrge0base 30871 |
. . . . . 6
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) |
17 | | eqid 2738 |
. . . . . 6
⊢
(.g‘(ℝ*𝑠
↾s (0[,]+∞))) =
(.g‘(ℝ*𝑠
↾s (0[,]+∞))) |
18 | 3, 16, 17 | gsumconstf 19175 |
. . . . 5
⊢
(((ℝ*𝑠 ↾s
(0[,]+∞)) ∈ Mnd ∧ 𝑥 ∈ Fin ∧ 𝐵 ∈ (0[,]+∞)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = ((♯‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵)) |
19 | 11, 14, 15, 18 | syl3anc 1372 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = ((♯‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵)) |
20 | | hashcl 13810 |
. . . . . 6
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) |
21 | 14, 20 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(♯‘𝑥) ∈
ℕ0) |
22 | | xrge0mulgnn0 30875 |
. . . . 5
⊢
(((♯‘𝑥)
∈ ℕ0 ∧ 𝐵 ∈ (0[,]+∞)) →
((♯‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵) =
((♯‘𝑥) ·e
𝐵)) |
23 | 21, 15, 22 | syl2anc 587 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((♯‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵) =
((♯‘𝑥) ·e
𝐵)) |
24 | 19, 23 | eqtrd 2773 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = ((♯‘𝑥) ·e 𝐵)) |
25 | 5, 1, 6, 7, 24 | esumval 31584 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)), ℝ*, <
)) |
26 | | nn0ssre 11981 |
. . . . . . . . . 10
⊢
ℕ0 ⊆ ℝ |
27 | | ressxr 10764 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ* |
28 | 26, 27 | sstri 3887 |
. . . . . . . . 9
⊢
ℕ0 ⊆ ℝ* |
29 | | pnfxr 10774 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
30 | | snssi 4697 |
. . . . . . . . . 10
⊢ (+∞
∈ ℝ* → {+∞} ⊆
ℝ*) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
⊢
{+∞} ⊆ ℝ* |
32 | 28, 31 | unssi 4076 |
. . . . . . . 8
⊢
(ℕ0 ∪ {+∞}) ⊆
ℝ* |
33 | | hashf 13791 |
. . . . . . . . 9
⊢
♯:V⟶(ℕ0 ∪ {+∞}) |
34 | | vex 3402 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
35 | | ffvelrn 6860 |
. . . . . . . . 9
⊢
((♯:V⟶(ℕ0 ∪ {+∞}) ∧ 𝑥 ∈ V) →
(♯‘𝑥) ∈
(ℕ0 ∪ {+∞})) |
36 | 33, 34, 35 | mp2an 692 |
. . . . . . . 8
⊢
(♯‘𝑥)
∈ (ℕ0 ∪ {+∞}) |
37 | 32, 36 | sselii 3875 |
. . . . . . 7
⊢
(♯‘𝑥)
∈ ℝ* |
38 | 37 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(♯‘𝑥) ∈
ℝ*) |
39 | | iccssxr 12905 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
40 | | simpr 488 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → 𝐵 ∈
(0[,]+∞)) |
41 | 39, 40 | sseldi 3876 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → 𝐵 ∈
ℝ*) |
42 | 41 | adantr 484 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐵 ∈
ℝ*) |
43 | 38, 42 | xmulcld 12779 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((♯‘𝑥)
·e 𝐵)
∈ ℝ*) |
44 | 43 | fmpttd 6890 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵)):(𝒫 𝐴 ∩
Fin)⟶ℝ*) |
45 | 44 | frnd 6513 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))
⊆ ℝ*) |
46 | | hashxrcl 13811 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ∈
ℝ*) |
47 | 46 | adantr 484 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
(♯‘𝐴) ∈
ℝ*) |
48 | 47, 41 | xmulcld 12779 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
((♯‘𝐴)
·e 𝐵)
∈ ℝ*) |
49 | | vex 3402 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
50 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵)) =
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵)) |
51 | 50 | elrnmpt 5800 |
. . . . . . . 8
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((♯‘𝑥) ·e 𝐵))) |
52 | 49, 51 | ax-mp 5 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((♯‘𝑥) ·e 𝐵)) |
53 | 52 | biimpi 219 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((♯‘𝑥) ·e 𝐵)) |
54 | 47 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(♯‘𝐴) ∈
ℝ*) |
55 | | 0xr 10767 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
56 | 55 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈
ℝ*) |
57 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → +∞
∈ ℝ*) |
58 | | iccgelb 12878 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐵 ∈ (0[,]+∞))
→ 0 ≤ 𝐵) |
59 | 56, 57, 15, 58 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ≤ 𝐵) |
60 | 42, 59 | jca 515 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐵 ∈ ℝ*
∧ 0 ≤ 𝐵)) |
61 | 6 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐴 ∈ 𝑉) |
62 | | inss1 4120 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 |
63 | 62 | sseli 3874 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) |
64 | | elpwi 4498 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
65 | 13, 63, 64 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ⊆ 𝐴) |
66 | | ssdomg 8602 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑥 ⊆ 𝐴 → 𝑥 ≼ 𝐴)) |
67 | 61, 65, 66 | sylc 65 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ≼ 𝐴) |
68 | | hashdomi 13834 |
. . . . . . . . 9
⊢ (𝑥 ≼ 𝐴 → (♯‘𝑥) ≤ (♯‘𝐴)) |
69 | 67, 68 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(♯‘𝑥) ≤
(♯‘𝐴)) |
70 | | xlemul1a 12765 |
. . . . . . . 8
⊢
((((♯‘𝑥)
∈ ℝ* ∧ (♯‘𝐴) ∈ ℝ* ∧ (𝐵 ∈ ℝ*
∧ 0 ≤ 𝐵)) ∧
(♯‘𝑥) ≤
(♯‘𝐴)) →
((♯‘𝑥)
·e 𝐵)
≤ ((♯‘𝐴)
·e 𝐵)) |
71 | 38, 54, 60, 69, 70 | syl31anc 1374 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((♯‘𝑥)
·e 𝐵)
≤ ((♯‘𝐴)
·e 𝐵)) |
72 | 71 | ralrimiva 3096 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵)) |
73 | | r19.29r 3168 |
. . . . . 6
⊢
((∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)𝑦 =
((♯‘𝑥)
·e 𝐵)
∧ ∀𝑥 ∈
(𝒫 𝐴 ∩
Fin)((♯‘𝑥)
·e 𝐵)
≤ ((♯‘𝐴)
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)(𝑦 =
((♯‘𝑥)
·e 𝐵)
∧ ((♯‘𝑥)
·e 𝐵)
≤ ((♯‘𝐴)
·e 𝐵))) |
74 | 53, 72, 73 | syl2anr 600 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((♯‘𝑥) ·e 𝐵) ∧ ((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵))) |
75 | | simpl 486 |
. . . . . . 7
⊢ ((𝑦 = ((♯‘𝑥) ·e 𝐵) ∧ ((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵)) → 𝑦 = ((♯‘𝑥) ·e 𝐵)) |
76 | | simpr 488 |
. . . . . . 7
⊢ ((𝑦 = ((♯‘𝑥) ·e 𝐵) ∧ ((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵)) → ((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵)) |
77 | 75, 76 | eqbrtrd 5053 |
. . . . . 6
⊢ ((𝑦 = ((♯‘𝑥) ·e 𝐵) ∧ ((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵)) → 𝑦 ≤ ((♯‘𝐴) ·e 𝐵)) |
78 | 77 | rexlimivw 3192 |
. . . . 5
⊢
(∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)(𝑦 =
((♯‘𝑥)
·e 𝐵)
∧ ((♯‘𝑥)
·e 𝐵)
≤ ((♯‘𝐴)
·e 𝐵))
→ 𝑦 ≤
((♯‘𝐴)
·e 𝐵)) |
79 | 74, 78 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))) → 𝑦 ≤ ((♯‘𝐴) ·e 𝐵)) |
80 | 79 | ralrimiva 3096 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ∀𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 ≤ ((♯‘𝐴) ·e 𝐵)) |
81 | | pwidg 4511 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Fin → 𝐴 ∈ 𝒫 𝐴) |
82 | 81 | ancri 553 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin)) |
83 | | elin 3860 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin)) |
84 | 82, 83 | sylibr 237 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin → 𝐴 ∈ (𝒫 𝐴 ∩ Fin)) |
85 | | eqid 2738 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
·e 𝐵) =
((♯‘𝐴)
·e 𝐵) |
86 | | fveq2 6675 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴)) |
87 | 86 | oveq1d 7186 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → ((♯‘𝑥) ·e 𝐵) = ((♯‘𝐴) ·e 𝐵)) |
88 | 87 | rspceeqv 3542 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝒫 𝐴 ∩ Fin) ∧
((♯‘𝐴)
·e 𝐵) =
((♯‘𝐴)
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((♯‘𝐴)
·e 𝐵) =
((♯‘𝑥)
·e 𝐵)) |
89 | 85, 88 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝒫 𝐴 ∩ Fin) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((♯‘𝐴) ·e 𝐵) = ((♯‘𝑥) ·e 𝐵)) |
90 | | ovex 7204 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
·e 𝐵)
∈ V |
91 | 50 | elrnmpt 5800 |
. . . . . . . . . . 11
⊢
(((♯‘𝐴)
·e 𝐵)
∈ V → (((♯‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((♯‘𝐴) ·e 𝐵) = ((♯‘𝑥) ·e 𝐵))) |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((♯‘𝐴)
·e 𝐵) =
((♯‘𝑥)
·e 𝐵)) |
93 | 89, 92 | sylibr 237 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝒫 𝐴 ∩ Fin) →
((♯‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))) |
94 | 84, 93 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin →
((♯‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))) |
95 | 94 | adantl 485 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → ((♯‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))) |
96 | | simplr 769 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → 𝑦 < ((♯‘𝐴) ·e 𝐵)) |
97 | | breq2 5035 |
. . . . . . . 8
⊢ (𝑧 = ((♯‘𝐴) ·e 𝐵) → (𝑦 < 𝑧 ↔ 𝑦 < ((♯‘𝐴) ·e 𝐵))) |
98 | 97 | rspcev 3527 |
. . . . . . 7
⊢
((((♯‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
∧ 𝑦 <
((♯‘𝐴)
·e 𝐵))
→ ∃𝑧 ∈ ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
99 | 95, 96, 98 | syl2anc 587 |
. . . . . 6
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
100 | | 0elpw 5223 |
. . . . . . . . . . . 12
⊢ ∅
∈ 𝒫 𝐴 |
101 | | 0fin 8771 |
. . . . . . . . . . . 12
⊢ ∅
∈ Fin |
102 | | elin 3860 |
. . . . . . . . . . . 12
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ∈ 𝒫 𝐴 ∧ ∅ ∈ Fin)) |
103 | 100, 101,
102 | mpbir2an 711 |
. . . . . . . . . . 11
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) |
104 | 103 | a1i 11 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∅ ∈ (𝒫 𝐴 ∩ Fin)) |
105 | | simpr 488 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝐵 = 0) |
106 | 105 | oveq2d 7187 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((♯‘∅)
·e 𝐵) =
((♯‘∅) ·e 0)) |
107 | | hash0 13821 |
. . . . . . . . . . . . 13
⊢
(♯‘∅) = 0 |
108 | 107, 55 | eqeltri 2829 |
. . . . . . . . . . . 12
⊢
(♯‘∅) ∈ ℝ* |
109 | | xmul01 12744 |
. . . . . . . . . . . 12
⊢
((♯‘∅) ∈ ℝ* →
((♯‘∅) ·e 0) = 0) |
110 | 108, 109 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((♯‘∅) ·e 0) = 0 |
111 | 106, 110 | eqtr2di 2790 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 0 = ((♯‘∅)
·e 𝐵)) |
112 | | fveq2 6675 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
113 | 112 | oveq1d 7186 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ →
((♯‘𝑥)
·e 𝐵) =
((♯‘∅) ·e 𝐵)) |
114 | 113 | rspceeqv 3542 |
. . . . . . . . . 10
⊢ ((∅
∈ (𝒫 𝐴 ∩
Fin) ∧ 0 = ((♯‘∅) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)0 = ((♯‘𝑥) ·e 𝐵)) |
115 | 104, 111,
114 | syl2anc 587 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)0 = ((♯‘𝑥) ·e 𝐵)) |
116 | | ovex 7204 |
. . . . . . . . . 10
⊢
((♯‘𝑥)
·e 𝐵)
∈ V |
117 | 50, 116 | elrnmpti 5804 |
. . . . . . . . 9
⊢ (0 ∈
ran (𝑥 ∈ (𝒫
𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩ Fin)0 =
((♯‘𝑥)
·e 𝐵)) |
118 | 115, 117 | sylibr 237 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 0 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))) |
119 | | simpllr 776 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝑦 < ((♯‘𝐴) ·e 𝐵)) |
120 | 105 | oveq2d 7187 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((♯‘𝐴) ·e 𝐵) = ((♯‘𝐴) ·e
0)) |
121 | 47 | ad4antr 732 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → (♯‘𝐴) ∈
ℝ*) |
122 | | xmul01 12744 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℝ* → ((♯‘𝐴) ·e 0) =
0) |
123 | 121, 122 | syl 17 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((♯‘𝐴) ·e 0) =
0) |
124 | 120, 123 | eqtrd 2773 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((♯‘𝐴) ·e 𝐵) = 0) |
125 | 119, 124 | breqtrd 5057 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝑦 < 0) |
126 | | breq2 5035 |
. . . . . . . . 9
⊢ (𝑧 = 0 → (𝑦 < 𝑧 ↔ 𝑦 < 0)) |
127 | 126 | rspcev 3527 |
. . . . . . . 8
⊢ ((0
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
∧ 𝑦 < 0) →
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
128 | 118, 125,
127 | syl2anc 587 |
. . . . . . 7
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
129 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑎 ∈ 𝒫 𝐴) |
130 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → (♯‘𝑎) = 𝑛) |
131 | | simp-4r 784 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑛 ∈ ℕ) |
132 | 130, 131 | eqeltrd 2833 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → (♯‘𝑎) ∈ ℕ) |
133 | | nnnn0 11984 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑎)
∈ ℕ → (♯‘𝑎) ∈
ℕ0) |
134 | | vex 3402 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑎 ∈ V |
135 | | hashclb 13812 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ V → (𝑎 ∈ Fin ↔
(♯‘𝑎) ∈
ℕ0)) |
136 | 134, 135 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ Fin ↔
(♯‘𝑎) ∈
ℕ0) |
137 | 133, 136 | sylibr 237 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑎)
∈ ℕ → 𝑎
∈ Fin) |
138 | 132, 137 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑎 ∈ Fin) |
139 | 129, 138 | elind 4085 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) |
140 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ((♯‘𝑎) ·e 𝐵) = ((♯‘𝑎) ·e 𝐵)) |
141 | | fveq2 6675 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (♯‘𝑥) = (♯‘𝑎)) |
142 | 141 | oveq1d 7186 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → ((♯‘𝑥) ·e 𝐵) = ((♯‘𝑎) ·e 𝐵)) |
143 | 142 | rspceeqv 3542 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧
((♯‘𝑎)
·e 𝐵) =
((♯‘𝑎)
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((♯‘𝑎)
·e 𝐵) =
((♯‘𝑥)
·e 𝐵)) |
144 | 139, 140,
143 | syl2anc 587 |
. . . . . . . . . . . 12
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((♯‘𝑎) ·e 𝐵) = ((♯‘𝑥) ·e 𝐵)) |
145 | 50, 116 | elrnmpti 5804 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑎)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((♯‘𝑎)
·e 𝐵) =
((♯‘𝑥)
·e 𝐵)) |
146 | 144, 145 | sylibr 237 |
. . . . . . . . . . 11
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ((♯‘𝑎) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))) |
147 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → (𝑦 / 𝐵) < 𝑛) |
148 | | simp-8r 792 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑦 ∈ ℝ) |
149 | 131 | nnred 11732 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑛 ∈ ℝ) |
150 | | simp-5r 786 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝐵 ∈
ℝ+) |
151 | 148, 149,
150 | ltdivmul2d 12567 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ((𝑦 / 𝐵) < 𝑛 ↔ 𝑦 < (𝑛 · 𝐵))) |
152 | 147, 151 | mpbid 235 |
. . . . . . . . . . . 12
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑦 < (𝑛 · 𝐵)) |
153 | 130 | oveq1d 7186 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ((♯‘𝑎) ·e 𝐵) = (𝑛 ·e 𝐵)) |
154 | 150 | rpred 12515 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝐵 ∈ ℝ) |
155 | | rexmul 12748 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑛 ·e 𝐵) = (𝑛 · 𝐵)) |
156 | 149, 154,
155 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → (𝑛 ·e 𝐵) = (𝑛 · 𝐵)) |
157 | 153, 156 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ((♯‘𝑎) ·e 𝐵) = (𝑛 · 𝐵)) |
158 | 152, 157 | breqtrrd 5059 |
. . . . . . . . . . 11
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑦 < ((♯‘𝑎) ·e 𝐵)) |
159 | | breq2 5035 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((♯‘𝑎) ·e 𝐵) → (𝑦 < 𝑧 ↔ 𝑦 < ((♯‘𝑎) ·e 𝐵))) |
160 | 159 | rspcev 3527 |
. . . . . . . . . . 11
⊢
((((♯‘𝑎)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
∧ 𝑦 <
((♯‘𝑎)
·e 𝐵))
→ ∃𝑧 ∈ ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
161 | 146, 158,
160 | syl2anc 587 |
. . . . . . . . . 10
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
162 | 161 | rexlimdva2 3197 |
. . . . . . . . 9
⊢
((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) → (∃𝑎 ∈ 𝒫 𝐴(♯‘𝑎) = 𝑛 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧)) |
163 | 162 | impr 458 |
. . . . . . . 8
⊢
((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ ((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(♯‘𝑎) = 𝑛)) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
164 | | simp-4r 784 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → 𝑦 ∈
ℝ) |
165 | | simpr 488 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → 𝐵 ∈
ℝ+) |
166 | 164, 165 | rerpdivcld 12546 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → (𝑦 / 𝐵) ∈ ℝ) |
167 | | arch 11974 |
. . . . . . . . . 10
⊢ ((𝑦 / 𝐵) ∈ ℝ → ∃𝑛 ∈ ℕ (𝑦 / 𝐵) < 𝑛) |
168 | 166, 167 | syl 17 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∃𝑛 ∈ ℕ
(𝑦 / 𝐵) < 𝑛) |
169 | | ishashinf 13916 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ Fin →
∀𝑛 ∈ ℕ
∃𝑎 ∈ 𝒫
𝐴(♯‘𝑎) = 𝑛) |
170 | 169 | ad2antlr 727 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∀𝑛 ∈ ℕ
∃𝑎 ∈ 𝒫
𝐴(♯‘𝑎) = 𝑛) |
171 | | r19.29r 3168 |
. . . . . . . . 9
⊢
((∃𝑛 ∈
ℕ (𝑦 / 𝐵) < 𝑛 ∧ ∀𝑛 ∈ ℕ ∃𝑎 ∈ 𝒫 𝐴(♯‘𝑎) = 𝑛) → ∃𝑛 ∈ ℕ ((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(♯‘𝑎) = 𝑛)) |
172 | 168, 170,
171 | syl2anc 587 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∃𝑛 ∈ ℕ
((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(♯‘𝑎) = 𝑛)) |
173 | 163, 172 | r19.29a 3199 |
. . . . . . 7
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
174 | | nfielex 8825 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ∈ Fin →
∃𝑙 𝑙 ∈ 𝐴) |
175 | 174 | adantr 484 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) → ∃𝑙 𝑙 ∈ 𝐴) |
176 | | snelpwi 5304 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ 𝐴 → {𝑙} ∈ 𝒫 𝐴) |
177 | | snfi 8643 |
. . . . . . . . . . . . . . 15
⊢ {𝑙} ∈ Fin |
178 | 176, 177 | jctir 524 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ 𝐴 → ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin)) |
179 | | elin 3860 |
. . . . . . . . . . . . . 14
⊢ ({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ↔ ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin)) |
180 | 178, 179 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ 𝐴 → {𝑙} ∈ (𝒫 𝐴 ∩ Fin)) |
181 | 180 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → {𝑙} ∈ (𝒫 𝐴 ∩ Fin)) |
182 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → 𝐵 = +∞) |
183 | 182 | oveq2d 7187 |
. . . . . . . . . . . . 13
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → ((♯‘{𝑙}) ·e 𝐵) = ((♯‘{𝑙}) ·e
+∞)) |
184 | | hashsng 13823 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ 𝐴 → (♯‘{𝑙}) = 1) |
185 | | 1re 10720 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ |
186 | 27, 185 | sselii 3875 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ* |
187 | 184, 186 | eqeltrdi 2841 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ 𝐴 → (♯‘{𝑙}) ∈
ℝ*) |
188 | | 0lt1 11241 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
1 |
189 | 188, 184 | breqtrrid 5069 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ 𝐴 → 0 < (♯‘{𝑙})) |
190 | | xmulpnf1 12751 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘{𝑙}) ∈ ℝ* ∧ 0 <
(♯‘{𝑙})) →
((♯‘{𝑙})
·e +∞) = +∞) |
191 | 187, 189,
190 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ 𝐴 → ((♯‘{𝑙}) ·e +∞) =
+∞) |
192 | 191 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → ((♯‘{𝑙}) ·e +∞) =
+∞) |
193 | 183, 192 | eqtr2d 2774 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → +∞ = ((♯‘{𝑙}) ·e 𝐵)) |
194 | | fveq2 6675 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = {𝑙} → (♯‘𝑥) = (♯‘{𝑙})) |
195 | 194 | oveq1d 7186 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {𝑙} → ((♯‘𝑥) ·e 𝐵) = ((♯‘{𝑙}) ·e 𝐵)) |
196 | 195 | rspceeqv 3542 |
. . . . . . . . . . . 12
⊢ (({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ∧ +∞ =
((♯‘{𝑙})
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)+∞ = ((♯‘𝑥) ·e 𝐵)) |
197 | 181, 193,
196 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((♯‘𝑥) ·e 𝐵)) |
198 | 175, 197 | exlimddv 1941 |
. . . . . . . . . 10
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ =
((♯‘𝑥)
·e 𝐵)) |
199 | 198 | adantll 714 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ =
((♯‘𝑥)
·e 𝐵)) |
200 | 50, 116 | elrnmpti 5804 |
. . . . . . . . 9
⊢ (+∞
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)+∞ = ((♯‘𝑥) ·e 𝐵)) |
201 | 199, 200 | sylibr 237 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))) |
202 | | simp-4r 784 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → 𝑦 ∈ ℝ) |
203 | | ltpnf 12599 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → 𝑦 < +∞) |
204 | 202, 203 | syl 17 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → 𝑦 < +∞) |
205 | | breq2 5035 |
. . . . . . . . 9
⊢ (𝑧 = +∞ → (𝑦 < 𝑧 ↔ 𝑦 < +∞)) |
206 | 205 | rspcev 3527 |
. . . . . . . 8
⊢
((+∞ ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)) ∧ 𝑦 < +∞) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
207 | 201, 204,
206 | syl2anc 587 |
. . . . . . 7
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
208 | | simp-4r 784 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → 𝐵 ∈ (0[,]+∞)) |
209 | | elxrge02 30781 |
. . . . . . . 8
⊢ (𝐵 ∈ (0[,]+∞) ↔
(𝐵 = 0 ∨ 𝐵 ∈ ℝ+ ∨
𝐵 =
+∞)) |
210 | 208, 209 | sylib 221 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → (𝐵 = 0 ∨ 𝐵 ∈ ℝ+ ∨ 𝐵 = +∞)) |
211 | 128, 173,
207, 210 | mpjao3dan 1432 |
. . . . . 6
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
212 | 99, 211 | pm2.61dan 813 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
213 | 212 | ex 416 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) → (𝑦 < ((♯‘𝐴) ·e 𝐵) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧)) |
214 | 213 | ralrimiva 3096 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ∀𝑦 ∈ ℝ (𝑦 < ((♯‘𝐴) ·e 𝐵) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧)) |
215 | | supxr2 12791 |
. . 3
⊢ (((ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))
⊆ ℝ* ∧ ((♯‘𝐴) ·e 𝐵) ∈ ℝ*) ∧
(∀𝑦 ∈ ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))𝑦 ≤ ((♯‘𝐴) ·e 𝐵) ∧ ∀𝑦 ∈ ℝ (𝑦 < ((♯‘𝐴) ·e 𝐵) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧))) → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)), ℝ*, < )
= ((♯‘𝐴)
·e 𝐵)) |
216 | 45, 48, 80, 214, 215 | syl22anc 838 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → sup(ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵)),
ℝ*, < ) = ((♯‘𝐴) ·e 𝐵)) |
217 | 25, 216 | eqtrd 2773 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
𝐴𝐵 = ((♯‘𝐴) ·e 𝐵)) |