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 42018
Description: Lemma 1 for bgoldbtbnd 42022: 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 11141 . . . . 5 7 ∈ ℝ
21rexri 10135 . . . 4 7 ∈ ℝ*
3 1nn0 11346 . . . . . . 7 1 ∈ ℕ0
4 3nn 11224 . . . . . . 7 3 ∈ ℕ
53, 4decnncl 11556 . . . . . 6 13 ∈ ℕ
65nnrei 11067 . . . . 5 13 ∈ ℝ
76rexri 10135 . . . 4 13 ∈ ℝ*
8 elico1 12256 . . . 4 ((7 ∈ ℝ*13 ∈ ℝ*) → (𝑁 ∈ (7[,)13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13)))
92, 7, 8mp2an 708 . . 3 (𝑁 ∈ (7[,)13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13))
10 7nn 11228 . . . . . . . . . 10 7 ∈ ℕ
1110nnzi 11439 . . . . . . . . 9 7 ∈ ℤ
12 oddz 41869 . . . . . . . . 9 (𝑁 ∈ Odd → 𝑁 ∈ ℤ)
13 zltp1le 11465 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (7 < 𝑁 ↔ (7 + 1) ≤ 𝑁))
14 7p1e8 11195 . . . . . . . . . . . 12 (7 + 1) = 8
1514breq1i 4692 . . . . . . . . . . 11 ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁)
1615a1i 11 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁))
17 8re 11143 . . . . . . . . . . . 12 8 ∈ ℝ
1817a1i 11 . . . . . . . . . . 11 (7 ∈ ℤ → 8 ∈ ℝ)
19 zre 11419 . . . . . . . . . . 11 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
20 leloe 10162 . . . . . . . . . . 11 ((8 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2118, 19, 20syl2an 493 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2213, 16, 213bitrd 294 . . . . . . . . 9 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2311, 12, 22sylancr 696 . . . . . . . 8 (𝑁 ∈ Odd → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
24 8nn 11229 . . . . . . . . . . . . . . 15 8 ∈ ℕ
2524nnzi 11439 . . . . . . . . . . . . . 14 8 ∈ ℤ
26 zltp1le 11465 . . . . . . . . . . . . . 14 ((8 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁))
2725, 12, 26sylancr 696 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁))
28 8p1e9 11196 . . . . . . . . . . . . . . 15 (8 + 1) = 9
2928breq1i 4692 . . . . . . . . . . . . . 14 ((8 + 1) ≤ 𝑁 ↔ 9 ≤ 𝑁)
3029a1i 11 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → ((8 + 1) ≤ 𝑁 ↔ 9 ≤ 𝑁))
31 9re 11145 . . . . . . . . . . . . . . 15 9 ∈ ℝ
3231a1i 11 . . . . . . . . . . . . . 14 (𝑁 ∈ Odd → 9 ∈ ℝ)
3312zred 11520 . . . . . . . . . . . . . 14 (𝑁 ∈ Odd → 𝑁 ∈ ℝ)
3432, 33leloed 10218 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → (9 ≤ 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁)))
3527, 30, 343bitrd 294 . . . . . . . . . . . 12 (𝑁 ∈ Odd → (8 < 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁)))
36 9nn 11230 . . . . . . . . . . . . . . . . . . 19 9 ∈ ℕ
3736nnzi 11439 . . . . . . . . . . . . . . . . . 18 9 ∈ ℤ
38 zltp1le 11465 . . . . . . . . . . . . . . . . . 18 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁))
3937, 12, 38sylancr 696 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁))
40 9p1e10 11534 . . . . . . . . . . . . . . . . . . 19 (9 + 1) = 10
4140breq1i 4692 . . . . . . . . . . . . . . . . . 18 ((9 + 1) ≤ 𝑁10 ≤ 𝑁)
4241a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → ((9 + 1) ≤ 𝑁10 ≤ 𝑁))
43 10re 11555 . . . . . . . . . . . . . . . . . . 19 10 ∈ ℝ
4443a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ Odd → 10 ∈ ℝ)
4544, 33leloed 10218 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → (10 ≤ 𝑁 ↔ (10 < 𝑁10 = 𝑁)))
4639, 42, 453bitrd 294 . . . . . . . . . . . . . . . 16 (𝑁 ∈ Odd → (9 < 𝑁 ↔ (10 < 𝑁10 = 𝑁)))
47 10nn 11552 . . . . . . . . . . . . . . . . . . . . . . 23 10 ∈ ℕ
4847nnzi 11439 . . . . . . . . . . . . . . . . . . . . . 22 10 ∈ ℤ
49 zltp1le 11465 . . . . . . . . . . . . . . . . . . . . . 22 ((10 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (10 < 𝑁 ↔ (10 + 1) ≤ 𝑁))
5048, 12, 49sylancr 696 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → (10 < 𝑁 ↔ (10 + 1) ≤ 𝑁))
51 dec10p 11591 . . . . . . . . . . . . . . . . . . . . . . 23 (10 + 1) = 11
5251breq1i 4692 . . . . . . . . . . . . . . . . . . . . . 22 ((10 + 1) ≤ 𝑁11 ≤ 𝑁)
5352a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → ((10 + 1) ≤ 𝑁11 ≤ 𝑁))
54 1nn 11069 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℕ
553, 54decnncl 11556 . . . . . . . . . . . . . . . . . . . . . . . 24 11 ∈ ℕ
5655nnrei 11067 . . . . . . . . . . . . . . . . . . . . . . 23 11 ∈ ℝ
5756a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ Odd → 11 ∈ ℝ)
5857, 33leloed 10218 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → (11 ≤ 𝑁 ↔ (11 < 𝑁11 = 𝑁)))
5950, 53, 583bitrd 294 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ Odd → (10 < 𝑁 ↔ (11 < 𝑁11 = 𝑁)))
6055nnzi 11439 . . . . . . . . . . . . . . . . . . . . . . . . . 26 11 ∈ ℤ
61 zltp1le 11465 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((11 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (11 < 𝑁 ↔ (11 + 1) ≤ 𝑁))
6260, 12, 61sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → (11 < 𝑁 ↔ (11 + 1) ≤ 𝑁))
6351eqcomi 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 11 = (10 + 1)
6463oveq1i 6700 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (11 + 1) = ((10 + 1) + 1)
6547nncni 11068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 10 ∈ ℂ
66 ax-1cn 10032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
6765, 66, 66addassi 10086 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((10 + 1) + 1) = (10 + (1 + 1))
68 1p1e2 11172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 + 1) = 2
6968oveq2i 6701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (10 + (1 + 1)) = (10 + 2)
70 dec10p 11591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (10 + 2) = 12
7169, 70eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (10 + (1 + 1)) = 12
7264, 67, 713eqtri 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (11 + 1) = 12
7372breq1i 4692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((11 + 1) ≤ 𝑁12 ≤ 𝑁)
7473a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → ((11 + 1) ≤ 𝑁12 ≤ 𝑁))
75 2nn 11223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℕ
763, 75decnncl 11556 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 12 ∈ ℕ
7776nnrei 11067 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 12 ∈ ℝ
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ Odd → 12 ∈ ℝ)
7978, 33leloed 10218 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → (12 ≤ 𝑁 ↔ (12 < 𝑁12 = 𝑁)))
8062, 74, 793bitrd 294 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ Odd → (11 < 𝑁 ↔ (12 < 𝑁12 = 𝑁)))
8176nnzi 11439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 12 ∈ ℤ
82 zltp1le 11465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((12 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (12 < 𝑁 ↔ (12 + 1) ≤ 𝑁))
8381, 12, 82sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → (12 < 𝑁 ↔ (12 + 1) ≤ 𝑁))
8470eqcomi 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 12 = (10 + 2)
8584oveq1i 6700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (12 + 1) = ((10 + 2) + 1)
86 2cn 11129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2 ∈ ℂ
8765, 86, 66addassi 10086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((10 + 2) + 1) = (10 + (2 + 1))
88 2p1e3 11189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (2 + 1) = 3
8988oveq2i 6701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (10 + (2 + 1)) = (10 + 3)
90 dec10p 11591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (10 + 3) = 13
9189, 90eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (10 + (2 + 1)) = 13
9285, 87, 913eqtri 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (12 + 1) = 13
9392breq1i 4692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((12 + 1) ≤ 𝑁13 ≤ 𝑁)
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → ((12 + 1) ≤ 𝑁13 ≤ 𝑁))
956a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ Odd → 13 ∈ ℝ)
9695, 33lenltd 10221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (12 = 𝑁 → (12 ∈ Odd ↔ 𝑁 ∈ Odd ))
102 6p6e12 11640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (6 + 6) = 12
103 6even 41945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 6 ∈ Even
104 epee 41939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((6 ∈ Even ∧ 6 ∈ Even ) → (6 + 6) ∈ Even )
105103, 103, 104mp2an 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (6 + 6) ∈ Even
106102, 105eqeltrri 2727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 12 ∈ Even
107 evennodd 41881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 393 . . . . . . . . . . . . . . . . . . . . . . . . 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 41988 . . . . . . . . . . . . . . . . . . . . . . . 24 11 ∈ GoldbachOdd
116 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . 24 (11 = 𝑁 → (11 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd ))
117115, 116mpbii 223 . . . . . . . . . . . . . . . . . . . . . . 23 (11 = 𝑁𝑁 ∈ GoldbachOdd )
1181172a1d 26 . . . . . . . . . . . . . . . . . . . . . 22 (11 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
119114, 118jaoi 393 . . . . . . . . . . . . . . . . . . . . 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 2718 . . . . . . . . . . . . . . . . . . 19 (10 = 𝑁 → (10 ∈ Odd ↔ 𝑁 ∈ Odd ))
124 5p5e10 11634 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 5) = 10
125 5odd 41944 . . . . . . . . . . . . . . . . . . . . . . 23 5 ∈ Odd
126 opoeALTV 41919 . . . . . . . . . . . . . . . . . . . . . . 23 ((5 ∈ Odd ∧ 5 ∈ Odd ) → (5 + 5) ∈ Even )
127125, 125, 126mp2an 708 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 5) ∈ Even
128124, 127eqeltrri 2727 . . . . . . . . . . . . . . . . . . . . 21 10 ∈ Even
129 evennodd 41881 . . . . . . . . . . . . . . . . . . . . 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 393 . . . . . . . . . . . . . . . . 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 41987 . . . . . . . . . . . . . . . 16 9 ∈ GoldbachOdd
138 eleq1 2718 . . . . . . . . . . . . . . . 16 (9 = 𝑁 → (9 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd ))
139137, 138mpbii 223 . . . . . . . . . . . . . . 15 (9 = 𝑁𝑁 ∈ GoldbachOdd )
1401392a1d 26 . . . . . . . . . . . . . 14 (9 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
141136, 140jaoi 393 . . . . . . . . . . . . 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 2718 . . . . . . . . . . 11 (8 = 𝑁 → (8 ∈ Odd ↔ 𝑁 ∈ Odd ))
146 8even 41947 . . . . . . . . . . . . 13 8 ∈ Even
147 evennodd 41881 . . . . . . . . . . . . 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 393 . . . . . . . . 9 ((8 < 𝑁 ∨ 8 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
152151com12 32 . . . . . . . 8 (𝑁 ∈ Odd → ((8 < 𝑁 ∨ 8 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
15323, 152sylbid 230 . . . . . . 7 (𝑁 ∈ Odd → (7 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
154153imp 444 . . . . . 6 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
155154com12 32 . . . . 5 (𝑁 < 13 → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOdd ))
1561553ad2ant3 1104 . . . 4 ((𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13) → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOdd ))
157156com12 32 . . 3 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → ((𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13) → 𝑁 ∈ GoldbachOdd ))
1589, 157syl5bi 232 . 2 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 ∈ (7[,)13) → 𝑁 ∈ GoldbachOdd ))
1591583impia 1280 1 ((𝑁 ∈ Odd ∧ 7 < 𝑁𝑁 ∈ (7[,)13)) → 𝑁 ∈ GoldbachOdd )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030   class class class wbr 4685  (class class class)co 6690  cr 9973  0cc0 9974  1c1 9975   + caddc 9977  *cxr 10111   < clt 10112  cle 10113  2c2 11108  3c3 11109  5c5 11111  6c6 11112  7c7 11113  8c8 11114  9c9 11115  cz 11415  cdc 11531  [,)cico 12215   Even ceven 41862   Odd codd 41863   GoldbachOdd cgbo 41960
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-rp 11871  df-ico 12219  df-fz 12365  df-seq 12842  df-exp 12901  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-dvds 15028  df-prm 15433  df-even 41864  df-odd 41865  df-gbo 41963
This theorem is referenced by:  bgoldbtbnd  42022
  Copyright terms: Public domain W3C validator