| Step | Hyp | Ref
| Expression |
| 1 | | esumcst.1 |
. . . . 5
⊢
Ⅎ𝑘𝐴 |
| 2 | 1 | nfel1 2922 |
. . . 4
⊢
Ⅎ𝑘 𝐴 ∈ 𝑉 |
| 3 | | esumcst.2 |
. . . . 5
⊢
Ⅎ𝑘𝐵 |
| 4 | 3 | nfel1 2922 |
. . . 4
⊢
Ⅎ𝑘 𝐵 ∈
(0[,]+∞) |
| 5 | 2, 4 | nfan 1899 |
. . 3
⊢
Ⅎ𝑘(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) |
| 6 | | simpl 482 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → 𝐴 ∈ 𝑉) |
| 7 | | simplr 769 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
| 8 | | xrge0tmd 33944 |
. . . . . . 7
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ TopMnd |
| 9 | | tmdmnd 24083 |
. . . . . . 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 4238 |
. . . . . 6
⊢
(𝒫 𝐴 ∩
Fin) ⊆ Fin |
| 13 | | simpr 484 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) |
| 14 | 12, 13 | sselid 3981 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin) |
| 15 | | simplr 769 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐵 ∈
(0[,]+∞)) |
| 16 | | xrge0base 33016 |
. . . . . 6
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 17 | | eqid 2737 |
. . . . . 6
⊢
(.g‘(ℝ*𝑠
↾s (0[,]+∞))) =
(.g‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 18 | 3, 16, 17 | gsumconstf 19953 |
. . . . 5
⊢
(((ℝ*𝑠 ↾s
(0[,]+∞)) ∈ Mnd ∧ 𝑥 ∈ Fin ∧ 𝐵 ∈ (0[,]+∞)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = ((♯‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵)) |
| 19 | 11, 14, 15, 18 | syl3anc 1373 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = ((♯‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵)) |
| 20 | | hashcl 14395 |
. . . . . 6
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) |
| 21 | 14, 20 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(♯‘𝑥) ∈
ℕ0) |
| 22 | | xrge0mulgnn0 33020 |
. . . . 5
⊢
(((♯‘𝑥)
∈ ℕ0 ∧ 𝐵 ∈ (0[,]+∞)) →
((♯‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵) =
((♯‘𝑥) ·e
𝐵)) |
| 23 | 21, 15, 22 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((♯‘𝑥)(.g‘(ℝ*𝑠
↾s (0[,]+∞)))𝐵) =
((♯‘𝑥) ·e
𝐵)) |
| 24 | 19, 23 | eqtrd 2777 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = ((♯‘𝑥) ·e 𝐵)) |
| 25 | 5, 1, 6, 7, 24 | esumval 34047 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)), ℝ*, <
)) |
| 26 | | nn0ssre 12530 |
. . . . . . . . . 10
⊢
ℕ0 ⊆ ℝ |
| 27 | | ressxr 11305 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ* |
| 28 | 26, 27 | sstri 3993 |
. . . . . . . . 9
⊢
ℕ0 ⊆ ℝ* |
| 29 | | pnfxr 11315 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
| 30 | | snssi 4808 |
. . . . . . . . . 10
⊢ (+∞
∈ ℝ* → {+∞} ⊆
ℝ*) |
| 31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
⊢
{+∞} ⊆ ℝ* |
| 32 | 28, 31 | unssi 4191 |
. . . . . . . 8
⊢
(ℕ0 ∪ {+∞}) ⊆
ℝ* |
| 33 | | hashf 14377 |
. . . . . . . . 9
⊢
♯:V⟶(ℕ0 ∪ {+∞}) |
| 34 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 35 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢
((♯:V⟶(ℕ0 ∪ {+∞}) ∧ 𝑥 ∈ V) →
(♯‘𝑥) ∈
(ℕ0 ∪ {+∞})) |
| 36 | 33, 34, 35 | mp2an 692 |
. . . . . . . 8
⊢
(♯‘𝑥)
∈ (ℕ0 ∪ {+∞}) |
| 37 | 32, 36 | sselii 3980 |
. . . . . . 7
⊢
(♯‘𝑥)
∈ ℝ* |
| 38 | 37 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(♯‘𝑥) ∈
ℝ*) |
| 39 | | iccssxr 13470 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
| 40 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → 𝐵 ∈
(0[,]+∞)) |
| 41 | 39, 40 | sselid 3981 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → 𝐵 ∈
ℝ*) |
| 42 | 41 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐵 ∈
ℝ*) |
| 43 | 38, 42 | xmulcld 13344 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((♯‘𝑥)
·e 𝐵)
∈ ℝ*) |
| 44 | 43 | fmpttd 7135 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵)):(𝒫 𝐴 ∩
Fin)⟶ℝ*) |
| 45 | 44 | frnd 6744 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))
⊆ ℝ*) |
| 46 | | hashxrcl 14396 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ∈
ℝ*) |
| 47 | 46 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
(♯‘𝐴) ∈
ℝ*) |
| 48 | 47, 41 | xmulcld 13344 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
((♯‘𝐴)
·e 𝐵)
∈ ℝ*) |
| 49 | | vex 3484 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
| 50 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵)) =
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵)) |
| 51 | 50 | elrnmpt 5969 |
. . . . . . . 8
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((♯‘𝑥) ·e 𝐵))) |
| 52 | 49, 51 | ax-mp 5 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((♯‘𝑥) ·e 𝐵)) |
| 53 | 52 | biimpi 216 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((♯‘𝑥) ·e 𝐵)) |
| 54 | 47 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(♯‘𝐴) ∈
ℝ*) |
| 55 | | 0xr 11308 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
| 56 | 55 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈
ℝ*) |
| 57 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → +∞
∈ ℝ*) |
| 58 | | iccgelb 13443 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐵 ∈ (0[,]+∞))
→ 0 ≤ 𝐵) |
| 59 | 56, 57, 15, 58 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ≤ 𝐵) |
| 60 | 42, 59 | jca 511 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐵 ∈ ℝ*
∧ 0 ≤ 𝐵)) |
| 61 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐴 ∈ 𝑉) |
| 62 | | inss1 4237 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 |
| 63 | 62 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) |
| 64 | | elpwi 4607 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
| 65 | 13, 63, 64 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ⊆ 𝐴) |
| 66 | | ssdomg 9040 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑥 ⊆ 𝐴 → 𝑥 ≼ 𝐴)) |
| 67 | 61, 65, 66 | sylc 65 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ≼ 𝐴) |
| 68 | | hashdomi 14419 |
. . . . . . . . 9
⊢ (𝑥 ≼ 𝐴 → (♯‘𝑥) ≤ (♯‘𝐴)) |
| 69 | 67, 68 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(♯‘𝑥) ≤
(♯‘𝐴)) |
| 70 | | xlemul1a 13330 |
. . . . . . . 8
⊢
((((♯‘𝑥)
∈ ℝ* ∧ (♯‘𝐴) ∈ ℝ* ∧ (𝐵 ∈ ℝ*
∧ 0 ≤ 𝐵)) ∧
(♯‘𝑥) ≤
(♯‘𝐴)) →
((♯‘𝑥)
·e 𝐵)
≤ ((♯‘𝐴)
·e 𝐵)) |
| 71 | 38, 54, 60, 69, 70 | syl31anc 1375 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((♯‘𝑥)
·e 𝐵)
≤ ((♯‘𝐴)
·e 𝐵)) |
| 72 | 71 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵)) |
| 73 | | r19.29r 3116 |
. . . . . 6
⊢
((∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)𝑦 =
((♯‘𝑥)
·e 𝐵)
∧ ∀𝑥 ∈
(𝒫 𝐴 ∩
Fin)((♯‘𝑥)
·e 𝐵)
≤ ((♯‘𝐴)
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)(𝑦 =
((♯‘𝑥)
·e 𝐵)
∧ ((♯‘𝑥)
·e 𝐵)
≤ ((♯‘𝐴)
·e 𝐵))) |
| 74 | 53, 72, 73 | syl2anr 597 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((♯‘𝑥) ·e 𝐵) ∧ ((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵))) |
| 75 | | simpl 482 |
. . . . . . 7
⊢ ((𝑦 = ((♯‘𝑥) ·e 𝐵) ∧ ((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵)) → 𝑦 = ((♯‘𝑥) ·e 𝐵)) |
| 76 | | simpr 484 |
. . . . . . 7
⊢ ((𝑦 = ((♯‘𝑥) ·e 𝐵) ∧ ((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵)) → ((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵)) |
| 77 | 75, 76 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝑦 = ((♯‘𝑥) ·e 𝐵) ∧ ((♯‘𝑥) ·e 𝐵) ≤ ((♯‘𝐴) ·e 𝐵)) → 𝑦 ≤ ((♯‘𝐴) ·e 𝐵)) |
| 78 | 77 | rexlimivw 3151 |
. . . . 5
⊢
(∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)(𝑦 =
((♯‘𝑥)
·e 𝐵)
∧ ((♯‘𝑥)
·e 𝐵)
≤ ((♯‘𝐴)
·e 𝐵))
→ 𝑦 ≤
((♯‘𝐴)
·e 𝐵)) |
| 79 | 74, 78 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))) → 𝑦 ≤ ((♯‘𝐴) ·e 𝐵)) |
| 80 | 79 | ralrimiva 3146 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ∀𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 ≤ ((♯‘𝐴) ·e 𝐵)) |
| 81 | | pwidg 4620 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Fin → 𝐴 ∈ 𝒫 𝐴) |
| 82 | 81 | ancri 549 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin)) |
| 83 | | elin 3967 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐴 ∧ 𝐴 ∈ Fin)) |
| 84 | 82, 83 | sylibr 234 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin → 𝐴 ∈ (𝒫 𝐴 ∩ Fin)) |
| 85 | | eqid 2737 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
·e 𝐵) =
((♯‘𝐴)
·e 𝐵) |
| 86 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴)) |
| 87 | 86 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → ((♯‘𝑥) ·e 𝐵) = ((♯‘𝐴) ·e 𝐵)) |
| 88 | 87 | rspceeqv 3645 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝒫 𝐴 ∩ Fin) ∧
((♯‘𝐴)
·e 𝐵) =
((♯‘𝐴)
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((♯‘𝐴)
·e 𝐵) =
((♯‘𝑥)
·e 𝐵)) |
| 89 | 85, 88 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝒫 𝐴 ∩ Fin) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((♯‘𝐴) ·e 𝐵) = ((♯‘𝑥) ·e 𝐵)) |
| 90 | | ovex 7464 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
·e 𝐵)
∈ V |
| 91 | 50 | elrnmpt 5969 |
. . . . . . . . . . 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 234 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝒫 𝐴 ∩ Fin) →
((♯‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))) |
| 94 | 84, 93 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin →
((♯‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))) |
| 95 | 94 | adantl 481 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → ((♯‘𝐴) ·e 𝐵) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))) |
| 96 | | simplr 769 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → 𝑦 < ((♯‘𝐴) ·e 𝐵)) |
| 97 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑧 = ((♯‘𝐴) ·e 𝐵) → (𝑦 < 𝑧 ↔ 𝑦 < ((♯‘𝐴) ·e 𝐵))) |
| 98 | 97 | rspcev 3622 |
. . . . . . 7
⊢
((((♯‘𝐴)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
∧ 𝑦 <
((♯‘𝐴)
·e 𝐵))
→ ∃𝑧 ∈ ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
| 99 | 95, 96, 98 | syl2anc 584 |
. . . . . 6
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ 𝐴 ∈ Fin) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
| 100 | | 0elpw 5356 |
. . . . . . . . . . . 12
⊢ ∅
∈ 𝒫 𝐴 |
| 101 | | 0fi 9082 |
. . . . . . . . . . . 12
⊢ ∅
∈ Fin |
| 102 | | elin 3967 |
. . . . . . . . . . . 12
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ∈ 𝒫 𝐴 ∧ ∅ ∈ Fin)) |
| 103 | 100, 101,
102 | mpbir2an 711 |
. . . . . . . . . . 11
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) |
| 104 | 103 | a1i 11 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∅ ∈ (𝒫 𝐴 ∩ Fin)) |
| 105 | | simpr 484 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝐵 = 0) |
| 106 | 105 | oveq2d 7447 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((♯‘∅)
·e 𝐵) =
((♯‘∅) ·e 0)) |
| 107 | | hash0 14406 |
. . . . . . . . . . . . 13
⊢
(♯‘∅) = 0 |
| 108 | 107, 55 | eqeltri 2837 |
. . . . . . . . . . . 12
⊢
(♯‘∅) ∈ ℝ* |
| 109 | | xmul01 13309 |
. . . . . . . . . . . 12
⊢
((♯‘∅) ∈ ℝ* →
((♯‘∅) ·e 0) = 0) |
| 110 | 108, 109 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((♯‘∅) ·e 0) = 0 |
| 111 | 106, 110 | eqtr2di 2794 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 0 = ((♯‘∅)
·e 𝐵)) |
| 112 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
| 113 | 112 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ →
((♯‘𝑥)
·e 𝐵) =
((♯‘∅) ·e 𝐵)) |
| 114 | 113 | rspceeqv 3645 |
. . . . . . . . . 10
⊢ ((∅
∈ (𝒫 𝐴 ∩
Fin) ∧ 0 = ((♯‘∅) ·e 𝐵)) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)0 = ((♯‘𝑥) ·e 𝐵)) |
| 115 | 104, 111,
114 | syl2anc 584 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)0 = ((♯‘𝑥) ·e 𝐵)) |
| 116 | | ovex 7464 |
. . . . . . . . . 10
⊢
((♯‘𝑥)
·e 𝐵)
∈ V |
| 117 | 50, 116 | elrnmpti 5973 |
. . . . . . . . 9
⊢ (0 ∈
ran (𝑥 ∈ (𝒫
𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩ Fin)0 =
((♯‘𝑥)
·e 𝐵)) |
| 118 | 115, 117 | sylibr 234 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 0 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))) |
| 119 | | simpllr 776 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝑦 < ((♯‘𝐴) ·e 𝐵)) |
| 120 | 105 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((♯‘𝐴) ·e 𝐵) = ((♯‘𝐴) ·e
0)) |
| 121 | 47 | ad4antr 732 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → (♯‘𝐴) ∈
ℝ*) |
| 122 | | xmul01 13309 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℝ* → ((♯‘𝐴) ·e 0) =
0) |
| 123 | 121, 122 | syl 17 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((♯‘𝐴) ·e 0) =
0) |
| 124 | 120, 123 | eqtrd 2777 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ((♯‘𝐴) ·e 𝐵) = 0) |
| 125 | 119, 124 | breqtrd 5169 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → 𝑦 < 0) |
| 126 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑧 = 0 → (𝑦 < 𝑧 ↔ 𝑦 < 0)) |
| 127 | 126 | rspcev 3622 |
. . . . . . . 8
⊢ ((0
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
∧ 𝑦 < 0) →
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
| 128 | 118, 125,
127 | syl2anc 584 |
. . . . . . 7
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = 0) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
| 129 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑎 ∈ 𝒫 𝐴) |
| 130 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → (♯‘𝑎) = 𝑛) |
| 131 | | simp-4r 784 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑛 ∈ ℕ) |
| 132 | 130, 131 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → (♯‘𝑎) ∈ ℕ) |
| 133 | | nnnn0 12533 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑎)
∈ ℕ → (♯‘𝑎) ∈
ℕ0) |
| 134 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑎 ∈ V |
| 135 | | hashclb 14397 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ V → (𝑎 ∈ Fin ↔
(♯‘𝑎) ∈
ℕ0)) |
| 136 | 134, 135 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ Fin ↔
(♯‘𝑎) ∈
ℕ0) |
| 137 | 133, 136 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑎)
∈ ℕ → 𝑎
∈ Fin) |
| 138 | 132, 137 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑎 ∈ Fin) |
| 139 | 129, 138 | elind 4200 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) |
| 140 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ((♯‘𝑎) ·e 𝐵) = ((♯‘𝑎) ·e 𝐵)) |
| 141 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (♯‘𝑥) = (♯‘𝑎)) |
| 142 | 141 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → ((♯‘𝑥) ·e 𝐵) = ((♯‘𝑎) ·e 𝐵)) |
| 143 | 142 | rspceeqv 3645 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧
((♯‘𝑎)
·e 𝐵) =
((♯‘𝑎)
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((♯‘𝑎)
·e 𝐵) =
((♯‘𝑥)
·e 𝐵)) |
| 144 | 139, 140,
143 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((♯‘𝑎) ·e 𝐵) = ((♯‘𝑥) ·e 𝐵)) |
| 145 | 50, 116 | elrnmpti 5973 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑎)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)((♯‘𝑎)
·e 𝐵) =
((♯‘𝑥)
·e 𝐵)) |
| 146 | 144, 145 | sylibr 234 |
. . . . . . . . . . 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 12281 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑛 ∈ ℝ) |
| 150 | | simp-5r 786 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝐵 ∈
ℝ+) |
| 151 | 148, 149,
150 | ltdivmul2d 13129 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ((𝑦 / 𝐵) < 𝑛 ↔ 𝑦 < (𝑛 · 𝐵))) |
| 152 | 147, 151 | mpbid 232 |
. . . . . . . . . . . 12
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑦 < (𝑛 · 𝐵)) |
| 153 | 130 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ((♯‘𝑎) ·e 𝐵) = (𝑛 ·e 𝐵)) |
| 154 | 150 | rpred 13077 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝐵 ∈ ℝ) |
| 155 | | rexmul 13313 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑛 ·e 𝐵) = (𝑛 · 𝐵)) |
| 156 | 149, 154,
155 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → (𝑛 ·e 𝐵) = (𝑛 · 𝐵)) |
| 157 | 153, 156 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ((♯‘𝑎) ·e 𝐵) = (𝑛 · 𝐵)) |
| 158 | 152, 157 | breqtrrd 5171 |
. . . . . . . . . . 11
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → 𝑦 < ((♯‘𝑎) ·e 𝐵)) |
| 159 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((♯‘𝑎) ·e 𝐵) → (𝑦 < 𝑧 ↔ 𝑦 < ((♯‘𝑎) ·e 𝐵))) |
| 160 | 159 | rspcev 3622 |
. . . . . . . . . . 11
⊢
((((♯‘𝑎)
·e 𝐵)
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
∧ 𝑦 <
((♯‘𝑎)
·e 𝐵))
→ ∃𝑧 ∈ ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
| 161 | 146, 158,
160 | syl2anc 584 |
. . . . . . . . . 10
⊢
((((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) ∧ 𝑎 ∈ 𝒫 𝐴) ∧ (♯‘𝑎) = 𝑛) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
| 162 | 161 | rexlimdva2 3157 |
. . . . . . . . 9
⊢
((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ (𝑦 / 𝐵) < 𝑛) → (∃𝑎 ∈ 𝒫 𝐴(♯‘𝑎) = 𝑛 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧)) |
| 163 | 162 | impr 454 |
. . . . . . . 8
⊢
((((((((𝐴 ∈
𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ ((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(♯‘𝑎) = 𝑛)) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
| 164 | | simp-4r 784 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → 𝑦 ∈
ℝ) |
| 165 | | simpr 484 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → 𝐵 ∈
ℝ+) |
| 166 | 164, 165 | rerpdivcld 13108 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) → (𝑦 / 𝐵) ∈ ℝ) |
| 167 | | arch 12523 |
. . . . . . . . . 10
⊢ ((𝑦 / 𝐵) ∈ ℝ → ∃𝑛 ∈ ℕ (𝑦 / 𝐵) < 𝑛) |
| 168 | 166, 167 | syl 17 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∃𝑛 ∈ ℕ
(𝑦 / 𝐵) < 𝑛) |
| 169 | | ishashinf 14502 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ Fin →
∀𝑛 ∈ ℕ
∃𝑎 ∈ 𝒫
𝐴(♯‘𝑎) = 𝑛) |
| 170 | 169 | ad2antlr 727 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∀𝑛 ∈ ℕ
∃𝑎 ∈ 𝒫
𝐴(♯‘𝑎) = 𝑛) |
| 171 | | r19.29r 3116 |
. . . . . . . . 9
⊢
((∃𝑛 ∈
ℕ (𝑦 / 𝐵) < 𝑛 ∧ ∀𝑛 ∈ ℕ ∃𝑎 ∈ 𝒫 𝐴(♯‘𝑎) = 𝑛) → ∃𝑛 ∈ ℕ ((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(♯‘𝑎) = 𝑛)) |
| 172 | 168, 170,
171 | syl2anc 584 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∃𝑛 ∈ ℕ
((𝑦 / 𝐵) < 𝑛 ∧ ∃𝑎 ∈ 𝒫 𝐴(♯‘𝑎) = 𝑛)) |
| 173 | 163, 172 | r19.29a 3162 |
. . . . . . 7
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ∈ ℝ+) →
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))𝑦 < 𝑧) |
| 174 | | nfielex 9307 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ∈ Fin →
∃𝑙 𝑙 ∈ 𝐴) |
| 175 | 174 | adantr 480 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) → ∃𝑙 𝑙 ∈ 𝐴) |
| 176 | | snelpwi 5448 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ 𝐴 → {𝑙} ∈ 𝒫 𝐴) |
| 177 | | snfi 9083 |
. . . . . . . . . . . . . . 15
⊢ {𝑙} ∈ Fin |
| 178 | 176, 177 | jctir 520 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ 𝐴 → ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin)) |
| 179 | | elin 3967 |
. . . . . . . . . . . . . 14
⊢ ({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ↔ ({𝑙} ∈ 𝒫 𝐴 ∧ {𝑙} ∈ Fin)) |
| 180 | 178, 179 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ 𝐴 → {𝑙} ∈ (𝒫 𝐴 ∩ Fin)) |
| 181 | 180 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → {𝑙} ∈ (𝒫 𝐴 ∩ Fin)) |
| 182 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → 𝐵 = +∞) |
| 183 | 182 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → ((♯‘{𝑙}) ·e 𝐵) = ((♯‘{𝑙}) ·e
+∞)) |
| 184 | | hashsng 14408 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ 𝐴 → (♯‘{𝑙}) = 1) |
| 185 | | 1re 11261 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ |
| 186 | 27, 185 | sselii 3980 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ* |
| 187 | 184, 186 | eqeltrdi 2849 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ 𝐴 → (♯‘{𝑙}) ∈
ℝ*) |
| 188 | | 0lt1 11785 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
1 |
| 189 | 188, 184 | breqtrrid 5181 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ 𝐴 → 0 < (♯‘{𝑙})) |
| 190 | | xmulpnf1 13316 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘{𝑙}) ∈ ℝ* ∧ 0 <
(♯‘{𝑙})) →
((♯‘{𝑙})
·e +∞) = +∞) |
| 191 | 187, 189,
190 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ 𝐴 → ((♯‘{𝑙}) ·e +∞) =
+∞) |
| 192 | 191 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → ((♯‘{𝑙}) ·e +∞) =
+∞) |
| 193 | 183, 192 | eqtr2d 2778 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → +∞ = ((♯‘{𝑙}) ·e 𝐵)) |
| 194 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = {𝑙} → (♯‘𝑥) = (♯‘{𝑙})) |
| 195 | 194 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {𝑙} → ((♯‘𝑥) ·e 𝐵) = ((♯‘{𝑙}) ·e 𝐵)) |
| 196 | 195 | rspceeqv 3645 |
. . . . . . . . . . . 12
⊢ (({𝑙} ∈ (𝒫 𝐴 ∩ Fin) ∧ +∞ =
((♯‘{𝑙})
·e 𝐵))
→ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)+∞ = ((♯‘𝑥) ·e 𝐵)) |
| 197 | 181, 193,
196 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) ∧ 𝑙 ∈ 𝐴) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ = ((♯‘𝑥) ·e 𝐵)) |
| 198 | 175, 197 | exlimddv 1935 |
. . . . . . . . . 10
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 = +∞) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ =
((♯‘𝑥)
·e 𝐵)) |
| 199 | 198 | adantll 714 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)+∞ =
((♯‘𝑥)
·e 𝐵)) |
| 200 | 50, 116 | elrnmpti 5973 |
. . . . . . . . 9
⊢ (+∞
∈ ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ ((♯‘𝑥)
·e 𝐵))
↔ ∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)+∞ = ((♯‘𝑥) ·e 𝐵)) |
| 201 | 199, 200 | sylibr 234 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵))) |
| 202 | | simp-4r 784 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → 𝑦 ∈ ℝ) |
| 203 | | ltpnf 13162 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → 𝑦 < +∞) |
| 204 | 202, 203 | syl 17 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → 𝑦 < +∞) |
| 205 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑧 = +∞ → (𝑦 < 𝑧 ↔ 𝑦 < +∞)) |
| 206 | 205 | rspcev 3622 |
. . . . . . . 8
⊢
((+∞ ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵)) ∧ 𝑦 < +∞) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
| 207 | 201, 204,
206 | syl2anc 584 |
. . . . . . 7
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = +∞) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
| 208 | | simp-4r 784 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → 𝐵 ∈ (0[,]+∞)) |
| 209 | | elxrge02 32914 |
. . . . . . . 8
⊢ (𝐵 ∈ (0[,]+∞) ↔
(𝐵 = 0 ∨ 𝐵 ∈ ℝ+ ∨
𝐵 =
+∞)) |
| 210 | 208, 209 | sylib 218 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → (𝐵 = 0 ∨ 𝐵 ∈ ℝ+ ∨ 𝐵 = +∞)) |
| 211 | 128, 173,
207, 210 | mpjao3dan 1434 |
. . . . . 6
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) ∧ ¬ 𝐴 ∈ Fin) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
| 212 | 99, 211 | pm2.61dan 813 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < ((♯‘𝐴) ·e 𝐵)) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧) |
| 213 | 212 | ex 412 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) ∧ 𝑦 ∈ ℝ) → (𝑦 < ((♯‘𝐴) ·e 𝐵) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧)) |
| 214 | 213 | ralrimiva 3146 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → ∀𝑦 ∈ ℝ (𝑦 < ((♯‘𝐴) ·e 𝐵) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((♯‘𝑥) ·e 𝐵))𝑦 < 𝑧)) |
| 215 | | supxr2 13356 |
. . 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 839 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → sup(ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((♯‘𝑥)
·e 𝐵)),
ℝ*, < ) = ((♯‘𝐴) ·e 𝐵)) |
| 217 | 25, 216 | eqtrd 2777 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
𝐴𝐵 = ((♯‘𝐴) ·e 𝐵)) |