Step | Hyp | Ref
| Expression |
1 | | esumcst.1 |
. . . . 5
⊢
Ⅎ𝑘𝐴 |
2 | 1 | nfel1 2765 |
. . . 4
⊢
Ⅎ𝑘 𝐴 ∈ 𝑉 |
3 | | esumcst.2 |
. . . . 5
⊢
Ⅎ𝑘𝐵 |
4 | 3 | nfel1 2765 |
. . . 4
⊢
Ⅎ𝑘 𝐵 ∈
(0[,]+∞) |
5 | 2, 4 | nfan 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) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ Mnd |
11 | 10 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ Mnd) |
12 | | inss2 3796 |
. . . . . 6
⊢
(𝒫 𝐴 ∩
Fin) ⊆ Fin |
13 | | simpr 476 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) |
14 | 12, 13 | sseldi 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[,]+∞))) |
18 | 3, 16, 17 | gsumconstf 18158 |
. . . . 5
⊢
(((ℝ*𝑠 ↾s
(0[,]+∞)) ∈ Mnd ∧ 𝑥 ∈ Fin ∧ 𝐵 ∈ (0[,]+∞)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = ((#‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵)) |
19 | 11, 14, 15, 18 | syl3anc 1318 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = ((#‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵)) |
20 | | hashcl 13009 |
. . . . . 6
⊢ (𝑥 ∈ Fin →
(#‘𝑥) ∈
ℕ0) |
21 | 14, 20 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(#‘𝑥) ∈
ℕ0) |
22 | | xrge0mulgnn0 29020 |
. . . . 5
⊢
(((#‘𝑥) ∈
ℕ0 ∧ 𝐵
∈ (0[,]+∞)) → ((#‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵) =
((#‘𝑥) ·e 𝐵)) |
23 | 21, 15, 22 | syl2anc 691 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((#‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵) =
((#‘𝑥) ·e 𝐵)) |
24 | 19, 23 | eqtrd 2644 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = ((#‘𝑥) ·e 𝐵)) |
25 | 5, 1, 6, 7, 24 | esumval 29435 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)), ℝ*, <
)) |
26 | | nn0ssre 11173 |
. . . . . . . . . 10
⊢
ℕ0 ⊆ ℝ |
27 | | ressxr 9962 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ* |
28 | 26, 27 | sstri 3577 |
. . . . . . . . 9
⊢
ℕ0 ⊆ ℝ* |
29 | | pnfxr 9971 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
30 | | snssi 4280 |
. . . . . . . . . 10
⊢ (+∞
∈ ℝ* → {+∞} ⊆
ℝ*) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
⊢
{+∞} ⊆ ℝ* |
32 | 28, 31 | unssi 3750 |
. . . . . . . 8
⊢
(ℕ0 ∪ {+∞}) ⊆
ℝ* |
33 | | hashf 12987 |
. . . . . . . . 9
⊢
#:V⟶(ℕ0 ∪ {+∞}) |
34 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
35 | | ffvelrn 6265 |
. . . . . . . . 9
⊢
((#:V⟶(ℕ0 ∪ {+∞}) ∧ 𝑥 ∈ V) → (#‘𝑥) ∈ (ℕ0
∪ {+∞})) |
36 | 33, 34, 35 | mp2an 704 |
. . . . . . . 8
⊢
(#‘𝑥) ∈
(ℕ0 ∪ {+∞}) |
37 | 32, 36 | sselii 3565 |
. . . . . . 7
⊢
(#‘𝑥) ∈
ℝ* |
38 | 37 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(#‘𝑥) ∈
ℝ*) |
39 | | iccssxr 12127 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
40 | | simpr 476 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → 𝐵 ∈
(0[,]+∞)) |
41 | 39, 40 | sseldi 3566 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → 𝐵 ∈
ℝ*) |
42 | 41 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐵 ∈
ℝ*) |
43 | 38, 42 | xmulcld 12004 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((#‘𝑥)
·e 𝐵)
∈ ℝ*) |
44 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵)) =
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵)) |
45 | 43, 44 | fmptd 6292 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵)):(𝒫 𝐴 ∩
Fin)⟶ℝ*) |
46 | | frn 5966 |
. . . 4
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵)):(𝒫 𝐴 ∩ Fin)⟶ℝ*
→ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((#‘𝑥)
·e 𝐵))
⊆ ℝ*) |
47 | 45, 46 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵))
⊆ ℝ*) |
48 | | hashxrcl 13010 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (#‘𝐴) ∈
ℝ*) |
49 | 48 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
(#‘𝐴) ∈
ℝ*) |
50 | 49, 41 | xmulcld 12004 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
((#‘𝐴)
·e 𝐵)
∈ ℝ*) |
51 | | vex 3176 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
52 | 44 | elrnmpt 5293 |
. . . . . . . 8
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((#‘𝑥) ·e 𝐵))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((#‘𝑥) ·e 𝐵)) |
54 | 53 | biimpi 205 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((#‘𝑥) ·e 𝐵)) |
55 | 49 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(#‘𝐴) ∈
ℝ*) |
56 | | 0xr 9965 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
57 | 56 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈
ℝ*) |
58 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → +∞
∈ ℝ*) |
59 | | iccgelb 12101 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐵 ∈ (0[,]+∞))
→ 0 ≤ 𝐵) |
60 | 57, 58, 15, 59 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ≤ 𝐵) |
61 | 42, 60 | jca 553 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐵 ∈ ℝ*
∧ 0 ≤ 𝐵)) |
62 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐴 ∈ 𝑉) |
63 | | inss1 3795 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 |
64 | 63 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) |
65 | | elpwi 4117 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
66 | 13, 64, 65 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ⊆ 𝐴) |
67 | | ssdomg 7887 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑥 ⊆ 𝐴 → 𝑥 ≼ 𝐴)) |
68 | 62, 66, 67 | sylc 63 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ≼ 𝐴) |
69 | | hashdomi 13030 |
. . . . . . . . 9
⊢ (𝑥 ≼ 𝐴 → (#‘𝑥) ≤ (#‘𝐴)) |
70 | 68, 69 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(#‘𝑥) ≤
(#‘𝐴)) |
71 | | xlemul1a 11990 |
. . . . . . . 8
⊢
((((#‘𝑥)
∈ ℝ* ∧ (#‘𝐴) ∈ ℝ* ∧ (𝐵 ∈ ℝ*
∧ 0 ≤ 𝐵)) ∧
(#‘𝑥) ≤
(#‘𝐴)) →
((#‘𝑥)
·e 𝐵)
≤ ((#‘𝐴)
·e 𝐵)) |
72 | 38, 55, 61, 70, 71 | syl31anc 1321 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((#‘𝑥)
·e 𝐵)
≤ ((#‘𝐴)
·e 𝐵)) |
73 | 72 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)) |
74 | | r19.29r 3055 |
. . . . . 6
⊢
((∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵))) |
75 | 54, 73, 74 | syl2anr 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 𝐵)) |
78 | 76, 77 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)) → 𝑦 ≤ ((#‘𝐴) ·e 𝐵)) |
79 | 78 | rexlimivw 3011 |
. . . . 5
⊢
(∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)(𝑦 = ((#‘𝑥) ·e 𝐵) ∧ ((#‘𝑥) ·e 𝐵) ≤ ((#‘𝐴) ·e 𝐵)) → 𝑦 ≤ ((#‘𝐴) ·e 𝐵)) |
80 | 75, 79 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))) → 𝑦 ≤ ((#‘𝐴) ·e 𝐵)) |
81 | 80 | ralrimiva 2949 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ∀𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 ≤ ((#‘𝐴) ·e 𝐵)) |
82 | | pwidg 4121 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Fin → 𝐴 ∈ 𝒫 𝐴) |
83 | 82 | ancri 573 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin)) |
84 | | elin 3758 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin)) |
85 | 83, 84 | sylibr 223 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin → 𝐴 ∈ (𝒫 𝐴 ∩ Fin)) |
86 | | eqid 2610 |
. . . . . . . . . . 11
⊢
((#‘𝐴)
·e 𝐵) =
((#‘𝐴)
·e 𝐵) |
87 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → (#‘𝑥) = (#‘𝐴)) |
88 | 87 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → ((#‘𝑥) ·e 𝐵) = ((#‘𝐴) ·e 𝐵)) |
89 | 88 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (((#‘𝐴) ·e 𝐵) = ((#‘𝑥) ·e 𝐵) ↔ ((#‘𝐴) ·e 𝐵) = ((#‘𝐴) ·e 𝐵))) |
90 | 89 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝒫 𝐴 ∩ Fin) ∧
((#‘𝐴)
·e 𝐵) =
((#‘𝐴)
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((#‘𝐴)
·e 𝐵) =
((#‘𝑥)
·e 𝐵)) |
91 | 86, 90 | mpan2 703 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝒫 𝐴 ∩ Fin) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝐴) ·e 𝐵) = ((#‘𝑥) ·e 𝐵)) |
92 | | ovex 6577 |
. . . . . . . . . . 11
⊢
((#‘𝐴)
·e 𝐵)
∈ V |
93 | 44 | elrnmpt 5293 |
. . . . . . . . . . 11
⊢
(((#‘𝐴)
·e 𝐵)
∈ V → (((#‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝐴) ·e 𝐵) = ((#‘𝑥) ·e 𝐵))) |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . 10
⊢
(((#‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((#‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((#‘𝐴)
·e 𝐵) =
((#‘𝑥)
·e 𝐵)) |
95 | 91, 94 | sylibr 223 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝒫 𝐴 ∩ Fin) →
((#‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((#‘𝑥)
·e 𝐵))) |
96 | 85, 95 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin →
((#‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((#‘𝑥)
·e 𝐵))) |
97 | 96 | adantl 481 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → ((#‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))) |
98 | | simplr 788 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → 𝑦 < ((#‘𝐴) ·e 𝐵)) |
99 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑧 = ((#‘𝐴) ·e 𝐵) → (𝑦 < 𝑧 ↔ 𝑦 < ((#‘𝐴) ·e 𝐵))) |
100 | 99 | rspcev 3282 |
. . . . . . 7
⊢
((((#‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((#‘𝑥)
·e 𝐵))
∧ 𝑦 <
((#‘𝐴)
·e 𝐵))
→ ∃𝑧 ∈ ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
101 | 97, 98, 100 | syl2anc 691 |
. . . . . 6
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
102 | | 0elpw 4760 |
. . . . . . . . . . . 12
⊢ ∅
∈ 𝒫 𝐴 |
103 | | 0fin 8073 |
. . . . . . . . . . . 12
⊢ ∅
∈ Fin |
104 | | elin 3758 |
. . . . . . . . . . . 12
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ∈ 𝒫 𝐴 ∧ ∅ ∈ Fin)) |
105 | 102, 103,
104 | mpbir2an 957 |
. . . . . . . . . . 11
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) |
106 | 105 | a1i 11 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∅ ∈ (𝒫 𝐴 ∩ Fin)) |
107 | | simpr 476 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝐵 = 0) |
108 | 107 | oveq2d 6565 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((#‘∅)
·e 𝐵) =
((#‘∅) ·e 0)) |
109 | | hash0 13019 |
. . . . . . . . . . . . 13
⊢
(#‘∅) = 0 |
110 | 109, 56 | eqeltri 2684 |
. . . . . . . . . . . 12
⊢
(#‘∅) ∈ ℝ* |
111 | | xmul01 11969 |
. . . . . . . . . . . 12
⊢
((#‘∅) ∈ ℝ* → ((#‘∅)
·e 0) = 0) |
112 | 110, 111 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((#‘∅) ·e 0) = 0 |
113 | 108, 112 | syl6req 2661 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 0 = ((#‘∅)
·e 𝐵)) |
114 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (#‘𝑥) =
(#‘∅)) |
115 | 114 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ →
((#‘𝑥)
·e 𝐵) =
((#‘∅) ·e 𝐵)) |
116 | 115 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (0 =
((#‘𝑥)
·e 𝐵)
↔ 0 = ((#‘∅) ·e 𝐵))) |
117 | 116 | rspcev 3282 |
. . . . . . . . . 10
⊢ ((∅
∈ (𝒫 𝐴 ∩
Fin) ∧ 0 = ((#‘∅) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)0 = ((#‘𝑥) ·e 𝐵)) |
118 | 106, 113,
117 | syl2anc 691 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)0 = ((#‘𝑥) ·e 𝐵)) |
119 | | ovex 6577 |
. . . . . . . . . 10
⊢
((#‘𝑥)
·e 𝐵)
∈ V |
120 | 44, 119 | elrnmpti 5297 |
. . . . . . . . 9
⊢ (0 ∈
ran (𝑥 ∈ (𝒫
𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩ Fin)0 =
((#‘𝑥)
·e 𝐵)) |
121 | 118, 120 | sylibr 223 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 0 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵))) |
122 | | simpllr 795 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝑦 < ((#‘𝐴) ·e 𝐵)) |
123 | 107 | oveq2d 6565 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((#‘𝐴) ·e 𝐵) = ((#‘𝐴) ·e 0)) |
124 | 49 | ad4antr 764 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → (#‘𝐴) ∈
ℝ*) |
125 | | xmul01 11969 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℝ* → ((#‘𝐴) ·e 0) =
0) |
126 | 124, 125 | syl 17 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((#‘𝐴) ·e 0) =
0) |
127 | 123, 126 | eqtrd 2644 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((#‘𝐴) ·e 𝐵) = 0) |
128 | 122, 127 | breqtrd 4609 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝑦 < 0) |
129 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑧 = 0 → (𝑦 < 𝑧 ↔ 𝑦 < 0)) |
130 | 129 | rspcev 3282 |
. . . . . . . 8
⊢ ((0
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((#‘𝑥)
·e 𝐵))
∧ 𝑦 < 0) →
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
131 | 121, 128,
130 | syl2anc 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) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑛 ∈ ℕ) |
135 | 133, 134 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → (#‘𝑎) ∈ ℕ) |
136 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑎) ∈
ℕ → (#‘𝑎)
∈ ℕ0) |
137 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑎 ∈ V |
138 | | hashclb 13011 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ V → (𝑎 ∈ Fin ↔
(#‘𝑎) ∈
ℕ0)) |
139 | 137, 138 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ Fin ↔
(#‘𝑎) ∈
ℕ0) |
140 | 136, 139 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑎) ∈
ℕ → 𝑎 ∈
Fin) |
141 | 135, 140 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑎 ∈ Fin) |
142 | 132, 141 | elind 3760 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) |
143 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ((#‘𝑎) ·e 𝐵) = ((#‘𝑎) ·e 𝐵)) |
144 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (#‘𝑥) = (#‘𝑎)) |
145 | 144 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → ((#‘𝑥) ·e 𝐵) = ((#‘𝑎) ·e 𝐵)) |
146 | 145 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (((#‘𝑎) ·e 𝐵) = ((#‘𝑥) ·e 𝐵) ↔ ((#‘𝑎) ·e 𝐵) = ((#‘𝑎) ·e 𝐵))) |
147 | 146 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧
((#‘𝑎)
·e 𝐵) =
((#‘𝑎)
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((#‘𝑎)
·e 𝐵) =
((#‘𝑥)
·e 𝐵)) |
148 | 142, 143,
147 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((#‘𝑎) ·e 𝐵) = ((#‘𝑥) ·e 𝐵)) |
149 | 44, 119 | elrnmpti 5297 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑎)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((#‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((#‘𝑎)
·e 𝐵) =
((#‘𝑥)
·e 𝐵)) |
150 | 148, 149 | sylibr 223 |
. . . . . . . . . . . 12
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ((#‘𝑎) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))) |
151 | | simpllr 795 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → (𝑦 / 𝐵) < 𝑛) |
152 | | simp-8r 811 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑦 ∈ ℝ) |
153 | 134 | nnred 10912 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑛 ∈ ℝ) |
154 | | simp-5r 805 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝐵 ∈
ℝ+) |
155 | 152, 153,
154 | ltdivmul2d 11800 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ((𝑦 / 𝐵) < 𝑛 ↔ 𝑦 < (𝑛 · 𝐵))) |
156 | 151, 155 | mpbid 221 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑦 < (𝑛 · 𝐵)) |
157 | 133 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ((#‘𝑎) ·e 𝐵) = (𝑛 ·e 𝐵)) |
158 | 154 | rpred 11748 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝐵 ∈ ℝ) |
159 | | rexmul 11973 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑛 ·e 𝐵) = (𝑛 · 𝐵)) |
160 | 153, 158,
159 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → (𝑛 ·e 𝐵) = (𝑛 · 𝐵)) |
161 | 157, 160 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ((#‘𝑎) ·e 𝐵) = (𝑛 · 𝐵)) |
162 | 156, 161 | breqtrrd 4611 |
. . . . . . . . . . . 12
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → 𝑦 < ((#‘𝑎) ·e 𝐵)) |
163 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((#‘𝑎) ·e 𝐵) → (𝑦 < 𝑧 ↔ 𝑦 < ((#‘𝑎) ·e 𝐵))) |
164 | 163 | rspcev 3282 |
. . . . . . . . . . . 12
⊢
((((#‘𝑎)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((#‘𝑥)
·e 𝐵))
∧ 𝑦 <
((#‘𝑎)
·e 𝐵))
→ ∃𝑧 ∈ ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
165 | 150, 162,
164 | syl2anc 691 |
. . . . . . . . . . 11
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (#‘𝑎) = 𝑛) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
166 | 165 | ex 449 |
. . . . . . . . . 10
⊢
(((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) → ((#‘𝑎) = 𝑛 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)) |
167 | 166 | rexlimdva 3013 |
. . . . . . . . 9
⊢
((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) → (∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)) |
168 | 167 | impr 647 |
. . . . . . . 8
⊢
((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ ((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛)) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
169 | | simp-4r 803 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → 𝑦 ∈
ℝ) |
170 | | simpr 476 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → 𝐵 ∈
ℝ+) |
171 | 169, 170 | rerpdivcld 11779 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → (𝑦 / 𝐵) ∈ ℝ) |
172 | | arch 11166 |
. . . . . . . . . 10
⊢ ((𝑦 / 𝐵) ∈ ℝ → ∃𝑛 ∈ ℕ (𝑦 / 𝐵) < 𝑛) |
173 | 171, 172 | syl 17 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∃𝑛 ∈ ℕ
(𝑦 / 𝐵) < 𝑛) |
174 | | ishashinf 13104 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ Fin →
∀𝑛 ∈ ℕ
∃𝑎 ∈ 𝒫
𝐴(#‘𝑎) = 𝑛) |
175 | 174 | ad2antlr 759 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∀𝑛 ∈ ℕ
∃𝑎 ∈ 𝒫
𝐴(#‘𝑎) = 𝑛) |
176 | | r19.29r 3055 |
. . . . . . . . 9
⊢
((∃𝑛 ∈
ℕ (𝑦 / 𝐵) < 𝑛 ∧ ∀𝑛 ∈ ℕ ∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛) → ∃𝑛 ∈ ℕ ((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛)) |
177 | 173, 175,
176 | syl2anc 691 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∃𝑛 ∈ ℕ
((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(#‘𝑎) = 𝑛)) |
178 | 168, 177 | r19.29a 3060 |
. . . . . . 7
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
179 | | nfielex 8074 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ∈ Fin →
∃𝑙 𝑙 ∈ 𝐴) |
180 | 179 | adantr 480 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) → ∃𝑙 𝑙 ∈ 𝐴) |
181 | | snelpwi 4839 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ 𝐴 → {𝑙} ∈ 𝒫 𝐴) |
182 | | snfi 7923 |
. . . . . . . . . . . . . . 15
⊢ {𝑙} ∈ Fin |
183 | 181, 182 | jctir 559 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ 𝐴 → ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin)) |
184 | | elin 3758 |
. . . . . . . . . . . . . 14
⊢ ({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ↔ ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin)) |
185 | 183, 184 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ 𝐴 → {𝑙} ∈ (𝒫 𝐴 ∩ Fin)) |
186 | 185 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → {𝑙} ∈ (𝒫 𝐴 ∩ Fin)) |
187 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → 𝐵 = +∞) |
188 | 187 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → ((#‘{𝑙}) ·e 𝐵) = ((#‘{𝑙}) ·e
+∞)) |
189 | | hashsng 13020 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ 𝐴 → (#‘{𝑙}) = 1) |
190 | | 1re 9918 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ |
191 | 27, 190 | sselii 3565 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ* |
192 | 189, 191 | syl6eqel 2696 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ 𝐴 → (#‘{𝑙}) ∈
ℝ*) |
193 | | 0lt1 10429 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
1 |
194 | 193, 189 | syl5breqr 4621 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ 𝐴 → 0 < (#‘{𝑙})) |
195 | | xmulpnf1 11976 |
. . . . . . . . . . . . . . 15
⊢
(((#‘{𝑙})
∈ ℝ* ∧ 0 < (#‘{𝑙})) → ((#‘{𝑙}) ·e +∞) =
+∞) |
196 | 192, 194,
195 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ 𝐴 → ((#‘{𝑙}) ·e +∞) =
+∞) |
197 | 196 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → ((#‘{𝑙}) ·e +∞) =
+∞) |
198 | 188, 197 | eqtr2d 2645 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → +∞ = ((#‘{𝑙}) ·e 𝐵)) |
199 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = {𝑙} → (#‘𝑥) = (#‘{𝑙})) |
200 | 199 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = {𝑙} → ((#‘𝑥) ·e 𝐵) = ((#‘{𝑙}) ·e 𝐵)) |
201 | 200 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {𝑙} → (+∞ = ((#‘𝑥) ·e 𝐵) ↔ +∞ =
((#‘{𝑙})
·e 𝐵))) |
202 | 201 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ (({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ∧ +∞ =
((#‘{𝑙})
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)+∞ = ((#‘𝑥)
·e 𝐵)) |
203 | 186, 198,
202 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((#‘𝑥) ·e 𝐵)) |
204 | 180, 203 | exlimddv 1850 |
. . . . . . . . . 10
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ =
((#‘𝑥)
·e 𝐵)) |
205 | 204 | adantll 746 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ =
((#‘𝑥)
·e 𝐵)) |
206 | 44, 119 | elrnmpti 5297 |
. . . . . . . . 9
⊢ (+∞
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((#‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)+∞ = ((#‘𝑥)
·e 𝐵)) |
207 | 205, 206 | sylibr 223 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵))) |
208 | | simp-4r 803 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → 𝑦 ∈ ℝ) |
209 | | ltpnf 11830 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → 𝑦 < +∞) |
210 | 208, 209 | syl 17 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → 𝑦 < +∞) |
211 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑧 = +∞ → (𝑦 < 𝑧 ↔ 𝑦 < +∞)) |
212 | 211 | rspcev 3282 |
. . . . . . . 8
⊢
((+∞ ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵)) ∧ 𝑦 < +∞) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
213 | 207, 210,
212 | syl2anc 691 |
. . . . . . 7
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
214 | | simp-4r 803 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → 𝐵 ∈ (0[,]+∞)) |
215 | | elxrge02 28971 |
. . . . . . . 8
⊢ (𝐵 ∈ (0[,]+∞) ↔
(𝐵 = 0 ∨ 𝐵 ∈ ℝ+ ∨
𝐵 =
+∞)) |
216 | 214, 215 | sylib 207 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → (𝐵 = 0 ∨ 𝐵 ∈ ℝ+ ∨ 𝐵 = +∞)) |
217 | 131, 178,
213, 216 | mpjao3dan 1387 |
. . . . . 6
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
218 | 101, 217 | pm2.61dan 828 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((#‘𝐴) ·e 𝐵)) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
219 | 218 | ex 449 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) → (𝑦 < ((#‘𝐴) ·e 𝐵) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((#‘𝑥) ·e 𝐵))𝑦 < 𝑧)) |
220 | 219 | ralrimiva 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 𝐵)) |
222 | 47, 50, 81, 220, 221 | syl22anc 1319 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → sup(ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((#‘𝑥)
·e 𝐵)),
ℝ*, < ) = ((#‘𝐴) ·e 𝐵)) |
223 | 25, 222 | eqtrd 2644 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
𝐴𝐵 = ((#‘𝐴) ·e 𝐵)) |