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	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℕ₀ )
5	2 4	fsumnn0cl	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℕ₀ )
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	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) ) → 𝐵 ∈ ℕ₀ )
26	22 25	fsumnn0cl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑗 } ) 𝐵 ∈ ℕ₀ )
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 < Σ 𝑘 ∈ 𝐴 𝐵 ) )
57		elnnnn0b	⊢ ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℕ ↔ ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℕ₀ ∧ 0 < Σ 𝑘 ∈ 𝐴 𝐵 ) )
58	56 57	sylibr	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℕ )

Metamath Proof Explorer

Theorem fsumnncl

Proof