chtublem - Intuitionistic Logic Explorer

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

Theorem chtublem 16307

Description: Lemma for chtqub 16308. (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 9478	. . . . . 6
2		nnmulcl 9335	. . . . . 6 $/\$
3	1, 2	mpan 428	. . . . 5
4		nnq 10050	. . . . 5
5	3, 4	syl 14	. . . 4
6		1z 9682	. . . . 5
7		zq 10043	. . . . 5
8	6, 7	ax-mp 5	. . . 4
9		qsubcl 10055	. . . 4 $/\$
10	5, 8, 9	sylancl 417	. . 3
11		chtqcl 16256	. . 3
12	10, 11	syl 14	. 2
13		nnq 10050	. . . 4
14		chtqcl 16256	. . . 4
15	13, 14	syl 14	. . 3
16		nnnn0 9582	. . . . . . 7
17		2m1e1 9432	. . . . . . . . . . 11
18	17	oveq2i 6099	. . . . . . . . . 10
19	3	nncnd 9328	. . . . . . . . . . . 12
20		2cn 9385	. . . . . . . . . . . . 13
21		ax-1cn 8279	. . . . . . . . . . . . 13
22		subsub 8564	. . . . . . . . . . . . 13 $/\$ $/\$
23	20, 21, 22	mp3an23 1370	. . . . . . . . . . . 12
24	19, 23	syl 14	. . . . . . . . . . 11
25		nncn 9322	. . . . . . . . . . . . . 14
26		subdi 8720	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	20, 21, 26	mp3an13 1369	. . . . . . . . . . . . . 14
28	25, 27	syl 14	. . . . . . . . . . . . 13
29		2t1e2 9468	. . . . . . . . . . . . . 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 9592	. . . . . . . . . . 11
36		nnm1nn0 9616	. . . . . . . . . . 11
37		nn0mulcl 9611	. . . . . . . . . . 11 $/\$
38	35, 36, 37	sylancr 418	. . . . . . . . . 10
39		nn0p1nn 9614	. . . . . . . . . 10
40	38, 39	syl 14	. . . . . . . . 9
41	34, 40	eqeltrd 2315	. . . . . . . 8
42		nnnn0 9582	. . . . . . . 8
43	41, 42	syl 14	. . . . . . 7
44		1re 8332	. . . . . . . . . . 11
45	44	a1i 9	. . . . . . . . . 10
46		nnre 9321	. . . . . . . . . 10
47		nnge1 9337	. . . . . . . . . 10
48	45, 46, 46, 47	leadd2dd 8896	. . . . . . . . 9
49	25	2timesd 9560	. . . . . . . . 9
50	48, 49	breqtrrd 4159	. . . . . . . 8
51	3	nnred 9327	. . . . . . . . 9
52		leaddsub 8774	. . . . . . . . 9 $/\$ $/\$
53	46, 45, 51, 52	syl3anc 1278	. . . . . . . 8
54	50, 53	mpbid 147	. . . . . . 7
55		elfz2nn0 10537	. . . . . . 7 $/\$ $/\$
56	16, 43, 54, 55	syl3anbrc 1212	. . . . . 6
57		bccl2 11229	. . . . . 6
58	56, 57	syl 14	. . . . 5
59	58	nnrpd 10113	. . . 4
60	59	relogcld 16124	. . 3
61	15, 60	readdcld 8362	. 2
62		4re 9391	. . . . . 6
63		4pos 9411	. . . . . 6
64	62, 63	elrpii 10075	. . . . 5
65		relogcl 16103	. . . . 5
66	64, 65	ax-mp 5	. . . 4
67	36	nn0red 9633	. . . 4
68		remulcl 8314	. . . 4 $/\$
69	66, 67, 68	sylancr 418	. . 3
70	15, 69	readdcld 8362	. 2
71		iftrue 3645	. . . . . . . . . . . 12
72	71	adantl 277	. . . . . . . . . . 11 $/\$ $/\$
73		simpr 110	. . . . . . . . . . . . . . . 16 $/\$
74	58	adantr 276	. . . . . . . . . . . . . . . 16 $/\$
75	73, 74	pccld 13109	. . . . . . . . . . . . . . 15 $/\$
76		nn0addge1 9621	. . . . . . . . . . . . . . 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 12914	. . . . . . . . . . . . . . . . . 18
84	83	ad2antlr 493	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
85		simprl 535	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
86		prmz 12915	. . . . . . . . . . . . . . . . . . . 20
87	41	nnzd 9779	. . . . . . . . . . . . . . . . . . . 20
88		eluz 9952	. . . . . . . . . . . . . . . . . . . 20 $/\$
89	86, 87, 88	syl2anr 290	. . . . . . . . . . . . . . . . . . 19 $/\$
90	89	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
91	85, 90	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92		dvdsfac 12653	. . . . . . . . . . . . . . . . 17 $/\$
93	84, 91, 92	syl2anc 415	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94		id 19	. . . . . . . . . . . . . . . . . 18
95	43	faccld 11197	. . . . . . . . . . . . . . . . . 18
96		pcelnn 13130	. . . . . . . . . . . . . . . . . 18 $/\$
97	94, 95, 96	syl2anr 290	. . . . . . . . . . . . . . . . 17 $/\$
98	97	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
99	93, 98	mpbird 167	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
100	99	nnge1d 9357	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101		iffalse 3648	. . . . . . . . . . . . . . . . 17
102	101	oveq1d 6103	. . . . . . . . . . . . . . . 16
103	102	ad2antll 495	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
104	75	nn0cnd 9634	. . . . . . . . . . . . . . . . 17 $/\$
105	104	addlidd 8484	. . . . . . . . . . . . . . . 16 $/\$
106	105	adantr 276	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
107		bcval2 11211	. . . . . . . . . . . . . . . . . . . . . 22
108	56, 107	syl 14	. . . . . . . . . . . . . . . . . . . . 21
109	36	nn0cnd 9634	. . . . . . . . . . . . . . . . . . . . . . . . 25
110	21	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . 26
111	49	oveq1d 6103	. . . . . . . . . . . . . . . . . . . . . . . . . 26
112	25, 25, 110, 111	assraddsubd 8702	. . . . . . . . . . . . . . . . . . . . . . . . 25
113	25, 109, 112	mvrladdd 8701	. . . . . . . . . . . . . . . . . . . . . . . 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 9675	. . . . . . . . . . . . . . . . . . . . . 22
121		nnne0 9342	. . . . . . . . . . . . . . . . . . . . . 22
122	120, 121	jca 306	. . . . . . . . . . . . . . . . . . . . 21 $/\$
123	95, 122	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$
124	123	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
125	36	faccld 11197	. . . . . . . . . . . . . . . . . . . . 21
126	16	faccld 11197	. . . . . . . . . . . . . . . . . . . . 21
127	125, 126	nnmulcld 9363	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 13111	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	73, 124, 128, 129	syl3anc 1278	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 9675	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 9342	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 306	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	125, 133	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 9675	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 9342	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 306	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 13110	. . . . . . . . . . . . . . . . . . . 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 12957	. . . . . . . . . . . . . . . . . . . . . . . . 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 9675	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 12624	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 11195	. . . . . . . . . . . . . . . . . . . . . . . . 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 13131	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	94, 125, 164	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 13131	. . . . . . . . . . . . . . . . . . . . . 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 8475	. . . . . . . . . . . . . . . . . 18
174	172, 173	eqtrdi 2287	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6104	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 13108	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	94, 95, 176	syl2anr 290	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 9634	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 8634	. . . . . . . . . . . . . . . . 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 9733	. . . . . . . . . . . . . . 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 9591	. . . . . . . . . . . . . 14
194	193	a1i 9	. . . . . . . . . . . . 13 $/\$
195		0nn0 9590	. . . . . . . . . . . . . 14
196	195	a1i 9	. . . . . . . . . . . . 13 $/\$
197	194, 196, 186	ifcldcd 3678	. . . . . . . . . . . 12 $/\$
198	197, 75	nn0addcld 9636	. . . . . . . . . . 11 $/\$
199	198	nn0ge0d 9635	. . . . . . . . . 10 $/\$
200		iffalse 3648	. . . . . . . . . . 11
201	200	breq1d 4141	. . . . . . . . . 10
202	199, 201	syl5ibrcom 157	. . . . . . . . 9 $/\$
203		zdcle 9733	. . . . . . . . . . 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 16294	. . . . . . . . . . . 12
210	41, 209	syl 14	. . . . . . . . . . 11
211	210	oveq2d 6104	. . . . . . . . . 10
212	211	adantr 276	. . . . . . . . 9 $/\$
213		nncn 9322	. . . . . . . . . . . . . 14
214	213	exp1d 11128	. . . . . . . . . . . . 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 13152	. . . . . . . . 9 $/\$
223	212, 222	eqtrd 2271	. . . . . . . 8 $/\$
224		efchtqcl 16258	. . . . . . . . . . . . 13
225	13, 224	syl 14	. . . . . . . . . . . 12
226	225	adantr 276	. . . . . . . . . . 11 $/\$
227		nnz 9675	. . . . . . . . . . . 12
228		nnne0 9342	. . . . . . . . . . . 12
229	227, 228	jca 306	. . . . . . . . . . 11 $/\$
230	226, 229	syl 14	. . . . . . . . . 10 $/\$ $/\$
231		nnz 9675	. . . . . . . . . . . 12
232		nnne0 9342	. . . . . . . . . . . 12
233	231, 232	jca 306	. . . . . . . . . . 11 $/\$
234	74, 233	syl 14	. . . . . . . . . 10 $/\$ $/\$
235		pcmul 13110	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
236	73, 230, 234, 235	syl3anc 1278	. . . . . . . . 9 $/\$
237	208	prmorcht 16294	. . . . . . . . . . . . 13
238	237	oveq2d 6104	. . . . . . . . . . . 12
239	238	adantr 276	. . . . . . . . . . 11 $/\$
240		simpl 109	. . . . . . . . . . . 12 $/\$
241	217, 219, 240, 73, 221	pcmpt 13152	. . . . . . . . . . 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 16258	. . . . . . . . 9
248	10, 247	syl 14	. . . . . . . 8
249	248	nnzd 9779	. . . . . . 7
250	225, 58	nnmulcld 9363	. . . . . . . 8
251	250	nnzd 9779	. . . . . . 7
252		pc2dvds 13139	. . . . . . 7 $/\$
253	249, 251, 252	syl2anc 415	. . . . . 6
254	246, 253	mpbird 167	. . . . 5
255		dvdsle 12637	. . . . . 6 $/\$
256	249, 250, 255	syl2anc 415	. . . . 5
257	254, 256	mpd 13	. . . 4
258	15	recnd 8361	. . . . . 6
259	60	recnd 8361	. . . . . 6
260		efadd 12468	. . . . . 6 $/\$
261	258, 259, 260	syl2anc 415	. . . . 5
262	59	reeflogd 16125	. . . . . 6
263	262	oveq2d 6104	. . . . 5
264	261, 263	eqtrd 2271	. . . 4
265	257, 264	breqtrrd 4159	. . 3
266		efle 16014	. . . 4 $/\$
267	12, 61, 266	syl2anc 415	. . 3
268	265, 267	mpbird 167	. 2
269		0zd 9668	. . . . . . . . . 10
270	269, 87	fzfigd 10890	. . . . . . . . 9
271		elfzelz 10446	. . . . . . . . . . 11
272		bccl 11228	. . . . . . . . . . 11 $/\$
273	43, 271, 272	syl2an 289	. . . . . . . . . 10 $/\$
274	273	nn0red 9633	. . . . . . . . 9 $/\$
275	273	nn0ge0d 9635	. . . . . . . . 9 $/\$
276		nn0uz 9974	. . . . . . . . . . . 12
277	36, 276	eleqtrdi 2331	. . . . . . . . . . 11
278		fzss1 10487	. . . . . . . . . . 11
279	277, 278	syl 14	. . . . . . . . . 10
280		eluz 9952	. . . . . . . . . . . . 13 $/\$
281	154, 87, 280	syl2anc 415	. . . . . . . . . . . 12
282	54, 281	mpbird 167	. . . . . . . . . . 11
283		fzss2 10488	. . . . . . . . . . 11
284	282, 283	syl 14	. . . . . . . . . 10
285	279, 284	sstrd 3258	. . . . . . . . 9
286	36	nn0zd 9778	. . . . . . . . . 10
287	286, 154	fzfigd 10890	. . . . . . . . 9
288	270, 274, 275, 285, 287	fsumlessfi 12253	. . . . . . . 8
289		bccmpl 11215	. . . . . . . . . . . . . . 15 $/\$
290	43, 154, 289	syl2anc 415	. . . . . . . . . . . . . 14
291	113	oveq2d 6104	. . . . . . . . . . . . . 14
292	290, 291	eqtrd 2271	. . . . . . . . . . . . 13
293	58	nncnd 9328	. . . . . . . . . . . . 13
294	292, 293	eqeltrrd 2316	. . . . . . . . . . . 12
295		oveq2 6096	. . . . . . . . . . . . 13
296	295	fsum1 12205	. . . . . . . . . . . 12 $/\$
297	286, 294, 296	syl2anc 415	. . . . . . . . . . 11
298	297, 292	eqtr4d 2274	. . . . . . . . . 10
299	298	oveq1d 6103	. . . . . . . . 9
300	25, 110	npcand 8649	. . . . . . . . . . 11
301	286	uzidd 9954	. . . . . . . . . . . 12
302		peano2uz 10000	. . . . . . . . . . . 12
303	301, 302	syl 14	. . . . . . . . . . 11
304	300, 303	eqeltrrd 2316	. . . . . . . . . 10
305	285	sselda 3248	. . . . . . . . . . 11 $/\$
306	273	nn0cnd 9634	. . . . . . . . . . 11 $/\$
307	305, 306	syldan 282	. . . . . . . . . 10 $/\$
308		oveq2 6096	. . . . . . . . . 10
309	304, 307, 308	fsumm1 12209	. . . . . . . . 9
310	293	2timesd 9560	. . . . . . . . 9
311	299, 309, 310	3eqtr4rd 2282	. . . . . . . 8
312		binom11 12279	. . . . . . . . 9
313	43, 312	syl 14	. . . . . . . 8
314	288, 311, 313	3brtr4d 4163	. . . . . . 7
315		mulcom 8315	. . . . . . . 8 $/\$
316	20, 293, 315	sylancr 418	. . . . . . 7
317	34	oveq2d 6104	. . . . . . . 8
318		expp1 11005	. . . . . . . . 9 $/\$
319	20, 38, 318	sylancr 418	. . . . . . . 8
320	20	a1i 9	. . . . . . . . . . 11
321	35	a1i 9	. . . . . . . . . . 11
322	320, 36, 321	expmuld 11136	. . . . . . . . . 10
323		sq2 11094	. . . . . . . . . . 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 9327	. . . . . . 7
330		reexpcl 11015	. . . . . . . 8 $/\$
331	62, 36, 330	sylancr 418	. . . . . . 7
332		2re 9384	. . . . . . . . 9
333		2pos 9405	. . . . . . . . 9
334	332, 333	pm3.2i 272	. . . . . . . 8 $/\$
335	334	a1i 9	. . . . . . 7 $/\$
336		lemul1 8930	. . . . . . 7 $/\$ $/\$ $/\$
337	329, 331, 335, 336	syl3anc 1278	. . . . . 6
338	328, 337	mpbird 167	. . . . 5
339	66	recni 8345	. . . . . . . 8
340		mulcom 8315	. . . . . . . 8 $/\$
341	339, 109, 340	sylancr 418	. . . . . . 7
342	341	fveq2d 5702	. . . . . 6
343		reexplog 16113	. . . . . . 7 $/\$
344	64, 286, 343	sylancr 418	. . . . . 6
345	342, 344	eqtr4d 2274	. . . . 5
346	338, 262, 345	3brtr4d 4163	. . . 4
347		efle 16014	. . . . 5 $/\$
348	60, 69, 347	syl2anc 415	. . . 4
349	346, 348	mpbird 167	. . 3
350	60, 69, 15, 349	leadd2dd 8896	. 2
351	12, 61, 70, 268, 350	letrd 8458	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 8184

cr 8185

cc0 8186

c1 8187

caddc 8189

cmul 8191

clt 8367

cle 8368

cmin 8505

cdiv 9011

cn 9314

c2 9365

c4 9367

cn0 9575

cz 9656

cuz 9938

cq 10036

crp 10072

cfz 10429

cseq 10906

cexp 10997

cfa 11186

cbc 11208

csu 12145

ce 12435

cdvds 12580

cprime 12911

cpc 13093

clog 16097

ccht 16245

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

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 7028 df-dom 7029 df-fin 7030 df-sup 7331 df-inf 7332 df-pnf 8369 df-mnf 8370 df-xr 8371 df-ltxr 8372 df-le 8373 df-sub 8507 df-neg 8508 df-reap 8912 df-ap 8919 df-div 9012 df-inn 9315 df-2 9373 df-3 9374 df-4 9375 df-n0 9576 df-xnn0 9643 df-z 9657 df-uz 9939 df-q 10037 df-rp 10073 df-xneg 10192 df-xadd 10193 df-ioo 10312 df-ico 10314 df-icc 10315 df-fz 10430 df-fzo 10568 df-fl 10723 df-mod 10782 df-seqfrec 10907 df-exp 10998 df-fac 11187 df-bc 11209 df-ihash 11238 df-shft 11603 df-cj 11630 df-re 11631 df-im 11632 df-rsqrt 11787 df-abs 11788 df-clim 12071 df-sumdc 12146 df-ef 12441 df-e 12442 df-dvds 12581 df-gcd 12757 df-prm 12912 df-pc 13094 df-rest 13655 df-topgen 13674 df-psmet 14990 df-xmet 14991 df-met 14992 df-bl 14993 df-mopn 14994 df-top 15236 df-topon 15249 df-bases 15281 df-ntr 15334 df-cn 15426 df-cnp 15427 df-tx 15491 df-cncf 15809 df-limced 15894 df-dvap 15895 df-relog 16099 df-cht 16248

This theorem is used by: chtqub 16308

W3C validator