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 42301
Description: Lemma 1 for bgoldbtbnd 42305: 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 11368 . . . . 5 7 ∈ ℝ
21rexri 10350 . . . 4 7 ∈ ℝ*
3 1nn0 11555 . . . . . . 7 1 ∈ ℕ0
4 3nn 11350 . . . . . . 7 3 ∈ ℕ
53, 4decnncl 11760 . . . . . 6 13 ∈ ℕ
65nnrei 11283 . . . . 5 13 ∈ ℝ
76rexri 10350 . . . 4 13 ∈ ℝ*
8 elico1 12419 . . . 4 ((7 ∈ ℝ*13 ∈ ℝ*) → (𝑁 ∈ (7[,)13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13)))
92, 7, 8mp2an 683 . . 3 (𝑁 ∈ (7[,)13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13))
10 7nn 11367 . . . . . . . . . 10 7 ∈ ℕ
1110nnzi 11647 . . . . . . . . 9 7 ∈ ℤ
12 oddz 42152 . . . . . . . . 9 (𝑁 ∈ Odd → 𝑁 ∈ ℤ)
13 zltp1le 11673 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (7 < 𝑁 ↔ (7 + 1) ≤ 𝑁))
14 7p1e8 11426 . . . . . . . . . . . 12 (7 + 1) = 8
1514breq1i 4815 . . . . . . . . . . 11 ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁)
1615a1i 11 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁))
17 8re 11372 . . . . . . . . . . . 12 8 ∈ ℝ
1817a1i 11 . . . . . . . . . . 11 (7 ∈ ℤ → 8 ∈ ℝ)
19 zre 11627 . . . . . . . . . . 11 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
20 leloe 10377 . . . . . . . . . . 11 ((8 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2118, 19, 20syl2an 589 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2213, 16, 213bitrd 296 . . . . . . . . 9 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2311, 12, 22sylancr 581 . . . . . . . 8 (𝑁 ∈ Odd → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
24 8nn 11371 . . . . . . . . . . . . . . 15 8 ∈ ℕ
2524nnzi 11647 . . . . . . . . . . . . . 14 8 ∈ ℤ
26 zltp1le 11673 . . . . . . . . . . . . . 14 ((8 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁))
2725, 12, 26sylancr 581 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁))
28 8p1e9 11427 . . . . . . . . . . . . . . 15 (8 + 1) = 9
2928breq1i 4815 . . . . . . . . . . . . . 14 ((8 + 1) ≤ 𝑁 ↔ 9 ≤ 𝑁)
3029a1i 11 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → ((8 + 1) ≤ 𝑁 ↔ 9 ≤ 𝑁))
31 9re 11376 . . . . . . . . . . . . . . 15 9 ∈ ℝ
3231a1i 11 . . . . . . . . . . . . . 14 (𝑁 ∈ Odd → 9 ∈ ℝ)
3312zred 11728 . . . . . . . . . . . . . 14 (𝑁 ∈ Odd → 𝑁 ∈ ℝ)
3432, 33leloed 10433 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → (9 ≤ 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁)))
3527, 30, 343bitrd 296 . . . . . . . . . . . 12 (𝑁 ∈ Odd → (8 < 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁)))
36 9nn 11375 . . . . . . . . . . . . . . . . . . 19 9 ∈ ℕ
3736nnzi 11647 . . . . . . . . . . . . . . . . . 18 9 ∈ ℤ
38 zltp1le 11673 . . . . . . . . . . . . . . . . . 18 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁))
3937, 12, 38sylancr 581 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁))
40 9p1e10 11741 . . . . . . . . . . . . . . . . . . 19 (9 + 1) = 10
4140breq1i 4815 . . . . . . . . . . . . . . . . . 18 ((9 + 1) ≤ 𝑁10 ≤ 𝑁)
4241a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → ((9 + 1) ≤ 𝑁10 ≤ 𝑁))
43 10re 11758 . . . . . . . . . . . . . . . . . . 19 10 ∈ ℝ
4443a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ Odd → 10 ∈ ℝ)
4544, 33leloed 10433 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → (10 ≤ 𝑁 ↔ (10 < 𝑁10 = 𝑁)))
4639, 42, 453bitrd 296 . . . . . . . . . . . . . . . 16 (𝑁 ∈ Odd → (9 < 𝑁 ↔ (10 < 𝑁10 = 𝑁)))
47 10nn 11755 . . . . . . . . . . . . . . . . . . . . . . 23 10 ∈ ℕ
4847nnzi 11647 . . . . . . . . . . . . . . . . . . . . . 22 10 ∈ ℤ
49 zltp1le 11673 . . . . . . . . . . . . . . . . . . . . . 22 ((10 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (10 < 𝑁 ↔ (10 + 1) ≤ 𝑁))
5048, 12, 49sylancr 581 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → (10 < 𝑁 ↔ (10 + 1) ≤ 𝑁))
51 dec10p 11783 . . . . . . . . . . . . . . . . . . . . . . 23 (10 + 1) = 11
5251breq1i 4815 . . . . . . . . . . . . . . . . . . . . . 22 ((10 + 1) ≤ 𝑁11 ≤ 𝑁)
5352a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → ((10 + 1) ≤ 𝑁11 ≤ 𝑁))
54 1nn 11286 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℕ
553, 54decnncl 11760 . . . . . . . . . . . . . . . . . . . . . . . 24 11 ∈ ℕ
5655nnrei 11283 . . . . . . . . . . . . . . . . . . . . . . 23 11 ∈ ℝ
5756a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ Odd → 11 ∈ ℝ)
5857, 33leloed 10433 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → (11 ≤ 𝑁 ↔ (11 < 𝑁11 = 𝑁)))
5950, 53, 583bitrd 296 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ Odd → (10 < 𝑁 ↔ (11 < 𝑁11 = 𝑁)))
6055nnzi 11647 . . . . . . . . . . . . . . . . . . . . . . . . . 26 11 ∈ ℤ
61 zltp1le 11673 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((11 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (11 < 𝑁 ↔ (11 + 1) ≤ 𝑁))
6260, 12, 61sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → (11 < 𝑁 ↔ (11 + 1) ≤ 𝑁))
6351eqcomi 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 11 = (10 + 1)
6463oveq1i 6851 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (11 + 1) = ((10 + 1) + 1)
6547nncni 11284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 10 ∈ ℂ
66 ax-1cn 10246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
6765, 66, 66addassi 10303 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((10 + 1) + 1) = (10 + (1 + 1))
68 1p1e2 11403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 + 1) = 2
6968oveq2i 6852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (10 + (1 + 1)) = (10 + 2)
70 dec10p 11783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (10 + 2) = 12
7169, 70eqtri 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (10 + (1 + 1)) = 12
7264, 67, 713eqtri 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (11 + 1) = 12
7372breq1i 4815 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((11 + 1) ≤ 𝑁12 ≤ 𝑁)
7473a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → ((11 + 1) ≤ 𝑁12 ≤ 𝑁))
75 2nn 11344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℕ
763, 75decnncl 11760 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 12 ∈ ℕ
7776nnrei 11283 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 12 ∈ ℝ
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ Odd → 12 ∈ ℝ)
7978, 33leloed 10433 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → (12 ≤ 𝑁 ↔ (12 < 𝑁12 = 𝑁)))
8062, 74, 793bitrd 296 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ Odd → (11 < 𝑁 ↔ (12 < 𝑁12 = 𝑁)))
8176nnzi 11647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 12 ∈ ℤ
82 zltp1le 11673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((12 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (12 < 𝑁 ↔ (12 + 1) ≤ 𝑁))
8381, 12, 82sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → (12 < 𝑁 ↔ (12 + 1) ≤ 𝑁))
8470eqcomi 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 12 = (10 + 2)
8584oveq1i 6851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (12 + 1) = ((10 + 2) + 1)
86 2cn 11346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2 ∈ ℂ
8765, 86, 66addassi 10303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((10 + 2) + 1) = (10 + (2 + 1))
88 2p1e3 11420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (2 + 1) = 3
8988oveq2i 6852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (10 + (2 + 1)) = (10 + 3)
90 dec10p 11783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (10 + 3) = 13
9189, 90eqtri 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (10 + (2 + 1)) = 13
9285, 87, 913eqtri 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (12 + 1) = 13
9392breq1i 4815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((12 + 1) ≤ 𝑁13 ≤ 𝑁)
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → ((12 + 1) ≤ 𝑁13 ≤ 𝑁))
956a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ Odd → 13 ∈ ℝ)
9695, 33lenltd 10436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → (13 ≤ 𝑁 ↔ ¬ 𝑁 < 13))
9783, 94, 963bitrd 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ Odd → (12 < 𝑁 ↔ ¬ 𝑁 < 13))
98 pm2.21 121 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑁 < 13 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
9997, 98syl6bi 244 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ Odd → (12 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
10099com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (12 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
101 eleq1 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (12 = 𝑁 → (12 ∈ Odd ↔ 𝑁 ∈ Odd ))
102 6p6e12 11814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (6 + 6) = 12
103 6even 42228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 6 ∈ Even
104 epee 42222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((6 ∈ Even ∧ 6 ∈ Even ) → (6 + 6) ∈ Even )
105103, 103, 104mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (6 + 6) ∈ Even
106102, 105eqeltrri 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 12 ∈ Even
107 evennodd 42164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (12 ∈ Even → ¬ 12 ∈ Odd )
108106, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ¬ 12 ∈ Odd
109108pm2.21i 117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (12 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
110101, 109syl6bir 245 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (12 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
111100, 110jaoi 883 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((12 < 𝑁12 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
112111com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ Odd → ((12 < 𝑁12 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
11380, 112sylbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ Odd → (11 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
114113com12 32 . . . . . . . . . . . . . . . . . . . . . 22 (11 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
115 11gbo 42271 . . . . . . . . . . . . . . . . . . . . . . . 24 11 ∈ GoldbachOdd
116 eleq1 2831 . . . . . . . . . . . . . . . . . . . . . . . 24 (11 = 𝑁 → (11 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd ))
117115, 116mpbii 224 . . . . . . . . . . . . . . . . . . . . . . 23 (11 = 𝑁𝑁 ∈ GoldbachOdd )
1181172a1d 26 . . . . . . . . . . . . . . . . . . . . . 22 (11 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
119114, 118jaoi 883 . . . . . . . . . . . . . . . . . . . . 21 ((11 < 𝑁11 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
120119com12 32 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ Odd → ((11 < 𝑁11 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
12159, 120sylbid 231 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ Odd → (10 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
122121com12 32 . . . . . . . . . . . . . . . . . 18 (10 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
123 eleq1 2831 . . . . . . . . . . . . . . . . . . 19 (10 = 𝑁 → (10 ∈ Odd ↔ 𝑁 ∈ Odd ))
124 5p5e10 11811 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 5) = 10
125 5odd 42227 . . . . . . . . . . . . . . . . . . . . . . 23 5 ∈ Odd
126 opoeALTV 42202 . . . . . . . . . . . . . . . . . . . . . . 23 ((5 ∈ Odd ∧ 5 ∈ Odd ) → (5 + 5) ∈ Even )
127125, 125, 126mp2an 683 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 5) ∈ Even
128124, 127eqeltrri 2840 . . . . . . . . . . . . . . . . . . . . 21 10 ∈ Even
129 evennodd 42164 . . . . . . . . . . . . . . . . . . . . 21 (10 ∈ Even → ¬ 10 ∈ Odd )
130128, 129ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ¬ 10 ∈ Odd
131130pm2.21i 117 . . . . . . . . . . . . . . . . . . 19 (10 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
132123, 131syl6bir 245 . . . . . . . . . . . . . . . . . 18 (10 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
133122, 132jaoi 883 . . . . . . . . . . . . . . . . 17 ((10 < 𝑁10 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
134133com12 32 . . . . . . . . . . . . . . . 16 (𝑁 ∈ Odd → ((10 < 𝑁10 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
13546, 134sylbid 231 . . . . . . . . . . . . . . 15 (𝑁 ∈ Odd → (9 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
136135com12 32 . . . . . . . . . . . . . 14 (9 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
137 9gbo 42270 . . . . . . . . . . . . . . . 16 9 ∈ GoldbachOdd
138 eleq1 2831 . . . . . . . . . . . . . . . 16 (9 = 𝑁 → (9 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd ))
139137, 138mpbii 224 . . . . . . . . . . . . . . 15 (9 = 𝑁𝑁 ∈ GoldbachOdd )
1401392a1d 26 . . . . . . . . . . . . . 14 (9 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
141136, 140jaoi 883 . . . . . . . . . . . . 13 ((9 < 𝑁 ∨ 9 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
142141com12 32 . . . . . . . . . . . 12 (𝑁 ∈ Odd → ((9 < 𝑁 ∨ 9 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
14335, 142sylbid 231 . . . . . . . . . . 11 (𝑁 ∈ Odd → (8 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
144143com12 32 . . . . . . . . . 10 (8 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
145 eleq1 2831 . . . . . . . . . . 11 (8 = 𝑁 → (8 ∈ Odd ↔ 𝑁 ∈ Odd ))
146 8even 42230 . . . . . . . . . . . . 13 8 ∈ Even
147 evennodd 42164 . . . . . . . . . . . . 13 (8 ∈ Even → ¬ 8 ∈ Odd )
148146, 147ax-mp 5 . . . . . . . . . . . 12 ¬ 8 ∈ Odd
149148pm2.21i 117 . . . . . . . . . . 11 (8 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
150145, 149syl6bir 245 . . . . . . . . . 10 (8 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
151144, 150jaoi 883 . . . . . . . . 9 ((8 < 𝑁 ∨ 8 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
152151com12 32 . . . . . . . 8 (𝑁 ∈ Odd → ((8 < 𝑁 ∨ 8 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
15323, 152sylbid 231 . . . . . . 7 (𝑁 ∈ Odd → (7 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd )))
154153imp 395 . . . . . 6 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOdd ))
155154com12 32 . . . . 5 (𝑁 < 13 → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOdd ))
1561553ad2ant3 1165 . . . 4 ((𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13) → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOdd ))
157156com12 32 . . 3 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → ((𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13) → 𝑁 ∈ GoldbachOdd ))
1589, 157syl5bi 233 . 2 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 ∈ (7[,)13) → 𝑁 ∈ GoldbachOdd ))
1591583impia 1145 1 ((𝑁 ∈ Odd ∧ 7 < 𝑁𝑁 ∈ (7[,)13)) → 𝑁 ∈ GoldbachOdd )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155   class class class wbr 4808  (class class class)co 6841  cr 10187  0cc0 10188  1c1 10189   + caddc 10191  *cxr 10326   < clt 10327  cle 10328  2c2 11326  3c3 11327  5c5 11329  6c6 11330  7c7 11331  8c8 11332  9c9 11333  cz 11623  cdc 11739  [,)cico 12378   Even ceven 42145   Odd codd 42146   GoldbachOdd cgbo 42243
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-er 7946  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-sup 8554  df-inf 8555  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-7 11339  df-8 11340  df-9 11341  df-n0 11538  df-z 11624  df-dec 11740  df-uz 11886  df-rp 12028  df-ico 12382  df-fz 12533  df-seq 13008  df-exp 13067  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-dvds 15267  df-prm 15667  df-even 42147  df-odd 42148  df-gbo 42246
This theorem is referenced by:  bgoldbtbnd  42305
  Copyright terms: Public domain W3C validator