Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bgoldbtbndlem1 Structured version   Visualization version   GIF version

Theorem bgoldbtbndlem1 41458
Description: Lemma 1 for bgoldbtbnd 41462: the odd numbers between 7 and 13 (exclusive) are odd Goldbach numbers. (Contributed by AV, 29-Jul-2020.)
Assertion
Ref Expression
bgoldbtbndlem1 ((𝑁 ∈ Odd ∧ 7 < 𝑁𝑁 ∈ (7[,)13)) → 𝑁 ∈ GoldbachOdd )

Proof of Theorem bgoldbtbndlem1
StepHypRef Expression
1 7re 11088 . . . . 5 7 ∈ ℝ
21rexri 10082 . . . 4 7 ∈ ℝ*
3 1nn0 11293 . . . . . . 7 1 ∈ ℕ0
4 3nn 11171 . . . . . . 7 3 ∈ ℕ
53, 4decnncl 11503 . . . . . 6 13 ∈ ℕ
65nnrei 11014 . . . . 5 13 ∈ ℝ
76rexri 10082 . . . 4 13 ∈ ℝ*
8 elico1 12203 . . . 4 ((7 ∈ ℝ*13 ∈ ℝ*) → (𝑁 ∈ (7[,)13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13)))
92, 7, 8mp2an 707 . . 3 (𝑁 ∈ (7[,)13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13))
10 7nn 11175 . . . . . . . . . 10 7 ∈ ℕ
1110nnzi 11386 . . . . . . . . 9 7 ∈ ℤ
12 oddz 41309 . . . . . . . . 9 (𝑁 ∈ Odd → 𝑁 ∈ ℤ)
13 zltp1le 11412 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (7 < 𝑁 ↔ (7 + 1) ≤ 𝑁))
14 7p1e8 11142 . . . . . . . . . . . 12 (7 + 1) = 8
1514breq1i 4651 . . . . . . . . . . 11 ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁)
1615a1i 11 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁))
17 8re 11090 . . . . . . . . . . . 12 8 ∈ ℝ
1817a1i 11 . . . . . . . . . . 11 (7 ∈ ℤ → 8 ∈ ℝ)
19 zre 11366 . . . . . . . . . . 11 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
20 leloe 10109 . . . . . . . . . . 11 ((8 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2118, 19, 20syl2an 494 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2213, 16, 213bitrd 294 . . . . . . . . 9 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2311, 12, 22sylancr 694 . . . . . . . 8 (𝑁 ∈ Odd → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
24 8nn 11176 . . . . . . . . . . . . . . 15 8 ∈ ℕ
2524nnzi 11386 . . . . . . . . . . . . . 14 8 ∈ ℤ
26 zltp1le 11412 . . . . . . . . . . . . . 14 ((8 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁))
2725, 12, 26sylancr 694 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁))
28 8p1e9 11143 . . . . . . . . . . . . . . 15 (8 + 1) = 9
2928breq1i 4651 . . . . . . . . . . . . . 14 ((8 + 1) ≤ 𝑁 ↔ 9 ≤ 𝑁)
3029a1i 11 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → ((8 + 1) ≤ 𝑁 ↔ 9 ≤ 𝑁))
31 9re 11092 . . . . . . . . . . . . . . 15 9 ∈ ℝ
3231a1i 11 . . . . . . . . . . . . . 14 (𝑁 ∈ Odd → 9 ∈ ℝ)
3312zred 11467 . . . . . . . . . . . . . 14 (𝑁 ∈ Odd → 𝑁 ∈ ℝ)
3432, 33leloed 10165 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → (9 ≤ 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁)))
3527, 30, 343bitrd 294 . . . . . . . . . . . 12 (𝑁 ∈ Odd → (8 < 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁)))
36 9nn 11177 . . . . . . . . . . . . . . . . . . 19 9 ∈ ℕ
3736nnzi 11386 . . . . . . . . . . . . . . . . . 18 9 ∈ ℤ
38 zltp1le 11412 . . . . . . . . . . . . . . . . . 18 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁))
3937, 12, 38sylancr 694 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁))
40 9p1e10 11481 . . . . . . . . . . . . . . . . . . 19 (9 + 1) = 10
4140breq1i 4651 . . . . . . . . . . . . . . . . . 18 ((9 + 1) ≤ 𝑁10 ≤ 𝑁)
4241a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → ((9 + 1) ≤ 𝑁10 ≤ 𝑁))
43 10re 11502 . . . . . . . . . . . . . . . . . . 19 10 ∈ ℝ
4443a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ Odd → 10 ∈ ℝ)
4544, 33leloed 10165 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → (10 ≤ 𝑁 ↔ (10 < 𝑁10 = 𝑁)))
4639, 42, 453bitrd 294 . . . . . . . . . . . . . . . 16 (𝑁 ∈ Odd → (9 < 𝑁 ↔ (10 < 𝑁10 = 𝑁)))
47 10nn 11499 . . . . . . . . . . . . . . . . . . . . . . 23 10 ∈ ℕ
4847nnzi 11386 . . . . . . . . . . . . . . . . . . . . . 22 10 ∈ ℤ
49 zltp1le 11412 . . . . . . . . . . . . . . . . . . . . . 22 ((10 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (10 < 𝑁 ↔ (10 + 1) ≤ 𝑁))
5048, 12, 49sylancr 694 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → (10 < 𝑁 ↔ (10 + 1) ≤ 𝑁))
51 dec10p 11538 . . . . . . . . . . . . . . . . . . . . . . 23 (10 + 1) = 11
5251breq1i 4651 . . . . . . . . . . . . . . . . . . . . . 22 ((10 + 1) ≤ 𝑁11 ≤ 𝑁)
5352a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → ((10 + 1) ≤ 𝑁11 ≤ 𝑁))
54 1nn 11016 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℕ
553, 54decnncl 11503 . . . . . . . . . . . . . . . . . . . . . . . 24 11 ∈ ℕ
5655nnrei 11014 . . . . . . . . . . . . . . . . . . . . . . 23 11 ∈ ℝ
5756a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ Odd → 11 ∈ ℝ)
5857, 33leloed 10165 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → (11 ≤ 𝑁 ↔ (11 < 𝑁11 = 𝑁)))
5950, 53, 583bitrd 294 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ Odd → (10 < 𝑁 ↔ (11 < 𝑁11 = 𝑁)))
6055nnzi 11386 . . . . . . . . . . . . . . . . . . . . . . . . . 26 11 ∈ ℤ
61 zltp1le 11412 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((11 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (11 < 𝑁 ↔ (11 + 1) ≤ 𝑁))
6260, 12, 61sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → (11 < 𝑁 ↔ (11 + 1) ≤ 𝑁))
6351eqcomi 2629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 11 = (10 + 1)
6463oveq1i 6645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (11 + 1) = ((10 + 1) + 1)
6547nncni 11015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 10 ∈ ℂ
66 ax-1cn 9979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
6765, 66, 66addassi 10033 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((10 + 1) + 1) = (10 + (1 + 1))
68 1p1e2 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 + 1) = 2
6968oveq2i 6646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (10 + (1 + 1)) = (10 + 2)
70 dec10p 11538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (10 + 2) = 12
7169, 70eqtri 2642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (10 + (1 + 1)) = 12
7264, 67, 713eqtri 2646 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (11 + 1) = 12
7372breq1i 4651 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((11 + 1) ≤ 𝑁12 ≤ 𝑁)
7473a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → ((11 + 1) ≤ 𝑁12 ≤ 𝑁))
75 2nn 11170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℕ
763, 75decnncl 11503 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 12 ∈ ℕ
7776nnrei 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 12 ∈ ℝ
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ Odd → 12 ∈ ℝ)
7978, 33leloed 10165 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → (12 ≤ 𝑁 ↔ (12 < 𝑁12 = 𝑁)))
8062, 74, 793bitrd 294 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ Odd → (11 < 𝑁 ↔ (12 < 𝑁12 = 𝑁)))
8176nnzi 11386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 12 ∈ ℤ
82 zltp1le 11412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((12 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (12 < 𝑁 ↔ (12 + 1) ≤ 𝑁))
8381, 12, 82sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → (12 < 𝑁 ↔ (12 + 1) ≤ 𝑁))
8470eqcomi 2629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 12 = (10 + 2)
8584oveq1i 6645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (12 + 1) = ((10 + 2) + 1)
86 2cn 11076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2 ∈ ℂ
8765, 86, 66addassi 10033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((10 + 2) + 1) = (10 + (2 + 1))
88 2p1e3 11136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (2 + 1) = 3
8988oveq2i 6646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (10 + (2 + 1)) = (10 + 3)
90 dec10p 11538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (10 + 3) = 13
9189, 90eqtri 2642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (10 + (2 + 1)) = 13
9285, 87, 913eqtri 2646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (12 + 1) = 13
9392breq1i 4651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((12 + 1) ≤ 𝑁13 ≤ 𝑁)
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → ((12 + 1) ≤ 𝑁13 ≤ 𝑁))
956a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ Odd → 13 ∈ ℝ)
9695, 33lenltd 10168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → (13 ≤ 𝑁 ↔ ¬ 𝑁 < 13))
9783, 94, 963bitrd 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ Odd → (12 < 𝑁 ↔ ¬ 𝑁 < 13))
98 pm2.21 120 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑁 < 13 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
9997, 98syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ Odd → (12 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
10099com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (12 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
101 eleq1 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (12 = 𝑁 → (12 ∈ Odd ↔ 𝑁 ∈ Odd ))
102 6p6e12 11587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (6 + 6) = 12
103 6even 41385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 6 ∈ Even
104 epee 41379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((6 ∈ Even ∧ 6 ∈ Even ) → (6 + 6) ∈ Even )
105103, 103, 104mp2an 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (6 + 6) ∈ Even
106102, 105eqeltrri 2696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 12 ∈ Even
107 evennodd 41321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (12 ∈ Even → ¬ 12 ∈ Odd )
108106, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ¬ 12 ∈ Odd
109108pm2.21i 116 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (12 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
110101, 109syl6bir 244 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (12 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
111100, 110jaoi 394 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((12 < 𝑁12 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
112111com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ Odd → ((12 < 𝑁12 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
11380, 112sylbid 230 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ Odd → (11 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
114113com12 32 . . . . . . . . . . . . . . . . . . . . . 22 (11 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
115 11gbo 41428 . . . . . . . . . . . . . . . . . . . . . . . 24 11 ∈ GoldbachOdd
116 eleq1 2687 . . . . . . . . . . . . . . . . . . . . . . . 24 (11 = 𝑁 → (11 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd ))
117115, 116mpbii 223 . . . . . . . . . . . . . . . . . . . . . . 23 (11 = 𝑁𝑁 ∈ GoldbachOdd )
1181172a1d 26 . . . . . . . . . . . . . . . . . . . . . 22 (11 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
119114, 118jaoi 394 . . . . . . . . . . . . . . . . . . . . 21 ((11 < 𝑁11 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
120119com12 32 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ Odd → ((11 < 𝑁11 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
12159, 120sylbid 230 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ Odd → (10 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
122121com12 32 . . . . . . . . . . . . . . . . . 18 (10 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
123 eleq1 2687 . . . . . . . . . . . . . . . . . . 19 (10 = 𝑁 → (10 ∈ Odd ↔ 𝑁 ∈ Odd ))
124 5p5e10 11581 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 5) = 10
125 5odd 41384 . . . . . . . . . . . . . . . . . . . . . . 23 5 ∈ Odd
126 opoeALTV 41359 . . . . . . . . . . . . . . . . . . . . . . 23 ((5 ∈ Odd ∧ 5 ∈ Odd ) → (5 + 5) ∈ Even )
127125, 125, 126mp2an 707 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 5) ∈ Even
128124, 127eqeltrri 2696 . . . . . . . . . . . . . . . . . . . . 21 10 ∈ Even
129 evennodd 41321 . . . . . . . . . . . . . . . . . . . . 21 (10 ∈ Even → ¬ 10 ∈ Odd )
130128, 129ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ¬ 10 ∈ Odd
131130pm2.21i 116 . . . . . . . . . . . . . . . . . . 19 (10 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
132123, 131syl6bir 244 . . . . . . . . . . . . . . . . . 18 (10 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
133122, 132jaoi 394 . . . . . . . . . . . . . . . . 17 ((10 < 𝑁10 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
134133com12 32 . . . . . . . . . . . . . . . 16 (𝑁 ∈ Odd → ((10 < 𝑁10 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
13546, 134sylbid 230 . . . . . . . . . . . . . . 15 (𝑁 ∈ Odd → (9 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
136135com12 32 . . . . . . . . . . . . . 14 (9 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
137 9gbo 41427 . . . . . . . . . . . . . . . 16 9 ∈ GoldbachOdd
138 eleq1 2687 . . . . . . . . . . . . . . . 16 (9 = 𝑁 → (9 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd ))
139137, 138mpbii 223 . . . . . . . . . . . . . . 15 (9 = 𝑁𝑁 ∈ GoldbachOdd )
1401392a1d 26 . . . . . . . . . . . . . 14 (9 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
141136, 140jaoi 394 . . . . . . . . . . . . 13 ((9 < 𝑁 ∨ 9 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
142141com12 32 . . . . . . . . . . . 12 (𝑁 ∈ Odd → ((9 < 𝑁 ∨ 9 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
14335, 142sylbid 230 . . . . . . . . . . 11 (𝑁 ∈ Odd → (8 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
144143com12 32 . . . . . . . . . 10 (8 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
145 eleq1 2687 . . . . . . . . . . 11 (8 = 𝑁 → (8 ∈ Odd ↔ 𝑁 ∈ Odd ))
146 8even 41387 . . . . . . . . . . . . 13 8 ∈ Even
147 evennodd 41321 . . . . . . . . . . . . 13 (8 ∈ Even → ¬ 8 ∈ Odd )
148146, 147ax-mp 5 . . . . . . . . . . . 12 ¬ 8 ∈ Odd
149148pm2.21i 116 . . . . . . . . . . 11 (8 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
150145, 149syl6bir 244 . . . . . . . . . 10 (8 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
151144, 150jaoi 394 . . . . . . . . 9 ((8 < 𝑁 ∨ 8 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
152151com12 32 . . . . . . . 8 (𝑁 ∈ Odd → ((8 < 𝑁 ∨ 8 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
15323, 152sylbid 230 . . . . . . 7 (𝑁 ∈ Odd → (7 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
154153imp 445 . . . . . 6 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
155154com12 32 . . . . 5 (𝑁 < 13 → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOdd ))
1561553ad2ant3 1082 . . . 4 ((𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13) → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOdd ))
157156com12 32 . . 3 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → ((𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13) → 𝑁 ∈ GoldbachOdd ))
1589, 157syl5bi 232 . 2 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 ∈ (7[,)13) → 𝑁 ∈ GoldbachOdd ))
1591583impia 1259 1 ((𝑁 ∈ Odd ∧ 7 < 𝑁𝑁 ∈ (7[,)13)) → 𝑁 ∈ GoldbachOdd )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1481  wcel 1988   class class class wbr 4644  (class class class)co 6635  cr 9920  0cc0 9921  1c1 9922   + caddc 9924  *cxr 10058   < clt 10059  cle 10060  2c2 11055  3c3 11056  5c5 11058  6c6 11059  7c7 11060  8c8 11061  9c9 11062  cz 11362  cdc 11478  [,)cico 12162   Even ceven 41302   Odd codd 41303   GoldbachOdd cgbo 41400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-sup 8333  df-inf 8334  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-rp 11818  df-ico 12166  df-fz 12312  df-seq 12785  df-exp 12844  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-dvds 14965  df-prm 15367  df-even 41304  df-odd 41305  df-gbo 41403
This theorem is referenced by:  bgoldbtbnd  41462
  Copyright terms: Public domain W3C validator