nn0sumshdiglemB - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > nn0sumshdiglemB		Structured version Visualization version Unicode version

Theorem nn0sumshdiglemB 40800

Description: Lemma for nn0sumshdig 40803 (induction step, odd multiplicant). (Contributed by AV, 7-Jun-2020.)

**Assertion**
Ref	Expression
nn0sumshdiglemB	$/\$ $/\$ #b ..^digit #b ..^ digit

Distinct variable group:

Proof of Theorem nn0sumshdiglemB Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elnn1uz2 11269	. . 3 $\/$
2		1t1e1 10791	. . . . . . . . 9
3	2	eqcomi 2471	. . . . . . . 8
4		simpl 463	. . . . . . . 8 $/\$ #b
5		oveq2 6328	. . . . . . . . . . . 12 #b ..^ ..^#b
6	5	eqcoms 2470	. . . . . . . . . . 11 #b ..^ ..^#b
7		fveq2 5892	. . . . . . . . . . . . . 14 #b #b
8		blen1 40764	. . . . . . . . . . . . . 14 #b
9	7, 8	syl6eq 2512	. . . . . . . . . . . . 13 #b
10	9	oveq2d 6336	. . . . . . . . . . . 12 ..^#b ..^
11		fzo01 12032	. . . . . . . . . . . 12 ..^
12	10, 11	syl6eq 2512	. . . . . . . . . . 11 ..^#b
13	6, 12	sylan9eqr 2518	. . . . . . . . . 10 $/\$ #b ..^
14	13	sumeq1d 13822	. . . . . . . . 9 $/\$ #b ..^ digit digit
15		oveq2 6328	. . . . . . . . . . . . 13 digit digit
16	15	oveq1d 6335	. . . . . . . . . . . 12 digit digit
17	16	sumeq2sdv 13825	. . . . . . . . . . 11 digit digit
18		c0ex 9668	. . . . . . . . . . . 12
19		ax-1cn 9628	. . . . . . . . . . . . 13
20	19, 19	mulcli 9679	. . . . . . . . . . . 12
21		oveq1 6327	. . . . . . . . . . . . . . 15 digit digit
22		1ex 9669	. . . . . . . . . . . . . . . . 17
23	22	prid2 4094	. . . . . . . . . . . . . . . 16
24		0dig2pr01 40790	. . . . . . . . . . . . . . . 16 digit
25	23, 24	ax-mp 5	. . . . . . . . . . . . . . 15 digit
26	21, 25	syl6eq 2512	. . . . . . . . . . . . . 14 digit
27		oveq2 6328	. . . . . . . . . . . . . . 15
28		2cn 10713	. . . . . . . . . . . . . . . 16
29		exp0 12314	. . . . . . . . . . . . . . . 16
30	28, 29	ax-mp 5	. . . . . . . . . . . . . . 15
31	27, 30	syl6eq 2512	. . . . . . . . . . . . . 14
32	26, 31	oveq12d 6338	. . . . . . . . . . . . 13 digit
33	32	sumsn 13862	. . . . . . . . . . . 12 $/\$ digit
34	18, 20, 33	mp2an 683	. . . . . . . . . . 11 digit
35	17, 34	syl6eq 2512	. . . . . . . . . 10 digit
36	35	adantr 471	. . . . . . . . 9 $/\$ #b digit
37	14, 36	eqtrd 2496	. . . . . . . 8 $/\$ #b ..^ digit
38	3, 4, 37	3eqtr4a 2522	. . . . . . 7 $/\$ #b ..^ digit
39	38	ex 440	. . . . . 6 #b ..^ digit
40	39	a1d 26	. . . . 5 #b ..^digit #b ..^ digit
41	40	2a1d 27	. . . 4 #b ..^digit #b ..^ digit
42		eluzge2nn0 11232	. . . . . . . . 9
43		nn0ob 40699	. . . . . . . . . 10
44	43	bicomd 206	. . . . . . . . 9
45	42, 44	syl 17	. . . . . . . 8
46		blennngt2o2 40772	. . . . . . . . 9 $/\$ #b #b
47	46	ex 440	. . . . . . . 8 #b #b
48	45, 47	sylbid 223	. . . . . . 7 #b #b
49	48	imp 435	. . . . . 6 $/\$ #b #b
50		fveq2 5892	. . . . . . . . . . . . . 14 #b #b
51	50	eqeq1d 2464	. . . . . . . . . . . . 13 #b #b
52		id 22	. . . . . . . . . . . . . 14
53		oveq2 6328	. . . . . . . . . . . . . . . 16 digit digit
54	53	oveq1d 6335	. . . . . . . . . . . . . . 15 digit digit
55	54	sumeq2sdv 13825	. . . . . . . . . . . . . 14 ..^digit ..^digit
56	52, 55	eqeq12d 2477	. . . . . . . . . . . . 13 ..^digit ..^digit
57	51, 56	imbi12d 326	. . . . . . . . . . . 12 #b ..^digit #b ..^digit
58	57	rspcva 3160	. . . . . . . . . . 11 $/\$ #b ..^digit #b ..^digit
59		eqeq1 2466	. . . . . . . . . . . . . . . 16 #b #b #b #b
60		nncn 10650	. . . . . . . . . . . . . . . . . . . . 21
61	60	ad2antll 740	. . . . . . . . . . . . . . . . . . . 20 #b $/\$ $/\$ $/\$
62		blennn0elnn 40757	. . . . . . . . . . . . . . . . . . . . . . 23 #b
63	62	nncnd 10658	. . . . . . . . . . . . . . . . . . . . . 22 #b
64	63	adantr 471	. . . . . . . . . . . . . . . . . . . . 21 $/\$ #b
65	64	ad2antrl 739	. . . . . . . . . . . . . . . . . . . 20 #b $/\$ $/\$ $/\$ #b
66		1cnd 9690	. . . . . . . . . . . . . . . . . . . 20 #b $/\$ $/\$ $/\$
67	61, 65, 66	addcan2d 9868	. . . . . . . . . . . . . . . . . . 19 #b $/\$ $/\$ $/\$ #b #b
68		eqcom 2469	. . . . . . . . . . . . . . . . . . . 20 #b #b
69		nnz 10993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
70	69	ad2antll 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$
71		fzval3 12020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
72	70, 71	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ ..^
73	72	eqcomd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ ..^
74	73	sumeq1d 13822	. . . . . . . . . . . . . . . . . . . . . . . . . 26 #b $/\$ $/\$ $/\$ ..^ digit digit
75		nnnn0 10910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
76		elnn0uz 11230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77	75, 76	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
78	77	ad2antll 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$
79		2nn 10801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
80	79	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
81		elfzelz 11835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	81	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
83		nn0rp0 11774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
84	42, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
85	84	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
86	85	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
87		digvalnn0 40779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ digit
88	80, 82, 86, 87	syl3anc 1276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ digit
89	88	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ digit
90	89	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ digit
91	90	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$ digit
92	91	nn0cnd 10961	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ $/\$ digit
93		2nn0 10920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
94	93	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
95		elfznn0 11922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
96	94, 95	nn0expcld 12476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
97	96	nn0cnd 10961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98	97	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ $/\$
99	92, 98	mulcld 9694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ $/\$ digit
100		oveq1 6327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 digit digit
101	100, 27	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 digit digit
102	30	oveq2i 6331	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 digit digit
103	101, 102	syl6eq 2512	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 digit digit
104	78, 99, 103	fsum1p 13869	. . . . . . . . . . . . . . . . . . . . . . . . . 26 #b $/\$ $/\$ $/\$ digit digit digit
105	42	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
106	42, 43	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
107	106	biimparc 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
108		0dig2nn0o 40793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ digit
109	105, 107, 108	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ digit
110	109	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ digit
111	110	oveq1d 6335	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ digit
112	111, 2	syl6eq 2512	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ digit
113		1z 11001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$
115		0p1e1 10754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
116	115, 113	eqeltri 2536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
117	116	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$
118	79	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
119		elfzelz 11835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
120	119	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
121	42	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
122	121, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
123	118, 120, 122, 87	syl3anc 1276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ digit
124	123	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 digit
125	124	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ digit
126	125	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 #b $/\$ $/\$ $/\$ digit
127	126	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ digit
128	127	nn0cnd 10961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$ digit
129		2cnd 10715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
130		elfznn 11863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
131	130	nnnn0d 10959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
132	115	oveq1i 6330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
133	131, 132	eleq2s 2558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
134	129, 133	expcld 12454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
135	134	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$
136	128, 135	mulcld 9694	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ $/\$ digit
137		oveq1 6327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 digit digit
138		oveq2 6328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
139	137, 138	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 digit digit
140	114, 117, 70, 136, 139	fsumshftm 13897	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ digit digit
141	112, 140	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . . . . . 26 #b $/\$ $/\$ $/\$ digit digit digit
142	74, 104, 141	3eqtrd 2500	. . . . . . . . . . . . . . . . . . . . . . . . 25 #b $/\$ $/\$ $/\$ ..^ digit digit
143	142	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^ digit digit
144	79	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ ..^
145		elfzoelz 11957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
146	145	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ ..^
147		nn0rp0 11774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
148	147	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
149	148	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ ..^
150		digvalnn0 40779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ digit
151	144, 146, 149, 150	syl3anc 1276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ ..^ digit
152	151	nn0cnd 10961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ ..^ digit
153	152	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ ..^ digit
154	153	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 #b $/\$ $/\$ $/\$ ..^ digit
155	154	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ ..^ digit
156	93	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
157		elfzonn0 11997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
158	156, 157	nn0expcld 12476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
159	158	nn0cnd 10961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
160	159	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ ..^
161		2cnd 10715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ ..^
162	155, 160, 161	mulassd 9697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$ ..^ digit digit
163	162	eqcomd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ $/\$ ..^ digit digit
164	163	sumeq2dv 13824	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ ..^digit ..^digit
165	164	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^digit ..^digit
166		0cn 9666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
167		pncan1 10076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
168	166, 167	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
170	169	oveq1d 6335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
171		fzoval 11958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
172	69, 171	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
173	170, 172	eqtr4d 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
174	173	ad2antll 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ ..^
175		simprlr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 #b $/\$ $/\$ $/\$
176		elfznn0 11922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177	168	oveq1i 6330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178	176, 177	eleq2s 2558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179		dignn0flhalf 40798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ digit digit
180	175, 178, 179	syl2an 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ digit digit
181		eluzelz 11202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
182	181	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
183		nn0z 10994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
184		zob 38898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
185	181, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
186	183, 185	syl5ibr 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
187	186	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
188	182, 187	jca 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
189	188	ancoms 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
190	189	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 #b $/\$ $/\$ $/\$ $/\$
191	190	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 #b $/\$ $/\$ $/\$ $/\$ $/\$
192		zofldiv2 40707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
193	191, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 #b $/\$ $/\$ $/\$ $/\$
194	193	oveq2d 6336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ digit digit
195	180, 194	eqtrd 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$ digit digit
196		2cnd 10715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
197	196, 178	expp1d 12455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
198	197	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$
199	195, 198	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ $/\$ digit digit
200	174, 199	sumeq12dv 13827	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ digit ..^digit
201	200	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^digit $/\$ #b $/\$ $/\$ $/\$ digit ..^digit
202		oveq1 6327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 digit digit
203		oveq2 6328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
204	202, 203	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 digit digit
205	204	cbvsumv 13817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^digit ..^digit
206	205	eqeq2i 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^digit ..^digit
207	206	biimpi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^digit ..^digit
208	207	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^digit
209	208	oveq1d 6335	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^digit
210		fzofi 12225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
211	210	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^
212		2cnd 10715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^digit $/\$ #b $/\$ $/\$ $/\$
213	159	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ ..^
214	152, 213	mulcld 9694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ ..^ digit
215	214	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ ..^ digit
216	215	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ ..^ digit
217	216	ad2antll 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^ digit
218	217	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^digit $/\$ #b $/\$ $/\$ $/\$ $/\$ ..^ digit
219	211, 212, 218	fsummulc1 13901	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^digit ..^digit
220	209, 219	eqtrd 2496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^digit
221	165, 201, 220	3eqtr4d 2506	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^digit $/\$ #b $/\$ $/\$ $/\$ digit
222	221	oveq2d 6336	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^digit $/\$ #b $/\$ $/\$ $/\$ digit
223		eluzelcn 11204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
224		peano2cnm 9971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
225	223, 224	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
226		2cnd 10715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
227		2ne0 10735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
228	227	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
229	225, 226, 228	3jca 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
230	229	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
231		divcan1 10312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
232	230, 231	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
233	232	oveq2d 6336	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
234		1cnd 9690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
235	234, 223	jca 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
236	235	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
237		pncan3 9914	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
238	236, 237	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
239	233, 238	eqtrd 2496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
240	239	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
241	240	ad2antll 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^digit $/\$ #b $/\$ $/\$ $/\$
242	143, 222, 241	3eqtrrd 2501	. . . . . . . . . . . . . . . . . . . . . . 23 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^ digit
243	242	ex 440	. . . . . . . . . . . . . . . . . . . . . 22 ..^digit #b $/\$ $/\$ $/\$ ..^ digit
244	243	imim2i 16	. . . . . . . . . . . . . . . . . . . . 21 #b ..^digit #b #b $/\$ $/\$ $/\$ ..^ digit
245	244	com13 83	. . . . . . . . . . . . . . . . . . . 20 #b $/\$ $/\$ $/\$ #b #b ..^digit ..^ digit
246	68, 245	syl5bi 225	. . . . . . . . . . . . . . . . . . 19 #b $/\$ $/\$ $/\$ #b #b ..^digit ..^ digit
247	67, 246	sylbid 223	. . . . . . . . . . . . . . . . . 18 #b $/\$ $/\$ $/\$ #b #b ..^digit ..^ digit
248	247	ex 440	. . . . . . . . . . . . . . . . 17 #b $/\$ $/\$ #b #b ..^digit ..^ digit
249	248	com23 81	. . . . . . . . . . . . . . . 16 #b #b $/\$ $/\$ #b ..^digit ..^ digit
250	59, 249	sylbid 223	. . . . . . . . . . . . . . 15 #b #b #b $/\$ $/\$ #b ..^digit ..^ digit
251	250	com23 81	. . . . . . . . . . . . . 14 #b $/\$ $/\$ #b #b #b ..^digit ..^ digit
252	251	com14 91	. . . . . . . . . . . . 13 #b ..^digit $/\$ $/\$ #b #b #b ..^ digit
253	252	exp4c 617	. . . . . . . . . . . 12 #b ..^digit #b #b #b ..^ digit
254	253	com35 93	. . . . . . . . . . 11 #b ..^digit #b #b #b ..^ digit
255	58, 254	syl 17	. . . . . . . . . 10 $/\$ #b ..^digit #b #b #b ..^ digit
256	255	ex 440	. . . . . . . . 9 #b ..^digit #b #b #b ..^ digit
257	256	pm2.43a 51	. . . . . . . 8 #b ..^digit #b #b #b ..^ digit
258	257	com25 94	. . . . . . 7 #b #b #b ..^digit #b ..^ digit
259	258	impcom 436	. . . . . 6 $/\$ #b #b #b ..^digit #b ..^ digit
260	49, 259	mpd 15	. . . . 5 $/\$ #b ..^digit #b ..^ digit
261	260	ex 440	. . . 4 #b ..^digit #b ..^ digit
262	41, 261	jaoi 385	. . 3 $\/$ #b ..^digit #b ..^ digit
263	1, 262	sylbi 200	. 2 #b ..^digit #b ..^ digit
264	263	imp31 438	1 $/\$ $/\$ #b ..^digit #b ..^ digit

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $\/$ wo 374 $/\$ wa 375 $/\$ w3a 991

wceq 1455

wcel 1898

wne 2633

wral 2749

cvv 3057

csn 3980

cpr 3982

cfv 5605 (class class class)co 6320

cfn 7600

cc 9568

cc0 9570

c1 9571

caddc 9573

cmul 9575

cpnf 9703

cmin 9891

cdiv 10302

cn 10642

c2 10692

cn0 10903

cz 10971

cuz 11193

cico 11671

cfz 11819 ..^cfzo 11952

cfl 12064

cexp 12310

csu 13807 #bcblen 40749 digitcdig 40775

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4531 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615 ax-inf2 8177 ax-cnex 9626 ax-resscn 9627 ax-1cn 9628 ax-icn 9629 ax-addcl 9630 ax-addrcl 9631 ax-mulcl 9632 ax-mulrcl 9633 ax-mulcom 9634 ax-addass 9635 ax-mulass 9636 ax-distr 9637 ax-i2m1 9638 ax-1ne0 9639 ax-1rid 9640 ax-rnegex 9641 ax-rrecex 9642 ax-cnre 9643 ax-pre-lttri 9644 ax-pre-lttrn 9645 ax-pre-ltadd 9646 ax-pre-mulgt0 9647 ax-pre-sup 9648 ax-addf 9649 ax-mulf 9650

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-fal 1461 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-iin 4295 df-br 4419 df-opab 4478 df-mpt 4479 df-tr 4514 df-eprel 4767 df-id 4771 df-po 4777 df-so 4778 df-fr 4815 df-se 4816 df-we 4817 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-pred 5403 df-ord 5449 df-on 5450 df-lim 5451 df-suc 5452 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-isom 5614 df-riota 6282 df-ov 6323 df-oprab 6324 df-mpt2 6325 df-of 6563 df-om 6725 df-1st 6825 df-2nd 6826 df-supp 6947 df-wrecs 7059 df-recs 7121 df-rdg 7159 df-1o 7213 df-2o 7214 df-oadd 7217 df-er 7394 df-map 7505 df-pm 7506 df-ixp 7554 df-en 7601 df-dom 7602 df-sdom 7603 df-fin 7604 df-fsupp 7915 df-fi 7956 df-sup 7987 df-inf 7988 df-oi 8056 df-card 8404 df-cda 8629 df-pnf 9708 df-mnf 9709 df-xr 9710 df-ltxr 9711 df-le 9712 df-sub 9893 df-neg 9894 df-div 10303 df-nn 10643 df-2 10701 df-3 10702 df-4 10703 df-5 10704 df-6 10705 df-7 10706 df-8 10707 df-9 10708 df-10 10709 df-n0 10904 df-z 10972 df-dec 11086 df-uz 11194 df-q 11299 df-rp 11337 df-xneg 11443 df-xadd 11444 df-xmul 11445 df-ioo 11673 df-ioc 11674 df-ico 11675 df-icc 11676 df-fz 11820 df-fzo 11953 df-fl 12066 df-mod 12135 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13185 df-cj 13217 df-re 13218 df-im 13219 df-sqrt 13353 df-abs 13354 df-limsup 13581 df-clim 13607 df-rlim 13608 df-sum 13808 df-ef 14176 df-sin 14178 df-cos 14179 df-pi 14181 df-dvds 14361 df-struct 15178 df-ndx 15179 df-slot 15180 df-base 15181 df-sets 15182 df-ress 15183 df-plusg 15258 df-mulr 15259 df-starv 15260 df-sca 15261 df-vsca 15262 df-ip 15263 df-tset 15264 df-ple 15265 df-ds 15267 df-unif 15268 df-hom 15269 df-cco 15270 df-rest 15376 df-topn 15377 df-0g 15395 df-gsum 15396 df-topgen 15397 df-pt 15398 df-prds 15401 df-xrs 15455 df-qtop 15461 df-imas 15462 df-xps 15465 df-mre 15547 df-mrc 15548 df-acs 15550 df-mgm 16543 df-sgrp 16582 df-mnd 16592 df-submnd 16638 df-mulg 16731 df-cntz 17026 df-cmn 17487 df-psmet 19017 df-xmet 19018 df-met 19019 df-bl 19020 df-mopn 19021 df-fbas 19022 df-fg 19023 df-cnfld 19026 df-top 19976 df-bases 19977 df-topon 19978 df-topsp 19979 df-cld 20089 df-ntr 20090 df-cls 20091 df-nei 20169 df-lp 20207 df-perf 20208 df-cn 20298 df-cnp 20299 df-haus 20386 df-tx 20632 df-hmeo 20825 df-fil 20916 df-fm 21008 df-flim 21009 df-flf 21010 df-xms 21390 df-ms 21391 df-tms 21392 df-cncf 21965 df-limc 22877 df-dv 22878 df-log 23562 df-cxp 23563 df-logb 23758 df-blen 40750 df-dig 40776

This theorem is referenced by: nn0sumshdiglem1 40801

W3C validator