bgoldbtbndlem2 - Mathbox for Alexander van der Vekens

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

Theorem bgoldbtbndlem2 38901

Description: Lemma 2 for bgoldbtbnd 38904. (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
bgoldbtbndlem2.s

**Assertion**
Ref	Expression
bgoldbtbndlem2	$/\$ Odd $/\$ ..^ $/\$ Even $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem bgoldbtbndlem2**
Step	Hyp	Ref	Expression
1		bgoldbtbnd.i	. . . . 5 ..^ $\$ $/\$ $/\$
2		elfzoelz 11920	. . . . . . 7 ..^
3		elfzoel2 11919	. . . . . . 7 ..^
4		elfzom1b 12010	. . . . . . . . 9 $/\$ ..^ ..^
5		fzossrbm1 11947	. . . . . . . . . . 11 ..^ ..^
6	5	adantl 468	. . . . . . . . . 10 $/\$ ..^ ..^
7	6	sseld 3431	. . . . . . . . 9 $/\$ ..^ ..^
8	4, 7	sylbid 219	. . . . . . . 8 $/\$ ..^ ..^
9	8	com12 32	. . . . . . 7 ..^ $/\$ ..^
10	2, 3, 9	mp2and 685	. . . . . 6 ..^ ..^
11		fveq2 5865	. . . . . . . . 9
12	11	eleq1d 2513	. . . . . . . 8 $\$ $\$
13		oveq1 6297	. . . . . . . . . . 11
14	13	fveq2d 5869	. . . . . . . . . 10
15	14, 11	oveq12d 6308	. . . . . . . . 9
16	15	breq1d 4412	. . . . . . . 8
17	15	breq2d 4414	. . . . . . . 8
18	12, 16, 17	3anbi123d 1339	. . . . . . 7 $\$ $/\$ $/\$ $\$ $/\$ $/\$
19	18	rspcv 3146	. . . . . 6 ..^ ..^ $\$ $/\$ $/\$ $\$ $/\$ $/\$
20	10, 19	syl 17	. . . . 5 ..^ ..^ $\$ $/\$ $/\$ $\$ $/\$ $/\$
21	1, 20	syl5com 31	. . . 4 ..^ $\$ $/\$ $/\$
22	21	a1d 26	. . 3 Odd ..^ $\$ $/\$ $/\$
23	22	3imp 1202	. 2 $/\$ Odd $/\$ ..^ $\$ $/\$ $/\$
24		bgoldbtbndlem2.s	. . . . 5
25		simp2 1009	. . . . . . . 8 $/\$ Odd $/\$ ..^ Odd
26		oddprmALTV 38816	. . . . . . . . 9 $\$ Odd
27	26	3ad2ant1 1029	. . . . . . . 8 $\$ $/\$ $/\$ Odd
28	25, 27	anim12i 570	. . . . . . 7 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ Odd $/\$ Odd
29	28	adantr 467	. . . . . 6 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ Odd $/\$ Odd
30		omoeALTV 38814	. . . . . 6 Odd $/\$ Odd Even
31	29, 30	syl 17	. . . . 5 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ Even
32	24, 31	syl5eqel 2533	. . . 4 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ Even
33	2	zcnd 11041	. . . . . . . . . . . . . . . . . . . 20 ..^
34	33	3ad2ant3 1031	. . . . . . . . . . . . . . . . . . 19 $/\$ Odd $/\$ ..^
35		npcan1 10044	. . . . . . . . . . . . . . . . . . 19
36	34, 35	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ Odd $/\$ ..^
37	36	fveq2d 5869	. . . . . . . . . . . . . . . . 17 $/\$ Odd $/\$ ..^
38	37	oveq1d 6305	. . . . . . . . . . . . . . . 16 $/\$ Odd $/\$ ..^
39	38	breq1d 4412	. . . . . . . . . . . . . . 15 $/\$ Odd $/\$ ..^
40	39	adantr 467	. . . . . . . . . . . . . 14 $/\$ Odd $/\$ ..^ $/\$ $\$
41		eldifi 3555	. . . . . . . . . . . . . . . 16 $\$
42		prmz 14626	. . . . . . . . . . . . . . . 16
43		zre 10941	. . . . . . . . . . . . . . . . 17
44		simp1 1008	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$ $/\$ $\$
45	44	ralimi 2781	. . . . . . . . . . . . . . . . . . . . 21 ..^ $\$ $/\$ $/\$ ..^ $\$
46		fzo0ss1 11948	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
47	46	sseli 3428	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
48	47	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ ..^
49		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
50	49	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
51	50	rspcv 3146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^ $\$ $\$
52	48, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ ..^ $\$ $\$
53	52	ex 436	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^ $\$ $\$
54	53	com23 81	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $\$ ..^ $\$
55	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 Odd ..^ $\$ ..^ $\$
56	55	com13 83	. . . . . . . . . . . . . . . . . . . . 21 ..^ $\$ Odd ..^ $\$
57	45, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20 ..^ $\$ $/\$ $/\$ Odd ..^ $\$
58	1, 57	mpcom 37	. . . . . . . . . . . . . . . . . . 19 Odd ..^ $\$
59	58	3imp 1202	. . . . . . . . . . . . . . . . . 18 $/\$ Odd $/\$ ..^ $\$
60		eldifi 3555	. . . . . . . . . . . . . . . . . . 19 $\$
61		prmz 14626	. . . . . . . . . . . . . . . . . . 19
62		zre 10941	. . . . . . . . . . . . . . . . . . . 20
63		bgoldbtbnd.n	. . . . . . . . . . . . . . . . . . . . . . 23 ;
64		eluzelz 11168	. . . . . . . . . . . . . . . . . . . . . . 23 ;
65		zre 10941	. . . . . . . . . . . . . . . . . . . . . . . 24
66		oddz 38760	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Odd
67	66	zred 11040	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Odd
68		simplr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
69		simprl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
70		4re 10686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
71	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
72	68, 69, 71	lesubaddd 10210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
73		simpllr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
74		simplrr 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
75	73, 74	resubcld 10047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
76	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
77		simplrl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
78	76, 77	readdcld 9670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
79	78, 74	resubcld 10047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
80		simplll 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
81	71, 69	readdcld 9670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
82		simprr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
83	68, 81, 82	lesub1d 10220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
84	83	biimpa 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
85	84	adantrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
86		resubcl 9938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
87	86	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
88		simpll 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
89		ltaddsub2 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
90	89	bicomd 205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
91	71, 87, 88, 90	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
92	91	biimpd 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
93	92	adantld 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
94	93	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
95		4cn 10687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96	95	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
97	69	recnd 9669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
98		recn 9629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
99	98	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
101	96, 97, 100	addsubassd 10006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
102	101	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
103	102	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
104	94, 103	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
105	75, 79, 80, 85, 104	lelttrd 9793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
106	105	exp32 610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
107	72, 106	sylbid 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
108	107	com23 81	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
109	108	exp32 610	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
110	67, 109	sylan2 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Odd
111	110	ex 436	. . . . . . . . . . . . . . . . . . . . . . . 24 Odd
112	65, 111	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 Odd
113	63, 64, 112	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 Odd
114	113	imp 431	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Odd
115	114	3adant3 1028	. . . . . . . . . . . . . . . . . . . 20 $/\$ Odd $/\$ ..^
116	62, 115	syl5com 31	. . . . . . . . . . . . . . . . . . 19 $/\$ Odd $/\$ ..^
117	60, 61, 116	3syl 18	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ Odd $/\$ ..^
118	59, 117	mpcom 37	. . . . . . . . . . . . . . . . 17 $/\$ Odd $/\$ ..^
119	43, 118	syl5com 31	. . . . . . . . . . . . . . . 16 $/\$ Odd $/\$ ..^
120	41, 42, 119	3syl 18	. . . . . . . . . . . . . . 15 $\$ $/\$ Odd $/\$ ..^
121	120	impcom 432	. . . . . . . . . . . . . 14 $/\$ Odd $/\$ ..^ $/\$ $\$
122	40, 121	sylbid 219	. . . . . . . . . . . . 13 $/\$ Odd $/\$ ..^ $/\$ $\$
123	122	expcom 437	. . . . . . . . . . . 12 $\$ $/\$ Odd $/\$ ..^
124	123	com23 81	. . . . . . . . . . 11 $\$ $/\$ Odd $/\$ ..^
125	124	imp 431	. . . . . . . . . 10 $\$ $/\$ $/\$ Odd $/\$ ..^
126	125	3adant3 1028	. . . . . . . . 9 $\$ $/\$ $/\$ $/\$ Odd $/\$ ..^
127	126	impcom 432	. . . . . . . 8 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$
128	127	com12 32	. . . . . . 7 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$
129	128	adantl 468	. . . . . 6 $/\$ $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$
130	129	impcom 432	. . . . 5 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
131	24, 130	syl5eqbr 4436	. . . 4 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
132	70	a1i 11	. . . . . 6 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
133		1eluzge0 11202	. . . . . . . . . . . . . . . 16
134		fzoss1 11945	. . . . . . . . . . . . . . . 16 ..^ ..^
135	133, 134	mp1i 13	. . . . . . . . . . . . . . 15 ..^ ..^
136	135	sselda 3432	. . . . . . . . . . . . . 14 $/\$ ..^ ..^
137		oveq1 6297	. . . . . . . . . . . . . . . . . . 19
138	137	fveq2d 5869	. . . . . . . . . . . . . . . . . 18
139	138, 49	oveq12d 6308	. . . . . . . . . . . . . . . . 17
140	139	breq1d 4412	. . . . . . . . . . . . . . . 16
141	139	breq2d 4414	. . . . . . . . . . . . . . . 16
142	50, 140, 141	3anbi123d 1339	. . . . . . . . . . . . . . 15 $\$ $/\$ $/\$ $\$ $/\$ $/\$
143	142	rspcv 3146	. . . . . . . . . . . . . 14 ..^ ..^ $\$ $/\$ $/\$ $\$ $/\$ $/\$
144	136, 143	syl 17	. . . . . . . . . . . . 13 $/\$ ..^ ..^ $\$ $/\$ $/\$ $\$ $/\$ $/\$
145	61	zred 11040	. . . . . . . . . . . . . . 15
146	60, 145	syl 17	. . . . . . . . . . . . . 14 $\$
147	146	3ad2ant1 1029	. . . . . . . . . . . . 13 $\$ $/\$ $/\$
148	144, 147	syl6 34	. . . . . . . . . . . 12 $/\$ ..^ ..^ $\$ $/\$ $/\$
149	148	ex 436	. . . . . . . . . . 11 ..^ ..^ $\$ $/\$ $/\$
150	1, 149	mpid 42	. . . . . . . . . 10 ..^
151	150	imp 431	. . . . . . . . 9 $/\$ ..^
152	151	3adant2 1027	. . . . . . . 8 $/\$ Odd $/\$ ..^
153	152	ad2antrr 732	. . . . . . 7 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
154	42	zred 11040	. . . . . . . . . 10
155	41, 154	syl 17	. . . . . . . . 9 $\$
156	155	3ad2ant1 1029	. . . . . . . 8 $\$ $/\$ $/\$
157	156	ad2antlr 733	. . . . . . 7 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
158	153, 157	resubcld 10047	. . . . . 6 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
159	67	3ad2ant2 1030	. . . . . . . 8 $/\$ Odd $/\$ ..^
160		resubcl 9938	. . . . . . . 8 $/\$
161	159, 156, 160	syl2an 480	. . . . . . 7 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$
162	161	adantr 467	. . . . . 6 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
163	33, 35	syl 17	. . . . . . . . . . . . . 14 ..^
164	163	3ad2ant3 1031	. . . . . . . . . . . . 13 $/\$ Odd $/\$ ..^
165	164	fveq2d 5869	. . . . . . . . . . . 12 $/\$ Odd $/\$ ..^
166	165	oveq1d 6305	. . . . . . . . . . 11 $/\$ Odd $/\$ ..^
167	166	breq2d 4414	. . . . . . . . . 10 $/\$ Odd $/\$ ..^
168	167	biimpcd 228	. . . . . . . . 9 $/\$ Odd $/\$ ..^
169	168	3ad2ant3 1031	. . . . . . . 8 $\$ $/\$ $/\$ $/\$ Odd $/\$ ..^
170	169	impcom 432	. . . . . . 7 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$
171	170	adantr 467	. . . . . 6 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
172	159	ad2antrr 732	. . . . . . 7 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
173		bgoldbtbnd.d	. . . . . . . . . . . . . . . . 17
174		eluzge3nn 11200	. . . . . . . . . . . . . . . . 17
175	173, 174	syl 17	. . . . . . . . . . . . . . . 16
176	175	adantr 467	. . . . . . . . . . . . . . 15 $/\$ ..^
177		bgoldbtbnd.f	. . . . . . . . . . . . . . . 16 RePart
178	177	adantr 467	. . . . . . . . . . . . . . 15 $/\$ ..^ RePart
179	133, 134	mp1i 13	. . . . . . . . . . . . . . . . . 18 ..^ ..^
180		fzossfz 11938	. . . . . . . . . . . . . . . . . 18 ..^
181	179, 180	syl6ss 3444	. . . . . . . . . . . . . . . . 17 ..^
182	173, 181	syl 17	. . . . . . . . . . . . . . . 16 ..^
183	182	sselda 3432	. . . . . . . . . . . . . . 15 $/\$ ..^
184	176, 178, 183	iccpartxr 38733	. . . . . . . . . . . . . 14 $/\$ ..^
185		fzofzp1 12008	. . . . . . . . . . . . . . . 16 ..^
186	136, 185	syl 17	. . . . . . . . . . . . . . 15 $/\$ ..^
187	176, 178, 186	iccpartxr 38733	. . . . . . . . . . . . . 14 $/\$ ..^
188	184, 187	jca 535	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
189	188	3adant2 1027	. . . . . . . . . . . 12 $/\$ Odd $/\$ ..^ $/\$
190		elico1 11679	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
191	189, 190	syl 17	. . . . . . . . . . 11 $/\$ Odd $/\$ ..^ $/\$ $/\$
192		simp2 1009	. . . . . . . . . . 11 $/\$ $/\$
193	191, 192	syl6bi 232	. . . . . . . . . 10 $/\$ Odd $/\$ ..^
194	193	adantrd 470	. . . . . . . . 9 $/\$ Odd $/\$ ..^ $/\$
195	194	adantr 467	. . . . . . . 8 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$
196	195	imp 431	. . . . . . 7 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
197	153, 172, 157, 196	lesub1dd 10229	. . . . . 6 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
198	132, 158, 162, 171, 197	ltletrd 9795	. . . . 5 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
199	198, 24	syl6breqr 4443	. . . 4 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
200	32, 131, 199	3jca 1188	. . 3 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ Even $/\$ $/\$
201	200	ex 436	. 2 $/\$ Odd $/\$ ..^ $/\$ $\$ $/\$ $/\$ $/\$ Even $/\$ $/\$
202	23, 201	mpdan 674	1 $/\$ Odd $/\$ ..^ $/\$ Even $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1444

wcel 1887

wral 2737 $\$ cdif 3401

wss 3404

csn 3968 class class class wbr 4402

cfv 5582 (class class class)co 6290

cc 9537

cr 9538

cc0 9539

c1 9540

caddc 9542

cxr 9674

clt 9675

cle 9676

cmin 9860

cn 10609

c2 10659

c3 10660

c4 10661

c7 10664

cz 10937 ;cdc 11051

cuz 11159

cico 11637

cfz 11784 ..^cfzo 11915

cprime 14622 RePartciccp 38727 Even ceven 38753 Odd codd 38754 GoldbachEven cgbe 38846

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-n0 10870 df-z 10938 df-uz 11160 df-ico 11641 df-fz 11785 df-fzo 11916 df-dvds 14306 df-prm 14623 df-iccp 38728 df-even 38755 df-odd 38756

This theorem is referenced by: bgoldbtbndlem4 38903

W3C validator