Step | Hyp | Ref
| Expression |
1 | | fsumnncl.afi |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
2 | | fsumnncl.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℕ) |
3 | 2 | nnnn0d 12293 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈
ℕ0) |
4 | 1, 3 | fsumnn0cl 15448 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈
ℕ0) |
5 | | fsumnncl.an0 |
. . . . 5
⊢ (𝜑 → 𝐴 ≠ ∅) |
6 | | n0 4280 |
. . . . 5
⊢ (𝐴 ≠ ∅ ↔
∃𝑗 𝑗 ∈ 𝐴) |
7 | 5, 6 | sylib 217 |
. . . 4
⊢ (𝜑 → ∃𝑗 𝑗 ∈ 𝐴) |
8 | | 0red 10978 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ∈ ℝ) |
9 | | nfv 1917 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝐴) |
10 | | nfcsb1v 3857 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 |
11 | 10 | nfel1 2923 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℕ |
12 | 9, 11 | nfim 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℕ) |
13 | | eleq1w 2821 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴)) |
14 | 13 | anbi2d 629 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑗 ∈ 𝐴))) |
15 | | csbeq1a 3846 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵) |
16 | 15 | eleq1d 2823 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℕ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℕ)) |
17 | 14, 16 | imbi12d 345 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℕ) ↔ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℕ))) |
18 | 12, 17, 2 | chvarfv 2233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℕ) |
19 | 18 | nnred 11988 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℝ) |
20 | 8, 19 | readdcld 11004 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (0 + ⦋𝑗 / 𝑘⦌𝐵) ∈ ℝ) |
21 | | diffi 8962 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → (𝐴 ∖ {𝑗}) ∈ Fin) |
22 | 1, 21 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∖ {𝑗}) ∈ Fin) |
23 | | eldifi 4061 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝐴 ∖ {𝑗}) → 𝑘 ∈ 𝐴) |
24 | 23 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝑘 ∈ 𝐴) |
25 | 24, 3 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝐵 ∈
ℕ0) |
26 | 22, 25 | fsumnn0cl 15448 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 ∈
ℕ0) |
27 | 26 | nn0red 12294 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 ∈ ℝ) |
28 | 27 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 ∈ ℝ) |
29 | 28, 19 | readdcld 11004 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 + ⦋𝑗 / 𝑘⦌𝐵) ∈ ℝ) |
30 | 18 | nnrpd 12770 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈
ℝ+) |
31 | 8, 30 | ltaddrpd 12805 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 < (0 + ⦋𝑗 / 𝑘⦌𝐵)) |
32 | 26 | nn0ge0d 12296 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵) |
33 | 32 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ≤ Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵) |
34 | 8, 28, 19, 33 | leadd1dd 11589 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (0 + ⦋𝑗 / 𝑘⦌𝐵) ≤ (Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 + ⦋𝑗 / 𝑘⦌𝐵)) |
35 | 8, 20, 29, 31, 34 | ltletrd 11135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 < (Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 + ⦋𝑗 / 𝑘⦌𝐵)) |
36 | | difsnid 4743 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝐴 → ((𝐴 ∖ {𝑗}) ∪ {𝑗}) = 𝐴) |
37 | 36 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐴 ∖ {𝑗}) ∪ {𝑗}) = 𝐴) |
38 | 37 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐴 = ((𝐴 ∖ {𝑗}) ∪ {𝑗})) |
39 | 38 | sumeq1d 15413 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ((𝐴 ∖ {𝑗}) ∪ {𝑗})𝐵) |
40 | 22 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐴 ∖ {𝑗}) ∈ Fin) |
41 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ 𝐴) |
42 | | neldifsnd 4726 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ¬ 𝑗 ∈ (𝐴 ∖ {𝑗})) |
43 | | simpl 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝜑) |
44 | 43, 24, 2 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝐵 ∈ ℕ) |
45 | 44 | nncnd 11989 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝐵 ∈ ℂ) |
46 | 45 | adantlr 712 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ (𝐴 ∖ {𝑗})) → 𝐵 ∈ ℂ) |
47 | | nnsscn 11978 |
. . . . . . . . . . 11
⊢ ℕ
⊆ ℂ |
48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ℕ ⊆
ℂ) |
49 | 48, 18 | sseldd 3922 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ) |
50 | 9, 10, 40, 41, 42, 46, 15, 49 | fsumsplitsn 15456 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → Σ𝑘 ∈ ((𝐴 ∖ {𝑗}) ∪ {𝑗})𝐵 = (Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 + ⦋𝑗 / 𝑘⦌𝐵)) |
51 | 39, 50 | eqtr2d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (Σ𝑘 ∈ (𝐴 ∖ {𝑗})𝐵 + ⦋𝑗 / 𝑘⦌𝐵) = Σ𝑘 ∈ 𝐴 𝐵) |
52 | 35, 51 | breqtrd 5100 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 < Σ𝑘 ∈ 𝐴 𝐵) |
53 | 52 | ex 413 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ 𝐴 → 0 < Σ𝑘 ∈ 𝐴 𝐵)) |
54 | 53 | exlimdv 1936 |
. . . 4
⊢ (𝜑 → (∃𝑗 𝑗 ∈ 𝐴 → 0 < Σ𝑘 ∈ 𝐴 𝐵)) |
55 | 7, 54 | mpd 15 |
. . 3
⊢ (𝜑 → 0 < Σ𝑘 ∈ 𝐴 𝐵) |
56 | 4, 55 | jca 512 |
. 2
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ0 ∧ 0 <
Σ𝑘 ∈ 𝐴 𝐵)) |
57 | | elnnnn0b 12277 |
. 2
⊢
(Σ𝑘 ∈
𝐴 𝐵 ∈ ℕ ↔ (Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ0 ∧ 0 <
Σ𝑘 ∈ 𝐴 𝐵)) |
58 | 56, 57 | sylibr 233 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ) |