chtublem - Intuitionistic Logic Explorer

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

Theorem chtublem 16295

Description: Lemma for chtqub 16296. (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 9477	. . . . . 6
2		nnmulcl 9334	. . . . . 6 $/\$
3	1, 2	mpan 428	. . . . 5
4		nnq 10049	. . . . 5
5	3, 4	syl 14	. . . 4
6		1z 9681	. . . . 5
7		zq 10042	. . . . 5
8	6, 7	ax-mp 5	. . . 4
9		qsubcl 10054	. . . 4 $/\$
10	5, 8, 9	sylancl 417	. . 3
11		chtqcl 16244	. . 3
12	10, 11	syl 14	. 2
13		nnq 10049	. . . 4
14		chtqcl 16244	. . . 4
15	13, 14	syl 14	. . 3
16		nnnn0 9581	. . . . . . 7
17		2m1e1 9431	. . . . . . . . . . 11
18	17	oveq2i 6099	. . . . . . . . . 10
19	3	nncnd 9327	. . . . . . . . . . . 12
20		2cn 9384	. . . . . . . . . . . . 13
21		ax-1cn 8278	. . . . . . . . . . . . 13
22		subsub 8563	. . . . . . . . . . . . 13 $/\$ $/\$
23	20, 21, 22	mp3an23 1370	. . . . . . . . . . . 12
24	19, 23	syl 14	. . . . . . . . . . 11
25		nncn 9321	. . . . . . . . . . . . . 14
26		subdi 8719	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	20, 21, 26	mp3an13 1369	. . . . . . . . . . . . . 14
28	25, 27	syl 14	. . . . . . . . . . . . 13
29		2t1e2 9467	. . . . . . . . . . . . . 14
30	29	oveq2i 6099	. . . . . . . . . . . . 13
31	28, 30	eqtrdi 2287	. . . . . . . . . . . 12
32	31	oveq1d 6103	. . . . . . . . . . 11
33	24, 32	eqtr4d 2274	. . . . . . . . . 10
34	18, 33	eqtr3id 2285	. . . . . . . . 9
35		2nn0 9591	. . . . . . . . . . 11
36		nnm1nn0 9615	. . . . . . . . . . 11
37		nn0mulcl 9610	. . . . . . . . . . 11 $/\$
38	35, 36, 37	sylancr 418	. . . . . . . . . 10
39		nn0p1nn 9613	. . . . . . . . . 10
40	38, 39	syl 14	. . . . . . . . 9
41	34, 40	eqeltrd 2315	. . . . . . . 8
42		nnnn0 9581	. . . . . . . 8
43	41, 42	syl 14	. . . . . . 7
44		1re 8331	. . . . . . . . . . 11
45	44	a1i 9	. . . . . . . . . 10
46		nnre 9320	. . . . . . . . . 10
47		nnge1 9336	. . . . . . . . . 10
48	45, 46, 46, 47	leadd2dd 8895	. . . . . . . . 9
49	25	2timesd 9559	. . . . . . . . 9
50	48, 49	breqtrrd 4159	. . . . . . . 8
51	3	nnred 9326	. . . . . . . . 9
52		leaddsub 8773	. . . . . . . . 9 $/\$ $/\$
53	46, 45, 51, 52	syl3anc 1278	. . . . . . . 8
54	50, 53	mpbid 147	. . . . . . 7
55		elfz2nn0 10536	. . . . . . 7 $/\$ $/\$
56	16, 43, 54, 55	syl3anbrc 1212	. . . . . 6
57		bccl2 11228	. . . . . 6
58	56, 57	syl 14	. . . . 5
59	58	nnrpd 10112	. . . 4
60	59	relogcld 16112	. . 3
61	15, 60	readdcld 8361	. 2
62		4re 9390	. . . . . 6
63		4pos 9410	. . . . . 6
64	62, 63	elrpii 10074	. . . . 5
65		relogcl 16091	. . . . 5
66	64, 65	ax-mp 5	. . . 4
67	36	nn0red 9632	. . . 4
68		remulcl 8313	. . . 4 $/\$
69	66, 67, 68	sylancr 418	. . 3
70	15, 69	readdcld 8361	. 2
71		iftrue 3645	. . . . . . . . . . . 12
72	71	adantl 277	. . . . . . . . . . 11 $/\$ $/\$
73		simpr 110	. . . . . . . . . . . . . . . 16 $/\$
74	58	adantr 276	. . . . . . . . . . . . . . . 16 $/\$
75	73, 74	pccld 13108	. . . . . . . . . . . . . . 15 $/\$
76		nn0addge1 9620	. . . . . . . . . . . . . . 15 $/\$
77	44, 75, 76	sylancr 418	. . . . . . . . . . . . . 14 $/\$
78		iftrue 3645	. . . . . . . . . . . . . . . 16
79	78	oveq1d 6103	. . . . . . . . . . . . . . 15
80	79	breq2d 4143	. . . . . . . . . . . . . 14
81	77, 80	syl5ibrcom 157	. . . . . . . . . . . . 13 $/\$
82	81	adantr 276	. . . . . . . . . . . 12 $/\$ $/\$
83		prmnn 12913	. . . . . . . . . . . . . . . . . 18
84	83	ad2antlr 493	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
85		simprl 535	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
86		prmz 12914	. . . . . . . . . . . . . . . . . . . 20
87	41	nnzd 9778	. . . . . . . . . . . . . . . . . . . 20
88		eluz 9951	. . . . . . . . . . . . . . . . . . . 20 $/\$
89	86, 87, 88	syl2anr 290	. . . . . . . . . . . . . . . . . . 19 $/\$
90	89	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
91	85, 90	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92		dvdsfac 12652	. . . . . . . . . . . . . . . . 17 $/\$
93	84, 91, 92	syl2anc 415	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94		id 19	. . . . . . . . . . . . . . . . . 18
95	43	faccld 11196	. . . . . . . . . . . . . . . . . 18
96		pcelnn 13129	. . . . . . . . . . . . . . . . . 18 $/\$
97	94, 95, 96	syl2anr 290	. . . . . . . . . . . . . . . . 17 $/\$
98	97	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
99	93, 98	mpbird 167	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
100	99	nnge1d 9356	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101		iffalse 3648	. . . . . . . . . . . . . . . . 17
102	101	oveq1d 6103	. . . . . . . . . . . . . . . 16
103	102	ad2antll 495	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
104	75	nn0cnd 9633	. . . . . . . . . . . . . . . . 17 $/\$
105	104	addlidd 8483	. . . . . . . . . . . . . . . 16 $/\$
106	105	adantr 276	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
107		bcval2 11210	. . . . . . . . . . . . . . . . . . . . . 22
108	56, 107	syl 14	. . . . . . . . . . . . . . . . . . . . 21
109	36	nn0cnd 9633	. . . . . . . . . . . . . . . . . . . . . . . . 25
110	21	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . 26
111	49	oveq1d 6103	. . . . . . . . . . . . . . . . . . . . . . . . . 26
112	25, 25, 110, 111	assraddsubd 8701	. . . . . . . . . . . . . . . . . . . . . . . . 25
113	25, 109, 112	mvrladdd 8700	. . . . . . . . . . . . . . . . . . . . . . . 24
114	113	fveq2d 5702	. . . . . . . . . . . . . . . . . . . . . . 23
115	114	oveq1d 6103	. . . . . . . . . . . . . . . . . . . . . 22
116	115	oveq2d 6104	. . . . . . . . . . . . . . . . . . . . 21
117	108, 116	eqtrd 2271	. . . . . . . . . . . . . . . . . . . 20
118	117	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$
119	118	oveq2d 6104	. . . . . . . . . . . . . . . . . 18 $/\$
120		nnz 9674	. . . . . . . . . . . . . . . . . . . . . 22
121		nnne0 9341	. . . . . . . . . . . . . . . . . . . . . 22
122	120, 121	jca 306	. . . . . . . . . . . . . . . . . . . . 21 $/\$
123	95, 122	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$
124	123	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
125	36	faccld 11196	. . . . . . . . . . . . . . . . . . . . 21
126	16	faccld 11196	. . . . . . . . . . . . . . . . . . . . 21
127	125, 126	nnmulcld 9362	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 13110	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	73, 124, 128, 129	syl3anc 1278	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 9674	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 9341	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 306	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	125, 133	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 9674	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 9341	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 306	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 13109	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	73, 135, 140, 141	syl3anc 1278	. . . . . . . . . . . . . . . . . . 19 $/\$
143	142	oveq2d 6104	. . . . . . . . . . . . . . . . . 18 $/\$
144	119, 130, 143	3eqtrd 2275	. . . . . . . . . . . . . . . . 17 $/\$
145	144	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
146		simprr 537	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
147		prmfac1 12956	. . . . . . . . . . . . . . . . . . . . . . . . 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 9674	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 12623	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 11194	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	breq2d 4143	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	157, 160	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	161	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
163	151, 162	mtod 673	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
164		pceq0 13130	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	94, 125, 164	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 13130	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	94, 126, 168	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	169	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
171	151, 170	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
172	167, 171	oveq12d 6106	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173		00id 8474	. . . . . . . . . . . . . . . . . 18
174	172, 173	eqtrdi 2287	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6104	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 13107	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	94, 95, 176	syl2anr 290	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 9633	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 8633	. . . . . . . . . . . . . . . . 17 $/\$
180	179	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	145, 175, 180	3eqtrd 2275	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	103, 106, 181	3eqtrd 2275	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183	100, 182	breqtrrd 4159	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
184	183	expr 375	. . . . . . . . . . . 12 $/\$ $/\$
185		zdcle 9732	. . . . . . . . . . . . . . 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 4153	. . . . . . . . . 10 $/\$ $/\$
192	191	ex 115	. . . . . . . . 9 $/\$
193		1nn0 9590	. . . . . . . . . . . . . 14
194	193	a1i 9	. . . . . . . . . . . . 13 $/\$
195		0nn0 9589	. . . . . . . . . . . . . 14
196	195	a1i 9	. . . . . . . . . . . . 13 $/\$
197	194, 196, 186	ifcldcd 3678	. . . . . . . . . . . 12 $/\$
198	197, 75	nn0addcld 9635	. . . . . . . . . . 11 $/\$
199	198	nn0ge0d 9634	. . . . . . . . . 10 $/\$
200		iffalse 3648	. . . . . . . . . . 11
201	200	breq1d 4141	. . . . . . . . . 10
202	199, 201	syl5ibrcom 157	. . . . . . . . 9 $/\$
203		zdcle 9732	. . . . . . . . . . 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 16282	. . . . . . . . . . . 12
210	41, 209	syl 14	. . . . . . . . . . 11
211	210	oveq2d 6104	. . . . . . . . . 10
212	211	adantr 276	. . . . . . . . 9 $/\$
213		nncn 9321	. . . . . . . . . . . . . 14
214	213	exp1d 11127	. . . . . . . . . . . . 13
215	214	ifeq1d 3658	. . . . . . . . . . . 12
216	215	mpteq2ia 4219	. . . . . . . . . . 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 13151	. . . . . . . . 9 $/\$
223	212, 222	eqtrd 2271	. . . . . . . 8 $/\$
224		efchtqcl 16246	. . . . . . . . . . . . 13
225	13, 224	syl 14	. . . . . . . . . . . 12
226	225	adantr 276	. . . . . . . . . . 11 $/\$
227		nnz 9674	. . . . . . . . . . . 12
228		nnne0 9341	. . . . . . . . . . . 12
229	227, 228	jca 306	. . . . . . . . . . 11 $/\$
230	226, 229	syl 14	. . . . . . . . . 10 $/\$ $/\$
231		nnz 9674	. . . . . . . . . . . 12
232		nnne0 9341	. . . . . . . . . . . 12
233	231, 232	jca 306	. . . . . . . . . . 11 $/\$
234	74, 233	syl 14	. . . . . . . . . 10 $/\$ $/\$
235		pcmul 13109	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
236	73, 230, 234, 235	syl3anc 1278	. . . . . . . . 9 $/\$
237	208	prmorcht 16282	. . . . . . . . . . . . 13
238	237	oveq2d 6104	. . . . . . . . . . . 12
239	238	adantr 276	. . . . . . . . . . 11 $/\$
240		simpl 109	. . . . . . . . . . . 12 $/\$
241	217, 219, 240, 73, 221	pcmpt 13151	. . . . . . . . . . 11 $/\$
242	239, 241	eqtrd 2271	. . . . . . . . . 10 $/\$
243	242	oveq1d 6103	. . . . . . . . 9 $/\$
244	236, 243	eqtrd 2271	. . . . . . . 8 $/\$
245	207, 223, 244	3brtr4d 4163	. . . . . . 7 $/\$
246	245	ralrimiva 2623	. . . . . 6
247		efchtqcl 16246	. . . . . . . . 9
248	10, 247	syl 14	. . . . . . . 8
249	248	nnzd 9778	. . . . . . 7
250	225, 58	nnmulcld 9362	. . . . . . . 8
251	250	nnzd 9778	. . . . . . 7
252		pc2dvds 13138	. . . . . . 7 $/\$
253	249, 251, 252	syl2anc 415	. . . . . 6
254	246, 253	mpbird 167	. . . . 5
255		dvdsle 12636	. . . . . 6 $/\$
256	249, 250, 255	syl2anc 415	. . . . 5
257	254, 256	mpd 13	. . . 4
258	15	recnd 8360	. . . . . 6
259	60	recnd 8360	. . . . . 6
260		efadd 12467	. . . . . 6 $/\$
261	258, 259, 260	syl2anc 415	. . . . 5
262	59	reeflogd 16113	. . . . . 6
263	262	oveq2d 6104	. . . . 5
264	261, 263	eqtrd 2271	. . . 4
265	257, 264	breqtrrd 4159	. . 3
266		efle 16002	. . . 4 $/\$
267	12, 61, 266	syl2anc 415	. . 3
268	265, 267	mpbird 167	. 2
269		0zd 9667	. . . . . . . . . 10
270	269, 87	fzfigd 10889	. . . . . . . . 9
271		elfzelz 10445	. . . . . . . . . . 11
272		bccl 11227	. . . . . . . . . . 11 $/\$
273	43, 271, 272	syl2an 289	. . . . . . . . . 10 $/\$
274	273	nn0red 9632	. . . . . . . . 9 $/\$
275	273	nn0ge0d 9634	. . . . . . . . 9 $/\$
276		nn0uz 9973	. . . . . . . . . . . 12
277	36, 276	eleqtrdi 2331	. . . . . . . . . . 11
278		fzss1 10486	. . . . . . . . . . 11
279	277, 278	syl 14	. . . . . . . . . 10
280		eluz 9951	. . . . . . . . . . . . 13 $/\$
281	154, 87, 280	syl2anc 415	. . . . . . . . . . . 12
282	54, 281	mpbird 167	. . . . . . . . . . 11
283		fzss2 10487	. . . . . . . . . . 11
284	282, 283	syl 14	. . . . . . . . . 10
285	279, 284	sstrd 3258	. . . . . . . . 9
286	36	nn0zd 9777	. . . . . . . . . 10
287	286, 154	fzfigd 10889	. . . . . . . . 9
288	270, 274, 275, 285, 287	fsumlessfi 12252	. . . . . . . 8
289		bccmpl 11214	. . . . . . . . . . . . . . 15 $/\$
290	43, 154, 289	syl2anc 415	. . . . . . . . . . . . . 14
291	113	oveq2d 6104	. . . . . . . . . . . . . 14
292	290, 291	eqtrd 2271	. . . . . . . . . . . . 13
293	58	nncnd 9327	. . . . . . . . . . . . 13
294	292, 293	eqeltrrd 2316	. . . . . . . . . . . 12
295		oveq2 6096	. . . . . . . . . . . . 13
296	295	fsum1 12204	. . . . . . . . . . . 12 $/\$
297	286, 294, 296	syl2anc 415	. . . . . . . . . . 11
298	297, 292	eqtr4d 2274	. . . . . . . . . 10
299	298	oveq1d 6103	. . . . . . . . 9
300	25, 110	npcand 8648	. . . . . . . . . . 11
301	286	uzidd 9953	. . . . . . . . . . . 12
302		peano2uz 9999	. . . . . . . . . . . 12
303	301, 302	syl 14	. . . . . . . . . . 11
304	300, 303	eqeltrrd 2316	. . . . . . . . . 10
305	285	sselda 3248	. . . . . . . . . . 11 $/\$
306	273	nn0cnd 9633	. . . . . . . . . . 11 $/\$
307	305, 306	syldan 282	. . . . . . . . . 10 $/\$
308		oveq2 6096	. . . . . . . . . 10
309	304, 307, 308	fsumm1 12208	. . . . . . . . 9
310	293	2timesd 9559	. . . . . . . . 9
311	299, 309, 310	3eqtr4rd 2282	. . . . . . . 8
312		binom11 12278	. . . . . . . . 9
313	43, 312	syl 14	. . . . . . . 8
314	288, 311, 313	3brtr4d 4163	. . . . . . 7
315		mulcom 8314	. . . . . . . 8 $/\$
316	20, 293, 315	sylancr 418	. . . . . . 7
317	34	oveq2d 6104	. . . . . . . 8
318		expp1 11004	. . . . . . . . 9 $/\$
319	20, 38, 318	sylancr 418	. . . . . . . 8
320	20	a1i 9	. . . . . . . . . . 11
321	35	a1i 9	. . . . . . . . . . 11
322	320, 36, 321	expmuld 11135	. . . . . . . . . 10
323		sq2 11093	. . . . . . . . . . 11
324	323	oveq1i 6098	. . . . . . . . . 10
325	322, 324	eqtrdi 2287	. . . . . . . . 9
326	325	oveq1d 6103	. . . . . . . 8
327	317, 319, 326	3eqtrd 2275	. . . . . . 7
328	314, 316, 327	3brtr3d 4162	. . . . . 6
329	58	nnred 9326	. . . . . . 7
330		reexpcl 11014	. . . . . . . 8 $/\$
331	62, 36, 330	sylancr 418	. . . . . . 7
332		2re 9383	. . . . . . . . 9
333		2pos 9404	. . . . . . . . 9
334	332, 333	pm3.2i 272	. . . . . . . 8 $/\$
335	334	a1i 9	. . . . . . 7 $/\$
336		lemul1 8929	. . . . . . 7 $/\$ $/\$ $/\$
337	329, 331, 335, 336	syl3anc 1278	. . . . . 6
338	328, 337	mpbird 167	. . . . 5
339	66	recni 8344	. . . . . . . 8
340		mulcom 8314	. . . . . . . 8 $/\$
341	339, 109, 340	sylancr 418	. . . . . . 7
342	341	fveq2d 5702	. . . . . 6
343		reexplog 16101	. . . . . . 7 $/\$
344	64, 286, 343	sylancr 418	. . . . . 6
345	342, 344	eqtr4d 2274	. . . . 5
346	338, 262, 345	3brtr4d 4163	. . . 4
347		efle 16002	. . . . 5 $/\$
348	60, 69, 347	syl2anc 415	. . . 4
349	346, 348	mpbird 167	. . 3
350	60, 69, 15, 349	leadd2dd 8895	. 2
351	12, 61, 70, 268, 350	letrd 8457	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 4131

cmpt 4193

cfv 5380 (class class class)co 6088

cc 8183

cr 8184

cc0 8185

c1 8186

caddc 8188

cmul 8190

clt 8366

cle 8367

cmin 8504

cdiv 9010

cn 9313

c2 9364

c4 9366

cn0 9574

cz 9655

cuz 9937

cq 10035

crp 10071

cfz 10428

cseq 10905

cexp 10996

cfa 11185

cbc 11207

csu 12144

ce 12434

cdvds 12579

cprime 12910

cpc 13092

clog 16085

ccht 16233

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 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8276 ax-resscn 8277 ax-1cn 8278 ax-1re 8279 ax-icn 8280 ax-addcl 8281 ax-addrcl 8282 ax-mulcl 8283 ax-mulrcl 8284 ax-addcom 8285 ax-mulcom 8286 ax-addass 8287 ax-mulass 8288 ax-distr 8289 ax-i2m1 8290 ax-0lt1 8291 ax-1rid 8292 ax-0id 8293 ax-rnegex 8294 ax-precex 8295 ax-cnre 8296 ax-pre-ltirr 8297 ax-pre-ltwlin 8298 ax-pre-lttrn 8299 ax-pre-apti 8300 ax-pre-ltadd 8301 ax-pre-mulgt0 8302 ax-pre-mulext 8303 ax-arch 8304 ax-caucvg 8305 ax-pre-suploc 8306 ax-addf 8307 ax-mulf 8308

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 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-isom 5389 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-of 6305 df-1st 6378 df-2nd 6379 df-recs 6580 df-irdg 6645 df-frec 6666 df-1o 6691 df-2o 6692 df-oadd 6695 df-er 6811 df-map 6928 df-pm 6929 df-en 7027 df-dom 7028 df-fin 7029 df-sup 7330 df-inf 7331 df-pnf 8368 df-mnf 8369 df-xr 8370 df-ltxr 8371 df-le 8372 df-sub 8506 df-neg 8507 df-reap 8911 df-ap 8918 df-div 9011 df-inn 9314 df-2 9372 df-3 9373 df-4 9374 df-n0 9575 df-xnn0 9642 df-z 9656 df-uz 9938 df-q 10036 df-rp 10072 df-xneg 10191 df-xadd 10192 df-ioo 10311 df-ico 10313 df-icc 10314 df-fz 10429 df-fzo 10567 df-fl 10722 df-mod 10781 df-seqfrec 10906 df-exp 10997 df-fac 11186 df-bc 11208 df-ihash 11237 df-shft 11602 df-cj 11629 df-re 11630 df-im 11631 df-rsqrt 11786 df-abs 11787 df-clim 12070 df-sumdc 12145 df-ef 12440 df-e 12441 df-dvds 12580 df-gcd 12756 df-prm 12911 df-pc 13093 df-rest 13654 df-topgen 13673 df-psmet 14989 df-xmet 14990 df-met 14991 df-bl 14992 df-mopn 14993 df-top 15224 df-topon 15237 df-bases 15269 df-ntr 15322 df-cn 15414 df-cnp 15415 df-tx 15479 df-cncf 15797 df-limced 15882 df-dvap 15883 df-relog 16087 df-cht 16236

This theorem is used by: chtqub 16296

W3C validator