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 40221
 Description: Lemma 1 for bgoldbtbnd 40225: the odd numbers between 7 and 13 (exclusive) are (strong) odd Goldbach numbers. (Contributed by AV, 29-Jul-2020.)
Assertion
Ref Expression
bgoldbtbndlem1 ((𝑁 ∈ Odd ∧ 7 < 𝑁𝑁 ∈ (7[,)13)) → 𝑁 ∈ GoldbachOddALTV )

Proof of Theorem bgoldbtbndlem1
StepHypRef Expression
1 7re 10980 . . . . 5 7 ∈ ℝ
21rexri 9976 . . . 4 7 ∈ ℝ*
3 1nn0 11185 . . . . . . 7 1 ∈ ℕ0
4 3nn 11063 . . . . . . 7 3 ∈ ℕ
53, 4decnncl 11394 . . . . . 6 13 ∈ ℕ
65nnrei 10906 . . . . 5 13 ∈ ℝ
76rexri 9976 . . . 4 13 ∈ ℝ*
8 elico1 12089 . . . 4 ((7 ∈ ℝ*13 ∈ ℝ*) → (𝑁 ∈ (7[,)13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13)))
92, 7, 8mp2an 704 . . 3 (𝑁 ∈ (7[,)13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13))
10 7nn 11067 . . . . . . . . . 10 7 ∈ ℕ
1110nnzi 11278 . . . . . . . . 9 7 ∈ ℤ
12 oddz 40082 . . . . . . . . 9 (𝑁 ∈ Odd → 𝑁 ∈ ℤ)
13 zltp1le 11304 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (7 < 𝑁 ↔ (7 + 1) ≤ 𝑁))
14 7p1e8 11034 . . . . . . . . . . . 12 (7 + 1) = 8
1514breq1i 4590 . . . . . . . . . . 11 ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁)
1615a1i 11 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁))
17 8re 10982 . . . . . . . . . . . 12 8 ∈ ℝ
1817a1i 11 . . . . . . . . . . 11 (7 ∈ ℤ → 8 ∈ ℝ)
19 zre 11258 . . . . . . . . . . 11 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
20 leloe 10003 . . . . . . . . . . 11 ((8 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2118, 19, 20syl2an 493 . . . . . . . . . 10 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2213, 16, 213bitrd 293 . . . . . . . . 9 ((7 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
2311, 12, 22sylancr 694 . . . . . . . 8 (𝑁 ∈ Odd → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁)))
24 8nn 11068 . . . . . . . . . . . . . . 15 8 ∈ ℕ
2524nnzi 11278 . . . . . . . . . . . . . 14 8 ∈ ℤ
26 zltp1le 11304 . . . . . . . . . . . . . 14 ((8 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁))
2725, 12, 26sylancr 694 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁))
28 8p1e9 11035 . . . . . . . . . . . . . . 15 (8 + 1) = 9
2928breq1i 4590 . . . . . . . . . . . . . 14 ((8 + 1) ≤ 𝑁 ↔ 9 ≤ 𝑁)
3029a1i 11 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → ((8 + 1) ≤ 𝑁 ↔ 9 ≤ 𝑁))
31 9re 10984 . . . . . . . . . . . . . . 15 9 ∈ ℝ
3231a1i 11 . . . . . . . . . . . . . 14 (𝑁 ∈ Odd → 9 ∈ ℝ)
3312zred 11358 . . . . . . . . . . . . . 14 (𝑁 ∈ Odd → 𝑁 ∈ ℝ)
3432, 33leloed 10059 . . . . . . . . . . . . 13 (𝑁 ∈ Odd → (9 ≤ 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁)))
3527, 30, 343bitrd 293 . . . . . . . . . . . 12 (𝑁 ∈ Odd → (8 < 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁)))
36 9nn 11069 . . . . . . . . . . . . . . . . . . 19 9 ∈ ℕ
3736nnzi 11278 . . . . . . . . . . . . . . . . . 18 9 ∈ ℤ
38 zltp1le 11304 . . . . . . . . . . . . . . . . . 18 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁))
3937, 12, 38sylancr 694 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁))
40 9p1e10 11372 . . . . . . . . . . . . . . . . . . 19 (9 + 1) = 10
4140breq1i 4590 . . . . . . . . . . . . . . . . . 18 ((9 + 1) ≤ 𝑁10 ≤ 𝑁)
4241a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → ((9 + 1) ≤ 𝑁10 ≤ 𝑁))
43 10re 11393 . . . . . . . . . . . . . . . . . . 19 10 ∈ ℝ
4443a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ Odd → 10 ∈ ℝ)
4544, 33leloed 10059 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ Odd → (10 ≤ 𝑁 ↔ (10 < 𝑁10 = 𝑁)))
4639, 42, 453bitrd 293 . . . . . . . . . . . . . . . 16 (𝑁 ∈ Odd → (9 < 𝑁 ↔ (10 < 𝑁10 = 𝑁)))
47 10nn 11390 . . . . . . . . . . . . . . . . . . . . . . 23 10 ∈ ℕ
4847nnzi 11278 . . . . . . . . . . . . . . . . . . . . . 22 10 ∈ ℤ
49 zltp1le 11304 . . . . . . . . . . . . . . . . . . . . . 22 ((10 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (10 < 𝑁 ↔ (10 + 1) ≤ 𝑁))
5048, 12, 49sylancr 694 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → (10 < 𝑁 ↔ (10 + 1) ≤ 𝑁))
51 dec10p 11429 . . . . . . . . . . . . . . . . . . . . . . 23 (10 + 1) = 11
5251breq1i 4590 . . . . . . . . . . . . . . . . . . . . . 22 ((10 + 1) ≤ 𝑁11 ≤ 𝑁)
5352a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → ((10 + 1) ≤ 𝑁11 ≤ 𝑁))
54 1nn 10908 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℕ
553, 54decnncl 11394 . . . . . . . . . . . . . . . . . . . . . . . 24 11 ∈ ℕ
5655nnrei 10906 . . . . . . . . . . . . . . . . . . . . . . 23 11 ∈ ℝ
5756a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ Odd → 11 ∈ ℝ)
5857, 33leloed 10059 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ Odd → (11 ≤ 𝑁 ↔ (11 < 𝑁11 = 𝑁)))
5950, 53, 583bitrd 293 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ Odd → (10 < 𝑁 ↔ (11 < 𝑁11 = 𝑁)))
6055nnzi 11278 . . . . . . . . . . . . . . . . . . . . . . . . . 26 11 ∈ ℤ
61 zltp1le 11304 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((11 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (11 < 𝑁 ↔ (11 + 1) ≤ 𝑁))
6260, 12, 61sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → (11 < 𝑁 ↔ (11 + 1) ≤ 𝑁))
6351eqcomi 2619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 11 = (10 + 1)
6463oveq1i 6559 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (11 + 1) = ((10 + 1) + 1)
6547nncni 10907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 10 ∈ ℂ
66 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
6765, 66, 66addassi 9927 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((10 + 1) + 1) = (10 + (1 + 1))
68 1p1e2 11011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 + 1) = 2
6968oveq2i 6560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (10 + (1 + 1)) = (10 + 2)
70 dec10p 11429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (10 + 2) = 12
7169, 70eqtri 2632 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (10 + (1 + 1)) = 12
7264, 67, 713eqtri 2636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (11 + 1) = 12
7372breq1i 4590 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((11 + 1) ≤ 𝑁12 ≤ 𝑁)
7473a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → ((11 + 1) ≤ 𝑁12 ≤ 𝑁))
75 2nn 11062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℕ
763, 75decnncl 11394 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 12 ∈ ℕ
7776nnrei 10906 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 12 ∈ ℝ
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ Odd → 12 ∈ ℝ)
7978, 33leloed 10059 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ Odd → (12 ≤ 𝑁 ↔ (12 < 𝑁12 = 𝑁)))
8062, 74, 793bitrd 293 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ Odd → (11 < 𝑁 ↔ (12 < 𝑁12 = 𝑁)))
8176nnzi 11278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 12 ∈ ℤ
82 zltp1le 11304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((12 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (12 < 𝑁 ↔ (12 + 1) ≤ 𝑁))
8381, 12, 82sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → (12 < 𝑁 ↔ (12 + 1) ≤ 𝑁))
8470eqcomi 2619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 12 = (10 + 2)
8584oveq1i 6559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (12 + 1) = ((10 + 2) + 1)
86 2cn 10968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2 ∈ ℂ
8765, 86, 66addassi 9927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((10 + 2) + 1) = (10 + (2 + 1))
88 2p1e3 11028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (2 + 1) = 3
8988oveq2i 6560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (10 + (2 + 1)) = (10 + 3)
90 dec10p 11429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (10 + 3) = 13
9189, 90eqtri 2632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (10 + (2 + 1)) = 13
9285, 87, 913eqtri 2636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (12 + 1) = 13
9392breq1i 4590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((12 + 1) ≤ 𝑁13 ≤ 𝑁)
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → ((12 + 1) ≤ 𝑁13 ≤ 𝑁))
956a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ Odd → 13 ∈ ℝ)
9695, 33lenltd 10062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ Odd → (13 ≤ 𝑁 ↔ ¬ 𝑁 < 13))
9783, 94, 963bitrd 293 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ Odd → (12 < 𝑁 ↔ ¬ 𝑁 < 13))
98 pm2.21 119 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑁 < 13 → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV ))
9997, 98syl6bi 242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ Odd → (12 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
10099com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (12 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
101 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (12 = 𝑁 → (12 ∈ Odd ↔ 𝑁 ∈ Odd ))
102 6p6e12 11478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (6 + 6) = 12
103 6even 40158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 6 ∈ Even
104 epee 40152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((6 ∈ Even ∧ 6 ∈ Even ) → (6 + 6) ∈ Even )
105103, 103, 104mp2an 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (6 + 6) ∈ Even
106102, 105eqeltrri 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 12 ∈ Even
107 evennodd 40094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (12 ∈ Even → ¬ 12 ∈ Odd )
108106, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ¬ 12 ∈ Odd
109108pm2.21i 115 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (12 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV ))
110101, 109syl6bir 243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (12 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
111100, 110jaoi 393 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((12 < 𝑁12 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
112111com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ Odd → ((12 < 𝑁12 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
11380, 112sylbid 229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ Odd → (11 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
114113com12 32 . . . . . . . . . . . . . . . . . . . . . 22 (11 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
115 11gboa 40197 . . . . . . . . . . . . . . . . . . . . . . . 24 11 ∈ GoldbachOddALTV
116 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . 24 (11 = 𝑁 → (11 ∈ GoldbachOddALTV ↔ 𝑁 ∈ GoldbachOddALTV ))
117115, 116mpbii 222 . . . . . . . . . . . . . . . . . . . . . . 23 (11 = 𝑁𝑁 ∈ GoldbachOddALTV )
1181172a1d 26 . . . . . . . . . . . . . . . . . . . . . 22 (11 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
119114, 118jaoi 393 . . . . . . . . . . . . . . . . . . . . 21 ((11 < 𝑁11 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
120119com12 32 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ Odd → ((11 < 𝑁11 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
12159, 120sylbid 229 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ Odd → (10 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
122121com12 32 . . . . . . . . . . . . . . . . . 18 (10 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
123 eleq1 2676 . . . . . . . . . . . . . . . . . . 19 (10 = 𝑁 → (10 ∈ Odd ↔ 𝑁 ∈ Odd ))
124 5p5e10 11472 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 5) = 10
125 5odd 40157 . . . . . . . . . . . . . . . . . . . . . . 23 5 ∈ Odd
126 opoeALTV 40132 . . . . . . . . . . . . . . . . . . . . . . 23 ((5 ∈ Odd ∧ 5 ∈ Odd ) → (5 + 5) ∈ Even )
127125, 125, 126mp2an 704 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 5) ∈ Even
128124, 127eqeltrri 2685 . . . . . . . . . . . . . . . . . . . . 21 10 ∈ Even
129 evennodd 40094 . . . . . . . . . . . . . . . . . . . . 21 (10 ∈ Even → ¬ 10 ∈ Odd )
130128, 129ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ¬ 10 ∈ Odd
131130pm2.21i 115 . . . . . . . . . . . . . . . . . . 19 (10 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV ))
132123, 131syl6bir 243 . . . . . . . . . . . . . . . . . 18 (10 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
133122, 132jaoi 393 . . . . . . . . . . . . . . . . 17 ((10 < 𝑁10 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
134133com12 32 . . . . . . . . . . . . . . . 16 (𝑁 ∈ Odd → ((10 < 𝑁10 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
13546, 134sylbid 229 . . . . . . . . . . . . . . 15 (𝑁 ∈ Odd → (9 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
136135com12 32 . . . . . . . . . . . . . 14 (9 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
137 9gboa 40196 . . . . . . . . . . . . . . . 16 9 ∈ GoldbachOddALTV
138 eleq1 2676 . . . . . . . . . . . . . . . 16 (9 = 𝑁 → (9 ∈ GoldbachOddALTV ↔ 𝑁 ∈ GoldbachOddALTV ))
139137, 138mpbii 222 . . . . . . . . . . . . . . 15 (9 = 𝑁𝑁 ∈ GoldbachOddALTV )
1401392a1d 26 . . . . . . . . . . . . . 14 (9 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
141136, 140jaoi 393 . . . . . . . . . . . . 13 ((9 < 𝑁 ∨ 9 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
142141com12 32 . . . . . . . . . . . 12 (𝑁 ∈ Odd → ((9 < 𝑁 ∨ 9 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
14335, 142sylbid 229 . . . . . . . . . . 11 (𝑁 ∈ Odd → (8 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
144143com12 32 . . . . . . . . . 10 (8 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
145 eleq1 2676 . . . . . . . . . . 11 (8 = 𝑁 → (8 ∈ Odd ↔ 𝑁 ∈ Odd ))
146 8even 40160 . . . . . . . . . . . . 13 8 ∈ Even
147 evennodd 40094 . . . . . . . . . . . . 13 (8 ∈ Even → ¬ 8 ∈ Odd )
148146, 147ax-mp 5 . . . . . . . . . . . 12 ¬ 8 ∈ Odd
149148pm2.21i 115 . . . . . . . . . . 11 (8 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV ))
150145, 149syl6bir 243 . . . . . . . . . 10 (8 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
151144, 150jaoi 393 . . . . . . . . 9 ((8 < 𝑁 ∨ 8 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
152151com12 32 . . . . . . . 8 (𝑁 ∈ Odd → ((8 < 𝑁 ∨ 8 = 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
15323, 152sylbid 229 . . . . . . 7 (𝑁 ∈ Odd → (7 < 𝑁 → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV )))
154153imp 444 . . . . . 6 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 < 13 → 𝑁 ∈ GoldbachOddALTV ))
155154com12 32 . . . . 5 (𝑁 < 13 → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOddALTV ))
1561553ad2ant3 1077 . . . 4 ((𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13) → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOddALTV ))
157156com12 32 . . 3 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → ((𝑁 ∈ ℝ* ∧ 7 ≤ 𝑁𝑁 < 13) → 𝑁 ∈ GoldbachOddALTV ))
1589, 157syl5bi 231 . 2 ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 ∈ (7[,)13) → 𝑁 ∈ GoldbachOddALTV ))
1591583impia 1253 1 ((𝑁 ∈ Odd ∧ 7 < 𝑁𝑁 ∈ (7[,)13)) → 𝑁 ∈ GoldbachOddALTV )
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   class class class wbr 4583  (class class class)co 6549  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818  ℝ*cxr 9952   < clt 9953   ≤ cle 9954  2c2 10947  3c3 10948  5c5 10950  6c6 10951  7c7 10952  8c8 10953  9c9 10954  ℤcz 11254  ;cdc 11369  [,)cico 12048   Even ceven 40075   Odd codd 40076   GoldbachOddALTV cgboa 40169 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-ico 12052  df-fz 12198  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-dvds 14822  df-prm 15224  df-even 40077  df-odd 40078  df-gboa 40172 This theorem is referenced by:  bgoldbtbnd  40225
 Copyright terms: Public domain W3C validator