2sqlem3 - Intuitionistic Logic Explorer

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

Theorem 2sqlem3 15627

Description: Lemma for 2sqlem5 15629. (Contributed by Mario Carneiro, 20-Jun-2015.)

**Hypotheses**
Ref	Expression
2sq.1
2sqlem5.1
2sqlem5.2
2sqlem4.3
2sqlem4.4
2sqlem4.5
2sqlem4.6
2sqlem4.7
2sqlem4.8
2sqlem4.9

**Assertion**
Ref	Expression
2sqlem3

Proof of Theorem 2sqlem3 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2sqlem4.3	. . . . . . . 8
2		2sqlem4.4	. . . . . . . 8
3		gzreim 12735	. . . . . . . 8 $/\$
4	1, 2, 3	syl2anc 411	. . . . . . 7
5		2sqlem4.5	. . . . . . . 8
6		2sqlem4.6	. . . . . . . 8
7		gzreim 12735	. . . . . . . 8 $/\$
8	5, 6, 7	syl2anc 411	. . . . . . 7
9		gzmulcl 12734	. . . . . . 7 $/\$
10	4, 8, 9	syl2anc 411	. . . . . 6
11		gzcn 12728	. . . . . 6
12	10, 11	syl 14	. . . . 5
13		2sqlem5.2	. . . . . . 7
14		prmnn 12465	. . . . . . 7
15	13, 14	syl 14	. . . . . 6
16	15	nncnd 9052	. . . . 5
17	15	nnap0d 9084	. . . . 5 #
18	12, 16, 17	divclapd 8865	. . . 4
19	15	nnred 9051	. . . . . 6
20	19, 12, 17	redivapd 11318	. . . . 5
21		prmz 12466	. . . . . . . . . . . 12
22	13, 21	syl 14	. . . . . . . . . . 11
23		zsqcl 10757	. . . . . . . . . . . 12
24	22, 23	syl 14	. . . . . . . . . . 11
25		2sqlem5.1	. . . . . . . . . . . . 13
26	25	nnzd 9496	. . . . . . . . . . . 12
27	26, 24	zmulcld 9503	. . . . . . . . . . 11
28		dvdsmul2 12158	. . . . . . . . . . . . 13 $/\$
29	22, 22, 28	syl2anc 411	. . . . . . . . . . . 12
30	16	sqvald 10817	. . . . . . . . . . . 12
31	29, 30	breqtrrd 4073	. . . . . . . . . . 11
32		dvdsmul2 12158	. . . . . . . . . . . 12 $/\$
33	26, 24, 32	syl2anc 411	. . . . . . . . . . 11
34	22, 24, 27, 31, 33	dvdstrd 12174	. . . . . . . . . 10
35		gzcn 12728	. . . . . . . . . . . . . . . 16
36	4, 35	syl 14	. . . . . . . . . . . . . . 15
37	36	abscld 11525	. . . . . . . . . . . . . 14
38	37	recnd 8103	. . . . . . . . . . . . 13
39		gzcn 12728	. . . . . . . . . . . . . . . 16
40	8, 39	syl 14	. . . . . . . . . . . . . . 15
41	40	abscld 11525	. . . . . . . . . . . . . 14
42	41	recnd 8103	. . . . . . . . . . . . 13
43	38, 42	sqmuld 10832	. . . . . . . . . . . 12
44	1	zred 9497	. . . . . . . . . . . . . . . . 17
45	2	zred 9497	. . . . . . . . . . . . . . . . 17
46	44, 45	crred 11320	. . . . . . . . . . . . . . . 16
47	46	oveq1d 5961	. . . . . . . . . . . . . . 15
48	44, 45	crimd 11321	. . . . . . . . . . . . . . . 16
49	48	oveq1d 5961	. . . . . . . . . . . . . . 15
50	47, 49	oveq12d 5964	. . . . . . . . . . . . . 14
51	36	absvalsq2d 11527	. . . . . . . . . . . . . 14
52		2sqlem4.7	. . . . . . . . . . . . . 14
53	50, 51, 52	3eqtr4d 2248	. . . . . . . . . . . . 13
54	5	zred 9497	. . . . . . . . . . . . . . . . 17
55	6	zred 9497	. . . . . . . . . . . . . . . . 17
56	54, 55	crred 11320	. . . . . . . . . . . . . . . 16
57	56	oveq1d 5961	. . . . . . . . . . . . . . 15
58	54, 55	crimd 11321	. . . . . . . . . . . . . . . 16
59	58	oveq1d 5961	. . . . . . . . . . . . . . 15
60	57, 59	oveq12d 5964	. . . . . . . . . . . . . 14
61	40	absvalsq2d 11527	. . . . . . . . . . . . . 14
62		2sqlem4.8	. . . . . . . . . . . . . 14
63	60, 61, 62	3eqtr4d 2248	. . . . . . . . . . . . 13
64	53, 63	oveq12d 5964	. . . . . . . . . . . 12
65	25	nncnd 9052	. . . . . . . . . . . . 13
66	65, 16, 16	mulassd 8098	. . . . . . . . . . . 12
67	43, 64, 66	3eqtrd 2242	. . . . . . . . . . 11
68	36, 40	absmuld 11538	. . . . . . . . . . . 12
69	68	oveq1d 5961	. . . . . . . . . . 11
70	30	oveq2d 5962	. . . . . . . . . . 11
71	67, 69, 70	3eqtr4d 2248	. . . . . . . . . 10
72	34, 71	breqtrrd 4073	. . . . . . . . 9
73	12	absvalsq2d 11527	. . . . . . . . . 10
74		elgz 12727	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	74	simp2bi 1016	. . . . . . . . . . . . . 14
76	10, 75	syl 14	. . . . . . . . . . . . 13
77		zsqcl 10757	. . . . . . . . . . . . 13
78	76, 77	syl 14	. . . . . . . . . . . 12
79	78	zcnd 9498	. . . . . . . . . . 11
80	74	simp3bi 1017	. . . . . . . . . . . . . 14
81	10, 80	syl 14	. . . . . . . . . . . . 13
82		zsqcl 10757	. . . . . . . . . . . . 13
83	81, 82	syl 14	. . . . . . . . . . . 12
84	83	zcnd 9498	. . . . . . . . . . 11
85	79, 84	addcomd 8225	. . . . . . . . . 10
86	73, 85	eqtrd 2238	. . . . . . . . 9
87	72, 86	breqtrd 4071	. . . . . . . 8
88		2sqlem4.9	. . . . . . . . . . . 12
89	5	zcnd 9498	. . . . . . . . . . . . . . 15
90	2	zcnd 9498	. . . . . . . . . . . . . . 15
91	89, 90	mulcld 8095	. . . . . . . . . . . . . 14
92	1	zcnd 9498	. . . . . . . . . . . . . . 15
93	6	zcnd 9498	. . . . . . . . . . . . . . 15
94	92, 93	mulcld 8095	. . . . . . . . . . . . . 14
95	91, 94	addcomd 8225	. . . . . . . . . . . . 13
96	89, 90	mulcomd 8096	. . . . . . . . . . . . . 14
97	96	oveq2d 5962	. . . . . . . . . . . . 13
98	95, 97	eqtrd 2238	. . . . . . . . . . . 12
99	88, 98	breqtrd 4071	. . . . . . . . . . 11
100	36, 40	immuld 11308	. . . . . . . . . . . 12
101	46, 58	oveq12d 5964	. . . . . . . . . . . . 13
102	48, 56	oveq12d 5964	. . . . . . . . . . . . 13
103	101, 102	oveq12d 5964	. . . . . . . . . . . 12
104	100, 103	eqtrd 2238	. . . . . . . . . . 11
105	99, 104	breqtrrd 4073	. . . . . . . . . 10
106		2nn 9200	. . . . . . . . . . . 12
107	106	a1i 9	. . . . . . . . . . 11
108		prmdvdsexp 12503	. . . . . . . . . . 11 $/\$ $/\$
109	13, 81, 107, 108	syl3anc 1250	. . . . . . . . . 10
110	105, 109	mpbird 167	. . . . . . . . 9
111		dvdsadd2b 12184	. . . . . . . . 9 $/\$ $/\$ $/\$
112	22, 78, 83, 110, 111	syl112anc 1254	. . . . . . . 8
113	87, 112	mpbird 167	. . . . . . 7
114		prmdvdsexp 12503	. . . . . . . 8 $/\$ $/\$
115	13, 76, 107, 114	syl3anc 1250	. . . . . . 7
116	113, 115	mpbid 147	. . . . . 6
117	15	nnne0d 9083	. . . . . . 7
118		dvdsval2 12134	. . . . . . 7 $/\$ $/\$
119	22, 117, 76, 118	syl3anc 1250	. . . . . 6
120	116, 119	mpbid 147	. . . . 5
121	20, 120	eqeltrd 2282	. . . 4
122	19, 12, 17	imdivapd 11319	. . . . 5
123		dvdsval2 12134	. . . . . . 7 $/\$ $/\$
124	22, 117, 81, 123	syl3anc 1250	. . . . . 6
125	105, 124	mpbid 147	. . . . 5
126	122, 125	eqeltrd 2282	. . . 4
127		elgz 12727	. . . 4 $/\$ $/\$
128	18, 121, 126, 127	syl3anbrc 1184	. . 3
129	12, 16, 17	absdivapd 11539	. . . . . 6
130	15	nnnn0d 9350	. . . . . . . . 9
131	130	nn0ge0d 9353	. . . . . . . 8
132	19, 131	absidd 11511	. . . . . . 7
133	132	oveq2d 5962	. . . . . 6
134	129, 133	eqtrd 2238	. . . . 5
135	134	oveq1d 5961	. . . 4
136	12	abscld 11525	. . . . . 6
137	136	recnd 8103	. . . . 5
138	137, 16, 17	sqdivapd 10833	. . . 4
139	71	oveq1d 5961	. . . . 5
140	15	nnsqcld 10841	. . . . . . 7
141	140	nncnd 9052	. . . . . 6
142	140	nnap0d 9084	. . . . . 6 #
143	65, 141, 142	divcanap4d 8871	. . . . 5
144	139, 143	eqtrd 2238	. . . 4
145	135, 138, 144	3eqtrrd 2243	. . 3
146		fveq2 5578	. . . . 5
147	146	oveq1d 5961	. . . 4
148	147	rspceeqv 2895	. . 3 $/\$
149	128, 145, 148	syl2anc 411	. 2
150		2sq.1	. . 3
151	150	2sqlem1 15624	. 2
152	149, 151	sylibr 134	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 105

wceq 1373

wcel 2176

wne 2376

wrex 2485 class class class wbr 4045

cmpt 4106

crn 4677

cfv 5272 (class class class)co 5946

cc 7925

cc0 7927

ci 7929

caddc 7930

cmul 7932

cdiv 8747

cn 9038

c2 9089

cz 9374

cexp 10685

cre 11184

cim 11185

cabs 11341

cdvds 12131

cprime 12462

cgz 12725

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-coll 4160 ax-sep 4163 ax-nul 4171 ax-pow 4219 ax-pr 4254 ax-un 4481 ax-setind 4586 ax-iinf 4637 ax-cnex 8018 ax-resscn 8019 ax-1cn 8020 ax-1re 8021 ax-icn 8022 ax-addcl 8023 ax-addrcl 8024 ax-mulcl 8025 ax-mulrcl 8026 ax-addcom 8027 ax-mulcom 8028 ax-addass 8029 ax-mulass 8030 ax-distr 8031 ax-i2m1 8032 ax-0lt1 8033 ax-1rid 8034 ax-0id 8035 ax-rnegex 8036 ax-precex 8037 ax-cnre 8038 ax-pre-ltirr 8039 ax-pre-ltwlin 8040 ax-pre-lttrn 8041 ax-pre-apti 8042 ax-pre-ltadd 8043 ax-pre-mulgt0 8044 ax-pre-mulext 8045 ax-arch 8046 ax-caucvg 8047

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-nel 2472 df-ral 2489 df-rex 2490 df-reu 2491 df-rmo 2492 df-rab 2493 df-v 2774 df-sbc 2999 df-csb 3094 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-if 3572 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-iun 3929 df-br 4046 df-opab 4107 df-mpt 4108 df-tr 4144 df-id 4341 df-po 4344 df-iso 4345 df-iord 4414 df-on 4416 df-ilim 4417 df-suc 4419 df-iom 4640 df-xp 4682 df-rel 4683 df-cnv 4684 df-co 4685 df-dm 4686 df-rn 4687 df-res 4688 df-ima 4689 df-iota 5233 df-fun 5274 df-fn 5275 df-f 5276 df-f1 5277 df-fo 5278 df-f1o 5279 df-fv 5280 df-riota 5901 df-ov 5949 df-oprab 5950 df-mpo 5951 df-1st 6228 df-2nd 6229 df-recs 6393 df-frec 6479 df-1o 6504 df-2o 6505 df-er 6622 df-en 6830 df-sup 7088 df-pnf 8111 df-mnf 8112 df-xr 8113 df-ltxr 8114 df-le 8115 df-sub 8247 df-neg 8248 df-reap 8650 df-ap 8657 df-div 8748 df-inn 9039 df-2 9097 df-3 9098 df-4 9099 df-n0 9298 df-z 9375 df-uz 9651 df-q 9743 df-rp 9778 df-fz 10133 df-fzo 10267 df-fl 10415 df-mod 10470 df-seqfrec 10595 df-exp 10686 df-cj 11186 df-re 11187 df-im 11188 df-rsqrt 11342 df-abs 11343 df-dvds 12132 df-gcd 12308 df-prm 12463 df-gz 12726

This theorem is referenced by: 2sqlem4 15628

W3C validator