2sqlem3 - Intuitionistic Logic Explorer

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

Theorem 2sqlem3 15274

Description: Lemma for 2sqlem5 15276. (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 12520	. . . . . . . 8 $/\$
4	1, 2, 3	syl2anc 411	. . . . . . 7
5		2sqlem4.5	. . . . . . . 8
6		2sqlem4.6	. . . . . . . 8
7		gzreim 12520	. . . . . . . 8 $/\$
8	5, 6, 7	syl2anc 411	. . . . . . 7
9		gzmulcl 12519	. . . . . . 7 $/\$
10	4, 8, 9	syl2anc 411	. . . . . 6
11		gzcn 12513	. . . . . 6
12	10, 11	syl 14	. . . . 5
13		2sqlem5.2	. . . . . . 7
14		prmnn 12251	. . . . . . 7
15	13, 14	syl 14	. . . . . 6
16	15	nncnd 8998	. . . . 5
17	15	nnap0d 9030	. . . . 5 #
18	12, 16, 17	divclapd 8811	. . . 4
19	15	nnred 8997	. . . . . 6
20	19, 12, 17	redivapd 11121	. . . . 5
21		prmz 12252	. . . . . . . . . . . 12
22	13, 21	syl 14	. . . . . . . . . . 11
23		zsqcl 10684	. . . . . . . . . . . 12
24	22, 23	syl 14	. . . . . . . . . . 11
25		2sqlem5.1	. . . . . . . . . . . . 13
26	25	nnzd 9441	. . . . . . . . . . . 12
27	26, 24	zmulcld 9448	. . . . . . . . . . 11
28		dvdsmul2 11960	. . . . . . . . . . . . 13 $/\$
29	22, 22, 28	syl2anc 411	. . . . . . . . . . . 12
30	16	sqvald 10744	. . . . . . . . . . . 12
31	29, 30	breqtrrd 4058	. . . . . . . . . . 11
32		dvdsmul2 11960	. . . . . . . . . . . 12 $/\$
33	26, 24, 32	syl2anc 411	. . . . . . . . . . 11
34	22, 24, 27, 31, 33	dvdstrd 11976	. . . . . . . . . 10
35		gzcn 12513	. . . . . . . . . . . . . . . 16
36	4, 35	syl 14	. . . . . . . . . . . . . . 15
37	36	abscld 11328	. . . . . . . . . . . . . 14
38	37	recnd 8050	. . . . . . . . . . . . 13
39		gzcn 12513	. . . . . . . . . . . . . . . 16
40	8, 39	syl 14	. . . . . . . . . . . . . . 15
41	40	abscld 11328	. . . . . . . . . . . . . 14
42	41	recnd 8050	. . . . . . . . . . . . 13
43	38, 42	sqmuld 10759	. . . . . . . . . . . 12
44	1	zred 9442	. . . . . . . . . . . . . . . . 17
45	2	zred 9442	. . . . . . . . . . . . . . . . 17
46	44, 45	crred 11123	. . . . . . . . . . . . . . . 16
47	46	oveq1d 5934	. . . . . . . . . . . . . . 15
48	44, 45	crimd 11124	. . . . . . . . . . . . . . . 16
49	48	oveq1d 5934	. . . . . . . . . . . . . . 15
50	47, 49	oveq12d 5937	. . . . . . . . . . . . . 14
51	36	absvalsq2d 11330	. . . . . . . . . . . . . 14
52		2sqlem4.7	. . . . . . . . . . . . . 14
53	50, 51, 52	3eqtr4d 2236	. . . . . . . . . . . . 13
54	5	zred 9442	. . . . . . . . . . . . . . . . 17
55	6	zred 9442	. . . . . . . . . . . . . . . . 17
56	54, 55	crred 11123	. . . . . . . . . . . . . . . 16
57	56	oveq1d 5934	. . . . . . . . . . . . . . 15
58	54, 55	crimd 11124	. . . . . . . . . . . . . . . 16
59	58	oveq1d 5934	. . . . . . . . . . . . . . 15
60	57, 59	oveq12d 5937	. . . . . . . . . . . . . 14
61	40	absvalsq2d 11330	. . . . . . . . . . . . . 14
62		2sqlem4.8	. . . . . . . . . . . . . 14
63	60, 61, 62	3eqtr4d 2236	. . . . . . . . . . . . 13
64	53, 63	oveq12d 5937	. . . . . . . . . . . 12
65	25	nncnd 8998	. . . . . . . . . . . . 13
66	65, 16, 16	mulassd 8045	. . . . . . . . . . . 12
67	43, 64, 66	3eqtrd 2230	. . . . . . . . . . 11
68	36, 40	absmuld 11341	. . . . . . . . . . . 12
69	68	oveq1d 5934	. . . . . . . . . . 11
70	30	oveq2d 5935	. . . . . . . . . . 11
71	67, 69, 70	3eqtr4d 2236	. . . . . . . . . 10
72	34, 71	breqtrrd 4058	. . . . . . . . 9
73	12	absvalsq2d 11330	. . . . . . . . . 10
74		elgz 12512	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	74	simp2bi 1015	. . . . . . . . . . . . . 14
76	10, 75	syl 14	. . . . . . . . . . . . 13
77		zsqcl 10684	. . . . . . . . . . . . 13
78	76, 77	syl 14	. . . . . . . . . . . 12
79	78	zcnd 9443	. . . . . . . . . . 11
80	74	simp3bi 1016	. . . . . . . . . . . . . 14
81	10, 80	syl 14	. . . . . . . . . . . . 13
82		zsqcl 10684	. . . . . . . . . . . . 13
83	81, 82	syl 14	. . . . . . . . . . . 12
84	83	zcnd 9443	. . . . . . . . . . 11
85	79, 84	addcomd 8172	. . . . . . . . . 10
86	73, 85	eqtrd 2226	. . . . . . . . 9
87	72, 86	breqtrd 4056	. . . . . . . 8
88		2sqlem4.9	. . . . . . . . . . . 12
89	5	zcnd 9443	. . . . . . . . . . . . . . 15
90	2	zcnd 9443	. . . . . . . . . . . . . . 15
91	89, 90	mulcld 8042	. . . . . . . . . . . . . 14
92	1	zcnd 9443	. . . . . . . . . . . . . . 15
93	6	zcnd 9443	. . . . . . . . . . . . . . 15
94	92, 93	mulcld 8042	. . . . . . . . . . . . . 14
95	91, 94	addcomd 8172	. . . . . . . . . . . . 13
96	89, 90	mulcomd 8043	. . . . . . . . . . . . . 14
97	96	oveq2d 5935	. . . . . . . . . . . . 13
98	95, 97	eqtrd 2226	. . . . . . . . . . . 12
99	88, 98	breqtrd 4056	. . . . . . . . . . 11
100	36, 40	immuld 11111	. . . . . . . . . . . 12
101	46, 58	oveq12d 5937	. . . . . . . . . . . . 13
102	48, 56	oveq12d 5937	. . . . . . . . . . . . 13
103	101, 102	oveq12d 5937	. . . . . . . . . . . 12
104	100, 103	eqtrd 2226	. . . . . . . . . . 11
105	99, 104	breqtrrd 4058	. . . . . . . . . 10
106		2nn 9146	. . . . . . . . . . . 12
107	106	a1i 9	. . . . . . . . . . 11
108		prmdvdsexp 12289	. . . . . . . . . . 11 $/\$ $/\$
109	13, 81, 107, 108	syl3anc 1249	. . . . . . . . . 10
110	105, 109	mpbird 167	. . . . . . . . 9
111		dvdsadd2b 11986	. . . . . . . . 9 $/\$ $/\$ $/\$
112	22, 78, 83, 110, 111	syl112anc 1253	. . . . . . . 8
113	87, 112	mpbird 167	. . . . . . 7
114		prmdvdsexp 12289	. . . . . . . 8 $/\$ $/\$
115	13, 76, 107, 114	syl3anc 1249	. . . . . . 7
116	113, 115	mpbid 147	. . . . . 6
117	15	nnne0d 9029	. . . . . . 7
118		dvdsval2 11936	. . . . . . 7 $/\$ $/\$
119	22, 117, 76, 118	syl3anc 1249	. . . . . 6
120	116, 119	mpbid 147	. . . . 5
121	20, 120	eqeltrd 2270	. . . 4
122	19, 12, 17	imdivapd 11122	. . . . 5
123		dvdsval2 11936	. . . . . . 7 $/\$ $/\$
124	22, 117, 81, 123	syl3anc 1249	. . . . . 6
125	105, 124	mpbid 147	. . . . 5
126	122, 125	eqeltrd 2270	. . . 4
127		elgz 12512	. . . 4 $/\$ $/\$
128	18, 121, 126, 127	syl3anbrc 1183	. . 3
129	12, 16, 17	absdivapd 11342	. . . . . 6
130	15	nnnn0d 9296	. . . . . . . . 9
131	130	nn0ge0d 9299	. . . . . . . 8
132	19, 131	absidd 11314	. . . . . . 7
133	132	oveq2d 5935	. . . . . 6
134	129, 133	eqtrd 2226	. . . . 5
135	134	oveq1d 5934	. . . 4
136	12	abscld 11328	. . . . . 6
137	136	recnd 8050	. . . . 5
138	137, 16, 17	sqdivapd 10760	. . . 4
139	71	oveq1d 5934	. . . . 5
140	15	nnsqcld 10768	. . . . . . 7
141	140	nncnd 8998	. . . . . 6
142	140	nnap0d 9030	. . . . . 6 #
143	65, 141, 142	divcanap4d 8817	. . . . 5
144	139, 143	eqtrd 2226	. . . 4
145	135, 138, 144	3eqtrrd 2231	. . 3
146		fveq2 5555	. . . . 5
147	146	oveq1d 5934	. . . 4
148	147	rspceeqv 2883	. . 3 $/\$
149	128, 145, 148	syl2anc 411	. 2
150		2sq.1	. . 3
151	150	2sqlem1 15271	. 2
152	149, 151	sylibr 134	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 105

wceq 1364

wcel 2164

wne 2364

wrex 2473 class class class wbr 4030

cmpt 4091

crn 4661

cfv 5255 (class class class)co 5919

cc 7872

cc0 7874

ci 7876

caddc 7877

cmul 7879

cdiv 8693

cn 8984

c2 9035

cz 9320

cexp 10612

cre 10987

cim 10988

cabs 11144

cdvds 11933

cprime 12248

cgz 12510

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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4145 ax-sep 4148 ax-nul 4156 ax-pow 4204 ax-pr 4239 ax-un 4465 ax-setind 4570 ax-iinf 4621 ax-cnex 7965 ax-resscn 7966 ax-1cn 7967 ax-1re 7968 ax-icn 7969 ax-addcl 7970 ax-addrcl 7971 ax-mulcl 7972 ax-mulrcl 7973 ax-addcom 7974 ax-mulcom 7975 ax-addass 7976 ax-mulass 7977 ax-distr 7978 ax-i2m1 7979 ax-0lt1 7980 ax-1rid 7981 ax-0id 7982 ax-rnegex 7983 ax-precex 7984 ax-cnre 7985 ax-pre-ltirr 7986 ax-pre-ltwlin 7987 ax-pre-lttrn 7988 ax-pre-apti 7989 ax-pre-ltadd 7990 ax-pre-mulgt0 7991 ax-pre-mulext 7992 ax-arch 7993 ax-caucvg 7994

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2987 df-csb 3082 df-dif 3156 df-un 3158 df-in 3160 df-ss 3167 df-nul 3448 df-if 3559 df-pw 3604 df-sn 3625 df-pr 3626 df-op 3628 df-uni 3837 df-int 3872 df-iun 3915 df-br 4031 df-opab 4092 df-mpt 4093 df-tr 4129 df-id 4325 df-po 4328 df-iso 4329 df-iord 4398 df-on 4400 df-ilim 4401 df-suc 4403 df-iom 4624 df-xp 4666 df-rel 4667 df-cnv 4668 df-co 4669 df-dm 4670 df-rn 4671 df-res 4672 df-ima 4673 df-iota 5216 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-riota 5874 df-ov 5922 df-oprab 5923 df-mpo 5924 df-1st 6195 df-2nd 6196 df-recs 6360 df-frec 6446 df-1o 6471 df-2o 6472 df-er 6589 df-en 6797 df-sup 7045 df-pnf 8058 df-mnf 8059 df-xr 8060 df-ltxr 8061 df-le 8062 df-sub 8194 df-neg 8195 df-reap 8596 df-ap 8603 df-div 8694 df-inn 8985 df-2 9043 df-3 9044 df-4 9045 df-n0 9244 df-z 9321 df-uz 9596 df-q 9688 df-rp 9723 df-fz 10078 df-fzo 10212 df-fl 10342 df-mod 10397 df-seqfrec 10522 df-exp 10613 df-cj 10989 df-re 10990 df-im 10991 df-rsqrt 11145 df-abs 11146 df-dvds 11934 df-gcd 12083 df-prm 12249 df-gz 12511

This theorem is referenced by: 2sqlem4 15275

W3C validator