Metamath Proof Explorer

Theorem fsummmodsndifre

Description: A finite sum of summands modulo a positive number with one of its summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018)

Ref Expression
Assertion fsummmodsndifre ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐵 mod 𝑁 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 csbeq1a ⊢ ( 𝑘 = 𝑥 → ( 𝐵 mod 𝑁 ) = ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) )
2 nfcv ⊢ Ⅎ 𝑥 ( 𝐵 mod 𝑁 )
3 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 )
4 1 2 3 cbvsum ⊢ Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐵 mod 𝑁 ) = Σ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 )
5 diffi ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝑋 } ) ∈ Fin )
6 5 3ad2ant1 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ( 𝐴 ∖ { 𝑋 } ) ∈ Fin )
7 eldifi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) → 𝑥 ∈ 𝐴 )
8 rspcsbela ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ )
9 7 8 sylan ⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ )
10 9 expcom ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ → ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) )
11 10 3ad2ant3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) )
12 11 imp ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ )
13 vex ⊢ 𝑥 ∈ V
14 csbov1g ⊢ ( 𝑥 ∈ V → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) = ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 mod 𝑁 ) )
15 13 14 ax-mp ⊢ ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) = ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 mod 𝑁 )
16 zre ⊢ ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℝ )
17 16 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℝ )
18 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
19 18 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) → 𝑁 ∈ ℝ+ )
20 17 19 modcld ⊢ ( ( 𝑁 ∈ ℕ ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 mod 𝑁 ) ∈ ℝ )
21 15 20 eqeltrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℝ )
22 21 ex ⊢ ( 𝑁 ∈ ℕ → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℝ ) )
23 22 3ad2ant2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℝ ) )
24 23 adantr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ) → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℝ ) )
25 12 24 mpd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ) → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℝ )
26 6 25 fsumrecl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ⦋ 𝑥 / 𝑘 ⦌ ( 𝐵 mod 𝑁 ) ∈ ℝ )
27 4 26 eqeltrid ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) ( 𝐵 mod 𝑁 ) ∈ ℝ )