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 42221
Description: Lemma 1 for bgoldbtbnd 42225: 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 11315 . . . . 5 7 ∈ ℝ
21rexri 10309 . . . 4 7 ∈ ℝ*
3 1nn0 11520 . . . . . . 7 1 ∈ ℕ0
4 3nn 11398 . . . . . . 7 3 ∈ ℕ
53, 4decnncl 11730 . . . . . 6 13 ∈ ℕ
65nnrei 11241 . . . . 5 13 ∈ ℝ
76rexri 10309 . . . 4 13 ∈ ℝ*
8 elico1 12431 . . . 4 ((7 ∈ ℝ*13 ∈ ℝ*) → (𝑁 ∈ (7[,)13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13)))
92, 7, 8mp2an 710 . . 3 (𝑁 ∈ (7[,)13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13))
10 7nn 11402 . . . . . . . . . 10 7 ∈ ℕ
1110nnzi 11613 . . . . . . . . 9 7 ∈ ℤ
12 oddz 42072 . . . . . . . . 9 (𝑁 ∈ Odd → 𝑁 ∈ ℤ)
13 zltp1le 11639 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (7 < 𝑁 ↔ (7 + 1) ≤ 𝑁))
14 7p1e8 11369 . . . . . . . . . . . 12 (7 + 1) = 8
1514breq1i 4811 . . . . . . . . . . 11 ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁)
1615a1i 11 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁))
17 8re 11317 . . . . . . . . . . . 12 8 ∈ ℝ
1817a1i 11 . . . . . . . . . . 11 (7 ∈ ℤ → 8 ∈ ℝ)
19 zre 11593 . . . . . . . . . . 11 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
20 leloe 10336 . . . . . . . . . . 11 ((8 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2118, 19, 20syl2an 495 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2213, 16, 213bitrd 294 . . . . . . . . 9 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2311, 12, 22sylancr 698 . . . . . . . 8 (𝑁 ∈ Odd → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
24 8nn 11403 . . . . . . . . . . . . . . 15 8 ∈ ℕ
2524nnzi 11613 . . . . . . . . . . . . . 14 8 ∈ ℤ
26 zltp1le 11639 . . . . . . . . . . . . . 14 ((8 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁))
2725, 12, 26sylancr 698 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁))
28 8p1e9 11370 . . . . . . . . . . . . . . 15 (8 + 1) = 9
2928breq1i 4811 . . . . . . . . . . . . . 14 ((8 + 1) ≤ 𝑁 ↔ 9 ≤ 𝑁)
3029a1i 11 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → ((8 + 1) ≤ 𝑁 ↔ 9 ≤ 𝑁))
31 9re 11319 . . . . . . . . . . . . . . 15 9 ∈ ℝ
3231a1i 11 . . . . . . . . . . . . . 14 (𝑁 ∈ Odd → 9 ∈ ℝ)
3312zred 11694 . . . . . . . . . . . . . 14 (𝑁 ∈ Odd → 𝑁 ∈ ℝ)
3432, 33leloed 10392 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → (9 ≤ 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁)))
3527, 30, 343bitrd 294 . . . . . . . . . . . 12 (𝑁 ∈ Odd → (8 < 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁)))
36 9nn 11404 . . . . . . . . . . . . . . . . . . 19 9 ∈ ℕ
3736nnzi 11613 . . . . . . . . . . . . . . . . . 18 9 ∈ ℤ
38 zltp1le 11639 . . . . . . . . . . . . . . . . . 18 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁))
3937, 12, 38sylancr 698 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁))
40 9p1e10 11708 . . . . . . . . . . . . . . . . . . 19 (9 + 1) = 10
4140breq1i 4811 . . . . . . . . . . . . . . . . . 18 ((9 + 1) ≤ 𝑁10 ≤ 𝑁)
4241a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → ((9 + 1) ≤ 𝑁10 ≤ 𝑁))
43 10re 11729 . . . . . . . . . . . . . . . . . . 19 10 ∈ ℝ
4443a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ Odd → 10 ∈ ℝ)
4544, 33leloed 10392 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → (10 ≤ 𝑁 ↔ (10 < 𝑁10 = 𝑁)))
4639, 42, 453bitrd 294 . . . . . . . . . . . . . . . 16 (𝑁 ∈ Odd → (9 < 𝑁 ↔ (10 < 𝑁10 = 𝑁)))
47 10nn 11726 . . . . . . . . . . . . . . . . . . . . . . 23 10 ∈ ℕ
4847nnzi 11613 . . . . . . . . . . . . . . . . . . . . . 22 10 ∈ ℤ
49 zltp1le 11639 . . . . . . . . . . . . . . . . . . . . . 22 ((10 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (10 < 𝑁 ↔ (10 + 1) ≤ 𝑁))
5048, 12, 49sylancr 698 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → (10 < 𝑁 ↔ (10 + 1) ≤ 𝑁))
51 dec10p 11765 . . . . . . . . . . . . . . . . . . . . . . 23 (10 + 1) = 11
5251breq1i 4811 . . . . . . . . . . . . . . . . . . . . . 22 ((10 + 1) ≤ 𝑁11 ≤ 𝑁)
5352a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → ((10 + 1) ≤ 𝑁11 ≤ 𝑁))
54 1nn 11243 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℕ
553, 54decnncl 11730 . . . . . . . . . . . . . . . . . . . . . . . 24 11 ∈ ℕ
5655nnrei 11241 . . . . . . . . . . . . . . . . . . . . . . 23 11 ∈ ℝ
5756a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ Odd → 11 ∈ ℝ)
5857, 33leloed 10392 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → (11 ≤ 𝑁 ↔ (11 < 𝑁11 = 𝑁)))
5950, 53, 583bitrd 294 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ Odd → (10 < 𝑁 ↔ (11 < 𝑁11 = 𝑁)))
6055nnzi 11613 . . . . . . . . . . . . . . . . . . . . . . . . . 26 11 ∈ ℤ
61 zltp1le 11639 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((11 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (11 < 𝑁 ↔ (11 + 1) ≤ 𝑁))
6260, 12, 61sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → (11 < 𝑁 ↔ (11 + 1) ≤ 𝑁))
6351eqcomi 2769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 11 = (10 + 1)
6463oveq1i 6824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (11 + 1) = ((10 + 1) + 1)
6547nncni 11242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 10 ∈ ℂ
66 ax-1cn 10206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
6765, 66, 66addassi 10260 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((10 + 1) + 1) = (10 + (1 + 1))
68 1p1e2 11346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 + 1) = 2
6968oveq2i 6825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (10 + (1 + 1)) = (10 + 2)
70 dec10p 11765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (10 + 2) = 12
7169, 70eqtri 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (10 + (1 + 1)) = 12
7264, 67, 713eqtri 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (11 + 1) = 12
7372breq1i 4811 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((11 + 1) ≤ 𝑁12 ≤ 𝑁)
7473a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → ((11 + 1) ≤ 𝑁12 ≤ 𝑁))
75 2nn 11397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℕ
763, 75decnncl 11730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 12 ∈ ℕ
7776nnrei 11241 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 12 ∈ ℝ
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ Odd → 12 ∈ ℝ)
7978, 33leloed 10392 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → (12 ≤ 𝑁 ↔ (12 < 𝑁12 = 𝑁)))
8062, 74, 793bitrd 294 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ Odd → (11 < 𝑁 ↔ (12 < 𝑁12 = 𝑁)))
8176nnzi 11613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 12 ∈ ℤ
82 zltp1le 11639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((12 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (12 < 𝑁 ↔ (12 + 1) ≤ 𝑁))
8381, 12, 82sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → (12 < 𝑁 ↔ (12 + 1) ≤ 𝑁))
8470eqcomi 2769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 12 = (10 + 2)
8584oveq1i 6824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (12 + 1) = ((10 + 2) + 1)
86 2cn 11303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2 ∈ ℂ
8765, 86, 66addassi 10260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((10 + 2) + 1) = (10 + (2 + 1))
88 2p1e3 11363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (2 + 1) = 3
8988oveq2i 6825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (10 + (2 + 1)) = (10 + 3)
90 dec10p 11765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (10 + 3) = 13
9189, 90eqtri 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (10 + (2 + 1)) = 13
9285, 87, 913eqtri 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (12 + 1) = 13
9392breq1i 4811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((12 + 1) ≤ 𝑁13 ≤ 𝑁)
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → ((12 + 1) ≤ 𝑁13 ≤ 𝑁))
956a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ Odd → 13 ∈ ℝ)
9695, 33lenltd 10395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (12 = 𝑁 → (12 ∈ Odd ↔ 𝑁 ∈ Odd ))
102 6p6e12 11814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (6 + 6) = 12
103 6even 42148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 6 ∈ Even
104 epee 42142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((6 ∈ Even ∧ 6 ∈ Even ) → (6 + 6) ∈ Even )
105103, 103, 104mp2an 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (6 + 6) ∈ Even
106102, 105eqeltrri 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 12 ∈ Even
107 evennodd 42084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 42191 . . . . . . . . . . . . . . . . . . . . . . . 24 11 ∈ GoldbachOdd
116 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . 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 2827 . . . . . . . . . . . . . . . . . . 19 (10 = 𝑁 → (10 ∈ Odd ↔ 𝑁 ∈ Odd ))
124 5p5e10 11808 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 5) = 10
125 5odd 42147 . . . . . . . . . . . . . . . . . . . . . . 23 5 ∈ Odd
126 opoeALTV 42122 . . . . . . . . . . . . . . . . . . . . . . 23 ((5 ∈ Odd ∧ 5 ∈ Odd ) → (5 + 5) ∈ Even )
127125, 125, 126mp2an 710 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 5) ∈ Even
128124, 127eqeltrri 2836 . . . . . . . . . . . . . . . . . . . . 21 10 ∈ Even
129 evennodd 42084 . . . . . . . . . . . . . . . . . . . . 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 42190 . . . . . . . . . . . . . . . 16 9 ∈ GoldbachOdd
138 eleq1 2827 . . . . . . . . . . . . . . . 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 2827 . . . . . . . . . . 11 (8 = 𝑁 → (8 ∈ Odd ↔ 𝑁 ∈ Odd ))
146 8even 42150 . . . . . . . . . . . . 13 8 ∈ Even
147 evennodd 42084 . . . . . . . . . . . . 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 1130 . . . 4 ((𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13) → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOdd ))
157156com12 32 . . 3 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → ((𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13) → 𝑁 ∈ GoldbachOdd ))
1589, 157syl5bi 232 . 2 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 ∈ (7[,)13) → 𝑁 ∈ GoldbachOdd ))
1591583impia 1110 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 1072   = wceq 1632  wcel 2139   class class class wbr 4804  (class class class)co 6814  cr 10147  0cc0 10148  1c1 10149   + caddc 10151  *cxr 10285   < clt 10286  cle 10287  2c2 11282  3c3 11283  5c5 11285  6c6 11286  7c7 11287  8c8 11288  9c9 11289  cz 11589  cdc 11705  [,)cico 12390   Even ceven 42065   Odd codd 42066   GoldbachOdd cgbo 42163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-2o 7731  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-sup 8515  df-inf 8516  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-5 11294  df-6 11295  df-7 11296  df-8 11297  df-9 11298  df-n0 11505  df-z 11590  df-dec 11706  df-uz 11900  df-rp 12046  df-ico 12394  df-fz 12540  df-seq 13016  df-exp 13075  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-dvds 15203  df-prm 15608  df-even 42067  df-odd 42068  df-gbo 42166
This theorem is referenced by:  bgoldbtbnd  42225
  Copyright terms: Public domain W3C validator