Theorem bgoldbtbndlem1 41693

Description: Lemma 1 for bgoldbtbnd 41697: the odd numbers between 7 and 13 (exclusive) are odd Goldbach numbers. (Contributed by AV, 29-Jul-2020.)

Assertion

Ref	Expression
bgoldbtbndlem1	|- ( ( N e. Odd /\ 7 < N /\ N e. ( 7 [,); 1 3 ) ) -> N e. GoldbachOdd )

Proof of Theorem bgoldbtbndlem1

Step	Hyp	Ref	Expression
1		7re 11103	. . . . 5 |- 7 e. RR
2	1	rexri 10097	. . . 4 |- 7 e. RR*
3		1nn0 11308	. . . . . . 7 |- 1 e. NN0
4		3nn 11186	. . . . . . 7 |- 3 e. NN
5	3, 4	decnncl 11518	. . . . . 6 |- ; 1 3 e. NN
6	5	nnrei 11029	. . . . 5 |- ; 1 3 e. RR
7	6	rexri 10097	. . . 4 |- ; 1 3 e. RR*
8		elico1 12218	. . . 4 |- ( ( 7 e. RR* /\ ; 1 3 e. RR* ) -> ( N e. ( 7 [,); 1 3 ) <-> ( N e. RR* /\ 7 <_ N /\ N < ; 1 3 ) ) )
9	2, 7, 8	mp2an 708	. . 3 |- ( N e. ( 7 [,); 1 3 ) <-> ( N e. RR* /\ 7 <_ N /\ N < ; 1 3 ) )
10		7nn 11190	. . . . . . . . . 10 |- 7 e. NN
11	10	nnzi 11401	. . . . . . . . 9 |- 7 e. ZZ
12		oddz 41544	. . . . . . . . 9 |- ( N e. Odd -> N e. ZZ )
13		zltp1le 11427	. . . . . . . . . 10 |- ( ( 7 e. ZZ /\ N e. ZZ ) -> ( 7 < N <-> ( 7 + 1 ) <_ N ) )
14		7p1e8 11157	. . . . . . . . . . . 12 |- ( 7 + 1 ) = 8
15	14	breq1i 4660	. . . . . . . . . . 11 |- ( ( 7 + 1 ) <_ N <-> 8 <_ N )
16	15	a1i 11	. . . . . . . . . 10 |- ( ( 7 e. ZZ /\ N e. ZZ ) -> ( ( 7 + 1 ) <_ N <-> 8 <_ N ) )
17		8re 11105	. . . . . . . . . . . 12 |- 8 e. RR
18	17	a1i 11	. . . . . . . . . . 11 |- ( 7 e. ZZ -> 8 e. RR )
19		zre 11381	. . . . . . . . . . 11 |- ( N e. ZZ -> N e. RR )
20		leloe 10124	. . . . . . . . . . 11 |- ( ( 8 e. RR /\ N e. RR ) -> ( 8 <_ N <-> ( 8 < N \/ 8 = N ) ) )
21	18, 19, 20	syl2an 494	. . . . . . . . . 10 |- ( ( 7 e. ZZ /\ N e. ZZ ) -> ( 8 <_ N <-> ( 8 < N \/ 8 = N ) ) )
22	13, 16, 21	3bitrd 294	. . . . . . . . 9 |- ( ( 7 e. ZZ /\ N e. ZZ ) -> ( 7 < N <-> ( 8 < N \/ 8 = N ) ) )
23	11, 12, 22	sylancr 695	. . . . . . . 8 |- ( N e. Odd -> ( 7 < N <-> ( 8 < N \/ 8 = N ) ) )
24		8nn 11191	. . . . . . . . . . . . . . 15 |- 8 e. NN
25	24	nnzi 11401	. . . . . . . . . . . . . 14 |- 8 e. ZZ
26		zltp1le 11427	. . . . . . . . . . . . . 14 |- ( ( 8 e. ZZ /\ N e. ZZ ) -> ( 8 < N <-> ( 8 + 1 ) <_ N ) )
27	25, 12, 26	sylancr 695	. . . . . . . . . . . . 13 |- ( N e. Odd -> ( 8 < N <-> ( 8 + 1 ) <_ N ) )
28		8p1e9 11158	. . . . . . . . . . . . . . 15 |- ( 8 + 1 ) = 9
29	28	breq1i 4660	. . . . . . . . . . . . . 14 |- ( ( 8 + 1 ) <_ N <-> 9 <_ N )
30	29	a1i 11	. . . . . . . . . . . . 13 |- ( N e. Odd -> ( ( 8 + 1 ) <_ N <-> 9 <_ N ) )
31		9re 11107	. . . . . . . . . . . . . . 15 |- 9 e. RR
32	31	a1i 11	. . . . . . . . . . . . . 14 |- ( N e. Odd -> 9 e. RR )
33	12	zred 11482	. . . . . . . . . . . . . 14 |- ( N e. Odd -> N e. RR )
34	32, 33	leloed 10180	. . . . . . . . . . . . 13 |- ( N e. Odd -> ( 9 <_ N <-> ( 9 < N \/ 9 = N ) ) )
35	27, 30, 34	3bitrd 294	. . . . . . . . . . . 12 |- ( N e. Odd -> ( 8 < N <-> ( 9 < N \/ 9 = N ) ) )
36		9nn 11192	. . . . . . . . . . . . . . . . . . 19 |- 9 e. NN
37	36	nnzi 11401	. . . . . . . . . . . . . . . . . 18 |- 9 e. ZZ
38		zltp1le 11427	. . . . . . . . . . . . . . . . . 18 |- ( ( 9 e. ZZ /\ N e. ZZ ) -> ( 9 < N <-> ( 9 + 1 ) <_ N ) )
39	37, 12, 38	sylancr 695	. . . . . . . . . . . . . . . . 17 |- ( N e. Odd -> ( 9 < N <-> ( 9 + 1 ) <_ N ) )
40		9p1e10 11496	. . . . . . . . . . . . . . . . . . 19 |- ( 9 + 1 ) = ; 1 0
41	40	breq1i 4660	. . . . . . . . . . . . . . . . . 18 |- ( ( 9 + 1 ) <_ N <-> ; 1 0 <_ N )
42	41	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( N e. Odd -> ( ( 9 + 1 ) <_ N <-> ; 1 0 <_ N ) )
43		10re 11517	. . . . . . . . . . . . . . . . . . 19 |- ; 1 0 e. RR
44	43	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( N e. Odd -> ; 1 0 e. RR )
45	44, 33	leloed 10180	. . . . . . . . . . . . . . . . 17 |- ( N e. Odd -> (; 1 0 <_ N <-> (; 1 0 < N \/ ; 1 0 = N ) ) )
46	39, 42, 45	3bitrd 294	. . . . . . . . . . . . . . . 16 |- ( N e. Odd -> ( 9 < N <-> (; 1 0 < N \/ ; 1 0 = N ) ) )
47		10nn 11514	. . . . . . . . . . . . . . . . . . . . . . 23 |- ; 1 0 e. NN
48	47	nnzi 11401	. . . . . . . . . . . . . . . . . . . . . 22 |- ; 1 0 e. ZZ
49		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . . 22 |- ( (; 1 0 e. ZZ /\ N e. ZZ ) -> (; 1 0 < N <-> (; 1 0 + 1 ) <_ N ) )
50	48, 12, 49	sylancr 695	. . . . . . . . . . . . . . . . . . . . 21 |- ( N e. Odd -> (; 1 0 < N <-> (; 1 0 + 1 ) <_ N ) )
51		dec10p 11553	. . . . . . . . . . . . . . . . . . . . . . 23 |- (; 1 0 + 1 ) = ; 1 1
52	51	breq1i 4660	. . . . . . . . . . . . . . . . . . . . . 22 |- ( (; 1 0 + 1 ) <_ N <-> ; 1 1 <_ N )
53	52	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( N e. Odd -> ( (; 1 0 + 1 ) <_ N <-> ; 1 1 <_ N ) )
54		1nn 11031	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1 e. NN
55	3, 54	decnncl 11518	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ; 1 1 e. NN
56	55	nnrei 11029	. . . . . . . . . . . . . . . . . . . . . . 23 |- ; 1 1 e. RR
57	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( N e. Odd -> ; 1 1 e. RR )
58	57, 33	leloed 10180	. . . . . . . . . . . . . . . . . . . . 21 |- ( N e. Odd -> (; 1 1 <_ N <-> (; 1 1 < N \/ ; 1 1 = N ) ) )
59	50, 53, 58	3bitrd 294	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. Odd -> (; 1 0 < N <-> (; 1 1 < N \/ ; 1 1 = N ) ) )
60	55	nnzi 11401	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ; 1 1 e. ZZ
61		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( (; 1 1 e. ZZ /\ N e. ZZ ) -> (; 1 1 < N <-> (; 1 1 + 1 ) <_ N ) )
62	60, 12, 61	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( N e. Odd -> (; 1 1 < N <-> (; 1 1 + 1 ) <_ N ) )
63	51	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ; 1 1 = (; 1 0 + 1 )
64	63	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (; 1 1 + 1 ) = ( (; 1 0 + 1 ) + 1 )
65	47	nncni 11030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ; 1 0 e. CC
66		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- 1 e. CC
67	65, 66, 66	addassi 10048	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( (; 1 0 + 1 ) + 1 ) = (; 1 0 + ( 1 + 1 ) )
68		1p1e2 11134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 1 + 1 ) = 2
69	68	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (; 1 0 + ( 1 + 1 ) ) = (; 1 0 + 2 )
70		dec10p 11553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (; 1 0 + 2 ) = ; 1 2
71	69, 70	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (; 1 0 + ( 1 + 1 ) ) = ; 1 2
72	64, 67, 71	3eqtri 2648	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (; 1 1 + 1 ) = ; 1 2
73	72	breq1i 4660	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( (; 1 1 + 1 ) <_ N <-> ; 1 2 <_ N )
74	73	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( N e. Odd -> ( (; 1 1 + 1 ) <_ N <-> ; 1 2 <_ N ) )
75		2nn 11185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- 2 e. NN
76	3, 75	decnncl 11518	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ; 1 2 e. NN
77	76	nnrei 11029	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ; 1 2 e. RR
78	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( N e. Odd -> ; 1 2 e. RR )
79	78, 33	leloed 10180	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( N e. Odd -> (; 1 2 <_ N <-> (; 1 2 < N \/ ; 1 2 = N ) ) )
80	62, 74, 79	3bitrd 294	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( N e. Odd -> (; 1 1 < N <-> (; 1 2 < N \/ ; 1 2 = N ) ) )
81	76	nnzi 11401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ; 1 2 e. ZZ
82		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( (; 1 2 e. ZZ /\ N e. ZZ ) -> (; 1 2 < N <-> (; 1 2 + 1 ) <_ N ) )
83	81, 12, 82	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. Odd -> (; 1 2 < N <-> (; 1 2 + 1 ) <_ N ) )
84	70	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ; 1 2 = (; 1 0 + 2 )
85	84	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (; 1 2 + 1 ) = ( (; 1 0 + 2 ) + 1 )
86		2cn 11091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- 2 e. CC
87	65, 86, 66	addassi 10048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( (; 1 0 + 2 ) + 1 ) = (; 1 0 + ( 2 + 1 ) )
88		2p1e3 11151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 2 + 1 ) = 3
89	88	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (; 1 0 + ( 2 + 1 ) ) = (; 1 0 + 3 )
90		dec10p 11553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (; 1 0 + 3 ) = ; 1 3
91	89, 90	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (; 1 0 + ( 2 + 1 ) ) = ; 1 3
92	85, 87, 91	3eqtri 2648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (; 1 2 + 1 ) = ; 1 3
93	92	breq1i 4660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( (; 1 2 + 1 ) <_ N <-> ; 1 3 <_ N )
94	93	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. Odd -> ( (; 1 2 + 1 ) <_ N <-> ; 1 3 <_ N ) )
95	6	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. Odd -> ; 1 3 e. RR )
96	95, 33	lenltd 10183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. Odd -> (; 1 3 <_ N <-> -. N < ; 1 3 ) )
97	83, 94, 96	3bitrd 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( N e. Odd -> (; 1 2 < N <-> -. N < ; 1 3 ) )
98		pm2.21 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. N < ; 1 3 -> ( N < ; 1 3 -> N e. GoldbachOdd ) )
99	97, 98	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( N e. Odd -> (; 1 2 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
100	99	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (; 1 2 < N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
101		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (; 1 2 = N -> (; 1 2 e. Odd <-> N e. Odd ) )
102		6p6e12 11602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 6 + 6 ) = ; 1 2
103		6even 41620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- 6 e. Even
104		epee 41614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 6 e. Even /\ 6 e. Even ) -> ( 6 + 6 ) e. Even )
105	103, 103, 104	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 6 + 6 ) e. Even
106	102, 105	eqeltrri 2698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ; 1 2 e. Even
107		evennodd 41556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (; 1 2 e. Even -> -. ; 1 2 e. Odd )
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- -. ; 1 2 e. Odd
109	108	pm2.21i 116	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (; 1 2 e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) )
110	101, 109	syl6bir 244	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (; 1 2 = N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
111	100, 110	jaoi 394	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( (; 1 2 < N \/ ; 1 2 = N ) -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
112	111	com12 32	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( N e. Odd -> ( (; 1 2 < N \/ ; 1 2 = N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
113	80, 112	sylbid 230	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( N e. Odd -> (; 1 1 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
114	113	com12 32	. . . . . . . . . . . . . . . . . . . . . 22 |- (; 1 1 < N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
115		11gbo 41663	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ; 1 1 e. GoldbachOdd
116		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (; 1 1 = N -> (; 1 1 e. GoldbachOdd <-> N e. GoldbachOdd ) )
117	115, 116	mpbii 223	. . . . . . . . . . . . . . . . . . . . . . 23 |- (; 1 1 = N -> N e. GoldbachOdd )
118	117	2a1d 26	. . . . . . . . . . . . . . . . . . . . . 22 |- (; 1 1 = N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
119	114, 118	jaoi 394	. . . . . . . . . . . . . . . . . . . . 21 |- ( (; 1 1 < N \/ ; 1 1 = N ) -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
120	119	com12 32	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. Odd -> ( (; 1 1 < N \/ ; 1 1 = N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
121	59, 120	sylbid 230	. . . . . . . . . . . . . . . . . . 19 |- ( N e. Odd -> (; 1 0 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
122	121	com12 32	. . . . . . . . . . . . . . . . . 18 |- (; 1 0 < N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
123		eleq1 2689	. . . . . . . . . . . . . . . . . . 19 |- (; 1 0 = N -> (; 1 0 e. Odd <-> N e. Odd ) )
124		5p5e10 11596	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 5 + 5 ) = ; 1 0
125		5odd 41619	. . . . . . . . . . . . . . . . . . . . . . 23 |- 5 e. Odd
126		opoeALTV 41594	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 5 e. Odd /\ 5 e. Odd ) -> ( 5 + 5 ) e. Even )
127	125, 125, 126	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 5 + 5 ) e. Even
128	124, 127	eqeltrri 2698	. . . . . . . . . . . . . . . . . . . . 21 |- ; 1 0 e. Even
129		evennodd 41556	. . . . . . . . . . . . . . . . . . . . 21 |- (; 1 0 e. Even -> -. ; 1 0 e. Odd )
130	128, 129	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- -. ; 1 0 e. Odd
131	130	pm2.21i 116	. . . . . . . . . . . . . . . . . . 19 |- (; 1 0 e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) )
132	123, 131	syl6bir 244	. . . . . . . . . . . . . . . . . 18 |- (; 1 0 = N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
133	122, 132	jaoi 394	. . . . . . . . . . . . . . . . 17 |- ( (; 1 0 < N \/ ; 1 0 = N ) -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
134	133	com12 32	. . . . . . . . . . . . . . . 16 |- ( N e. Odd -> ( (; 1 0 < N \/ ; 1 0 = N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
135	46, 134	sylbid 230	. . . . . . . . . . . . . . 15 |- ( N e. Odd -> ( 9 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
136	135	com12 32	. . . . . . . . . . . . . 14 |- ( 9 < N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
137		9gbo 41662	. . . . . . . . . . . . . . . 16 |- 9 e. GoldbachOdd
138		eleq1 2689	. . . . . . . . . . . . . . . 16 |- ( 9 = N -> ( 9 e. GoldbachOdd <-> N e. GoldbachOdd ) )
139	137, 138	mpbii 223	. . . . . . . . . . . . . . 15 |- ( 9 = N -> N e. GoldbachOdd )
140	139	2a1d 26	. . . . . . . . . . . . . 14 |- ( 9 = N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
141	136, 140	jaoi 394	. . . . . . . . . . . . 13 |- ( ( 9 < N \/ 9 = N ) -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
142	141	com12 32	. . . . . . . . . . . 12 |- ( N e. Odd -> ( ( 9 < N \/ 9 = N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
143	35, 142	sylbid 230	. . . . . . . . . . 11 |- ( N e. Odd -> ( 8 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
144	143	com12 32	. . . . . . . . . 10 |- ( 8 < N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
145		eleq1 2689	. . . . . . . . . . 11 |- ( 8 = N -> ( 8 e. Odd <-> N e. Odd ) )
146		8even 41622	. . . . . . . . . . . . 13 |- 8 e. Even
147		evennodd 41556	. . . . . . . . . . . . 13 |- ( 8 e. Even -> -. 8 e. Odd )
148	146, 147	ax-mp 5	. . . . . . . . . . . 12 |- -. 8 e. Odd
149	148	pm2.21i 116	. . . . . . . . . . 11 |- ( 8 e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) )
150	145, 149	syl6bir 244	. . . . . . . . . 10 |- ( 8 = N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
151	144, 150	jaoi 394	. . . . . . . . 9 |- ( ( 8 < N \/ 8 = N ) -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
152	151	com12 32	. . . . . . . 8 |- ( N e. Odd -> ( ( 8 < N \/ 8 = N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
153	23, 152	sylbid 230	. . . . . . 7 |- ( N e. Odd -> ( 7 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
154	153	imp 445	. . . . . 6 |- ( ( N e. Odd /\ 7 < N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) )
155	154	com12 32	. . . . 5 |- ( N < ; 1 3 -> ( ( N e. Odd /\ 7 < N ) -> N e. GoldbachOdd ) )
156	155	3ad2ant3 1084	. . . 4 |- ( ( N e. RR* /\ 7 <_ N /\ N < ; 1 3 ) -> ( ( N e. Odd /\ 7 < N ) -> N e. GoldbachOdd ) )
157	156	com12 32	. . 3 |- ( ( N e. Odd /\ 7 < N ) -> ( ( N e. RR* /\ 7 <_ N /\ N < ; 1 3 ) -> N e. GoldbachOdd ) )
158	9, 157	syl5bi 232	. 2 |- ( ( N e. Odd /\ 7 < N ) -> ( N e. ( 7 [,); 1 3 ) -> N e. GoldbachOdd ) )
159	158	3impia 1261	1 |- ( ( N e. Odd /\ 7 < N /\ N e. ( 7 [,); 1 3 ) ) -> N e. GoldbachOdd )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   class class class wbr 4653  (class class class)co 6650   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   RR*cxr 10073   < clt 10074   <_ cle 10075   2c2 11070   3c3 11071   5c5 11073   6c6 11074   7c7 11075   8c8 11076   9c9 11077   ZZcz 11377  ;cdc 11493   [,)cico 12177   Even ceven 41537   Odd codd 41538   GoldbachOdd cgbo 41635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-ico 12181  df-fz 12327  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-dvds 14984  df-prm 15386  df-even 41539  df-odd 41540  df-gbo 41638

This theorem is referenced by:  bgoldbtbnd  41697