Step | Hyp | Ref
| Expression |
1 | | fsumnncl.afi |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
2 | | fsumnncl.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℕ) |
3 | 2 | nnnn0d 12029 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈
ℕ0) |
4 | 1, 3 | fsumnn0cl 15179 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈
ℕ0) |
5 | | fsumnncl.an0 |
. . . . 5
⊢ (𝜑 → 𝐴 ≠ ∅) |
6 | | n0 4233 |
. . . . 5
⊢ (𝐴 ≠ ∅ ↔
∃𝑗 𝑗 ∈ 𝐴) |
7 | 5, 6 | sylib 221 |
. . . 4
⊢ (𝜑 → ∃𝑗 𝑗 ∈ 𝐴) |
8 | | 0red 10715 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ∈ ℝ) |
9 | | nfv 1920 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝐴) |
10 | | nfcsb1v 3812 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 |
11 | 10 | nfel1 2915 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℕ |
12 | 9, 11 | nfim 1902 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℕ) |
13 | | eleq1w 2815 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴)) |
14 | 13 | anbi2d 632 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑗 ∈ 𝐴))) |
15 | | csbeq1a 3802 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵) |
16 | 15 | eleq1d 2817 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℕ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℕ)) |
17 | 14, 16 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℕ) ↔ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℕ))) |
18 | 12, 17, 2 | chvarfv 2241 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℕ) |
19 | 18 | nnred 11724 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℝ) |
20 | 8, 19 | readdcld 10741 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (0 + ⦋𝑗 / 𝑘⦌𝐵) ∈ ℝ) |
21 | | diffi 8820 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → (𝐴 ∖ {𝑗}) ∈ Fin) |
22 | 1, 21 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∖ {𝑗}) ∈ Fin) |
23 | | eldifi 4015 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝐴 ∖ {𝑗}) → 𝑘 ∈ 𝐴) |
24 | 23 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝑘 ∈ 𝐴) |
25 | 24, 3 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝐵 ∈
ℕ0) |
26 | 22, 25 | fsumnn0cl 15179 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 ∈
ℕ0) |
27 | 26 | nn0red 12030 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 ∈ ℝ) |
28 | 27 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 ∈ ℝ) |
29 | 28, 19 | readdcld 10741 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 + ⦋𝑗 / 𝑘⦌𝐵) ∈ ℝ) |
30 | 18 | nnrpd 12505 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈
ℝ+) |
31 | 8, 30 | ltaddrpd 12540 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 < (0 + ⦋𝑗 / 𝑘⦌𝐵)) |
32 | 26 | nn0ge0d 12032 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵) |
33 | 32 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ≤ Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵) |
34 | 8, 28, 19, 33 | leadd1dd 11325 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (0 + ⦋𝑗 / 𝑘⦌𝐵) ≤ (Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 + ⦋𝑗 / 𝑘⦌𝐵)) |
35 | 8, 20, 29, 31, 34 | ltletrd 10871 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 < (Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 + ⦋𝑗 / 𝑘⦌𝐵)) |
36 | | difsnid 4695 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝐴 → ((𝐴 ∖ {𝑗}) ∪ {𝑗}) = 𝐴) |
37 | 36 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐴 ∖ {𝑗}) ∪ {𝑗}) = 𝐴) |
38 | 37 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐴 = ((𝐴 ∖ {𝑗}) ∪ {𝑗})) |
39 | 38 | sumeq1d 15144 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ((𝐴 ∖ {𝑗}) ∪ {𝑗})𝐵) |
40 | 22 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐴 ∖ {𝑗}) ∈ Fin) |
41 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ 𝐴) |
42 | | neldifsnd 4678 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ¬ 𝑗 ∈ (𝐴 ∖ {𝑗})) |
43 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝜑) |
44 | 43, 24, 2 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝐵 ∈ ℕ) |
45 | 44 | nncnd 11725 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝐵 ∈ ℂ) |
46 | 45 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝐵 ∈ ℂ) |
47 | | nnsscn 11714 |
. . . . . . . . . . 11
⊢ ℕ
⊆ ℂ |
48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ℕ ⊆
ℂ) |
49 | 48, 18 | sseldd 3876 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ) |
50 | 9, 10, 40, 41, 42, 46, 15, 49 | fsumsplitsn 15186 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → Σ𝑘 ∈ ((𝐴 ∖ {𝑗}) ∪ {𝑗})𝐵 = (Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 + ⦋𝑗 / 𝑘⦌𝐵)) |
51 | 39, 50 | eqtr2d 2774 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 + ⦋𝑗 / 𝑘⦌𝐵) = Σ𝑘 ∈ 𝐴 𝐵) |
52 | 35, 51 | breqtrd 5053 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 < Σ𝑘 ∈ 𝐴 𝐵) |
53 | 52 | ex 416 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ 𝐴 → 0 < Σ𝑘 ∈ 𝐴 𝐵)) |
54 | 53 | exlimdv 1939 |
. . . 4
⊢ (𝜑 → (∃𝑗 𝑗 ∈ 𝐴 → 0 < Σ𝑘 ∈ 𝐴 𝐵)) |
55 | 7, 54 | mpd 15 |
. . 3
⊢ (𝜑 → 0 < Σ𝑘 ∈ 𝐴 𝐵) |
56 | 4, 55 | jca 515 |
. 2
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ0 ∧ 0 <
Σ𝑘 ∈ 𝐴 𝐵)) |
57 | | elnnnn0b 12013 |
. 2
⊢
(Σ𝑘 ∈
𝐴 𝐵 ∈ ℕ ↔ (Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ0 ∧ 0 <
Σ𝑘 ∈ 𝐴 𝐵)) |
58 | 56, 57 | sylibr 237 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ) |