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∈Odd∧7<N∧N∈713→N∈GoldbachOdd

Proof

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