bgoldbtbndlem4 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > bgoldbtbndlem4		Structured version Visualization version Unicode version

Theorem bgoldbtbndlem4 38897

Description: Lemma 4 for bgoldbtbnd 38898. (Contributed by AV, 1-Aug-2020.)

**Hypotheses**
Ref	Expression
bgoldbtbnd.m	;
bgoldbtbnd.n	;
bgoldbtbnd.b	Even $/\$ GoldbachEven
bgoldbtbnd.d
bgoldbtbnd.f	RePart
bgoldbtbnd.i	..^ $\$ $/\$ $/\$
bgoldbtbnd.0
bgoldbtbnd.1	;
bgoldbtbnd.l
bgoldbtbnd.r

**Assertion**
Ref	Expression
bgoldbtbndlem4	$/\$ ..^ $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem bgoldbtbndlem4 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 759	. . 3 $/\$ ..^ $/\$ Odd
2		simpr 463	. . 3 $/\$ ..^ $/\$ Odd Odd
3		simplr 761	. . 3 $/\$ ..^ $/\$ Odd ..^
4		bgoldbtbnd.m	. . . 4 ;
5		bgoldbtbnd.n	. . . 4 ;
6		bgoldbtbnd.b	. . . 4 Even $/\$ GoldbachEven
7		bgoldbtbnd.d	. . . 4
8		bgoldbtbnd.f	. . . 4 RePart
9		bgoldbtbnd.i	. . . 4 ..^ $\$ $/\$ $/\$
10		bgoldbtbnd.0	. . . 4
11		bgoldbtbnd.1	. . . 4 ;
12		bgoldbtbnd.l	. . . 4
13		eqid 2450	. . . 4
14	4, 5, 6, 7, 8, 9, 10, 11, 12, 13	bgoldbtbndlem2 38895	. . 3 $/\$ Odd $/\$ ..^ $/\$ Even $/\$ $/\$
15	1, 2, 3, 14	syl3anc 1267	. 2 $/\$ ..^ $/\$ Odd $/\$ Even $/\$ $/\$
16		breq2 4405	. . . . . . . . . . . 12
17		breq1 4404	. . . . . . . . . . . 12
18	16, 17	anbi12d 716	. . . . . . . . . . 11 $/\$ $/\$
19		eleq1 2516	. . . . . . . . . . 11 GoldbachEven GoldbachEven
20	18, 19	imbi12d 322	. . . . . . . . . 10 $/\$ GoldbachEven $/\$ GoldbachEven
21	20	cbvralv 3018	. . . . . . . . 9 Even $/\$ GoldbachEven Even $/\$ GoldbachEven
22		breq2 4405	. . . . . . . . . . . 12
23		breq1 4404	. . . . . . . . . . . 12
24	22, 23	anbi12d 716	. . . . . . . . . . 11 $/\$ $/\$
25		eleq1 2516	. . . . . . . . . . 11 GoldbachEven GoldbachEven
26	24, 25	imbi12d 322	. . . . . . . . . 10 $/\$ GoldbachEven $/\$ GoldbachEven
27	26	rspcv 3145	. . . . . . . . 9 Even Even $/\$ GoldbachEven $/\$ GoldbachEven
28	21, 27	syl5bi 221	. . . . . . . 8 Even Even $/\$ GoldbachEven $/\$ GoldbachEven
29		id 22	. . . . . . . . . . 11 $/\$ GoldbachEven $/\$ GoldbachEven
30		isgbe 38846	. . . . . . . . . . . . 13 GoldbachEven Even $/\$ Odd $/\$ Odd $/\$
31		simp1 1007	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $/\$ $\$
32	31	ralimi 2780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $\$ $/\$ $/\$ ..^ $\$
33		elfzo1 11962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^ $/\$ $/\$
34		nnm1nn0 10908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
35	34	3ad2ant1 1028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
36	33, 35	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
37	36	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
38		eluzge3nn 11197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
39	38	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
40		elfzo2 11920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^ $/\$ $/\$
41		eluzelre 11166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
42	41	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
43	42	ltm1d 10536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
44		1red 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
45	42, 44	resubcld 10044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
46		zre 10938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
47	46	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
48		lttr 9707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$
49	45, 42, 47, 48	syl3anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
50	43, 49	mpand 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
51	50	3impia 1204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
52	40, 51	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
53	52	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
54	37, 39, 53	3jcad 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ $/\$ $/\$
55	7, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$ $/\$
56	55	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ ..^ $/\$ $/\$
57		elfzo0 11953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$
58	56, 57	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ ..^ ..^
59		fveq2 5863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
60	59	eleq1d 2512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
61	60	rspcv 3145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^ $\$ $\$
62	58, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^ ..^ $\$ $\$
63		eldifi 3554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
64	62, 63	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ ..^ $\$
65	64	expcom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^ $\$
66	65	com13 83	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $\$ ..^
67	32, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $\$ $/\$ $/\$ ..^
68	9, 67	mpcom 37	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^
69	68	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 Even $/\$ ..^
70	69	imp 431	. . . . . . . . . . . . . . . . . . . . . 22 Even $/\$ $/\$ ..^
71	70	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . 21 Even $/\$ $/\$ ..^ $/\$ Odd $/\$
72	71	ad2antrr 731	. . . . . . . . . . . . . . . . . . . 20 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$ $/\$ Odd $/\$ Odd $/\$
73		eleq1 2516	. . . . . . . . . . . . . . . . . . . . . . 23 Odd Odd
74	73	3anbi3d 1344	. . . . . . . . . . . . . . . . . . . . . 22 Odd $/\$ Odd $/\$ Odd Odd $/\$ Odd $/\$ Odd
75		oveq2 6296	. . . . . . . . . . . . . . . . . . . . . . 23
76	75	eqeq2d 2460	. . . . . . . . . . . . . . . . . . . . . 22
77	74, 76	anbi12d 716	. . . . . . . . . . . . . . . . . . . . 21 Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$
78	77	adantl 468	. . . . . . . . . . . . . . . . . . . 20 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$ $/\$ Odd $/\$ Odd $/\$ $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$
79		oddprmALTV 38810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ Odd
80	62, 79	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ ..^ ..^ $\$ Odd
81	80	expcom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^ $\$ Odd
82	81	com13 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ $\$ ..^ Odd
83	32, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $\$ $/\$ $/\$ ..^ Odd
84	9, 83	mpcom 37	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ Odd
85	84	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . 25 Even $/\$ ..^ Odd
86	85	imp 431	. . . . . . . . . . . . . . . . . . . . . . . 24 Even $/\$ $/\$ ..^ Odd
87	86	ad3antrrr 735	. . . . . . . . . . . . . . . . . . . . . . 23 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$ Odd
88		3simpa 1004	. . . . . . . . . . . . . . . . . . . . . . 23 Odd $/\$ Odd $/\$ Odd $/\$ Odd
89	87, 88	anim12ci 570	. . . . . . . . . . . . . . . . . . . . . 22 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$ $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd
90		df-3an 986	. . . . . . . . . . . . . . . . . . . . . 22 Odd $/\$ Odd $/\$ Odd Odd $/\$ Odd $/\$ Odd
91	89, 90	sylibr 216	. . . . . . . . . . . . . . . . . . . . 21 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$ $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd
92		oddz 38754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Odd
93	92	zcnd 11038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Odd
94	93	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Even $/\$ $/\$ ..^ $/\$ Odd
95	94	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$
96	95	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Odd $/\$ Odd $/\$ Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$
97		prmz 14619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
98	97	zcnd 11038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
99	63, 98	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $\$
100	62, 99	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ ..^ ..^ $\$
101	100	expcom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ ..^ $\$
102	101	com13 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ $\$ ..^
103	32, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $\$ $/\$ $/\$ ..^
104	9, 103	mpcom 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
105	104	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Even $/\$ ..^
106	105	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Even $/\$ $/\$ ..^
107	106	ad3antrrr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$
108	107	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Odd $/\$ Odd $/\$ Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$
109	96, 108	npcand 9987	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Odd $/\$ Odd $/\$ Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$
110		oveq1 6295	. . . . . . . . . . . . . . . . . . . . . . . . . 26
111	109, 110	sylan9req 2505	. . . . . . . . . . . . . . . . . . . . . . . . 25 Odd $/\$ Odd $/\$ Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$ $/\$
112	111	exp31 608	. . . . . . . . . . . . . . . . . . . . . . . 24 Odd $/\$ Odd Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$
113	112	com23 81	. . . . . . . . . . . . . . . . . . . . . . 23 Odd $/\$ Odd Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$
114	113	3impia 1204	. . . . . . . . . . . . . . . . . . . . . 22 Odd $/\$ Odd $/\$ Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$
115	114	impcom 432	. . . . . . . . . . . . . . . . . . . . 21 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$ $/\$ Odd $/\$ Odd $/\$
116	91, 115	jca 535	. . . . . . . . . . . . . . . . . . . 20 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$ $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$
117	72, 78, 116	rspcedvd 3154	. . . . . . . . . . . . . . . . . . 19 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$ $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$
118	117	ex 436	. . . . . . . . . . . . . . . . . 18 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$
119	118	reximdva 2861	. . . . . . . . . . . . . . . . 17 Even $/\$ $/\$ ..^ $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$
120	119	reximdva 2861	. . . . . . . . . . . . . . . 16 Even $/\$ $/\$ ..^ $/\$ Odd Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$
121	120	exp41 614	. . . . . . . . . . . . . . 15 Even ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$
122	121	com25 94	. . . . . . . . . . . . . 14 Even Odd $/\$ Odd $/\$ ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$
123	122	imp 431	. . . . . . . . . . . . 13 Even $/\$ Odd $/\$ Odd $/\$ ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$
124	30, 123	sylbi 199	. . . . . . . . . . . 12 GoldbachEven ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$
125	124	a1d 26	. . . . . . . . . . 11 GoldbachEven Even ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$
126	29, 125	syl6com 36	. . . . . . . . . 10 $/\$ $/\$ GoldbachEven Even ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$
127	126	ancoms 455	. . . . . . . . 9 $/\$ $/\$ GoldbachEven Even ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$
128	127	com13 83	. . . . . . . 8 Even $/\$ GoldbachEven $/\$ ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$
129	28, 128	syld 45	. . . . . . 7 Even Even $/\$ GoldbachEven $/\$ ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$
130	129	com23 81	. . . . . 6 Even $/\$ Even $/\$ GoldbachEven ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$
131	130	3impib 1205	. . . . 5 Even $/\$ $/\$ Even $/\$ GoldbachEven ..^ Odd Odd $/\$ Odd $/\$ Odd $/\$
132	131	com15 96	. . . 4 Even $/\$ GoldbachEven ..^ Odd Even $/\$ $/\$ Odd $/\$ Odd $/\$ Odd $/\$
133	6, 132	mpd 15	. . 3 ..^ Odd Even $/\$ $/\$ Odd $/\$ Odd $/\$ Odd $/\$
134	133	imp31 434	. 2 $/\$ ..^ $/\$ Odd Even $/\$ $/\$ Odd $/\$ Odd $/\$ Odd $/\$
135	15, 134	syld 45	1 $/\$ ..^ $/\$ Odd $/\$ Odd $/\$ Odd $/\$ Odd $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

wral 2736

wrex 2737 $\$ cdif 3400

csn 3967 class class class wbr 4401

cfv 5581 (class class class)co 6288

cc 9534

cr 9535

cc0 9536

c1 9537

caddc 9539

clt 9672

cle 9673

cmin 9857

cn 10606

c2 10656

c3 10657

c4 10658

c7 10661

cn0 10866

cz 10934 ;cdc 11048

cuz 11156

cico 11634 ..^cfzo 11912

cprime 14615 RePartciccp 38721 Even ceven 38747 Odd codd 38748 GoldbachEven cgbe 38840

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-2o 7180 df-oadd 7183 df-er 7360 df-map 7471 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-4 10667 df-n0 10867 df-z 10935 df-uz 11157 df-ico 11638 df-fz 11782 df-fzo 11913 df-dvds 14299 df-prm 14616 df-iccp 38722 df-even 38749 df-odd 38750 df-gbe 38843

This theorem is referenced by: bgoldbtbnd 38898

W3C validator