Metamath Proof Explorer

Theorem fsumnncl

Description: Closure of a nonempty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fsumnncl.an0 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
fsumnncl.afi ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumnncl.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℕ )
Assertion fsumnncl ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℕ )

Proof

Step Hyp Ref Expression
1 fsumnncl.an0 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
2 fsumnncl.afi ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 fsumnncl.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℕ )
4 3 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℕ0 )
5 2 4 fsumnn0cl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℕ0 )
6 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑗 𝑗 ∈ 𝐴 )
7 1 6 sylib ⊢ ( 𝜑 → ∃ 𝑗 𝑗 ∈ 𝐴 )
8 0red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 0 ∈ ℝ )
9 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
10 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
11 10 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℕ
12 9 11 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℕ )
13 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
14 13 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ) )
15 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
16 15 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℕ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℕ ) )
17 14 16 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℕ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℕ ) ) )
18 12 17 3 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℕ )
19 18 nnred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
20 8 19 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 0 + ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
21 diffi ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝑗 } ) ∈ Fin )
22 2 21 syl ⊢ ( 𝜑 → ( 𝐴 ∖ { 𝑗 } ) ∈ Fin )
23 eldifi ⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) → 𝑘 ∈ 𝐴 )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) ) → 𝑘 ∈ 𝐴 )
25 24 4 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) ) → 𝐵 ∈ ℕ0 )
26 22 25 fsumnn0cl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 ∈ ℕ0 )
27 26 nn0red ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 ∈ ℝ )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 ∈ ℝ )
29 28 19 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
30 18 nnrpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ+ )
31 8 30 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 0 < ( 0 + ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
32 26 nn0ge0d ⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 0 ≤ Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 )
34 8 28 19 33 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 0 + ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ≤ ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
35 8 20 29 31 34 ltletrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 0 < ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
36 difsnid ⊢ ( 𝑗 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑗 } ) ∪ { 𝑗 } ) = 𝐴 )
37 36 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑗 } ) ∪ { 𝑗 } ) = 𝐴 )
38 37 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐴 = ( ( 𝐴 ∖ { 𝑗 } ) ∪ { 𝑗 } ) )
39 38 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ ( ( 𝐴 ∖ { 𝑗 } ) ∪ { 𝑗 } ) 𝐵 )
40 22 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑗 } ) ∈ Fin )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝐴 )
42 neldifsnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ¬ 𝑗 ∈ ( 𝐴 ∖ { 𝑗 } ) )
43 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) ) → 𝜑 )
44 43 24 3 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) ) → 𝐵 ∈ ℕ )
45 44 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) ) → 𝐵 ∈ ℂ )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) ) → 𝐵 ∈ ℂ )
47 nnsscn ⊢ ℕ ⊆ ℂ
48 47 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ℕ ⊆ ℂ )
49 48 18 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ )
50 9 10 40 41 42 46 15 49 fsumsplitsn ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → Σ 𝑘 ∈ ( ( 𝐴 ∖ { 𝑗 } ) ∪ { 𝑗 } ) 𝐵 = ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
51 39 50 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) = Σ 𝑘 ∈ 𝐴 𝐵 )
52 35 51 breqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 0 < Σ 𝑘 ∈ 𝐴 𝐵 )
53 52 ex ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 → 0 < Σ 𝑘 ∈ 𝐴 𝐵 ) )
54 53 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑗 𝑗 ∈ 𝐴 → 0 < Σ 𝑘 ∈ 𝐴 𝐵 ) )
55 7 54 mpd ⊢ ( 𝜑 → 0 < Σ 𝑘 ∈ 𝐴 𝐵 )
56 5 55 jca ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℕ0 ∧ 0 < Σ 𝑘 ∈ 𝐴 𝐵 ) )
57 elnnnn0b ⊢ ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℕ ↔ ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℕ0 ∧ 0 < Σ 𝑘 ∈ 𝐴 𝐵 ) )
58 56 57 sylibr ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℕ )