gausslemma2dlem1f1o - Intuitionistic Logic Explorer

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

Theorem gausslemma2dlem1f1o 15124

Description: Lemma for gausslemma2dlem1 15125. (Contributed by Jim Kingdon, 9-Aug-2025.)

**Hypotheses**
Ref	Expression
gausslemma2d.p	$\$
gausslemma2d.h
gausslemma2d.r

**Assertion**
Ref	Expression
gausslemma2dlem1f1o

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem gausslemma2dlem1f1o Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gausslemma2d.p	. . . . . . . . . 10 $\$
2	1	adantr 276	. . . . . . . . 9 $/\$ $\$
3		gausslemma2d.h	. . . . . . . . 9
4		gausslemma2d.r	. . . . . . . . 9
5		simpr 110	. . . . . . . . 9 $/\$
6	2, 3, 4, 5	gausslemma2dlem1cl 15123	. . . . . . . 8 $/\$
7	6	ralrimiva 2567	. . . . . . 7
8	4	fnmpt 5372	. . . . . . 7
9	7, 8	syl 14	. . . . . 6
10		dffn4 5474	. . . . . 6
11	9, 10	sylib 122	. . . . 5
12	1, 3, 4	gausslemma2dlem1a 15122	. . . . . 6
13		foeq3 5466	. . . . . 6
14	12, 13	syl 14	. . . . 5
15	11, 14	mpbid 147	. . . 4
16		fof 5468	. . . 4
17	15, 16	syl 14	. . 3
18		simprl 529	. . . . . . . . . . 11 $/\$ $/\$
19	18	elfzelzd 10082	. . . . . . . . . 10 $/\$ $/\$
20	19	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$
21	20	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
22	21	zcnd 9430	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
23		simprr 531	. . . . . . . . . 10 $/\$ $/\$
24	23	elfzelzd 10082	. . . . . . . . 9 $/\$ $/\$
25	24	ad2antrr 488	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
26	25	zcnd 9430	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
27		2cnd 9045	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
28		2ap0 9065	. . . . . . . 8 #
29	28	a1i 9	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ #
30		simplr 528	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
31		oveq1 5917	. . . . . . . . . . . . 13
32	31	breq1d 4039	. . . . . . . . . . . 12
33	31	oveq2d 5926	. . . . . . . . . . . 12
34	32, 31, 33	ifbieq12d 3583	. . . . . . . . . . 11
35	1	adantr 276	. . . . . . . . . . . 12 $/\$ $/\$ $\$
36	35, 3, 4, 18	gausslemma2dlem1cl 15123	. . . . . . . . . . 11 $/\$ $/\$
37	4, 34, 18, 36	fvmptd3 5643	. . . . . . . . . 10 $/\$ $/\$
38	37	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
39		simpr 110	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
40	39	iftrued 3564	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
41	38, 40	eqtrd 2226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
42		oveq1 5917	. . . . . . . . . . . . 13
43	42	breq1d 4039	. . . . . . . . . . . 12
44	42	oveq2d 5926	. . . . . . . . . . . 12
45	43, 42, 44	ifbieq12d 3583	. . . . . . . . . . 11
46	35, 3, 4, 23	gausslemma2dlem1cl 15123	. . . . . . . . . . 11 $/\$ $/\$
47	4, 45, 23, 46	fvmptd3 5643	. . . . . . . . . 10 $/\$ $/\$
48	47	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
49		2z 9335	. . . . . . . . . . . . . . . 16
50		dvdsmul2 11947	. . . . . . . . . . . . . . . 16 $/\$
51	19, 49, 50	sylancl 413	. . . . . . . . . . . . . . 15 $/\$ $/\$
52	51	ad2antrr 488	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
53	52, 41	breqtrrd 4057	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
54	53	adantr 276	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
55		eldifi 3281	. . . . . . . . . . . . . . . . . . 19 $\$
56		prmz 12239	. . . . . . . . . . . . . . . . . . 19
57	55, 56	syl 14	. . . . . . . . . . . . . . . . . 18 $\$
58	35, 57	syl 14	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
59		oddn2prm 12389	. . . . . . . . . . . . . . . . . . 19 $\$
60	1, 59	syl 14	. . . . . . . . . . . . . . . . . 18
61	60	adantr 276	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
62	49	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
63	24, 62	zmulcld 9435	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
64		dvdsmul2 11947	. . . . . . . . . . . . . . . . . 18 $/\$
65	24, 49, 64	sylancl 413	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
66		omeo 12029	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
67	58, 61, 63, 65, 66	syl22anc 1250	. . . . . . . . . . . . . . . 16 $/\$ $/\$
68	67	adantr 276	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
69	47	adantr 276	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
70		simpr 110	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
71	70	iffalsed 3567	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
72	69, 71	eqtrd 2226	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
73	72	breq2d 4041	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
74	68, 73	mtbird 674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
75	74	ad4ant14 514	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
76		simpr 110	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
77	76	breq2d 4041	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
78	77	ad2antrr 488	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
79	75, 78	mtbird 674	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
80	54, 79	pm2.65da 662	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
81		zq 9681	. . . . . . . . . . . . . . 15
82	63, 81	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$
83	1, 57	syl 14	. . . . . . . . . . . . . . . 16
84		2nn 9133	. . . . . . . . . . . . . . . 16
85		znq 9679	. . . . . . . . . . . . . . . 16 $/\$
86	83, 84, 85	sylancl 413	. . . . . . . . . . . . . . 15
87	86	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
88		qdclt 10305	. . . . . . . . . . . . . 14 $/\$ DECID
89	82, 87, 88	syl2anc 411	. . . . . . . . . . . . 13 $/\$ $/\$ DECID
90		exmiddc 837	. . . . . . . . . . . . 13 DECID $\/$
91	89, 90	syl 14	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
92	91	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\/$
93	80, 92	ecased 1360	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
94	93	iftrued 3564	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
95	48, 94	eqtrd 2226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
96	30, 41, 95	3eqtr3d 2234	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
97	22, 26, 27, 29, 96	mulcanap2ad 8673	. . . . . 6 $/\$ $/\$ $/\$ $/\$
98	19	zcnd 9430	. . . . . . . 8 $/\$ $/\$
99	98	ad2antrr 488	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
100	24	zcnd 9430	. . . . . . . 8 $/\$ $/\$
101	100	ad2antrr 488	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
102		2cnd 9045	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
103	28	a1i 9	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ #
104	83	zcnd 9430	. . . . . . . . 9
105	104	ad3antrrr 492	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
106	19, 62	zmulcld 9435	. . . . . . . . . 10 $/\$ $/\$
107	106	zcnd 9430	. . . . . . . . 9 $/\$ $/\$
108	107	ad2antrr 488	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
109	63	zcnd 9430	. . . . . . . . 9 $/\$ $/\$
110	109	ad2antrr 488	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
111		simplr 528	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
112	37	ad2antrr 488	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
113		simpr 110	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
114	113	iffalsed 3567	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
115	112, 114	eqtrd 2226	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
116	47	ad2antrr 488	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
117	65	ad3antrrr 492	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
118	47	ad3antrrr 492	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
119		simpr 110	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
120	119	iftrued 3564	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
121	118, 120	eqtrd 2226	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
122	117, 121	breqtrrd 4057	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
123	77	ad2antrr 488	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
124	122, 123	mpbird 167	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
125		omeo 12029	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
126	58, 61, 106, 51, 125	syl22anc 1250	. . . . . . . . . . . . . 14 $/\$ $/\$
127	126	ad3antrrr 492	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
128	37	ad3antrrr 492	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
129		simplr 528	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
130	129	iffalsed 3567	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
131	128, 130	eqtrd 2226	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
132	131	breq2d 4041	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
133	127, 132	mtbird 674	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
134	124, 133	pm2.65da 662	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
135	134	iffalsed 3567	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
136	116, 135	eqtrd 2226	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
137	111, 115, 136	3eqtr3d 2234	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
138	105, 108, 110, 137	subcand 8361	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
139	99, 101, 102, 103, 138	mulcanap2ad 8673	. . . . . 6 $/\$ $/\$ $/\$ $/\$
140	49	a1i 9	. . . . . . . . . 10 $/\$ $/\$ $/\$
141	20, 140	zmulcld 9435	. . . . . . . . 9 $/\$ $/\$ $/\$
142		zq 9681	. . . . . . . . 9
143	141, 142	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$
144	86	ad2antrr 488	. . . . . . . 8 $/\$ $/\$ $/\$
145		qdclt 10305	. . . . . . . 8 $/\$ DECID
146	143, 144, 145	syl2anc 411	. . . . . . 7 $/\$ $/\$ $/\$ DECID
147		exmiddc 837	. . . . . . 7 DECID $\/$
148	146, 147	syl 14	. . . . . 6 $/\$ $/\$ $/\$ $\/$
149	97, 139, 148	mpjaodan 799	. . . . 5 $/\$ $/\$ $/\$
150	149	ex 115	. . . 4 $/\$ $/\$
151	150	ralrimivva 2576	. . 3
152		dff13 5803	. . 3 $/\$
153	17, 151, 152	sylanbrc 417	. 2
154		df-f1o 5253	. 2 $/\$
155	153, 15, 154	sylanbrc 417	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709 DECID wdc 835

wceq 1364

wcel 2164

wral 2472 $\$ cdif 3150

cif 3557

csn 3618 class class class wbr 4029

cmpt 4090

crn 4656

wfn 5241

wf 5242

wf1 5243

wfo 5244

wf1o 5245

cfv 5246 (class class class)co 5910

cc 7860

cc0 7862

c1 7863

cmul 7867

clt 8044

cmin 8180 # cap 8590

cdiv 8681

cn 8972

c2 9023

cz 9307

cq 9674

cfz 10064

cdvds 11920

cprime 12235

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 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4462 ax-setind 4565 ax-iinf 4616 ax-cnex 7953 ax-resscn 7954 ax-1cn 7955 ax-1re 7956 ax-icn 7957 ax-addcl 7958 ax-addrcl 7959 ax-mulcl 7960 ax-mulrcl 7961 ax-addcom 7962 ax-mulcom 7963 ax-addass 7964 ax-mulass 7965 ax-distr 7966 ax-i2m1 7967 ax-0lt1 7968 ax-1rid 7969 ax-0id 7970 ax-rnegex 7971 ax-precex 7972 ax-cnre 7973 ax-pre-ltirr 7974 ax-pre-ltwlin 7975 ax-pre-lttrn 7976 ax-pre-apti 7977 ax-pre-ltadd 7978 ax-pre-mulgt0 7979 ax-pre-mulext 7980 ax-arch 7981 ax-caucvg 7982

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-xor 1387 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 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4322 df-po 4325 df-iso 4326 df-iord 4395 df-on 4397 df-ilim 4398 df-suc 4400 df-iom 4619 df-xp 4661 df-rel 4662 df-cnv 4663 df-co 4664 df-dm 4665 df-rn 4666 df-res 4667 df-ima 4668 df-iota 5207 df-fun 5248 df-fn 5249 df-f 5250 df-f1 5251 df-fo 5252 df-f1o 5253 df-fv 5254 df-riota 5865 df-ov 5913 df-oprab 5914 df-mpo 5915 df-1st 6184 df-2nd 6185 df-recs 6349 df-frec 6435 df-1o 6460 df-2o 6461 df-er 6578 df-en 6786 df-pnf 8046 df-mnf 8047 df-xr 8048 df-ltxr 8049 df-le 8050 df-sub 8182 df-neg 8183 df-reap 8584 df-ap 8591 df-div 8682 df-inn 8973 df-2 9031 df-3 9032 df-4 9033 df-n0 9231 df-z 9308 df-uz 9583 df-q 9675 df-rp 9710 df-ioo 9948 df-fz 10065 df-fl 10329 df-mod 10384 df-seqfrec 10509 df-exp 10600 df-cj 10976 df-re 10977 df-im 10978 df-rsqrt 11132 df-abs 11133 df-dvds 11921 df-prm 12236

This theorem is referenced by: gausslemma2dlem1 15125

W3C validator