lgsquad2lem1 - Intuitionistic Logic Explorer

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

Theorem lgsquad2lem1 15725

Description: Lemma for lgsquad2 15727. (Contributed by Mario Carneiro, 19-Jun-2015.)

**Hypotheses**
Ref	Expression
lgsquad2.1
lgsquad2.2
lgsquad2.3
lgsquad2.4
lgsquad2.5
lgsquad2lem1.a
lgsquad2lem1.b
lgsquad2lem1.m
lgsquad2lem1.1
lgsquad2lem1.2

**Assertion**
Ref	Expression
lgsquad2lem1

**Proof of Theorem lgsquad2lem1**
Step	Hyp	Ref	Expression
1		lgsquad2lem1.m	. . . . . . . . . . 11
2		lgsquad2lem1.a	. . . . . . . . . . . . . . . 16
3	2	nnzd 9536	. . . . . . . . . . . . . . 15
4	3	zcnd 9538	. . . . . . . . . . . . . 14
5		ax-1cn 8060	. . . . . . . . . . . . . 14
6		npcan 8323	. . . . . . . . . . . . . 14 $/\$
7	4, 5, 6	sylancl 413	. . . . . . . . . . . . 13
8		lgsquad2lem1.b	. . . . . . . . . . . . . . . 16
9	8	nnzd 9536	. . . . . . . . . . . . . . 15
10	9	zcnd 9538	. . . . . . . . . . . . . 14
11		npcan 8323	. . . . . . . . . . . . . 14 $/\$
12	10, 5, 11	sylancl 413	. . . . . . . . . . . . 13
13	7, 12	oveq12d 5992	. . . . . . . . . . . 12
14		peano2zm 9452	. . . . . . . . . . . . . . . 16
15	3, 14	syl 14	. . . . . . . . . . . . . . 15
16	15	zcnd 9538	. . . . . . . . . . . . . 14
17	5	a1i 9	. . . . . . . . . . . . . 14
18		peano2zm 9452	. . . . . . . . . . . . . . . 16
19	9, 18	syl 14	. . . . . . . . . . . . . . 15
20	19	zcnd 9538	. . . . . . . . . . . . . 14
21	16, 17, 20, 17	muladdd 8530	. . . . . . . . . . . . 13
22		1t1e1 9231	. . . . . . . . . . . . . . . 16
23	22	a1i 9	. . . . . . . . . . . . . . 15
24	23	oveq2d 5990	. . . . . . . . . . . . . 14
25	16	mulridd 8131	. . . . . . . . . . . . . . 15
26	20	mulridd 8131	. . . . . . . . . . . . . . 15
27	25, 26	oveq12d 5992	. . . . . . . . . . . . . 14
28	24, 27	oveq12d 5992	. . . . . . . . . . . . 13
29	21, 28	eqtrd 2242	. . . . . . . . . . . 12
30	13, 29	eqtr3d 2244	. . . . . . . . . . 11
31	1, 30	eqtr3d 2244	. . . . . . . . . 10
32	31	oveq1d 5989	. . . . . . . . 9
33	16, 20	mulcld 8135	. . . . . . . . . . 11
34		addcl 8092	. . . . . . . . . . 11 $/\$
35	33, 5, 34	sylancl 413	. . . . . . . . . 10
36	16, 20	addcld 8134	. . . . . . . . . 10
37	35, 36, 17	addsubd 8446	. . . . . . . . 9
38		pncan 8320	. . . . . . . . . . 11 $/\$
39	33, 5, 38	sylancl 413	. . . . . . . . . 10
40	39	oveq1d 5989	. . . . . . . . 9
41	32, 37, 40	3eqtrd 2246	. . . . . . . 8
42	41	oveq1d 5989	. . . . . . 7
43		2cnd 9151	. . . . . . . 8
44		2ap0 9171	. . . . . . . . 9 #
45	44	a1i 9	. . . . . . . 8 #
46	33, 36, 43, 45	divdirapd 8944	. . . . . . 7
47	16, 20, 43, 45	divassapd 8941	. . . . . . . . 9
48	16, 43, 45	divcanap2d 8907	. . . . . . . . . 10
49	48	oveq1d 5989	. . . . . . . . 9
50		lgsquad2.2	. . . . . . . . . . . . . 14
51		dvdsmul1 12290	. . . . . . . . . . . . . . . . 17 $/\$
52	3, 9, 51	syl2anc 411	. . . . . . . . . . . . . . . 16
53	52, 1	breqtrd 4088	. . . . . . . . . . . . . . 15
54		2z 9442	. . . . . . . . . . . . . . . 16
55		lgsquad2.1	. . . . . . . . . . . . . . . . 17
56	55	nnzd 9536	. . . . . . . . . . . . . . . 16
57		dvdstr 12305	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
58	54, 3, 56, 57	mp3an2i 1357	. . . . . . . . . . . . . . 15 $/\$
59	53, 58	mpan2d 428	. . . . . . . . . . . . . 14
60	50, 59	mtod 667	. . . . . . . . . . . . 13
61		1zzd 9441	. . . . . . . . . . . . 13
62		2prm 12615	. . . . . . . . . . . . . 14
63		nprmdvds1 12628	. . . . . . . . . . . . . 14
64	62, 63	mp1i 10	. . . . . . . . . . . . 13
65		omoe 12373	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
66	3, 60, 61, 64, 65	syl22anc 1253	. . . . . . . . . . . 12
67		2ne0 9170	. . . . . . . . . . . . . 14
68	67	a1i 9	. . . . . . . . . . . . 13
69		dvdsval2 12267	. . . . . . . . . . . . 13 $/\$ $/\$
70	54, 68, 15, 69	mp3an2i 1357	. . . . . . . . . . . 12
71	66, 70	mpbid 147	. . . . . . . . . . 11
72	71	zcnd 9538	. . . . . . . . . 10
73		dvdsmul2 12291	. . . . . . . . . . . . . . . . 17 $/\$
74	3, 9, 73	syl2anc 411	. . . . . . . . . . . . . . . 16
75	74, 1	breqtrd 4088	. . . . . . . . . . . . . . 15
76		dvdstr 12305	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
77	54, 9, 56, 76	mp3an2i 1357	. . . . . . . . . . . . . . 15 $/\$
78	75, 77	mpan2d 428	. . . . . . . . . . . . . 14
79	50, 78	mtod 667	. . . . . . . . . . . . 13
80		omoe 12373	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
81	9, 79, 61, 64, 80	syl22anc 1253	. . . . . . . . . . . 12
82		dvdsval2 12267	. . . . . . . . . . . . 13 $/\$ $/\$
83	54, 68, 19, 82	mp3an2i 1357	. . . . . . . . . . . 12
84	81, 83	mpbid 147	. . . . . . . . . . 11
85	84	zcnd 9538	. . . . . . . . . 10
86	43, 72, 85	mulassd 8138	. . . . . . . . 9
87	47, 49, 86	3eqtr2d 2248	. . . . . . . 8
88	16, 20, 43, 45	divdirapd 8944	. . . . . . . 8
89	87, 88	oveq12d 5992	. . . . . . 7
90	42, 46, 89	3eqtrd 2246	. . . . . 6
91	90	oveq1d 5989	. . . . 5
92	54	a1i 9	. . . . . . . 8
93	71, 84	zmulcld 9543	. . . . . . . 8
94	92, 93	zmulcld 9543	. . . . . . 7
95	94	zcnd 9538	. . . . . 6
96	71, 84	zaddcld 9541	. . . . . . 7
97	96	zcnd 9538	. . . . . 6
98		lgsquad2.3	. . . . . . . . . 10
99	98	nnzd 9536	. . . . . . . . 9
100		lgsquad2.4	. . . . . . . . 9
101		omoe 12373	. . . . . . . . 9 $/\$ $/\$ $/\$
102	99, 100, 61, 64, 101	syl22anc 1253	. . . . . . . 8
103		peano2zm 9452	. . . . . . . . . 10
104	99, 103	syl 14	. . . . . . . . 9
105		dvdsval2 12267	. . . . . . . . 9 $/\$ $/\$
106	54, 68, 104, 105	mp3an2i 1357	. . . . . . . 8
107	102, 106	mpbid 147	. . . . . . 7
108	107	zcnd 9538	. . . . . 6
109	95, 97, 108	adddird 8140	. . . . 5
110	93	zcnd 9538	. . . . . . 7
111	43, 110, 108	mulassd 8138	. . . . . 6
112	111	oveq1d 5989	. . . . 5
113	91, 109, 112	3eqtrd 2246	. . . 4
114	113	oveq2d 5990	. . 3
115		neg1cn 9183	. . . . . 6
116	115	a1i 9	. . . . 5
117		neg1ap0 9187	. . . . . 6 #
118	117	a1i 9	. . . . 5 #
119	93, 107	zmulcld 9543	. . . . . 6
120	92, 119	zmulcld 9543	. . . . 5
121	96, 107	zmulcld 9543	. . . . 5
122		expaddzap 10772	. . . . 5 $/\$ # $/\$ $/\$
123	116, 118, 120, 121, 122	syl22anc 1253	. . . 4
124		expmulzap 10774	. . . . . . 7 $/\$ # $/\$ $/\$
125	116, 118, 92, 119, 124	syl22anc 1253	. . . . . 6
126		neg1sqe1 10823	. . . . . . . 8
127	126	oveq1i 5984	. . . . . . 7
128		1exp 10757	. . . . . . . 8
129	119, 128	syl 14	. . . . . . 7
130	127, 129	eqtrid 2254	. . . . . 6
131	125, 130	eqtrd 2242	. . . . 5
132	131	oveq1d 5989	. . . 4
133	123, 132	eqtrd 2242	. . 3
134	116, 118, 121	expclzapd 10867	. . . . 5
135	134	mullidd 8132	. . . 4
136	72, 85, 108	adddird 8140	. . . . 5
137	136	oveq2d 5990	. . . 4
138	135, 137	eqtrd 2242	. . 3
139	114, 133, 138	3eqtrd 2246	. 2
140		lgsquad2lem1.1	. . . 4
141		lgsquad2lem1.2	. . . 4
142	140, 141	oveq12d 5992	. . 3
143	71, 107	zmulcld 9543	. . . 4
144	84, 107	zmulcld 9543	. . . 4
145		expaddzap 10772	. . . 4 $/\$ # $/\$ $/\$
146	116, 118, 143, 144, 145	syl22anc 1253	. . 3
147	142, 146	eqtr4d 2245	. 2
148		lgscl 15658	. . . . . 6 $/\$
149	3, 99, 148	syl2anc 411	. . . . 5
150	149	zcnd 9538	. . . 4
151		lgscl 15658	. . . . . 6 $/\$
152	9, 99, 151	syl2anc 411	. . . . 5
153	152	zcnd 9538	. . . 4
154		lgscl 15658	. . . . . 6 $/\$
155	99, 3, 154	syl2anc 411	. . . . 5
156	155	zcnd 9538	. . . 4
157		lgscl 15658	. . . . . 6 $/\$
158	99, 9, 157	syl2anc 411	. . . . 5
159	158	zcnd 9538	. . . 4
160	150, 153, 156, 159	mul4d 8269	. . 3
161	2	nnne0d 9123	. . . . . 6
162	8	nnne0d 9123	. . . . . 6
163		lgsdir 15679	. . . . . 6 $/\$ $/\$ $/\$ $/\$
164	3, 9, 99, 161, 162, 163	syl32anc 1260	. . . . 5
165	1	oveq1d 5989	. . . . 5
166	164, 165	eqtr3d 2244	. . . 4
167		lgsdi 15681	. . . . . 6 $/\$ $/\$ $/\$ $/\$
168	99, 3, 9, 161, 162, 167	syl32anc 1260	. . . . 5
169	1	oveq2d 5990	. . . . 5
170	168, 169	eqtr3d 2244	. . . 4
171	166, 170	oveq12d 5992	. . 3
172	160, 171	eqtr3d 2244	. 2
173	139, 147, 172	3eqtr2rd 2249	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105

wceq 1375

wcel 2180

wne 2380 class class class wbr 4062 (class class class)co 5974

cc 7965

cc0 7967

c1 7968

caddc 7970

cmul 7972

cmin 8285

cneg 8286 # cap 8696

cdiv 8787

cn 9078

c2 9129

cz 9414

cexp 10727

cdvds 12264

cgcd 12440

cprime 12595

clgs 15641

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 713 ax-5 1473 ax-7 1474 ax-gen 1475 ax-ie1 1519 ax-ie2 1520 ax-8 1530 ax-10 1531 ax-11 1532 ax-i12 1533 ax-bndl 1535 ax-4 1536 ax-17 1552 ax-i9 1556 ax-ial 1560 ax-i5r 1561 ax-13 2182 ax-14 2183 ax-ext 2191 ax-coll 4178 ax-sep 4181 ax-nul 4189 ax-pow 4237 ax-pr 4272 ax-un 4501 ax-setind 4606 ax-iinf 4657 ax-cnex 8058 ax-resscn 8059 ax-1cn 8060 ax-1re 8061 ax-icn 8062 ax-addcl 8063 ax-addrcl 8064 ax-mulcl 8065 ax-mulrcl 8066 ax-addcom 8067 ax-mulcom 8068 ax-addass 8069 ax-mulass 8070 ax-distr 8071 ax-i2m1 8072 ax-0lt1 8073 ax-1rid 8074 ax-0id 8075 ax-rnegex 8076 ax-precex 8077 ax-cnre 8078 ax-pre-ltirr 8079 ax-pre-ltwlin 8080 ax-pre-lttrn 8081 ax-pre-apti 8082 ax-pre-ltadd 8083 ax-pre-mulgt0 8084 ax-pre-mulext 8085 ax-arch 8086 ax-caucvg 8087

This theorem depends on definitions: df-bi 117 df-stab 835 df-dc 839 df-3or 984 df-3an 985 df-tru 1378 df-fal 1381 df-xor 1398 df-nf 1487 df-sb 1789 df-eu 2060 df-mo 2061 df-clab 2196 df-cleq 2202 df-clel 2205 df-nfc 2341 df-ne 2381 df-nel 2476 df-ral 2493 df-rex 2494 df-reu 2495 df-rmo 2496 df-rab 2497 df-v 2781 df-sbc 3009 df-csb 3105 df-dif 3179 df-un 3181 df-in 3183 df-ss 3190 df-nul 3472 df-if 3583 df-pw 3631 df-sn 3652 df-pr 3653 df-op 3655 df-uni 3868 df-int 3903 df-iun 3946 df-br 4063 df-opab 4125 df-mpt 4126 df-tr 4162 df-id 4361 df-po 4364 df-iso 4365 df-iord 4434 df-on 4436 df-ilim 4437 df-suc 4439 df-iom 4660 df-xp 4702 df-rel 4703 df-cnv 4704 df-co 4705 df-dm 4706 df-rn 4707 df-res 4708 df-ima 4709 df-iota 5254 df-fun 5296 df-fn 5297 df-f 5298 df-f1 5299 df-fo 5300 df-f1o 5301 df-fv 5302 df-isom 5303 df-riota 5927 df-ov 5977 df-oprab 5978 df-mpo 5979 df-1st 6256 df-2nd 6257 df-recs 6421 df-irdg 6486 df-frec 6507 df-1o 6532 df-2o 6533 df-oadd 6536 df-er 6650 df-en 6858 df-dom 6859 df-fin 6860 df-sup 7119 df-inf 7120 df-pnf 8151 df-mnf 8152 df-xr 8153 df-ltxr 8154 df-le 8155 df-sub 8287 df-neg 8288 df-reap 8690 df-ap 8697 df-div 8788 df-inn 9079 df-2 9137 df-3 9138 df-4 9139 df-5 9140 df-6 9141 df-7 9142 df-8 9143 df-9 9144 df-n0 9338 df-z 9415 df-uz 9691 df-q 9783 df-rp 9818 df-fz 10173 df-fzo 10307 df-fl 10457 df-mod 10512 df-seqfrec 10637 df-exp 10728 df-ihash 10965 df-cj 11319 df-re 11320 df-im 11321 df-rsqrt 11475 df-abs 11476 df-clim 11756 df-proddc 12028 df-dvds 12265 df-gcd 12441 df-prm 12596 df-phi 12699 df-pc 12774 df-lgs 15642

This theorem is referenced by: lgsquad2lem2 15726

W3C validator