2sqpwodd - Intuitionistic Logic Explorer

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

Theorem 2sqpwodd 12208

Description: The greatest power of two dividing twice the square of an integer is an odd power of two. (Contributed by Jim Kingdon, 17-Nov-2021.)

**Hypotheses**
Ref	Expression
oddpwdc.j
oddpwdc.f

**Assertion**
Ref	Expression
2sqpwodd

Distinct variable groups:

Allowed substitution hint:

(

)

**Proof of Theorem 2sqpwodd**
Step	Hyp	Ref	Expression
1		oddpwdc.j	. . . . . . . . 9
2		oddpwdc.f	. . . . . . . . 9
3	1, 2	oddpwdc 12206	. . . . . . . 8
4		f1ocnv 5493	. . . . . . . 8
5		f1of 5480	. . . . . . . 8
6	3, 4, 5	mp2b 8	. . . . . . 7
7	6	ffvelcdmi 5671	. . . . . 6
8		xp2nd 6191	. . . . . 6
9	7, 8	syl 14	. . . . 5
10	9	nn0zd 9403	. . . 4
11		2nn 9110	. . . . . 6
12	11	a1i 9	. . . . 5
13	12	nnzd 9404	. . . 4
14	10, 13	zmulcld 9411	. . 3
15		dvdsmul2 11853	. . . 4 $/\$
16	10, 13, 15	syl2anc 411	. . 3
17		oddp1even 11913	. . . . 5
18	17	biimprd 158	. . . 4
19	18	con2d 625	. . 3
20	14, 16, 19	sylc 62	. 2
21		xp1st 6190	. . . . . . . . . . 11
22	7, 21	syl 14	. . . . . . . . . 10
23		breq2 4022	. . . . . . . . . . . . 13
24	23	notbid 668	. . . . . . . . . . . 12
25	24, 1	elrab2 2911	. . . . . . . . . . 11 $/\$
26	25	simplbi 274	. . . . . . . . . 10
27	22, 26	syl 14	. . . . . . . . 9
28	27	nnsqcld 10706	. . . . . . . 8
29	25	simprbi 275	. . . . . . . . . . 11
30	22, 29	syl 14	. . . . . . . . . 10
31		2prm 12159	. . . . . . . . . . 11
32	27	nnzd 9404	. . . . . . . . . . 11
33		euclemma 12178	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
34		oridm 758	. . . . . . . . . . . 12 $\/$
35	33, 34	bitrdi 196	. . . . . . . . . . 11 $/\$ $/\$
36	31, 32, 32, 35	mp3an2i 1353	. . . . . . . . . 10
37	30, 36	mtbird 674	. . . . . . . . 9
38	27	nncnd 8963	. . . . . . . . . . 11
39	38	sqvald 10682	. . . . . . . . . 10
40	39	breq2d 4030	. . . . . . . . 9
41	37, 40	mtbird 674	. . . . . . . 8
42		breq2 4022	. . . . . . . . . 10
43	42	notbid 668	. . . . . . . . 9
44	43, 1	elrab2 2911	. . . . . . . 8 $/\$
45	28, 41, 44	sylanbrc 417	. . . . . . 7
46	12	nnnn0d 9259	. . . . . . . . 9
47	9, 46	nn0mulcld 9264	. . . . . . . 8
48		peano2nn0 9246	. . . . . . . 8
49	47, 48	syl 14	. . . . . . 7
50		opelxp 4674	. . . . . . 7 $/\$
51	45, 49, 50	sylanbrc 417	. . . . . 6
52	12	nncnd 8963	. . . . . . . . . . 11
53	52, 47	expp1d 10686	. . . . . . . . . 10
54	52, 47	expcld 10685	. . . . . . . . . . 11
55	54, 52	mulcomd 8009	. . . . . . . . . 10
56	52, 46, 9	expmuld 10688	. . . . . . . . . . 11
57	56	oveq2d 5912	. . . . . . . . . 10
58	53, 55, 57	3eqtrd 2226	. . . . . . . . 9
59	58	oveq1d 5911	. . . . . . . 8
60	12, 49	nnexpcld 10707	. . . . . . . . . 10
61	60, 28	nnmulcld 8998	. . . . . . . . 9
62		oveq2 5904	. . . . . . . . . 10
63		oveq2 5904	. . . . . . . . . . 11
64	63	oveq1d 5911	. . . . . . . . . 10
65	62, 64, 2	ovmpog 6031	. . . . . . . . 9 $/\$ $/\$
66	45, 49, 61, 65	syl3anc 1249	. . . . . . . 8
67		f1ocnvfv2 5800	. . . . . . . . . . . . . . . 16 $/\$
68	3, 67	mpan 424	. . . . . . . . . . . . . . 15
69		1st2nd2 6200	. . . . . . . . . . . . . . . . 17
70	7, 69	syl 14	. . . . . . . . . . . . . . . 16
71	70	fveq2d 5538	. . . . . . . . . . . . . . 15
72	68, 71	eqtr3d 2224	. . . . . . . . . . . . . 14
73		df-ov 5899	. . . . . . . . . . . . . 14
74	72, 73	eqtr4di 2240	. . . . . . . . . . . . 13
75	12, 9	nnexpcld 10707	. . . . . . . . . . . . . . 15
76	75, 27	nnmulcld 8998	. . . . . . . . . . . . . 14
77		oveq2 5904	. . . . . . . . . . . . . . 15
78		oveq2 5904	. . . . . . . . . . . . . . . 16
79	78	oveq1d 5911	. . . . . . . . . . . . . . 15
80	77, 79, 2	ovmpog 6031	. . . . . . . . . . . . . 14 $/\$ $/\$
81	22, 9, 76, 80	syl3anc 1249	. . . . . . . . . . . . 13
82	74, 81	eqtrd 2222	. . . . . . . . . . . 12
83	82	oveq1d 5911	. . . . . . . . . . 11
84	75	nncnd 8963	. . . . . . . . . . . 12
85	84, 38	sqmuld 10697	. . . . . . . . . . 11
86	83, 85	eqtrd 2222	. . . . . . . . . 10
87	86	oveq2d 5912	. . . . . . . . 9
88	56, 54	eqeltrrd 2267	. . . . . . . . . 10
89	28	nncnd 8963	. . . . . . . . . 10
90	52, 88, 89	mulassd 8011	. . . . . . . . 9
91	87, 90	eqtr4d 2225	. . . . . . . 8
92	59, 66, 91	3eqtr4rd 2233	. . . . . . 7
93		df-ov 5899	. . . . . . 7
94	92, 93	eqtr2di 2239	. . . . . 6
95		f1ocnvfv 5801	. . . . . . 7 $/\$
96	3, 95	mpan 424	. . . . . 6
97	51, 94, 96	sylc 62	. . . . 5
98	97	fveq2d 5538	. . . 4
99		op2ndg 6176	. . . . 5 $/\$
100	45, 49, 99	syl2anc 411	. . . 4
101	98, 100	eqtrd 2222	. . 3
102	101	breq2d 4030	. 2
103	20, 102	mtbird 674	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 105 $\/$ wo 709 $/\$ w3a 980

wceq 1364

wcel 2160

crab 2472

cop 3610 class class class wbr 4018

cxp 4642

ccnv 4643

wf 5231

wf1o 5234

cfv 5235 (class class class)co 5896

cmpo 5898

c1st 6163

c2nd 6164

cc 7839

c1 7842

caddc 7844

cmul 7846

cn 8949

c2 9000

cn0 9206

cz 9283

cexp 10550

cdvds 11826

cprime 12139

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 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4192 ax-pr 4227 ax-un 4451 ax-setind 4554 ax-iinf 4605 ax-cnex 7932 ax-resscn 7933 ax-1cn 7934 ax-1re 7935 ax-icn 7936 ax-addcl 7937 ax-addrcl 7938 ax-mulcl 7939 ax-mulrcl 7940 ax-addcom 7941 ax-mulcom 7942 ax-addass 7943 ax-mulass 7944 ax-distr 7945 ax-i2m1 7946 ax-0lt1 7947 ax-1rid 7948 ax-0id 7949 ax-rnegex 7950 ax-precex 7951 ax-cnre 7952 ax-pre-ltirr 7953 ax-pre-ltwlin 7954 ax-pre-lttrn 7955 ax-pre-apti 7956 ax-pre-ltadd 7957 ax-pre-mulgt0 7958 ax-pre-mulext 7959 ax-arch 7960 ax-caucvg 7961

This theorem depends on definitions: df-bi 117 df-stab 832 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 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4311 df-po 4314 df-iso 4315 df-iord 4384 df-on 4386 df-ilim 4387 df-suc 4389 df-iom 4608 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-rn 4655 df-res 4656 df-ima 4657 df-iota 5196 df-fun 5237 df-fn 5238 df-f 5239 df-f1 5240 df-fo 5241 df-f1o 5242 df-fv 5243 df-riota 5852 df-ov 5899 df-oprab 5900 df-mpo 5901 df-1st 6165 df-2nd 6166 df-recs 6330 df-frec 6416 df-1o 6441 df-2o 6442 df-er 6559 df-en 6767 df-sup 7013 df-pnf 8024 df-mnf 8025 df-xr 8026 df-ltxr 8027 df-le 8028 df-sub 8160 df-neg 8161 df-reap 8562 df-ap 8569 df-div 8660 df-inn 8950 df-2 9008 df-3 9009 df-4 9010 df-n0 9207 df-z 9284 df-uz 9559 df-q 9650 df-rp 9684 df-fz 10039 df-fzo 10173 df-fl 10301 df-mod 10354 df-seqfrec 10477 df-exp 10551 df-cj 10883 df-re 10884 df-im 10885 df-rsqrt 11039 df-abs 11040 df-dvds 11827 df-gcd 11976 df-prm 12140

This theorem is referenced by: sqne2sq 12209

W3C validator