chtublem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > chtublem		Unicode version

Theorem chtublem 16214

Description: Lemma for chtqub 16215. (Contributed by Mario Carneiro, 13-Mar-2014.)

**Assertion**
Ref	Expression
chtublem

Proof of Theorem chtublem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2nn 9470	. . . . . 6
2		nnmulcl 9327	. . . . . 6 $/\$
3	1, 2	mpan 428	. . . . 5
4		nnq 10042	. . . . 5
5	3, 4	syl 14	. . . 4
6		1z 9674	. . . . 5
7		zq 10035	. . . . 5
8	6, 7	ax-mp 5	. . . 4
9		qsubcl 10047	. . . 4 $/\$
10	5, 8, 9	sylancl 417	. . 3
11		chtqcl 16163	. . 3
12	10, 11	syl 14	. 2
13		nnq 10042	. . . 4
14		chtqcl 16163	. . . 4
15	13, 14	syl 14	. . 3
16		nnnn0 9574	. . . . . . 7
17		2m1e1 9424	. . . . . . . . . . 11
18	17	oveq2i 6096	. . . . . . . . . 10
19	3	nncnd 9320	. . . . . . . . . . . 12
20		2cn 9377	. . . . . . . . . . . . 13
21		ax-1cn 8272	. . . . . . . . . . . . 13
22		subsub 8557	. . . . . . . . . . . . 13 $/\$ $/\$
23	20, 21, 22	mp3an23 1370	. . . . . . . . . . . 12
24	19, 23	syl 14	. . . . . . . . . . 11
25		nncn 9314	. . . . . . . . . . . . . 14
26		subdi 8713	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	20, 21, 26	mp3an13 1369	. . . . . . . . . . . . . 14
28	25, 27	syl 14	. . . . . . . . . . . . 13
29		2t1e2 9460	. . . . . . . . . . . . . 14
30	29	oveq2i 6096	. . . . . . . . . . . . 13
31	28, 30	eqtrdi 2287	. . . . . . . . . . . 12
32	31	oveq1d 6100	. . . . . . . . . . 11
33	24, 32	eqtr4d 2274	. . . . . . . . . 10
34	18, 33	eqtr3id 2285	. . . . . . . . 9
35		2nn0 9584	. . . . . . . . . . 11
36		nnm1nn0 9608	. . . . . . . . . . 11
37		nn0mulcl 9603	. . . . . . . . . . 11 $/\$
38	35, 36, 37	sylancr 418	. . . . . . . . . 10
39		nn0p1nn 9606	. . . . . . . . . 10
40	38, 39	syl 14	. . . . . . . . 9
41	34, 40	eqeltrd 2315	. . . . . . . 8
42		nnnn0 9574	. . . . . . . 8
43	41, 42	syl 14	. . . . . . 7
44		1re 8325	. . . . . . . . . . 11
45	44	a1i 9	. . . . . . . . . 10
46		nnre 9313	. . . . . . . . . 10
47		nnge1 9329	. . . . . . . . . 10
48	45, 46, 46, 47	leadd2dd 8889	. . . . . . . . 9
49	25	2timesd 9552	. . . . . . . . 9
50	48, 49	breqtrrd 4158	. . . . . . . 8
51	3	nnred 9319	. . . . . . . . 9
52		leaddsub 8767	. . . . . . . . 9 $/\$ $/\$
53	46, 45, 51, 52	syl3anc 1278	. . . . . . . 8
54	50, 53	mpbid 147	. . . . . . 7
55		elfz2nn0 10529	. . . . . . 7 $/\$ $/\$
56	16, 43, 54, 55	syl3anbrc 1212	. . . . . 6
57		bccl2 11220	. . . . . 6
58	56, 57	syl 14	. . . . 5
59	58	nnrpd 10105	. . . 4
60	59	relogcld 16034	. . 3
61	15, 60	readdcld 8355	. 2
62		4re 9383	. . . . . 6
63		4pos 9403	. . . . . 6
64	62, 63	elrpii 10067	. . . . 5
65		relogcl 16013	. . . . 5
66	64, 65	ax-mp 5	. . . 4
67	36	nn0red 9625	. . . 4
68		remulcl 8307	. . . 4 $/\$
69	66, 67, 68	sylancr 418	. . 3
70	15, 69	readdcld 8355	. 2
71		iftrue 3645	. . . . . . . . . . . 12
72	71	adantl 277	. . . . . . . . . . 11 $/\$ $/\$
73		simpr 110	. . . . . . . . . . . . . . . 16 $/\$
74	58	adantr 276	. . . . . . . . . . . . . . . 16 $/\$
75	73, 74	pccld 13099	. . . . . . . . . . . . . . 15 $/\$
76		nn0addge1 9613	. . . . . . . . . . . . . . 15 $/\$
77	44, 75, 76	sylancr 418	. . . . . . . . . . . . . 14 $/\$
78		iftrue 3645	. . . . . . . . . . . . . . . 16
79	78	oveq1d 6100	. . . . . . . . . . . . . . 15
80	79	breq2d 4142	. . . . . . . . . . . . . 14
81	77, 80	syl5ibrcom 157	. . . . . . . . . . . . 13 $/\$
82	81	adantr 276	. . . . . . . . . . . 12 $/\$ $/\$
83		prmnn 12904	. . . . . . . . . . . . . . . . . 18
84	83	ad2antlr 493	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
85		simprl 535	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
86		prmz 12905	. . . . . . . . . . . . . . . . . . . 20
87	41	nnzd 9771	. . . . . . . . . . . . . . . . . . . 20
88		eluz 9944	. . . . . . . . . . . . . . . . . . . 20 $/\$
89	86, 87, 88	syl2anr 290	. . . . . . . . . . . . . . . . . . 19 $/\$
90	89	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
91	85, 90	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92		dvdsfac 12643	. . . . . . . . . . . . . . . . 17 $/\$
93	84, 91, 92	syl2anc 415	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94		id 19	. . . . . . . . . . . . . . . . . 18
95	43	faccld 11188	. . . . . . . . . . . . . . . . . 18
96		pcelnn 13120	. . . . . . . . . . . . . . . . . 18 $/\$
97	94, 95, 96	syl2anr 290	. . . . . . . . . . . . . . . . 17 $/\$
98	97	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
99	93, 98	mpbird 167	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
100	99	nnge1d 9349	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101		iffalse 3648	. . . . . . . . . . . . . . . . 17
102	101	oveq1d 6100	. . . . . . . . . . . . . . . 16
103	102	ad2antll 495	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
104	75	nn0cnd 9626	. . . . . . . . . . . . . . . . 17 $/\$
105	104	addlidd 8477	. . . . . . . . . . . . . . . 16 $/\$
106	105	adantr 276	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
107		bcval2 11202	. . . . . . . . . . . . . . . . . . . . . 22
108	56, 107	syl 14	. . . . . . . . . . . . . . . . . . . . 21
109	36	nn0cnd 9626	. . . . . . . . . . . . . . . . . . . . . . . . 25
110	21	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . 26
111	49	oveq1d 6100	. . . . . . . . . . . . . . . . . . . . . . . . . 26
112	25, 25, 110, 111	assraddsubd 8695	. . . . . . . . . . . . . . . . . . . . . . . . 25
113	25, 109, 112	mvrladdd 8694	. . . . . . . . . . . . . . . . . . . . . . . 24
114	113	fveq2d 5699	. . . . . . . . . . . . . . . . . . . . . . 23
115	114	oveq1d 6100	. . . . . . . . . . . . . . . . . . . . . 22
116	115	oveq2d 6101	. . . . . . . . . . . . . . . . . . . . 21
117	108, 116	eqtrd 2271	. . . . . . . . . . . . . . . . . . . 20
118	117	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$
119	118	oveq2d 6101	. . . . . . . . . . . . . . . . . 18 $/\$
120		nnz 9667	. . . . . . . . . . . . . . . . . . . . . 22
121		nnne0 9334	. . . . . . . . . . . . . . . . . . . . . 22
122	120, 121	jca 306	. . . . . . . . . . . . . . . . . . . . 21 $/\$
123	95, 122	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$
124	123	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
125	36	faccld 11188	. . . . . . . . . . . . . . . . . . . . 21
126	16	faccld 11188	. . . . . . . . . . . . . . . . . . . . 21
127	125, 126	nnmulcld 9355	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 13101	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	73, 124, 128, 129	syl3anc 1278	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 9667	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 9334	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 306	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	125, 133	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 9667	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 9334	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 306	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 13100	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	73, 135, 140, 141	syl3anc 1278	. . . . . . . . . . . . . . . . . . 19 $/\$
143	142	oveq2d 6101	. . . . . . . . . . . . . . . . . 18 $/\$
144	119, 130, 143	3eqtrd 2275	. . . . . . . . . . . . . . . . 17 $/\$
145	144	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
146		simprr 537	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
147		prmfac1 12947	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
148	147	3expia 1236	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
149	16, 148	sylan 283	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
150	149	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151	146, 150	mtod 673	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
152	86	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
153	135	simpld 112	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
154		nnz 9667	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 12614	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 11186	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	breq2d 4142	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	157, 160	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	161	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
163	151, 162	mtod 673	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
164		pceq0 13121	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	94, 125, 164	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 13121	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	94, 126, 168	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	169	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
171	151, 170	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
172	167, 171	oveq12d 6103	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173		00id 8468	. . . . . . . . . . . . . . . . . 18
174	172, 173	eqtrdi 2287	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6101	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 13098	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	94, 95, 176	syl2anr 290	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 9626	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 8627	. . . . . . . . . . . . . . . . 17 $/\$
180	179	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	145, 175, 180	3eqtrd 2275	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	103, 106, 181	3eqtrd 2275	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183	100, 182	breqtrrd 4158	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
184	183	expr 375	. . . . . . . . . . . 12 $/\$ $/\$
185		zdcle 9725	. . . . . . . . . . . . . . 15 $/\$ DECID
186	86, 154, 185	syl2anr 290	. . . . . . . . . . . . . 14 $/\$ DECID
187		exmiddc 848	. . . . . . . . . . . . . 14 DECID $\/$
188	186, 187	syl 14	. . . . . . . . . . . . 13 $/\$ $\/$
189	188	adantr 276	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
190	82, 184, 189	mpjaod 730	. . . . . . . . . . 11 $/\$ $/\$
191	72, 190	eqbrtrd 4152	. . . . . . . . . 10 $/\$ $/\$
192	191	ex 115	. . . . . . . . 9 $/\$
193		1nn0 9583	. . . . . . . . . . . . . 14
194	193	a1i 9	. . . . . . . . . . . . 13 $/\$
195		0nn0 9582	. . . . . . . . . . . . . 14
196	195	a1i 9	. . . . . . . . . . . . 13 $/\$
197	194, 196, 186	ifcldcd 3678	. . . . . . . . . . . 12 $/\$
198	197, 75	nn0addcld 9628	. . . . . . . . . . 11 $/\$
199	198	nn0ge0d 9627	. . . . . . . . . 10 $/\$
200		iffalse 3648	. . . . . . . . . . 11
201	200	breq1d 4140	. . . . . . . . . 10
202	199, 201	syl5ibrcom 157	. . . . . . . . 9 $/\$
203		zdcle 9725	. . . . . . . . . . 11 $/\$ DECID
204	86, 87, 203	syl2anr 290	. . . . . . . . . 10 $/\$ DECID
205		exmiddc 848	. . . . . . . . . 10 DECID $\/$
206	204, 205	syl 14	. . . . . . . . 9 $/\$ $\/$
207	192, 202, 206	mpjaod 730	. . . . . . . 8 $/\$
208		eqid 2238	. . . . . . . . . . . . 13
209	208	prmorcht 16201	. . . . . . . . . . . 12
210	41, 209	syl 14	. . . . . . . . . . 11
211	210	oveq2d 6101	. . . . . . . . . 10
212	211	adantr 276	. . . . . . . . 9 $/\$
213		nncn 9314	. . . . . . . . . . . . . 14
214	213	exp1d 11119	. . . . . . . . . . . . 13
215	214	ifeq1d 3658	. . . . . . . . . . . 12
216	215	mpteq2ia 4217	. . . . . . . . . . 11
217	216	eqcomi 2242	. . . . . . . . . 10
218	193	a1i 9	. . . . . . . . . . 11 $/\$ $/\$
219	218	ralrimiva 2623	. . . . . . . . . 10 $/\$
220	41	adantr 276	. . . . . . . . . 10 $/\$
221		eqidd 2239	. . . . . . . . . 10
222	217, 219, 220, 73, 221	pcmpt 13142	. . . . . . . . 9 $/\$
223	212, 222	eqtrd 2271	. . . . . . . 8 $/\$
224		efchtqcl 16165	. . . . . . . . . . . . 13
225	13, 224	syl 14	. . . . . . . . . . . 12
226	225	adantr 276	. . . . . . . . . . 11 $/\$
227		nnz 9667	. . . . . . . . . . . 12
228		nnne0 9334	. . . . . . . . . . . 12
229	227, 228	jca 306	. . . . . . . . . . 11 $/\$
230	226, 229	syl 14	. . . . . . . . . 10 $/\$ $/\$
231		nnz 9667	. . . . . . . . . . . 12
232		nnne0 9334	. . . . . . . . . . . 12
233	231, 232	jca 306	. . . . . . . . . . 11 $/\$
234	74, 233	syl 14	. . . . . . . . . 10 $/\$ $/\$
235		pcmul 13100	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
236	73, 230, 234, 235	syl3anc 1278	. . . . . . . . 9 $/\$
237	208	prmorcht 16201	. . . . . . . . . . . . 13
238	237	oveq2d 6101	. . . . . . . . . . . 12
239	238	adantr 276	. . . . . . . . . . 11 $/\$
240		simpl 109	. . . . . . . . . . . 12 $/\$
241	217, 219, 240, 73, 221	pcmpt 13142	. . . . . . . . . . 11 $/\$
242	239, 241	eqtrd 2271	. . . . . . . . . 10 $/\$
243	242	oveq1d 6100	. . . . . . . . 9 $/\$
244	236, 243	eqtrd 2271	. . . . . . . 8 $/\$
245	207, 223, 244	3brtr4d 4162	. . . . . . 7 $/\$
246	245	ralrimiva 2623	. . . . . 6
247		efchtqcl 16165	. . . . . . . . 9
248	10, 247	syl 14	. . . . . . . 8
249	248	nnzd 9771	. . . . . . 7
250	225, 58	nnmulcld 9355	. . . . . . . 8
251	250	nnzd 9771	. . . . . . 7
252		pc2dvds 13129	. . . . . . 7 $/\$
253	249, 251, 252	syl2anc 415	. . . . . 6
254	246, 253	mpbird 167	. . . . 5
255		dvdsle 12627	. . . . . 6 $/\$
256	249, 250, 255	syl2anc 415	. . . . 5
257	254, 256	mpd 13	. . . 4
258	15	recnd 8354	. . . . . 6
259	60	recnd 8354	. . . . . 6
260		efadd 12458	. . . . . 6 $/\$
261	258, 259, 260	syl2anc 415	. . . . 5
262	59	reeflogd 16035	. . . . . 6
263	262	oveq2d 6101	. . . . 5
264	261, 263	eqtrd 2271	. . . 4
265	257, 264	breqtrrd 4158	. . 3
266		efle 15926	. . . 4 $/\$
267	12, 61, 266	syl2anc 415	. . 3
268	265, 267	mpbird 167	. 2
269		0zd 9660	. . . . . . . . . 10
270	269, 87	fzfigd 10881	. . . . . . . . 9
271		elfzelz 10438	. . . . . . . . . . 11
272		bccl 11219	. . . . . . . . . . 11 $/\$
273	43, 271, 272	syl2an 289	. . . . . . . . . 10 $/\$
274	273	nn0red 9625	. . . . . . . . 9 $/\$
275	273	nn0ge0d 9627	. . . . . . . . 9 $/\$
276		nn0uz 9966	. . . . . . . . . . . 12
277	36, 276	eleqtrdi 2331	. . . . . . . . . . 11
278		fzss1 10479	. . . . . . . . . . 11
279	277, 278	syl 14	. . . . . . . . . 10
280		eluz 9944	. . . . . . . . . . . . 13 $/\$
281	154, 87, 280	syl2anc 415	. . . . . . . . . . . 12
282	54, 281	mpbird 167	. . . . . . . . . . 11
283		fzss2 10480	. . . . . . . . . . 11
284	282, 283	syl 14	. . . . . . . . . 10
285	279, 284	sstrd 3258	. . . . . . . . 9
286	36	nn0zd 9770	. . . . . . . . . 10
287	286, 154	fzfigd 10881	. . . . . . . . 9
288	270, 274, 275, 285, 287	fsumlessfi 12243	. . . . . . . 8
289		bccmpl 11206	. . . . . . . . . . . . . . 15 $/\$
290	43, 154, 289	syl2anc 415	. . . . . . . . . . . . . 14
291	113	oveq2d 6101	. . . . . . . . . . . . . 14
292	290, 291	eqtrd 2271	. . . . . . . . . . . . 13
293	58	nncnd 9320	. . . . . . . . . . . . 13
294	292, 293	eqeltrrd 2316	. . . . . . . . . . . 12
295		oveq2 6093	. . . . . . . . . . . . 13
296	295	fsum1 12195	. . . . . . . . . . . 12 $/\$
297	286, 294, 296	syl2anc 415	. . . . . . . . . . 11
298	297, 292	eqtr4d 2274	. . . . . . . . . 10
299	298	oveq1d 6100	. . . . . . . . 9
300	25, 110	npcand 8642	. . . . . . . . . . 11
301	286	uzidd 9946	. . . . . . . . . . . 12
302		peano2uz 9992	. . . . . . . . . . . 12
303	301, 302	syl 14	. . . . . . . . . . 11
304	300, 303	eqeltrrd 2316	. . . . . . . . . 10
305	285	sselda 3248	. . . . . . . . . . 11 $/\$
306	273	nn0cnd 9626	. . . . . . . . . . 11 $/\$
307	305, 306	syldan 282	. . . . . . . . . 10 $/\$
308		oveq2 6093	. . . . . . . . . 10
309	304, 307, 308	fsumm1 12199	. . . . . . . . 9
310	293	2timesd 9552	. . . . . . . . 9
311	299, 309, 310	3eqtr4rd 2282	. . . . . . . 8
312		binom11 12269	. . . . . . . . 9
313	43, 312	syl 14	. . . . . . . 8
314	288, 311, 313	3brtr4d 4162	. . . . . . 7
315		mulcom 8308	. . . . . . . 8 $/\$
316	20, 293, 315	sylancr 418	. . . . . . 7
317	34	oveq2d 6101	. . . . . . . 8
318		expp1 10996	. . . . . . . . 9 $/\$
319	20, 38, 318	sylancr 418	. . . . . . . 8
320	20	a1i 9	. . . . . . . . . . 11
321	35	a1i 9	. . . . . . . . . . 11
322	320, 36, 321	expmuld 11127	. . . . . . . . . 10
323		sq2 11085	. . . . . . . . . . 11
324	323	oveq1i 6095	. . . . . . . . . 10
325	322, 324	eqtrdi 2287	. . . . . . . . 9
326	325	oveq1d 6100	. . . . . . . 8
327	317, 319, 326	3eqtrd 2275	. . . . . . 7
328	314, 316, 327	3brtr3d 4161	. . . . . 6
329	58	nnred 9319	. . . . . . 7
330		reexpcl 11006	. . . . . . . 8 $/\$
331	62, 36, 330	sylancr 418	. . . . . . 7
332		2re 9376	. . . . . . . . 9
333		2pos 9397	. . . . . . . . 9
334	332, 333	pm3.2i 272	. . . . . . . 8 $/\$
335	334	a1i 9	. . . . . . 7 $/\$
336		lemul1 8923	. . . . . . 7 $/\$ $/\$ $/\$
337	329, 331, 335, 336	syl3anc 1278	. . . . . 6
338	328, 337	mpbird 167	. . . . 5
339	66	recni 8338	. . . . . . . 8
340		mulcom 8308	. . . . . . . 8 $/\$
341	339, 109, 340	sylancr 418	. . . . . . 7
342	341	fveq2d 5699	. . . . . 6
343		reexplog 16023	. . . . . . 7 $/\$
344	64, 286, 343	sylancr 418	. . . . . 6
345	342, 344	eqtr4d 2274	. . . . 5
346	338, 262, 345	3brtr4d 4162	. . . 4
347		efle 15926	. . . . 5 $/\$
348	60, 69, 347	syl2anc 415	. . . 4
349	346, 348	mpbird 167	. . 3
350	60, 69, 15, 349	leadd2dd 8889	. 2
351	12, 61, 70, 268, 350	letrd 8451	1

Colors of variables: wff set class

This proof depends on syntax axioms:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 720 DECID wdc 846

wceq 1402

wcel 2209

wne 2420

wral 2528

wss 3220

cif 3638 class class class wbr 4130

cmpt 4192

cfv 5377 (class class class)co 6085

cc 8177

cr 8178

cc0 8179

c1 8180

caddc 8182

cmul 8184

clt 8360

cle 8361

cmin 8498

cdiv 9004

cn 9306

c2 9357

c4 9359

cn0 9567

cz 9648

cuz 9930

cq 10028

crp 10064

cfz 10421

cseq 10897

cexp 10988

cfa 11177

cbc 11199

csu 12135

ce 12425

cdvds 12570

cprime 12901

cpc 13083

clog 16007

ccht 16152

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299 ax-pre-suploc 8300 ax-addf 8301 ax-mulf 8302

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-disj 4107 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-of 6302 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-2o 6688 df-oadd 6691 df-er 6807 df-map 6924 df-pm 6925 df-en 7023 df-dom 7024 df-fin 7025 df-sup 7324 df-inf 7325 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8500 df-neg 8501 df-reap 8905 df-ap 8912 df-div 9005 df-inn 9307 df-2 9365 df-3 9366 df-4 9367 df-n0 9568 df-xnn0 9635 df-z 9649 df-uz 9931 df-q 10029 df-rp 10065 df-xneg 10184 df-xadd 10185 df-ioo 10304 df-ico 10306 df-icc 10307 df-fz 10422 df-fzo 10560 df-fl 10715 df-mod 10773 df-seqfrec 10898 df-exp 10989 df-fac 11178 df-bc 11200 df-ihash 11229 df-shft 11594 df-cj 11621 df-re 11622 df-im 11623 df-rsqrt 11778 df-abs 11779 df-clim 12061 df-sumdc 12136 df-ef 12431 df-e 12432 df-dvds 12571 df-gcd 12747 df-prm 12902 df-pc 13084 df-rest 13644 df-topgen 13663 df-psmet 14929 df-xmet 14930 df-met 14931 df-bl 14932 df-mopn 14933 df-top 15148 df-topon 15161 df-bases 15193 df-ntr 15246 df-cn 15338 df-cnp 15339 df-tx 15403 df-cncf 15721 df-limced 15806 df-dvap 15807 df-relog 16009 df-cht 16155

This theorem is used by: chtqub 16215

W3C validator