Metamath Proof Explorer

Theorem bgoldbtbndlem1

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

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

Proof

Step Hyp Ref Expression
1 7re 
 |-  7 e. RR
2 1 rexri 
 |-  7 e. RR*
3 1nn0 
 |-  1 e. NN0
4 3nn 
 |-  3 e. NN
5 3 4 decnncl 
 |-  ; 1 3 e. NN
6 5 nnrei 
 |-  ; 1 3 e. RR
7 6 rexri 
 |-  ; 1 3 e. RR*
8 elico1 
 |-  ( ( 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 
 |-  ( N e. ( 7 [,) ; 1 3 ) <-> ( N e. RR* /\ 7 <_ N /\ N < ; 1 3 ) )
10 7nn 
 |-  7 e. NN
11 10 nnzi 
 |-  7 e. ZZ
12 oddz 
 |-  ( N e. Odd -> N e. ZZ )
13 zltp1le 
 |-  ( ( 7 e. ZZ /\ N e. ZZ ) -> ( 7 < N <-> ( 7 + 1 ) <_ N ) )
14 7p1e8 
 |-  ( 7 + 1 ) = 8
15 14 breq1i 
 |-  ( ( 7 + 1 ) <_ N <-> 8 <_ N )
16 15 a1i 
 |-  ( ( 7 e. ZZ /\ N e. ZZ ) -> ( ( 7 + 1 ) <_ N <-> 8 <_ N ) )
17 8re 
 |-  8 e. RR
18 17 a1i 
 |-  ( 7 e. ZZ -> 8 e. RR )
19 zre 
 |-  ( N e. ZZ -> N e. RR )
20 leloe 
 |-  ( ( 8 e. RR /\ N e. RR ) -> ( 8 <_ N <-> ( 8 < N \/ 8 = N ) ) )
21 18 19 20 syl2an 
 |-  ( ( 7 e. ZZ /\ N e. ZZ ) -> ( 8 <_ N <-> ( 8 < N \/ 8 = N ) ) )
22 13 16 21 3bitrd 
 |-  ( ( 7 e. ZZ /\ N e. ZZ ) -> ( 7 < N <-> ( 8 < N \/ 8 = N ) ) )
23 11 12 22 sylancr 
 |-  ( N e. Odd -> ( 7 < N <-> ( 8 < N \/ 8 = N ) ) )
24 8nn 
 |-  8 e. NN
25 24 nnzi 
 |-  8 e. ZZ
26 zltp1le 
 |-  ( ( 8 e. ZZ /\ N e. ZZ ) -> ( 8 < N <-> ( 8 + 1 ) <_ N ) )
27 25 12 26 sylancr 
 |-  ( N e. Odd -> ( 8 < N <-> ( 8 + 1 ) <_ N ) )
28 8p1e9 
 |-  ( 8 + 1 ) = 9
29 28 breq1i 
 |-  ( ( 8 + 1 ) <_ N <-> 9 <_ N )
30 29 a1i 
 |-  ( N e. Odd -> ( ( 8 + 1 ) <_ N <-> 9 <_ N ) )
31 9re 
 |-  9 e. RR
32 31 a1i 
 |-  ( N e. Odd -> 9 e. RR )
33 12 zred 
 |-  ( N e. Odd -> N e. RR )
34 32 33 leloed 
 |-  ( N e. Odd -> ( 9 <_ N <-> ( 9 < N \/ 9 = N ) ) )
35 27 30 34 3bitrd 
 |-  ( N e. Odd -> ( 8 < N <-> ( 9 < N \/ 9 = N ) ) )
36 9nn 
 |-  9 e. NN
37 36 nnzi 
 |-  9 e. ZZ
38 zltp1le 
 |-  ( ( 9 e. ZZ /\ N e. ZZ ) -> ( 9 < N <-> ( 9 + 1 ) <_ N ) )
39 37 12 38 sylancr 
 |-  ( N e. Odd -> ( 9 < N <-> ( 9 + 1 ) <_ N ) )
40 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
41 40 breq1i 
 |-  ( ( 9 + 1 ) <_ N <-> ; 1 0 <_ N )
42 41 a1i 
 |-  ( N e. Odd -> ( ( 9 + 1 ) <_ N <-> ; 1 0 <_ N ) )
43 10re 
 |-  ; 1 0 e. RR
44 43 a1i 
 |-  ( N e. Odd -> ; 1 0 e. RR )
45 44 33 leloed 
 |-  ( N e. Odd -> ( ; 1 0 <_ N <-> ( ; 1 0 < N \/ ; 1 0 = N ) ) )
46 39 42 45 3bitrd 
 |-  ( N e. Odd -> ( 9 < N <-> ( ; 1 0 < N \/ ; 1 0 = N ) ) )
47 10nn 
 |-  ; 1 0 e. NN
48 47 nnzi 
 |-  ; 1 0 e. ZZ
49 zltp1le 
 |-  ( ( ; 1 0 e. ZZ /\ N e. ZZ ) -> ( ; 1 0 < N <-> ( ; 1 0 + 1 ) <_ N ) )
50 48 12 49 sylancr 
 |-  ( N e. Odd -> ( ; 1 0 < N <-> ( ; 1 0 + 1 ) <_ N ) )
51 dec10p 
 |-  ( ; 1 0 + 1 ) = ; 1 1
52 51 breq1i 
 |-  ( ( ; 1 0 + 1 ) <_ N <-> ; 1 1 <_ N )
53 52 a1i 
 |-  ( N e. Odd -> ( ( ; 1 0 + 1 ) <_ N <-> ; 1 1 <_ N ) )
54 1nn 
 |-  1 e. NN
55 3 54 decnncl 
 |-  ; 1 1 e. NN
56 55 nnrei 
 |-  ; 1 1 e. RR
57 56 a1i 
 |-  ( N e. Odd -> ; 1 1 e. RR )
58 57 33 leloed 
 |-  ( N e. Odd -> ( ; 1 1 <_ N <-> ( ; 1 1 < N \/ ; 1 1 = N ) ) )
59 50 53 58 3bitrd 
 |-  ( N e. Odd -> ( ; 1 0 < N <-> ( ; 1 1 < N \/ ; 1 1 = N ) ) )
60 55 nnzi 
 |-  ; 1 1 e. ZZ
61 zltp1le 
 |-  ( ( ; 1 1 e. ZZ /\ N e. ZZ ) -> ( ; 1 1 < N <-> ( ; 1 1 + 1 ) <_ N ) )
62 60 12 61 sylancr 
 |-  ( N e. Odd -> ( ; 1 1 < N <-> ( ; 1 1 + 1 ) <_ N ) )
63 51 eqcomi 
 |-  ; 1 1 = ( ; 1 0 + 1 )
64 63 oveq1i 
 |-  ( ; 1 1 + 1 ) = ( ( ; 1 0 + 1 ) + 1 )
65 47 nncni 
 |-  ; 1 0 e. CC
66 ax-1cn 
 |-  1 e. CC
67 65 66 66 addassi 
 |-  ( ( ; 1 0 + 1 ) + 1 ) = ( ; 1 0 + ( 1 + 1 ) )
68 1p1e2 
 |-  ( 1 + 1 ) = 2
69 68 oveq2i 
 |-  ( ; 1 0 + ( 1 + 1 ) ) = ( ; 1 0 + 2 )
70 dec10p 
 |-  ( ; 1 0 + 2 ) = ; 1 2
71 69 70 eqtri 
 |-  ( ; 1 0 + ( 1 + 1 ) ) = ; 1 2
72 64 67 71 3eqtri 
 |-  ( ; 1 1 + 1 ) = ; 1 2
73 72 breq1i 
 |-  ( ( ; 1 1 + 1 ) <_ N <-> ; 1 2 <_ N )
74 73 a1i 
 |-  ( N e. Odd -> ( ( ; 1 1 + 1 ) <_ N <-> ; 1 2 <_ N ) )
75 2nn 
 |-  2 e. NN
76 3 75 decnncl 
 |-  ; 1 2 e. NN
77 76 nnrei 
 |-  ; 1 2 e. RR
78 77 a1i 
 |-  ( N e. Odd -> ; 1 2 e. RR )
79 78 33 leloed 
 |-  ( N e. Odd -> ( ; 1 2 <_ N <-> ( ; 1 2 < N \/ ; 1 2 = N ) ) )
80 62 74 79 3bitrd 
 |-  ( N e. Odd -> ( ; 1 1 < N <-> ( ; 1 2 < N \/ ; 1 2 = N ) ) )
81 76 nnzi 
 |-  ; 1 2 e. ZZ
82 zltp1le 
 |-  ( ( ; 1 2 e. ZZ /\ N e. ZZ ) -> ( ; 1 2 < N <-> ( ; 1 2 + 1 ) <_ N ) )
83 81 12 82 sylancr 
 |-  ( N e. Odd -> ( ; 1 2 < N <-> ( ; 1 2 + 1 ) <_ N ) )
84 70 eqcomi 
 |-  ; 1 2 = ( ; 1 0 + 2 )
85 84 oveq1i 
 |-  ( ; 1 2 + 1 ) = ( ( ; 1 0 + 2 ) + 1 )
86 2cn 
 |-  2 e. CC
87 65 86 66 addassi 
 |-  ( ( ; 1 0 + 2 ) + 1 ) = ( ; 1 0 + ( 2 + 1 ) )
88 2p1e3 
 |-  ( 2 + 1 ) = 3
89 88 oveq2i 
 |-  ( ; 1 0 + ( 2 + 1 ) ) = ( ; 1 0 + 3 )
90 dec10p 
 |-  ( ; 1 0 + 3 ) = ; 1 3
91 89 90 eqtri 
 |-  ( ; 1 0 + ( 2 + 1 ) ) = ; 1 3
92 85 87 91 3eqtri 
 |-  ( ; 1 2 + 1 ) = ; 1 3
93 92 breq1i 
 |-  ( ( ; 1 2 + 1 ) <_ N <-> ; 1 3 <_ N )
94 93 a1i 
 |-  ( N e. Odd -> ( ( ; 1 2 + 1 ) <_ N <-> ; 1 3 <_ N ) )
95 6 a1i 
 |-  ( N e. Odd -> ; 1 3 e. RR )
96 95 33 lenltd 
 |-  ( N e. Odd -> ( ; 1 3 <_ N <-> -. N < ; 1 3 ) )
97 83 94 96 3bitrd 
 |-  ( N e. Odd -> ( ; 1 2 < N <-> -. N < ; 1 3 ) )
98 pm2.21 
 |-  ( -. N < ; 1 3 -> ( N < ; 1 3 -> N e. GoldbachOdd ) )
99 97 98 syl6bi 
 |-  ( N e. Odd -> ( ; 1 2 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
100 99 com12 
 |-  ( ; 1 2 < N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
101 eleq1 
 |-  ( ; 1 2 = N -> ( ; 1 2 e. Odd <-> N e. Odd ) )
102 6p6e12 
 |-  ( 6 + 6 ) = ; 1 2
103 6even 
 |-  6 e. Even
104 epee 
 |-  ( ( 6 e. Even /\ 6 e. Even ) -> ( 6 + 6 ) e. Even )
105 103 103 104 mp2an 
 |-  ( 6 + 6 ) e. Even
106 102 105 eqeltrri 
 |-  ; 1 2 e. Even
107 evennodd 
 |-  ( ; 1 2 e. Even -> -. ; 1 2 e. Odd )
108 106 107 ax-mp 
 |-  -. ; 1 2 e. Odd
109 108 pm2.21i 
 |-  ( ; 1 2 e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) )
110 101 109 syl6bir 
 |-  ( ; 1 2 = N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
111 100 110 jaoi 
 |-  ( ( ; 1 2 < N \/ ; 1 2 = N ) -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
112 111 com12 
 |-  ( N e. Odd -> ( ( ; 1 2 < N \/ ; 1 2 = N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
113 80 112 sylbid 
 |-  ( N e. Odd -> ( ; 1 1 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
114 113 com12 
 |-  ( ; 1 1 < N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
115 11gbo 
 |-  ; 1 1 e. GoldbachOdd
116 eleq1 
 |-  ( ; 1 1 = N -> ( ; 1 1 e. GoldbachOdd <-> N e. GoldbachOdd ) )
117 115 116 mpbii 
 |-  ( ; 1 1 = N -> N e. GoldbachOdd )
118 117 2a1d 
 |-  ( ; 1 1 = N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
119 114 118 jaoi 
 |-  ( ( ; 1 1 < N \/ ; 1 1 = N ) -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
120 119 com12 
 |-  ( N e. Odd -> ( ( ; 1 1 < N \/ ; 1 1 = N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
121 59 120 sylbid 
 |-  ( N e. Odd -> ( ; 1 0 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
122 121 com12 
 |-  ( ; 1 0 < N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
123 eleq1 
 |-  ( ; 1 0 = N -> ( ; 1 0 e. Odd <-> N e. Odd ) )
124 5p5e10 
 |-  ( 5 + 5 ) = ; 1 0
125 5odd 
 |-  5 e. Odd
126 opoeALTV 
 |-  ( ( 5 e. Odd /\ 5 e. Odd ) -> ( 5 + 5 ) e. Even )
127 125 125 126 mp2an 
 |-  ( 5 + 5 ) e. Even
128 124 127 eqeltrri 
 |-  ; 1 0 e. Even
129 evennodd 
 |-  ( ; 1 0 e. Even -> -. ; 1 0 e. Odd )
130 128 129 ax-mp 
 |-  -. ; 1 0 e. Odd
131 130 pm2.21i 
 |-  ( ; 1 0 e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) )
132 123 131 syl6bir 
 |-  ( ; 1 0 = N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
133 122 132 jaoi 
 |-  ( ( ; 1 0 < N \/ ; 1 0 = N ) -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
134 133 com12 
 |-  ( N e. Odd -> ( ( ; 1 0 < N \/ ; 1 0 = N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
135 46 134 sylbid 
 |-  ( N e. Odd -> ( 9 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
136 135 com12 
 |-  ( 9 < N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
137 9gbo 
 |-  9 e. GoldbachOdd
138 eleq1 
 |-  ( 9 = N -> ( 9 e. GoldbachOdd <-> N e. GoldbachOdd ) )
139 137 138 mpbii 
 |-  ( 9 = N -> N e. GoldbachOdd )
140 139 2a1d 
 |-  ( 9 = N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
141 136 140 jaoi 
 |-  ( ( 9 < N \/ 9 = N ) -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
142 141 com12 
 |-  ( N e. Odd -> ( ( 9 < N \/ 9 = N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
143 35 142 sylbid 
 |-  ( N e. Odd -> ( 8 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
144 143 com12 
 |-  ( 8 < N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
145 eleq1 
 |-  ( 8 = N -> ( 8 e. Odd <-> N e. Odd ) )
146 8even 
 |-  8 e. Even
147 evennodd 
 |-  ( 8 e. Even -> -. 8 e. Odd )
148 146 147 ax-mp 
 |-  -. 8 e. Odd
149 148 pm2.21i 
 |-  ( 8 e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) )
150 145 149 syl6bir 
 |-  ( 8 = N -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
151 144 150 jaoi 
 |-  ( ( 8 < N \/ 8 = N ) -> ( N e. Odd -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
152 151 com12 
 |-  ( N e. Odd -> ( ( 8 < N \/ 8 = N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
153 23 152 sylbid 
 |-  ( N e. Odd -> ( 7 < N -> ( N < ; 1 3 -> N e. GoldbachOdd ) ) )
154 153 imp 
 |-  ( ( N e. Odd /\ 7 < N ) -> ( N < ; 1 3 -> N e. GoldbachOdd ) )
155 154 com12 
 |-  ( N < ; 1 3 -> ( ( N e. Odd /\ 7 < N ) -> N e. GoldbachOdd ) )
156 155 3ad2ant3 
 |-  ( ( N e. RR* /\ 7 <_ N /\ N < ; 1 3 ) -> ( ( N e. Odd /\ 7 < N ) -> N e. GoldbachOdd ) )
157 156 com12 
 |-  ( ( N e. Odd /\ 7 < N ) -> ( ( N e. RR* /\ 7 <_ N /\ N < ; 1 3 ) -> N e. GoldbachOdd ) )
158 9 157 syl5bi 
 |-  ( ( N e. Odd /\ 7 < N ) -> ( N e. ( 7 [,) ; 1 3 ) -> N e. GoldbachOdd ) )
159 158 3impia 
 |-  ( ( N e. Odd /\ 7 < N /\ N e. ( 7 [,) ; 1 3 ) ) -> N e. GoldbachOdd )