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 Unicode version

Theorem nn0sumshdiglemB 38732

Description: Lemma for nn0sumshdig 38735 (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 11202	. . 3 $\/$
2		1t1e1 10723	. . . . . . . . . 10
3	2	eqcomi 2415	. . . . . . . . 9
4		simpl 455	. . . . . . . . 9 $/\$ #b
5		oveq2 6285	. . . . . . . . . . . . 13 #b ..^ ..^#b
6	5	eqcoms 2414	. . . . . . . . . . . 12 #b ..^ ..^#b
7		fveq2 5848	. . . . . . . . . . . . . . 15 #b #b
8		blen1 38696	. . . . . . . . . . . . . . 15 #b
9	7, 8	syl6eq 2459	. . . . . . . . . . . . . 14 #b
10	9	oveq2d 6293	. . . . . . . . . . . . 13 ..^#b ..^
11		fzo01 11931	. . . . . . . . . . . . 13 ..^
12	10, 11	syl6eq 2459	. . . . . . . . . . . 12 ..^#b
13	6, 12	sylan9eqr 2465	. . . . . . . . . . 11 $/\$ #b ..^
14	13	sumeq1d 13670	. . . . . . . . . 10 $/\$ #b ..^ digit digit
15		oveq2 6285	. . . . . . . . . . . . . 14 digit digit
16	15	oveq1d 6292	. . . . . . . . . . . . 13 digit digit
17	16	sumeq2sdv 13673	. . . . . . . . . . . 12 digit digit
18		c0ex 9619	. . . . . . . . . . . . 13
19		ax-1cn 9579	. . . . . . . . . . . . . 14
20	19, 19	mulcli 9630	. . . . . . . . . . . . 13
21		oveq1 6284	. . . . . . . . . . . . . . . 16 digit digit
22		1ex 9620	. . . . . . . . . . . . . . . . . 18
23	22	prid2 4080	. . . . . . . . . . . . . . . . 17
24		0dig2pr01 38722	. . . . . . . . . . . . . . . . 17 digit
25	23, 24	ax-mp 5	. . . . . . . . . . . . . . . 16 digit
26	21, 25	syl6eq 2459	. . . . . . . . . . . . . . 15 digit
27		oveq2 6285	. . . . . . . . . . . . . . . 16
28		2cn 10646	. . . . . . . . . . . . . . . . 17
29		exp0 12212	. . . . . . . . . . . . . . . . 17
30	28, 29	ax-mp 5	. . . . . . . . . . . . . . . 16
31	27, 30	syl6eq 2459	. . . . . . . . . . . . . . 15
32	26, 31	oveq12d 6295	. . . . . . . . . . . . . 14 digit
33	32	sumsn 13710	. . . . . . . . . . . . 13 $/\$ digit
34	18, 20, 33	mp2an 670	. . . . . . . . . . . 12 digit
35	17, 34	syl6eq 2459	. . . . . . . . . . 11 digit
36	35	adantr 463	. . . . . . . . . 10 $/\$ #b digit
37	14, 36	eqtrd 2443	. . . . . . . . 9 $/\$ #b ..^ digit
38	3, 4, 37	3eqtr4a 2469	. . . . . . . 8 $/\$ #b ..^ digit
39	38	ex 432	. . . . . . 7 #b ..^ digit
40	39	a1d 25	. . . . . 6 #b ..^digit #b ..^ digit
41	40	a1d 25	. . . . 5 #b ..^digit #b ..^ digit
42	41	a1d 25	. . . 4 #b ..^digit #b ..^ digit
43		eluzge2nn0 11165	. . . . . . . . 9
44		nn0ob 38631	. . . . . . . . . 10
45	44	bicomd 201	. . . . . . . . 9
46	43, 45	syl 17	. . . . . . . 8
47		blennngt2o2 38704	. . . . . . . . 9 $/\$ #b #b
48	47	ex 432	. . . . . . . 8 #b #b
49	46, 48	sylbid 215	. . . . . . 7 #b #b
50	49	imp 427	. . . . . 6 $/\$ #b #b
51		fveq2 5848	. . . . . . . . . . . . . 14 #b #b
52	51	eqeq1d 2404	. . . . . . . . . . . . 13 #b #b
53		id 22	. . . . . . . . . . . . . 14
54		oveq2 6285	. . . . . . . . . . . . . . . 16 digit digit
55	54	oveq1d 6292	. . . . . . . . . . . . . . 15 digit digit
56	55	sumeq2sdv 13673	. . . . . . . . . . . . . 14 ..^digit ..^digit
57	53, 56	eqeq12d 2424	. . . . . . . . . . . . 13 ..^digit ..^digit
58	52, 57	imbi12d 318	. . . . . . . . . . . 12 #b ..^digit #b ..^digit
59	58	rspcva 3157	. . . . . . . . . . 11 $/\$ #b ..^digit #b ..^digit
60		eqeq1 2406	. . . . . . . . . . . . . . . 16 #b #b #b #b
61		nncn 10583	. . . . . . . . . . . . . . . . . . . . 21
62	61	ad2antll 727	. . . . . . . . . . . . . . . . . . . 20 #b $/\$ $/\$ $/\$
63		blennn0elnn 38689	. . . . . . . . . . . . . . . . . . . . . . 23 #b
64	63	nncnd 10591	. . . . . . . . . . . . . . . . . . . . . 22 #b
65	64	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$ #b
66	65	ad2antrl 726	. . . . . . . . . . . . . . . . . . . 20 #b $/\$ $/\$ $/\$ #b
67		1cnd 9641	. . . . . . . . . . . . . . . . . . . 20 #b $/\$ $/\$ $/\$
68	62, 66, 67	addcan2d 9817	. . . . . . . . . . . . . . . . . . 19 #b $/\$ $/\$ $/\$ #b #b
69		eqcom 2411	. . . . . . . . . . . . . . . . . . . 20 #b #b
70		nnz 10926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
71	70	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$
72		fzval3 11919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ ..^
74	73	eqcomd 2410	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ ..^
75	74	sumeq1d 13670	. . . . . . . . . . . . . . . . . . . . . . . . . 26 #b $/\$ $/\$ $/\$ ..^ digit digit
76		nnnn0 10842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77		elnn0uz 11163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
78	76, 77	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
79	78	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$
80		2nn 10733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
81	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
82		elfzelz 11740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
83	82	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
84		nn0rp0 38616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
85	43, 84	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
86	85	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
87	86	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
88		digvalnn0 38711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ digit
89	81, 83, 87, 88	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ digit
90	89	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ digit
91	90	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ digit
92	91	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$ digit
93	92	nn0cnd 10894	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ $/\$ digit
94		2nn0 10852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
95	94	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
96		elfznn0 11824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	95, 96	nn0expcld 12374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	97	nn0cnd 10894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	98	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ $/\$
100	93, 99	mulcld 9645	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ $/\$ digit
101		oveq1 6284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 digit digit
102	101, 27	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 digit digit
103	30	oveq2i 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 digit digit
104	102, 103	syl6eq 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 digit digit
105	79, 100, 104	fsum1p 13717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 #b $/\$ $/\$ $/\$ digit digit digit
106	43	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
107	43, 44	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
108	107	biimparc 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
109		0dig2nn0o 38725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ digit
110	106, 108, 109	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ digit
111	110	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ digit
112	111	oveq1d 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ digit
113	112, 2	syl6eq 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ digit
114		1z 10934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
115	114	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$
116		0p1e1 10687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
117	116, 114	eqeltri 2486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
118	117	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$
119	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
120		elfzelz 11740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
121	120	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
122	43	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
123	122, 84	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
124	119, 121, 123, 88	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ digit
125	124	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 digit
126	125	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ digit
127	126	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 #b $/\$ $/\$ $/\$ digit
128	127	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ digit
129	128	nn0cnd 10894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$ digit
130		2cnd 10648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
131		elfznn 11766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
132	131	nnnn0d 10892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
133	116	oveq1i 6287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
134	132, 133	eleq2s 2510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
135	130, 134	expcld 12352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
136	135	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$
137	129, 136	mulcld 9645	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ $/\$ digit
138		oveq1 6284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 digit digit
139		oveq2 6285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
140	138, 139	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 digit digit
141	115, 118, 71, 137, 140	fsumshftm 13745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ digit digit
142	113, 141	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . . . 26 #b $/\$ $/\$ $/\$ digit digit digit
143	75, 105, 142	3eqtrd 2447	. . . . . . . . . . . . . . . . . . . . . . . . 25 #b $/\$ $/\$ $/\$ ..^ digit digit
144	143	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^ digit digit
145	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ ..^
146		elfzoelz 11857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
147	146	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ ..^
148		nn0rp0 38616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
149	148	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
150	149	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ ..^
151		digvalnn0 38711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ digit
152	145, 147, 150, 151	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ ..^ digit
153	152	nn0cnd 10894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ ..^ digit
154	153	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ ..^ digit
155	154	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 #b $/\$ $/\$ $/\$ ..^ digit
156	155	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ ..^ digit
157	94	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
158		elfzonn0 11897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
159	157, 158	nn0expcld 12374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
160	159	nn0cnd 10894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
161	160	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ ..^
162		2cnd 10648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ ..^
163	156, 161, 162	mulassd 9648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$ ..^ digit digit
164	163	eqcomd 2410	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ $/\$ ..^ digit digit
165	164	sumeq2dv 13672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ ..^digit ..^digit
166	165	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^digit ..^digit
167		0cn 9617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
168		pncan1 10023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
169	167, 168	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
170	169	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
171	170	oveq1d 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
172		fzoval 11858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
173	70, 172	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
174	171, 173	eqtr4d 2446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
175	174	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ ..^
176		simprlr 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 #b $/\$ $/\$ $/\$
177		elfznn0 11824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178	169	oveq1i 6287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
179	177, 178	eleq2s 2510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
180		dignn0flhalf 38730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ digit digit
181	176, 179, 180	syl2an 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ digit digit
182		eluzelz 11135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
183	182	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
184		nn0z 10927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
185		zob 37697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
186	182, 185	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
187	184, 186	syl5ibr 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
188	187	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
189	183, 188	jca 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
190	189	ancoms 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
191	190	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 #b $/\$ $/\$ $/\$ $/\$
192	191	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 #b $/\$ $/\$ $/\$ $/\$ $/\$
193		zofldiv2 38639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
194	192, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 #b $/\$ $/\$ $/\$ $/\$
195	194	oveq2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 #b $/\$ $/\$ $/\$ $/\$ digit digit
196	181, 195	eqtrd 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$ digit digit
197		2cnd 10648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
198	197, 179	expp1d 12353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
199	198	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 #b $/\$ $/\$ $/\$ $/\$
200	196, 199	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 #b $/\$ $/\$ $/\$ $/\$ digit digit
201	175, 200	sumeq12dv 13675	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 #b $/\$ $/\$ $/\$ digit ..^digit
202	201	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^digit $/\$ #b $/\$ $/\$ $/\$ digit ..^digit
203		oveq1 6284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 digit digit
204		oveq2 6285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
205	203, 204	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 digit digit
206	205	cbvsumv 13665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^digit ..^digit
207	206	eqeq2i 2420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^digit ..^digit
208	207	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^digit ..^digit
209	208	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^digit
210	209	oveq1d 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^digit
211		fzofi 12123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^
213		2cnd 10648	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^digit $/\$ #b $/\$ $/\$ $/\$
214	160	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ ..^
215	153, 214	mulcld 9645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ ..^ digit
216	215	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ ..^ digit
217	216	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ ..^ digit
218	217	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^ digit
219	218	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^digit $/\$ #b $/\$ $/\$ $/\$ $/\$ ..^ digit
220	212, 213, 219	fsummulc1 13749	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^digit ..^digit
221	210, 220	eqtrd 2443	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^digit
222	166, 202, 221	3eqtr4d 2453	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^digit $/\$ #b $/\$ $/\$ $/\$ digit
223	222	oveq2d 6293	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^digit $/\$ #b $/\$ $/\$ $/\$ digit
224		eluzelcn 11137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
225		peano2cnm 9920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
226	224, 225	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
227		2cnd 10648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
228		2ne0 10668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
229	228	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
230	226, 227, 229	3jca 1177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
231	230	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
232		divcan1 10256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
233	231, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
234	233	oveq2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
235		1cnd 9641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
236	235, 224	jca 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
237	236	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
238		pncan3 9863	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
239	237, 238	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
240	234, 239	eqtrd 2443	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
241	240	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
242	241	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^digit $/\$ #b $/\$ $/\$ $/\$
243	144, 223, 242	3eqtrrd 2448	. . . . . . . . . . . . . . . . . . . . . . 23 ..^digit $/\$ #b $/\$ $/\$ $/\$ ..^ digit
244	243	ex 432	. . . . . . . . . . . . . . . . . . . . . 22 ..^digit #b $/\$ $/\$ $/\$ ..^ digit
245	244	imim2i 16	. . . . . . . . . . . . . . . . . . . . 21 #b ..^digit #b #b $/\$ $/\$ $/\$ ..^ digit
246	245	com13 80	. . . . . . . . . . . . . . . . . . . 20 #b $/\$ $/\$ $/\$ #b #b ..^digit ..^ digit
247	69, 246	syl5bi 217	. . . . . . . . . . . . . . . . . . 19 #b $/\$ $/\$ $/\$ #b #b ..^digit ..^ digit
248	68, 247	sylbid 215	. . . . . . . . . . . . . . . . . 18 #b $/\$ $/\$ $/\$ #b #b ..^digit ..^ digit
249	248	ex 432	. . . . . . . . . . . . . . . . 17 #b $/\$ $/\$ #b #b ..^digit ..^ digit
250	249	com23 78	. . . . . . . . . . . . . . . 16 #b #b $/\$ $/\$ #b ..^digit ..^ digit
251	60, 250	sylbid 215	. . . . . . . . . . . . . . 15 #b #b #b $/\$ $/\$ #b ..^digit ..^ digit
252	251	com23 78	. . . . . . . . . . . . . 14 #b $/\$ $/\$ #b #b #b ..^digit ..^ digit
253	252	com14 88	. . . . . . . . . . . . 13 #b ..^digit $/\$ $/\$ #b #b #b ..^ digit
254	253	exp4c 606	. . . . . . . . . . . 12 #b ..^digit #b #b #b ..^ digit
255	254	com35 90	. . . . . . . . . . 11 #b ..^digit #b #b #b ..^ digit
256	59, 255	syl 17	. . . . . . . . . 10 $/\$ #b ..^digit #b #b #b ..^ digit
257	256	ex 432	. . . . . . . . 9 #b ..^digit #b #b #b ..^ digit
258	257	pm2.43a 48	. . . . . . . 8 #b ..^digit #b #b #b ..^ digit
259	258	com25 91	. . . . . . 7 #b #b #b ..^digit #b ..^ digit
260	259	impcom 428	. . . . . 6 $/\$ #b #b #b ..^digit #b ..^ digit
261	50, 260	mpd 15	. . . . 5 $/\$ #b ..^digit #b ..^ digit
262	261	ex 432	. . . 4 #b ..^digit #b ..^ digit
263	42, 262	jaoi 377	. . 3 $\/$ #b ..^digit #b ..^ digit
264	1, 263	sylbi 195	. 2 #b ..^digit #b ..^ digit
265	264	imp31 430	1 $/\$ $/\$ #b ..^digit #b ..^ digit

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wne 2598

wral 2753

cvv 3058

csn 3971

cpr 3973

cfv 5568 (class class class)co 6277

cfn 7553

cc 9519

cc0 9521

c1 9522

caddc 9524

cmul 9526

cpnf 9654

cmin 9840

cdiv 10246

cn 10575

c2 10625

cn0 10835

cz 10904

cuz 11126

cico 11583

cfz 11724 ..^cfzo 11852

cfl 11962

cexp 12208

csu 13655 #bcblen 38681 digitcdig 38707

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6573 ax-inf2 8090 ax-cnex 9577 ax-resscn 9578 ax-1cn 9579 ax-icn 9580 ax-addcl 9581 ax-addrcl 9582 ax-mulcl 9583 ax-mulrcl 9584 ax-mulcom 9585 ax-addass 9586 ax-mulass 9587 ax-distr 9588 ax-i2m1 9589 ax-1ne0 9590 ax-1rid 9591 ax-rnegex 9592 ax-rrecex 9593 ax-cnre 9594 ax-pre-lttri 9595 ax-pre-lttrn 9596 ax-pre-ltadd 9597 ax-pre-mulgt0 9598 ax-pre-sup 9599 ax-addf 9600 ax-mulf 9601

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-fal 1411 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2758 df-rex 2759 df-reu 2760 df-rmo 2761 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-pss 3429 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-tp 3976 df-op 3978 df-uni 4191 df-int 4227 df-iun 4272 df-iin 4273 df-br 4395 df-opab 4453 df-mpt 4454 df-tr 4489 df-eprel 4733 df-id 4737 df-po 4743 df-so 4744 df-fr 4781 df-se 4782 df-we 4783 df-xp 4828 df-rel 4829 df-cnv 4830 df-co 4831 df-dm 4832 df-rn 4833 df-res 4834 df-ima 4835 df-pred 5366 df-ord 5412 df-on 5413 df-lim 5414 df-suc 5415 df-iota 5532 df-fun 5570 df-fn 5571 df-f 5572 df-f1 5573 df-fo 5574 df-f1o 5575 df-fv 5576 df-isom 5577 df-riota 6239 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-of 6520 df-om 6683 df-1st 6783 df-2nd 6784 df-supp 6902 df-wrecs 7012 df-recs 7074 df-rdg 7112 df-1o 7166 df-2o 7167 df-oadd 7170 df-er 7347 df-map 7458 df-pm 7459 df-ixp 7507 df-en 7554 df-dom 7555 df-sdom 7556 df-fin 7557 df-fsupp 7863 df-fi 7904 df-sup 7934 df-oi 7968 df-card 8351 df-cda 8579 df-pnf 9659 df-mnf 9660 df-xr 9661 df-ltxr 9662 df-le 9663 df-sub 9842 df-neg 9843 df-div 10247 df-nn 10576 df-2 10634 df-3 10635 df-4 10636 df-5 10637 df-6 10638 df-7 10639 df-8 10640 df-9 10641 df-10 10642 df-n0 10836 df-z 10905 df-dec 11019 df-uz 11127 df-q 11227 df-rp 11265 df-xneg 11370 df-xadd 11371 df-xmul 11372 df-ioo 11585 df-ioc 11586 df-ico 11587 df-icc 11588 df-fz 11725 df-fzo 11853 df-fl 11964 df-mod 12033 df-seq 12150 df-exp 12209 df-fac 12396 df-bc 12423 df-hash 12451 df-shft 13047 df-cj 13079 df-re 13080 df-im 13081 df-sqrt 13215 df-abs 13216 df-limsup 13441 df-clim 13458 df-rlim 13459 df-sum 13656 df-ef 14010 df-sin 14012 df-cos 14013 df-pi 14015 df-dvds 14194 df-struct 14841 df-ndx 14842 df-slot 14843 df-base 14844 df-sets 14845 df-ress 14846 df-plusg 14920 df-mulr 14921 df-starv 14922 df-sca 14923 df-vsca 14924 df-ip 14925 df-tset 14926 df-ple 14927 df-ds 14929 df-unif 14930 df-hom 14931 df-cco 14932 df-rest 15035 df-topn 15036 df-0g 15054 df-gsum 15055 df-topgen 15056 df-pt 15057 df-prds 15060 df-xrs 15114 df-qtop 15119 df-imas 15120 df-xps 15122 df-mre 15198 df-mrc 15199 df-acs 15201 df-mgm 16194 df-sgrp 16233 df-mnd 16243 df-submnd 16289 df-mulg 16382 df-cntz 16677 df-cmn 17122 df-psmet 18729 df-xmet 18730 df-met 18731 df-bl 18732 df-mopn 18733 df-fbas 18734 df-fg 18735 df-cnfld 18739 df-top 19689 df-bases 19691 df-topon 19692 df-topsp 19693 df-cld 19810 df-ntr 19811 df-cls 19812 df-nei 19890 df-lp 19928 df-perf 19929 df-cn 20019 df-cnp 20020 df-haus 20107 df-tx 20353 df-hmeo 20546 df-fil 20637 df-fm 20729 df-flim 20730 df-flf 20731 df-xms 21113 df-ms 21114 df-tms 21115 df-cncf 21672 df-limc 22560 df-dv 22561 df-log 23234 df-cxp 23235 df-logb 23430 df-blen 38682 df-dig 38708

This theorem is referenced by: nn0sumshdiglem1 38733

W3C validator