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 ∈ 7 13 → 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 ∈ 7 13 ↔ N ∈ ℝ * ∧ 7 ≤ N ∧ N < 13
9 2 7 8 mp2an ⊢ N ∈ 7 13 ↔ 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 biimtrdi ⊢ 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 biimtrrdi ⊢ 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 biimtrrdi ⊢ 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 biimtrrdi ⊢ 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 ∈ 7 13 → N ∈ GoldbachOdd
159 158 3impia ⊢ N ∈ Odd ∧ 7 < N ∧ N ∈ 7 13 → N ∈ GoldbachOdd