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 syl6bi ( 𝑁 ∈ 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 syl6bir ( 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 syl6bir ( 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 syl6bir ( 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 syl5bi ( ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ) → ( 𝑁 ∈ ( 7 [,) 1 3 ) → 𝑁 ∈ GoldbachOdd ) )
159 158 3impia ( ( 𝑁 ∈ Odd ∧ 7 < 𝑁𝑁 ∈ ( 7 [,) 1 3 ) ) → 𝑁 ∈ GoldbachOdd )