gausslemma2dlem1f1o - Intuitionistic Logic Explorer

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

Theorem gausslemma2dlem1f1o 15268

Description: Lemma for gausslemma2dlem1 15269. (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 15267	. . . . . . . 8 $/\$
7	6	ralrimiva 2570	. . . . . . 7
8	4	fnmpt 5384	. . . . . . 7
9	7, 8	syl 14	. . . . . 6
10		dffn4 5486	. . . . . 6
11	9, 10	sylib 122	. . . . 5
12	1, 3, 4	gausslemma2dlem1a 15266	. . . . . 6
13		foeq3 5478	. . . . . 6
14	12, 13	syl 14	. . . . 5
15	11, 14	mpbid 147	. . . 4
16		fof 5480	. . . 4
17	15, 16	syl 14	. . 3
18		simprl 529	. . . . . . . . . . 11 $/\$ $/\$
19	18	elfzelzd 10098	. . . . . . . . . 10 $/\$ $/\$
20	19	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$
21	20	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
22	21	zcnd 9446	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
23		simprr 531	. . . . . . . . . 10 $/\$ $/\$
24	23	elfzelzd 10098	. . . . . . . . 9 $/\$ $/\$
25	24	ad2antrr 488	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
26	25	zcnd 9446	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
27		2cnd 9060	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
28		2ap0 9080	. . . . . . . 8 #
29	28	a1i 9	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ #
30		simplr 528	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
31		oveq1 5929	. . . . . . . . . . . . 13
32	31	breq1d 4043	. . . . . . . . . . . 12
33	31	oveq2d 5938	. . . . . . . . . . . 12
34	32, 31, 33	ifbieq12d 3587	. . . . . . . . . . 11
35	1	adantr 276	. . . . . . . . . . . 12 $/\$ $/\$ $\$
36	35, 3, 4, 18	gausslemma2dlem1cl 15267	. . . . . . . . . . 11 $/\$ $/\$
37	4, 34, 18, 36	fvmptd3 5655	. . . . . . . . . 10 $/\$ $/\$
38	37	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
39		simpr 110	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
40	39	iftrued 3568	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
41	38, 40	eqtrd 2229	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
42		oveq1 5929	. . . . . . . . . . . . 13
43	42	breq1d 4043	. . . . . . . . . . . 12
44	42	oveq2d 5938	. . . . . . . . . . . 12
45	43, 42, 44	ifbieq12d 3587	. . . . . . . . . . 11
46	35, 3, 4, 23	gausslemma2dlem1cl 15267	. . . . . . . . . . 11 $/\$ $/\$
47	4, 45, 23, 46	fvmptd3 5655	. . . . . . . . . 10 $/\$ $/\$
48	47	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
49		2z 9351	. . . . . . . . . . . . . . . 16
50		dvdsmul2 11963	. . . . . . . . . . . . . . . 16 $/\$
51	19, 49, 50	sylancl 413	. . . . . . . . . . . . . . 15 $/\$ $/\$
52	51	ad2antrr 488	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
53	52, 41	breqtrrd 4061	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
54	53	adantr 276	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
55		eldifi 3285	. . . . . . . . . . . . . . . . . . 19 $\$
56		prmz 12255	. . . . . . . . . . . . . . . . . . 19
57	55, 56	syl 14	. . . . . . . . . . . . . . . . . 18 $\$
58	35, 57	syl 14	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
59		oddn2prm 12406	. . . . . . . . . . . . . . . . . . 19 $\$
60	1, 59	syl 14	. . . . . . . . . . . . . . . . . 18
61	60	adantr 276	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
62	49	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
63	24, 62	zmulcld 9451	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
64		dvdsmul2 11963	. . . . . . . . . . . . . . . . . 18 $/\$
65	24, 49, 64	sylancl 413	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
66		omeo 12045	. . . . . . . . . . . . . . . . 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 3571	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
72	69, 71	eqtrd 2229	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
73	72	breq2d 4045	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
74	68, 73	mtbird 674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
75	74	ad4ant14 514	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
76		simpr 110	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
77	76	breq2d 4045	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
78	77	ad2antrr 488	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
79	75, 78	mtbird 674	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
80	54, 79	pm2.65da 662	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
81		zq 9697	. . . . . . . . . . . . . . 15
82	63, 81	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$
83	1, 57	syl 14	. . . . . . . . . . . . . . . 16
84		2nn 9149	. . . . . . . . . . . . . . . 16
85		znq 9695	. . . . . . . . . . . . . . . 16 $/\$
86	83, 84, 85	sylancl 413	. . . . . . . . . . . . . . 15
87	86	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
88		qdclt 10321	. . . . . . . . . . . . . 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 3568	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
95	48, 94	eqtrd 2229	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
96	30, 41, 95	3eqtr3d 2237	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
97	22, 26, 27, 29, 96	mulcanap2ad 8688	. . . . . 6 $/\$ $/\$ $/\$ $/\$
98	19	zcnd 9446	. . . . . . . 8 $/\$ $/\$
99	98	ad2antrr 488	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
100	24	zcnd 9446	. . . . . . . 8 $/\$ $/\$
101	100	ad2antrr 488	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
102		2cnd 9060	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
103	28	a1i 9	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ #
104	83	zcnd 9446	. . . . . . . . 9
105	104	ad3antrrr 492	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
106	19, 62	zmulcld 9451	. . . . . . . . . 10 $/\$ $/\$
107	106	zcnd 9446	. . . . . . . . 9 $/\$ $/\$
108	107	ad2antrr 488	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
109	63	zcnd 9446	. . . . . . . . 9 $/\$ $/\$
110	109	ad2antrr 488	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
111		simplr 528	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
112	37	ad2antrr 488	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
113		simpr 110	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
114	113	iffalsed 3571	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
115	112, 114	eqtrd 2229	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
116	47	ad2antrr 488	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
117	65	ad3antrrr 492	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
118	47	ad3antrrr 492	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
119		simpr 110	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
120	119	iftrued 3568	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
121	118, 120	eqtrd 2229	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
122	117, 121	breqtrrd 4061	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
123	77	ad2antrr 488	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
124	122, 123	mpbird 167	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
125		omeo 12045	. . . . . . . . . . . . . . 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 3571	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
131	128, 130	eqtrd 2229	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
132	131	breq2d 4045	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
133	127, 132	mtbird 674	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
134	124, 133	pm2.65da 662	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
135	134	iffalsed 3571	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
136	116, 135	eqtrd 2229	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
137	111, 115, 136	3eqtr3d 2237	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
138	105, 108, 110, 137	subcand 8376	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
139	99, 101, 102, 103, 138	mulcanap2ad 8688	. . . . . 6 $/\$ $/\$ $/\$ $/\$
140	49	a1i 9	. . . . . . . . . 10 $/\$ $/\$ $/\$
141	20, 140	zmulcld 9451	. . . . . . . . 9 $/\$ $/\$ $/\$
142		zq 9697	. . . . . . . . 9
143	141, 142	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$
144	86	ad2antrr 488	. . . . . . . 8 $/\$ $/\$ $/\$
145		qdclt 10321	. . . . . . . 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 2579	. . 3
152		dff13 5815	. . 3 $/\$
153	17, 151, 152	sylanbrc 417	. 2
154		df-f1o 5265	. 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 2167

wral 2475 $\$ cdif 3154

cif 3561

csn 3622 class class class wbr 4033

cmpt 4094

crn 4664

wfn 5253

wf 5254

wf1 5255

wfo 5256

wf1o 5257

cfv 5258 (class class class)co 5922

cc 7875

cc0 7877

c1 7878

cmul 7882

clt 8059

cmin 8195 # cap 8605

cdiv 8696

cn 8987

c2 9038

cz 9323

cq 9690

cfz 10080

cdvds 11936

cprime 12251

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7968 ax-resscn 7969 ax-1cn 7970 ax-1re 7971 ax-icn 7972 ax-addcl 7973 ax-addrcl 7974 ax-mulcl 7975 ax-mulrcl 7976 ax-addcom 7977 ax-mulcom 7978 ax-addass 7979 ax-mulass 7980 ax-distr 7981 ax-i2m1 7982 ax-0lt1 7983 ax-1rid 7984 ax-0id 7985 ax-rnegex 7986 ax-precex 7987 ax-cnre 7988 ax-pre-ltirr 7989 ax-pre-ltwlin 7990 ax-pre-lttrn 7991 ax-pre-apti 7992 ax-pre-ltadd 7993 ax-pre-mulgt0 7994 ax-pre-mulext 7995 ax-arch 7996 ax-caucvg 7997

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 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-frec 6449 df-1o 6474 df-2o 6475 df-er 6592 df-en 6800 df-pnf 8061 df-mnf 8062 df-xr 8063 df-ltxr 8064 df-le 8065 df-sub 8197 df-neg 8198 df-reap 8599 df-ap 8606 df-div 8697 df-inn 8988 df-2 9046 df-3 9047 df-4 9048 df-n0 9247 df-z 9324 df-uz 9599 df-q 9691 df-rp 9726 df-ioo 9964 df-fz 10081 df-fl 10345 df-mod 10400 df-seqfrec 10525 df-exp 10616 df-cj 10992 df-re 10993 df-im 10994 df-rsqrt 11148 df-abs 11149 df-dvds 11937 df-prm 12252

This theorem is referenced by: gausslemma2dlem1 15269

W3C validator