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 ( ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 ∈ ( 7 [,) 1 3 ) ) → 𝑁 ∈ GoldbachOdd )

Proof

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