1sgm2ppw - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 1sgm2ppw		GIF version

Theorem 1sgm2ppw 15203

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

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

Proof of Theorem 1sgm2ppw Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1cn 7970	. . 3 ⊢ 1 ∈ ℂ
2		2prm 12271	. . 3 ⊢ 2 ∈ ℙ
3		nnm1nn0 9287	. . 3 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
4		sgmppw 15200	. . 3 ⊢ ((1 ∈ ℂ ∧ 2 ∈ ℙ ∧ (𝑁 − 1) ∈ ℕ₀) → (1 σ (2↑(𝑁 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((2↑_𝑐1)↑𝑘))
5	1, 2, 3, 4	mp3an12i 1352	. 2 ⊢ (𝑁 ∈ ℕ → (1 σ (2↑(𝑁 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((2↑_𝑐1)↑𝑘))
6		2rp 9730	. . . . . 6 ⊢ 2 ∈ ℝ⁺
7		rpcxp1 15108	. . . . . 6 ⊢ (2 ∈ ℝ⁺ → (2↑_𝑐1) = 2)
8	6, 7	mp1i 10	. . . . 5 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → (2↑_𝑐1) = 2)
9	8	oveq1d 5937	. . . 4 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((2↑_𝑐1)↑𝑘) = (2↑𝑘))
10	9	sumeq2i 11513	. . 3 ⊢ Σ𝑘 ∈ (0...(𝑁 − 1))((2↑_𝑐1)↑𝑘) = Σ𝑘 ∈ (0...(𝑁 − 1))(2↑𝑘)
11		2cn 9058	. . . . 5 ⊢ 2 ∈ ℂ
12	11	a1i 9	. . . 4 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℂ)
13		1ap2 9195	. . . . . 6 ⊢ 1 # 2
14		apsym 8630	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ 2 ∈ ℂ) → (1 # 2 ↔ 2 # 1))
15	1, 11, 14	mp2an 426	. . . . . 6 ⊢ (1 # 2 ↔ 2 # 1)
16	13, 15	mpbi 145	. . . . 5 ⊢ 2 # 1
17	16	a1i 9	. . . 4 ⊢ (𝑁 ∈ ℕ → 2 # 1)
18		nnnn0 9253	. . . 4 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
19	12, 17, 18	geoserap 11656	. . 3 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...(𝑁 − 1))(2↑𝑘) = ((1 − (2↑𝑁)) / (1 − 2)))
20	10, 19	eqtrid 2241	. 2 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...(𝑁 − 1))((2↑_𝑐1)↑𝑘) = ((1 − (2↑𝑁)) / (1 − 2)))
21		2nn 9149	. . . . . . 7 ⊢ 2 ∈ ℕ
22		nnexpcl 10629	. . . . . . 7 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2↑𝑁) ∈ ℕ)
23	21, 18, 22	sylancr 414	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (2↑𝑁) ∈ ℕ)
24	23	nncnd 9001	. . . . 5 ⊢ (𝑁 ∈ ℕ → (2↑𝑁) ∈ ℂ)
25		subcl 8223	. . . . 5 ⊢ (((2↑𝑁) ∈ ℂ ∧ 1 ∈ ℂ) → ((2↑𝑁) − 1) ∈ ℂ)
26	24, 1, 25	sylancl 413	. . . 4 ⊢ (𝑁 ∈ ℕ → ((2↑𝑁) − 1) ∈ ℂ)
27	1	a1i 9	. . . 4 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
28		1ap0 8614	. . . . 5 ⊢ 1 # 0
29	28	a1i 9	. . . 4 ⊢ (𝑁 ∈ ℕ → 1 # 0)
30	26, 27, 29	div2negapd 8829	. . 3 ⊢ (𝑁 ∈ ℕ → (-((2↑𝑁) − 1) / -1) = (((2↑𝑁) − 1) / 1))
31		negsubdi2 8283	. . . . 5 ⊢ (((2↑𝑁) ∈ ℂ ∧ 1 ∈ ℂ) → -((2↑𝑁) − 1) = (1 − (2↑𝑁)))
32	24, 1, 31	sylancl 413	. . . 4 ⊢ (𝑁 ∈ ℕ → -((2↑𝑁) − 1) = (1 − (2↑𝑁)))
33		df-neg 8198	. . . . . 6 ⊢ -1 = (0 − 1)
34		0cn 8016	. . . . . . 7 ⊢ 0 ∈ ℂ
35		pnpcan 8263	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ 0 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 0) − (1 + 1)) = (0 − 1))
36	1, 34, 1, 35	mp3an 1348	. . . . . 6 ⊢ ((1 + 0) − (1 + 1)) = (0 − 1)
37		1p0e1 9103	. . . . . . 7 ⊢ (1 + 0) = 1
38		1p1e2 9104	. . . . . . 7 ⊢ (1 + 1) = 2
39	37, 38	oveq12i 5934	. . . . . 6 ⊢ ((1 + 0) − (1 + 1)) = (1 − 2)
40	33, 36, 39	3eqtr2i 2223	. . . . 5 ⊢ -1 = (1 − 2)
41	40	a1i 9	. . . 4 ⊢ (𝑁 ∈ ℕ → -1 = (1 − 2))
42	32, 41	oveq12d 5940	. . 3 ⊢ (𝑁 ∈ ℕ → (-((2↑𝑁) − 1) / -1) = ((1 − (2↑𝑁)) / (1 − 2)))
43	26	div1d 8804	. . 3 ⊢ (𝑁 ∈ ℕ → (((2↑𝑁) − 1) / 1) = ((2↑𝑁) − 1))
44	30, 42, 43	3eqtr3d 2237	. 2 ⊢ (𝑁 ∈ ℕ → ((1 − (2↑𝑁)) / (1 − 2)) = ((2↑𝑁) − 1))
45	5, 20, 44	3eqtrd 2233	1 ⊢ (𝑁 ∈ ℕ → (1 σ (2↑(𝑁 − 1))) = ((2↑𝑁) − 1))

Colors of variables: wff set class

Syntax hints: → wi 4 ↔ wb 105 = wceq 1364 ∈ wcel 2167 class class class wbr 4033 (class class class)co 5922 ℂcc 7875 0cc0 7877 1c1 7878 + caddc 7880 − cmin 8195 -cneg 8196 # cap 8605 / cdiv 8696 ℕcn 8987 2c2 9038 ℕ₀cn0 9246 ℝ⁺crp 9725 ...cfz 10080 ↑cexp 10615 Σcsu 11502 ℙcprime 12251 ↑_𝑐ccxp 15066 σ csgm 15189

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7968 ax-resscn 7969 ax-1cn 7970 ax-1re 7971 ax-icn 7972 ax-addcl 7973 ax-addrcl 7974 ax-mulcl 7975 ax-mulrcl 7976 ax-addcom 7977 ax-mulcom 7978 ax-addass 7979 ax-mulass 7980 ax-distr 7981 ax-i2m1 7982 ax-0lt1 7983 ax-1rid 7984 ax-0id 7985 ax-rnegex 7986 ax-precex 7987 ax-cnre 7988 ax-pre-ltirr 7989 ax-pre-ltwlin 7990 ax-pre-lttrn 7991 ax-pre-apti 7992 ax-pre-ltadd 7993 ax-pre-mulgt0 7994 ax-pre-mulext 7995 ax-arch 7996 ax-caucvg 7997 ax-pre-suploc 7998 ax-addf 7999 ax-mulf 8000

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-disj 4011 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-isom 5267 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-of 6135 df-1st 6198 df-2nd 6199 df-recs 6363 df-irdg 6428 df-frec 6449 df-1o 6474 df-2o 6475 df-oadd 6478 df-er 6592 df-map 6709 df-pm 6710 df-en 6800 df-dom 6801 df-fin 6802 df-sup 7048 df-inf 7049 df-pnf 8061 df-mnf 8062 df-xr 8063 df-ltxr 8064 df-le 8065 df-sub 8197 df-neg 8198 df-reap 8599 df-ap 8606 df-div 8697 df-inn 8988 df-2 9046 df-3 9047 df-4 9048 df-n0 9247 df-xnn0 9310 df-z 9324 df-uz 9599 df-q 9691 df-rp 9726 df-xneg 9844 df-xadd 9845 df-ioo 9964 df-ico 9966 df-icc 9967 df-fz 10081 df-fzo 10215 df-fl 10345 df-mod 10400 df-seqfrec 10525 df-exp 10616 df-fac 10803 df-bc 10825 df-ihash 10853 df-shft 10965 df-cj 10992 df-re 10993 df-im 10994 df-rsqrt 11148 df-abs 11149 df-clim 11428 df-sumdc 11503 df-ef 11797 df-e 11798 df-dvds 11937 df-gcd 12086 df-prm 12252 df-pc 12430 df-rest 12888 df-topgen 12907 df-psmet 14075 df-xmet 14076 df-met 14077 df-bl 14078 df-mopn 14079 df-top 14210 df-topon 14223 df-bases 14255 df-ntr 14308 df-cn 14400 df-cnp 14401 df-tx 14465 df-cncf 14783 df-limced 14868 df-dvap 14869 df-relog 15067 df-rpcxp 15068 df-sgm 15190

This theorem is referenced by: (None)

W3C validator