2sqlem3 - Intuitionistic Logic Explorer

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

Theorem 2sqlem3 15833

Description: Lemma for 2sqlem5 15835. (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 12939	. . . . . . . 8 $/\$
4	1, 2, 3	syl2anc 411	. . . . . . 7
5		2sqlem4.5	. . . . . . . 8
6		2sqlem4.6	. . . . . . . 8
7		gzreim 12939	. . . . . . . 8 $/\$
8	5, 6, 7	syl2anc 411	. . . . . . 7
9		gzmulcl 12938	. . . . . . 7 $/\$
10	4, 8, 9	syl2anc 411	. . . . . 6
11		gzcn 12932	. . . . . 6
12	10, 11	syl 14	. . . . 5
13		2sqlem5.2	. . . . . . 7
14		prmnn 12669	. . . . . . 7
15	13, 14	syl 14	. . . . . 6
16	15	nncnd 9145	. . . . 5
17	15	nnap0d 9177	. . . . 5 #
18	12, 16, 17	divclapd 8958	. . . 4
19	15	nnred 9144	. . . . . 6
20	19, 12, 17	redivapd 11522	. . . . 5
21		prmz 12670	. . . . . . . . . . . 12
22	13, 21	syl 14	. . . . . . . . . . 11
23		zsqcl 10860	. . . . . . . . . . . 12
24	22, 23	syl 14	. . . . . . . . . . 11
25		2sqlem5.1	. . . . . . . . . . . . 13
26	25	nnzd 9589	. . . . . . . . . . . 12
27	26, 24	zmulcld 9596	. . . . . . . . . . 11
28		dvdsmul2 12362	. . . . . . . . . . . . 13 $/\$
29	22, 22, 28	syl2anc 411	. . . . . . . . . . . 12
30	16	sqvald 10920	. . . . . . . . . . . 12
31	29, 30	breqtrrd 4112	. . . . . . . . . . 11
32		dvdsmul2 12362	. . . . . . . . . . . 12 $/\$
33	26, 24, 32	syl2anc 411	. . . . . . . . . . 11
34	22, 24, 27, 31, 33	dvdstrd 12378	. . . . . . . . . 10
35		gzcn 12932	. . . . . . . . . . . . . . . 16
36	4, 35	syl 14	. . . . . . . . . . . . . . 15
37	36	abscld 11729	. . . . . . . . . . . . . 14
38	37	recnd 8196	. . . . . . . . . . . . 13
39		gzcn 12932	. . . . . . . . . . . . . . . 16
40	8, 39	syl 14	. . . . . . . . . . . . . . 15
41	40	abscld 11729	. . . . . . . . . . . . . 14
42	41	recnd 8196	. . . . . . . . . . . . 13
43	38, 42	sqmuld 10935	. . . . . . . . . . . 12
44	1	zred 9590	. . . . . . . . . . . . . . . . 17
45	2	zred 9590	. . . . . . . . . . . . . . . . 17
46	44, 45	crred 11524	. . . . . . . . . . . . . . . 16
47	46	oveq1d 6026	. . . . . . . . . . . . . . 15
48	44, 45	crimd 11525	. . . . . . . . . . . . . . . 16
49	48	oveq1d 6026	. . . . . . . . . . . . . . 15
50	47, 49	oveq12d 6029	. . . . . . . . . . . . . 14
51	36	absvalsq2d 11731	. . . . . . . . . . . . . 14
52		2sqlem4.7	. . . . . . . . . . . . . 14
53	50, 51, 52	3eqtr4d 2272	. . . . . . . . . . . . 13
54	5	zred 9590	. . . . . . . . . . . . . . . . 17
55	6	zred 9590	. . . . . . . . . . . . . . . . 17
56	54, 55	crred 11524	. . . . . . . . . . . . . . . 16
57	56	oveq1d 6026	. . . . . . . . . . . . . . 15
58	54, 55	crimd 11525	. . . . . . . . . . . . . . . 16
59	58	oveq1d 6026	. . . . . . . . . . . . . . 15
60	57, 59	oveq12d 6029	. . . . . . . . . . . . . 14
61	40	absvalsq2d 11731	. . . . . . . . . . . . . 14
62		2sqlem4.8	. . . . . . . . . . . . . 14
63	60, 61, 62	3eqtr4d 2272	. . . . . . . . . . . . 13
64	53, 63	oveq12d 6029	. . . . . . . . . . . 12
65	25	nncnd 9145	. . . . . . . . . . . . 13
66	65, 16, 16	mulassd 8191	. . . . . . . . . . . 12
67	43, 64, 66	3eqtrd 2266	. . . . . . . . . . 11
68	36, 40	absmuld 11742	. . . . . . . . . . . 12
69	68	oveq1d 6026	. . . . . . . . . . 11
70	30	oveq2d 6027	. . . . . . . . . . 11
71	67, 69, 70	3eqtr4d 2272	. . . . . . . . . 10
72	34, 71	breqtrrd 4112	. . . . . . . . 9
73	12	absvalsq2d 11731	. . . . . . . . . 10
74		elgz 12931	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	74	simp2bi 1037	. . . . . . . . . . . . . 14
76	10, 75	syl 14	. . . . . . . . . . . . 13
77		zsqcl 10860	. . . . . . . . . . . . 13
78	76, 77	syl 14	. . . . . . . . . . . 12
79	78	zcnd 9591	. . . . . . . . . . 11
80	74	simp3bi 1038	. . . . . . . . . . . . . 14
81	10, 80	syl 14	. . . . . . . . . . . . 13
82		zsqcl 10860	. . . . . . . . . . . . 13
83	81, 82	syl 14	. . . . . . . . . . . 12
84	83	zcnd 9591	. . . . . . . . . . 11
85	79, 84	addcomd 8318	. . . . . . . . . 10
86	73, 85	eqtrd 2262	. . . . . . . . 9
87	72, 86	breqtrd 4110	. . . . . . . 8
88		2sqlem4.9	. . . . . . . . . . . 12
89	5	zcnd 9591	. . . . . . . . . . . . . . 15
90	2	zcnd 9591	. . . . . . . . . . . . . . 15
91	89, 90	mulcld 8188	. . . . . . . . . . . . . 14
92	1	zcnd 9591	. . . . . . . . . . . . . . 15
93	6	zcnd 9591	. . . . . . . . . . . . . . 15
94	92, 93	mulcld 8188	. . . . . . . . . . . . . 14
95	91, 94	addcomd 8318	. . . . . . . . . . . . 13
96	89, 90	mulcomd 8189	. . . . . . . . . . . . . 14
97	96	oveq2d 6027	. . . . . . . . . . . . 13
98	95, 97	eqtrd 2262	. . . . . . . . . . . 12
99	88, 98	breqtrd 4110	. . . . . . . . . . 11
100	36, 40	immuld 11512	. . . . . . . . . . . 12
101	46, 58	oveq12d 6029	. . . . . . . . . . . . 13
102	48, 56	oveq12d 6029	. . . . . . . . . . . . 13
103	101, 102	oveq12d 6029	. . . . . . . . . . . 12
104	100, 103	eqtrd 2262	. . . . . . . . . . 11
105	99, 104	breqtrrd 4112	. . . . . . . . . 10
106		2nn 9293	. . . . . . . . . . . 12
107	106	a1i 9	. . . . . . . . . . 11
108		prmdvdsexp 12707	. . . . . . . . . . 11 $/\$ $/\$
109	13, 81, 107, 108	syl3anc 1271	. . . . . . . . . 10
110	105, 109	mpbird 167	. . . . . . . . 9
111		dvdsadd2b 12388	. . . . . . . . 9 $/\$ $/\$ $/\$
112	22, 78, 83, 110, 111	syl112anc 1275	. . . . . . . 8
113	87, 112	mpbird 167	. . . . . . 7
114		prmdvdsexp 12707	. . . . . . . 8 $/\$ $/\$
115	13, 76, 107, 114	syl3anc 1271	. . . . . . 7
116	113, 115	mpbid 147	. . . . . 6
117	15	nnne0d 9176	. . . . . . 7
118		dvdsval2 12338	. . . . . . 7 $/\$ $/\$
119	22, 117, 76, 118	syl3anc 1271	. . . . . 6
120	116, 119	mpbid 147	. . . . 5
121	20, 120	eqeltrd 2306	. . . 4
122	19, 12, 17	imdivapd 11523	. . . . 5
123		dvdsval2 12338	. . . . . . 7 $/\$ $/\$
124	22, 117, 81, 123	syl3anc 1271	. . . . . 6
125	105, 124	mpbid 147	. . . . 5
126	122, 125	eqeltrd 2306	. . . 4
127		elgz 12931	. . . 4 $/\$ $/\$
128	18, 121, 126, 127	syl3anbrc 1205	. . 3
129	12, 16, 17	absdivapd 11743	. . . . . 6
130	15	nnnn0d 9443	. . . . . . . . 9
131	130	nn0ge0d 9446	. . . . . . . 8
132	19, 131	absidd 11715	. . . . . . 7
133	132	oveq2d 6027	. . . . . 6
134	129, 133	eqtrd 2262	. . . . 5
135	134	oveq1d 6026	. . . 4
136	12	abscld 11729	. . . . . 6
137	136	recnd 8196	. . . . 5
138	137, 16, 17	sqdivapd 10936	. . . 4
139	71	oveq1d 6026	. . . . 5
140	15	nnsqcld 10944	. . . . . . 7
141	140	nncnd 9145	. . . . . 6
142	140	nnap0d 9177	. . . . . 6 #
143	65, 141, 142	divcanap4d 8964	. . . . 5
144	139, 143	eqtrd 2262	. . . 4
145	135, 138, 144	3eqtrrd 2267	. . 3
146		fveq2 5633	. . . . 5
147	146	oveq1d 6026	. . . 4
148	147	rspceeqv 2926	. . 3 $/\$
149	128, 145, 148	syl2anc 411	. 2
150		2sq.1	. . 3
151	150	2sqlem1 15830	. 2
152	149, 151	sylibr 134	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 105

wceq 1395

wcel 2200

wne 2400

wrex 2509 class class class wbr 4084

cmpt 4146

crn 4722

cfv 5322 (class class class)co 6011

cc 8018

cc0 8020

ci 8022

caddc 8023

cmul 8025

cdiv 8840

cn 9131

c2 9182

cz 9467

cexp 10788

cre 11388

cim 11389

cabs 11545

cdvds 12335

cprime 12666

cgz 12929

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4200 ax-sep 4203 ax-nul 4211 ax-pow 4260 ax-pr 4295 ax-un 4526 ax-setind 4631 ax-iinf 4682 ax-cnex 8111 ax-resscn 8112 ax-1cn 8113 ax-1re 8114 ax-icn 8115 ax-addcl 8116 ax-addrcl 8117 ax-mulcl 8118 ax-mulrcl 8119 ax-addcom 8120 ax-mulcom 8121 ax-addass 8122 ax-mulass 8123 ax-distr 8124 ax-i2m1 8125 ax-0lt1 8126 ax-1rid 8127 ax-0id 8128 ax-rnegex 8129 ax-precex 8130 ax-cnre 8131 ax-pre-ltirr 8132 ax-pre-ltwlin 8133 ax-pre-lttrn 8134 ax-pre-apti 8135 ax-pre-ltadd 8136 ax-pre-mulgt0 8137 ax-pre-mulext 8138 ax-arch 8139 ax-caucvg 8140

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2802 df-sbc 3030 df-csb 3126 df-dif 3200 df-un 3202 df-in 3204 df-ss 3211 df-nul 3493 df-if 3604 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3890 df-int 3925 df-iun 3968 df-br 4085 df-opab 4147 df-mpt 4148 df-tr 4184 df-id 4386 df-po 4389 df-iso 4390 df-iord 4459 df-on 4461 df-ilim 4462 df-suc 4464 df-iom 4685 df-xp 4727 df-rel 4728 df-cnv 4729 df-co 4730 df-dm 4731 df-rn 4732 df-res 4733 df-ima 4734 df-iota 5282 df-fun 5324 df-fn 5325 df-f 5326 df-f1 5327 df-fo 5328 df-f1o 5329 df-fv 5330 df-riota 5964 df-ov 6014 df-oprab 6015 df-mpo 6016 df-1st 6296 df-2nd 6297 df-recs 6464 df-frec 6550 df-1o 6575 df-2o 6576 df-er 6695 df-en 6903 df-sup 7172 df-pnf 8204 df-mnf 8205 df-xr 8206 df-ltxr 8207 df-le 8208 df-sub 8340 df-neg 8341 df-reap 8743 df-ap 8750 df-div 8841 df-inn 9132 df-2 9190 df-3 9191 df-4 9192 df-n0 9391 df-z 9468 df-uz 9744 df-q 9842 df-rp 9877 df-fz 10232 df-fzo 10366 df-fl 10518 df-mod 10573 df-seqfrec 10698 df-exp 10789 df-cj 11390 df-re 11391 df-im 11392 df-rsqrt 11546 df-abs 11547 df-dvds 12336 df-gcd 12512 df-prm 12667 df-gz 12930

This theorem is referenced by: 2sqlem4 15834

W3C validator