This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1sgm2ppw

Description: The sum of the divisors of 2 ^ ( N - 1 ) . (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion 1sgm2ppw ( 𝑁 ∈ ℕ → ( 1 σ ( 2 ↑ ( 𝑁 − 1 ) ) ) = ( ( 2 ↑ 𝑁 ) − 1 ) )

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 2prm ⊢ 2 ∈ ℙ
3 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
4 sgmppw ⊢ ( ( 1 ∈ ℂ ∧ 2 ∈ ℙ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 1 σ ( 2 ↑ ( 𝑁 − 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 2 ↑𝑐 1 ) ↑ 𝑘 ) )
5 1 2 3 4 mp3an12i ⊢ ( 𝑁 ∈ ℕ → ( 1 σ ( 2 ↑ ( 𝑁 − 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 2 ↑𝑐 1 ) ↑ 𝑘 ) )
6 2cn ⊢ 2 ∈ ℂ
7 cxp1 ⊢ ( 2 ∈ ℂ → ( 2 ↑𝑐 1 ) = 2 )
8 6 7 mp1i ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 2 ↑𝑐 1 ) = 2 )
9 8 oveq1d ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 2 ↑𝑐 1 ) ↑ 𝑘 ) = ( 2 ↑ 𝑘 ) )
10 9 sumeq2i ⊢ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 2 ↑𝑐 1 ) ↑ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 ↑ 𝑘 )
11 6 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
12 1ne2 ⊢ 1 ≠ 2
13 12 necomi ⊢ 2 ≠ 1
14 13 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 1 )
15 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
16 11 14 15 geoser ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 ↑ 𝑘 ) = ( ( 1 − ( 2 ↑ 𝑁 ) ) / ( 1 − 2 ) ) )
17 10 16 eqtrid ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 2 ↑𝑐 1 ) ↑ 𝑘 ) = ( ( 1 − ( 2 ↑ 𝑁 ) ) / ( 1 − 2 ) ) )
18 2nn ⊢ 2 ∈ ℕ
19 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℕ )
20 18 15 19 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℕ )
21 20 nncnd ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℂ )
22 subcl ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 2 ↑ 𝑁 ) − 1 ) ∈ ℂ )
23 21 1 22 sylancl ⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ 𝑁 ) − 1 ) ∈ ℂ )
24 1 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
25 ax-1ne0 ⊢ 1 ≠ 0
26 25 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ≠ 0 )
27 23 24 26 div2negd ⊢ ( 𝑁 ∈ ℕ → ( - ( ( 2 ↑ 𝑁 ) − 1 ) / - 1 ) = ( ( ( 2 ↑ 𝑁 ) − 1 ) / 1 ) )
28 negsubdi2 ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ 1 ∈ ℂ ) → - ( ( 2 ↑ 𝑁 ) − 1 ) = ( 1 − ( 2 ↑ 𝑁 ) ) )
29 21 1 28 sylancl ⊢ ( 𝑁 ∈ ℕ → - ( ( 2 ↑ 𝑁 ) − 1 ) = ( 1 − ( 2 ↑ 𝑁 ) ) )
30 df-neg ⊢ - 1 = ( 0 − 1 )
31 0cn ⊢ 0 ∈ ℂ
32 pnpcan ⊢ ( ( 1 ∈ ℂ ∧ 0 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 1 + 0 ) − ( 1 + 1 ) ) = ( 0 − 1 ) )
33 1 31 1 32 mp3an ⊢ ( ( 1 + 0 ) − ( 1 + 1 ) ) = ( 0 − 1 )
34 1p0e1 ⊢ ( 1 + 0 ) = 1
35 1p1e2 ⊢ ( 1 + 1 ) = 2
36 34 35 oveq12i ⊢ ( ( 1 + 0 ) − ( 1 + 1 ) ) = ( 1 − 2 )
37 30 33 36 3eqtr2i ⊢ - 1 = ( 1 − 2 )
38 37 a1i ⊢ ( 𝑁 ∈ ℕ → - 1 = ( 1 − 2 ) )
39 29 38 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( - ( ( 2 ↑ 𝑁 ) − 1 ) / - 1 ) = ( ( 1 − ( 2 ↑ 𝑁 ) ) / ( 1 − 2 ) ) )
40 23 div1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 ↑ 𝑁 ) − 1 ) / 1 ) = ( ( 2 ↑ 𝑁 ) − 1 ) )
41 27 39 40 3eqtr3d ⊢ ( 𝑁 ∈ ℕ → ( ( 1 − ( 2 ↑ 𝑁 ) ) / ( 1 − 2 ) ) = ( ( 2 ↑ 𝑁 ) − 1 ) )
42 5 17 41 3eqtrd ⊢ ( 𝑁 ∈ ℕ → ( 1 σ ( 2 ↑ ( 𝑁 − 1 ) ) ) = ( ( 2 ↑ 𝑁 ) − 1 ) )