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

Metamath Proof Explorer

Theorem 1sgmprm

Description: The sum of divisors for a prime is P + 1 because the only divisors are 1 and P . (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion 1sgmprm ( 𝑃 ∈ ℙ → ( 1 σ 𝑃 ) = ( 𝑃 + 1 ) )

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 1nn0 ⊢ 1 ∈ ℕ0
3 sgmppw ⊢ ( ( 1 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 1 ∈ ℕ0 ) → ( 1 σ ( 𝑃 ↑ 1 ) ) = Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑃 ↑𝑐 1 ) ↑ 𝑘 ) )
4 1 2 3 mp3an13 ⊢ ( 𝑃 ∈ ℙ → ( 1 σ ( 𝑃 ↑ 1 ) ) = Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑃 ↑𝑐 1 ) ↑ 𝑘 ) )
5 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
6 5 nncnd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
7 6 exp1d ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ 1 ) = 𝑃 )
8 7 oveq2d ⊢ ( 𝑃 ∈ ℙ → ( 1 σ ( 𝑃 ↑ 1 ) ) = ( 1 σ 𝑃 ) )
9 6 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( 0 ... 1 ) ) → 𝑃 ∈ ℂ )
10 9 cxp1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( 0 ... 1 ) ) → ( 𝑃 ↑𝑐 1 ) = 𝑃 )
11 10 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( 0 ... 1 ) ) → ( ( 𝑃 ↑𝑐 1 ) ↑ 𝑘 ) = ( 𝑃 ↑ 𝑘 ) )
12 11 sumeq2dv ⊢ ( 𝑃 ∈ ℙ → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑃 ↑𝑐 1 ) ↑ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... 1 ) ( 𝑃 ↑ 𝑘 ) )
13 1m1e0 ⊢ ( 1 − 1 ) = 0
14 13 oveq2i ⊢ ( 0 ... ( 1 − 1 ) ) = ( 0 ... 0 )
15 14 sumeq1i ⊢ Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( 𝑃 ↑ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑃 ↑ 𝑘 )
16 0z ⊢ 0 ∈ ℤ
17 6 exp0d ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ 0 ) = 1 )
18 17 1 eqeltrdi ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ 0 ) ∈ ℂ )
19 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑃 ↑ 𝑘 ) = ( 𝑃 ↑ 0 ) )
20 19 fsum1 ⊢ ( ( 0 ∈ ℤ ∧ ( 𝑃 ↑ 0 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑃 ↑ 𝑘 ) = ( 𝑃 ↑ 0 ) )
21 16 18 20 sylancr ⊢ ( 𝑃 ∈ ℙ → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑃 ↑ 𝑘 ) = ( 𝑃 ↑ 0 ) )
22 21 17 eqtrd ⊢ ( 𝑃 ∈ ℙ → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑃 ↑ 𝑘 ) = 1 )
23 15 22 eqtrid ⊢ ( 𝑃 ∈ ℙ → Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( 𝑃 ↑ 𝑘 ) = 1 )
24 23 7 oveq12d ⊢ ( 𝑃 ∈ ℙ → ( Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( 𝑃 ↑ 𝑘 ) + ( 𝑃 ↑ 1 ) ) = ( 1 + 𝑃 ) )
25 2 a1i ⊢ ( 𝑃 ∈ ℙ → 1 ∈ ℕ0 )
26 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
27 25 26 eleqtrdi ⊢ ( 𝑃 ∈ ℙ → 1 ∈ ( ℤ≥ ‘ 0 ) )
28 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 1 ) → 𝑘 ∈ ℕ0 )
29 expcl ⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑘 ) ∈ ℂ )
30 6 28 29 syl2an ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( 0 ... 1 ) ) → ( 𝑃 ↑ 𝑘 ) ∈ ℂ )
31 oveq2 ⊢ ( 𝑘 = 1 → ( 𝑃 ↑ 𝑘 ) = ( 𝑃 ↑ 1 ) )
32 27 30 31 fsumm1 ⊢ ( 𝑃 ∈ ℙ → Σ 𝑘 ∈ ( 0 ... 1 ) ( 𝑃 ↑ 𝑘 ) = ( Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( 𝑃 ↑ 𝑘 ) + ( 𝑃 ↑ 1 ) ) )
33 addcom ⊢ ( ( 𝑃 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑃 + 1 ) = ( 1 + 𝑃 ) )
34 6 1 33 sylancl ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 + 1 ) = ( 1 + 𝑃 ) )
35 24 32 34 3eqtr4d ⊢ ( 𝑃 ∈ ℙ → Σ 𝑘 ∈ ( 0 ... 1 ) ( 𝑃 ↑ 𝑘 ) = ( 𝑃 + 1 ) )
36 12 35 eqtrd ⊢ ( 𝑃 ∈ ℙ → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑃 ↑𝑐 1 ) ↑ 𝑘 ) = ( 𝑃 + 1 ) )
37 4 8 36 3eqtr3d ⊢ ( 𝑃 ∈ ℙ → ( 1 σ 𝑃 ) = ( 𝑃 + 1 ) )