Proof of Theorem bgoldbtbndlem1
| Step | Hyp | Ref
| Expression |
| 1 | | 7re 12359 |
. . . . 5
⊢ 7 ∈
ℝ |
| 2 | 1 | rexri 11319 |
. . . 4
⊢ 7 ∈
ℝ* |
| 3 | | 1nn0 12542 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
| 4 | | 3nn 12345 |
. . . . . . 7
⊢ 3 ∈
ℕ |
| 5 | 3, 4 | decnncl 12753 |
. . . . . 6
⊢ ;13 ∈ ℕ |
| 6 | 5 | nnrei 12275 |
. . . . 5
⊢ ;13 ∈ ℝ |
| 7 | 6 | rexri 11319 |
. . . 4
⊢ ;13 ∈
ℝ* |
| 8 | | elico1 13430 |
. . . 4
⊢ ((7
∈ ℝ* ∧ ;13 ∈ ℝ*) → (𝑁 ∈ (7[,);13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤
𝑁 ∧ 𝑁 < ;13))) |
| 9 | 2, 7, 8 | mp2an 692 |
. . 3
⊢ (𝑁 ∈ (7[,);13) ↔ (𝑁 ∈ ℝ* ∧ 7 ≤
𝑁 ∧ 𝑁 < ;13)) |
| 10 | | 7nn 12358 |
. . . . . . . . . 10
⊢ 7 ∈
ℕ |
| 11 | 10 | nnzi 12641 |
. . . . . . . . 9
⊢ 7 ∈
ℤ |
| 12 | | oddz 47618 |
. . . . . . . . 9
⊢ (𝑁 ∈ Odd → 𝑁 ∈
ℤ) |
| 13 | | zltp1le 12667 |
. . . . . . . . . 10
⊢ ((7
∈ ℤ ∧ 𝑁
∈ ℤ) → (7 < 𝑁 ↔ (7 + 1) ≤ 𝑁)) |
| 14 | | 7p1e8 12415 |
. . . . . . . . . . . 12
⊢ (7 + 1) =
8 |
| 15 | 14 | breq1i 5150 |
. . . . . . . . . . 11
⊢ ((7 + 1)
≤ 𝑁 ↔ 8 ≤ 𝑁) |
| 16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ ((7
∈ ℤ ∧ 𝑁
∈ ℤ) → ((7 + 1) ≤ 𝑁 ↔ 8 ≤ 𝑁)) |
| 17 | | 8re 12362 |
. . . . . . . . . . . 12
⊢ 8 ∈
ℝ |
| 18 | 17 | a1i 11 |
. . . . . . . . . . 11
⊢ (7 ∈
ℤ → 8 ∈ ℝ) |
| 19 | | zre 12617 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
| 20 | | leloe 11347 |
. . . . . . . . . . 11
⊢ ((8
∈ ℝ ∧ 𝑁
∈ ℝ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁))) |
| 21 | 18, 19, 20 | syl2an 596 |
. . . . . . . . . 10
⊢ ((7
∈ ℤ ∧ 𝑁
∈ ℤ) → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁))) |
| 22 | 13, 16, 21 | 3bitrd 305 |
. . . . . . . . 9
⊢ ((7
∈ ℤ ∧ 𝑁
∈ ℤ) → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁))) |
| 23 | 11, 12, 22 | sylancr 587 |
. . . . . . . 8
⊢ (𝑁 ∈ Odd → (7 < 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁))) |
| 24 | | 8nn 12361 |
. . . . . . . . . . . . . . 15
⊢ 8 ∈
ℕ |
| 25 | 24 | nnzi 12641 |
. . . . . . . . . . . . . 14
⊢ 8 ∈
ℤ |
| 26 | | zltp1le 12667 |
. . . . . . . . . . . . . 14
⊢ ((8
∈ ℤ ∧ 𝑁
∈ ℤ) → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁)) |
| 27 | 25, 12, 26 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ Odd → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁)) |
| 28 | | 8p1e9 12416 |
. . . . . . . . . . . . . . 15
⊢ (8 + 1) =
9 |
| 29 | 28 | breq1i 5150 |
. . . . . . . . . . . . . 14
⊢ ((8 + 1)
≤ 𝑁 ↔ 9 ≤ 𝑁) |
| 30 | 29 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ Odd → ((8 + 1) ≤
𝑁 ↔ 9 ≤ 𝑁)) |
| 31 | | 9re 12365 |
. . . . . . . . . . . . . . 15
⊢ 9 ∈
ℝ |
| 32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ Odd → 9 ∈
ℝ) |
| 33 | 12 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ Odd → 𝑁 ∈
ℝ) |
| 34 | 32, 33 | leloed 11404 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ Odd → (9 ≤ 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁))) |
| 35 | 27, 30, 34 | 3bitrd 305 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ Odd → (8 < 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁))) |
| 36 | | 9nn 12364 |
. . . . . . . . . . . . . . . . . . 19
⊢ 9 ∈
ℕ |
| 37 | 36 | nnzi 12641 |
. . . . . . . . . . . . . . . . . 18
⊢ 9 ∈
ℤ |
| 38 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . . 18
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ) → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁)) |
| 39 | 37, 12, 38 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ Odd → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁)) |
| 40 | | 9p1e10 12735 |
. . . . . . . . . . . . . . . . . . 19
⊢ (9 + 1) =
;10 |
| 41 | 40 | breq1i 5150 |
. . . . . . . . . . . . . . . . . 18
⊢ ((9 + 1)
≤ 𝑁 ↔ ;10 ≤ 𝑁) |
| 42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ Odd → ((9 + 1) ≤
𝑁 ↔ ;10 ≤ 𝑁)) |
| 43 | | 10re 12752 |
. . . . . . . . . . . . . . . . . . 19
⊢ ;10 ∈ ℝ |
| 44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ Odd → ;10 ∈ ℝ) |
| 45 | 44, 33 | leloed 11404 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ Odd → (;10 ≤ 𝑁 ↔ (;10 < 𝑁 ∨ ;10 = 𝑁))) |
| 46 | 39, 42, 45 | 3bitrd 305 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ Odd → (9 < 𝑁 ↔ (;10 < 𝑁 ∨ ;10 = 𝑁))) |
| 47 | | 10nn 12749 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ;10 ∈ ℕ |
| 48 | 47 | nnzi 12641 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ;10 ∈ ℤ |
| 49 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((;10 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (;10 < 𝑁 ↔ (;10 + 1) ≤ 𝑁)) |
| 50 | 48, 12, 49 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ Odd → (;10 < 𝑁 ↔ (;10 + 1) ≤ 𝑁)) |
| 51 | | dec10p 12776 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (;10 + 1) = ;11 |
| 52 | 51 | breq1i 5150 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((;10 + 1) ≤ 𝑁 ↔ ;11 ≤ 𝑁) |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ Odd → ((;10 + 1) ≤ 𝑁 ↔ ;11 ≤ 𝑁)) |
| 54 | | 1nn 12277 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℕ |
| 55 | 3, 54 | decnncl 12753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ;11 ∈ ℕ |
| 56 | 55 | nnrei 12275 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ;11 ∈ ℝ |
| 57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ Odd → ;11 ∈ ℝ) |
| 58 | 57, 33 | leloed 11404 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ Odd → (;11 ≤ 𝑁 ↔ (;11 < 𝑁 ∨ ;11 = 𝑁))) |
| 59 | 50, 53, 58 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ Odd → (;10 < 𝑁 ↔ (;11 < 𝑁 ∨ ;11 = 𝑁))) |
| 60 | 55 | nnzi 12641 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ;11 ∈ ℤ |
| 61 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((;11 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (;11 < 𝑁 ↔ (;11 + 1) ≤ 𝑁)) |
| 62 | 60, 12, 61 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ Odd → (;11 < 𝑁 ↔ (;11 + 1) ≤ 𝑁)) |
| 63 | 51 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ;11 = (;10 + 1) |
| 64 | 63 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (;11 + 1) = ((;10 + 1) + 1) |
| 65 | 47 | nncni 12276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ;10 ∈ ℂ |
| 66 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℂ |
| 67 | 65, 66, 66 | addassi 11271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((;10 + 1) + 1) = (;10 + (1 + 1)) |
| 68 | | 1p1e2 12391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (1 + 1) =
2 |
| 69 | 68 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (;10 + (1 + 1)) = (;10 + 2) |
| 70 | | dec10p 12776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (;10 + 2) = ;12 |
| 71 | 69, 70 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (;10 + (1 + 1)) = ;12 |
| 72 | 64, 67, 71 | 3eqtri 2769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (;11 + 1) = ;12 |
| 73 | 72 | breq1i 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((;11 + 1) ≤ 𝑁 ↔ ;12 ≤ 𝑁) |
| 74 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ Odd → ((;11 + 1) ≤ 𝑁 ↔ ;12 ≤ 𝑁)) |
| 75 | | 2nn 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℕ |
| 76 | 3, 75 | decnncl 12753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ;12 ∈ ℕ |
| 77 | 76 | nnrei 12275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ;12 ∈ ℝ |
| 78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ Odd → ;12 ∈ ℝ) |
| 79 | 78, 33 | leloed 11404 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ Odd → (;12 ≤ 𝑁 ↔ (;12 < 𝑁 ∨ ;12 = 𝑁))) |
| 80 | 62, 74, 79 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ Odd → (;11 < 𝑁 ↔ (;12 < 𝑁 ∨ ;12 = 𝑁))) |
| 81 | 76 | nnzi 12641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ;12 ∈ ℤ |
| 82 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((;12 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (;12 < 𝑁 ↔ (;12 + 1) ≤ 𝑁)) |
| 83 | 81, 12, 82 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ Odd → (;12 < 𝑁 ↔ (;12 + 1) ≤ 𝑁)) |
| 84 | 70 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ;12 = (;10 + 2) |
| 85 | 84 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (;12 + 1) = ((;10 + 2) + 1) |
| 86 | | 2cn 12341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 2 ∈
ℂ |
| 87 | 65, 86, 66 | addassi 11271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((;10 + 2) + 1) = (;10 + (2 + 1)) |
| 88 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (2 + 1) =
3 |
| 89 | 88 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (;10 + (2 + 1)) = (;10 + 3) |
| 90 | | dec10p 12776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (;10 + 3) = ;13 |
| 91 | 89, 90 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (;10 + (2 + 1)) = ;13 |
| 92 | 85, 87, 91 | 3eqtri 2769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (;12 + 1) = ;13 |
| 93 | 92 | breq1i 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((;12 + 1) ≤ 𝑁 ↔ ;13 ≤ 𝑁) |
| 94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ Odd → ((;12 + 1) ≤ 𝑁 ↔ ;13 ≤ 𝑁)) |
| 95 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ Odd → ;13 ∈ ℝ) |
| 96 | 95, 33 | lenltd 11407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ Odd → (;13 ≤ 𝑁 ↔ ¬ 𝑁 < ;13)) |
| 97 | 83, 94, 96 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ Odd → (;12 < 𝑁 ↔ ¬ 𝑁 < ;13)) |
| 98 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
𝑁 < ;13 → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd )) |
| 99 | 97, 98 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ Odd → (;12 < 𝑁 → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 100 | 99 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (;12 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 101 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (;12 = 𝑁 → (;12 ∈ Odd ↔ 𝑁 ∈ Odd )) |
| 102 | | 6p6e12 12807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (6 + 6) =
;12 |
| 103 | | 6even 47698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 6 ∈
Even |
| 104 | | epee 47692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((6
∈ Even ∧ 6 ∈ Even ) → (6 + 6) ∈ Even ) |
| 105 | 103, 103,
104 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (6 + 6)
∈ Even |
| 106 | 102, 105 | eqeltrri 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ;12 ∈ Even |
| 107 | | evennodd 47630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (;12 ∈ Even → ¬ ;12 ∈ Odd ) |
| 108 | 106, 107 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ¬
;12 ∈ Odd |
| 109 | 108 | pm2.21i 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (;12 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd )) |
| 110 | 101, 109 | biimtrrdi 254 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (;12 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 111 | 100, 110 | jaoi 858 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((;12 < 𝑁 ∨ ;12 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 112 | 111 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ Odd → ((;12 < 𝑁 ∨ ;12 = 𝑁) → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 113 | 80, 112 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ Odd → (;11 < 𝑁 → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 114 | 113 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (;11 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 115 | | 11gbo 47762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ;11 ∈ GoldbachOdd |
| 116 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (;11 = 𝑁 → (;11 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd )) |
| 117 | 115, 116 | mpbii 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (;11 = 𝑁 → 𝑁 ∈ GoldbachOdd ) |
| 118 | 117 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (;11 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 119 | 114, 118 | jaoi 858 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((;11 < 𝑁 ∨ ;11 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 120 | 119 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ Odd → ((;11 < 𝑁 ∨ ;11 = 𝑁) → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 121 | 59, 120 | sylbid 240 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ Odd → (;10 < 𝑁 → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 122 | 121 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (;10 < 𝑁 → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 123 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . 19
⊢ (;10 = 𝑁 → (;10 ∈ Odd ↔ 𝑁 ∈ Odd )) |
| 124 | | 5p5e10 12804 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (5 + 5) =
;10 |
| 125 | | 5odd 47697 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 5 ∈
Odd |
| 126 | | opoeALTV 47670 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((5
∈ Odd ∧ 5 ∈ Odd ) → (5 + 5) ∈ Even ) |
| 127 | 125, 125,
126 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (5 + 5)
∈ Even |
| 128 | 124, 127 | eqeltrri 2838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ;10 ∈ Even |
| 129 | | evennodd 47630 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (;10 ∈ Even → ¬ ;10 ∈ Odd ) |
| 130 | 128, 129 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ¬
;10 ∈ Odd |
| 131 | 130 | pm2.21i 119 |
. . . . . . . . . . . . . . . . . . 19
⊢ (;10 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd )) |
| 132 | 123, 131 | biimtrrdi 254 |
. . . . . . . . . . . . . . . . . 18
⊢ (;10 = 𝑁 → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 133 | 122, 132 | jaoi 858 |
. . . . . . . . . . . . . . . . 17
⊢ ((;10 < 𝑁 ∨ ;10 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 134 | 133 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ Odd → ((;10 < 𝑁 ∨ ;10 = 𝑁) → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 135 | 46, 134 | sylbid 240 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ Odd → (9 < 𝑁 → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 136 | 135 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (9 <
𝑁 → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 137 | | 9gbo 47761 |
. . . . . . . . . . . . . . . 16
⊢ 9 ∈
GoldbachOdd |
| 138 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢ (9 =
𝑁 → (9 ∈
GoldbachOdd ↔ 𝑁 ∈
GoldbachOdd )) |
| 139 | 137, 138 | mpbii 233 |
. . . . . . . . . . . . . . 15
⊢ (9 =
𝑁 → 𝑁 ∈ GoldbachOdd ) |
| 140 | 139 | 2a1d 26 |
. . . . . . . . . . . . . 14
⊢ (9 =
𝑁 → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 141 | 136, 140 | jaoi 858 |
. . . . . . . . . . . . 13
⊢ ((9 <
𝑁 ∨ 9 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 142 | 141 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ Odd → ((9 <
𝑁 ∨ 9 = 𝑁) → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 143 | 35, 142 | sylbid 240 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ Odd → (8 < 𝑁 → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 144 | 143 | com12 32 |
. . . . . . . . . 10
⊢ (8 <
𝑁 → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 145 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (8 =
𝑁 → (8 ∈ Odd
↔ 𝑁 ∈ Odd
)) |
| 146 | | 8even 47700 |
. . . . . . . . . . . . 13
⊢ 8 ∈
Even |
| 147 | | evennodd 47630 |
. . . . . . . . . . . . 13
⊢ (8 ∈
Even → ¬ 8 ∈ Odd ) |
| 148 | 146, 147 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ¬ 8
∈ Odd |
| 149 | 148 | pm2.21i 119 |
. . . . . . . . . . 11
⊢ (8 ∈
Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd )) |
| 150 | 145, 149 | biimtrrdi 254 |
. . . . . . . . . 10
⊢ (8 =
𝑁 → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 151 | 144, 150 | jaoi 858 |
. . . . . . . . 9
⊢ ((8 <
𝑁 ∨ 8 = 𝑁) → (𝑁 ∈ Odd → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 152 | 151 | com12 32 |
. . . . . . . 8
⊢ (𝑁 ∈ Odd → ((8 <
𝑁 ∨ 8 = 𝑁) → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 153 | 23, 152 | sylbid 240 |
. . . . . . 7
⊢ (𝑁 ∈ Odd → (7 < 𝑁 → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd ))) |
| 154 | 153 | imp 406 |
. . . . . 6
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 < ;13 → 𝑁 ∈ GoldbachOdd )) |
| 155 | 154 | com12 32 |
. . . . 5
⊢ (𝑁 < ;13 → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOdd )) |
| 156 | 155 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝑁 ∈ ℝ*
∧ 7 ≤ 𝑁 ∧ 𝑁 < ;13) → ((𝑁 ∈ Odd ∧ 7 < 𝑁) → 𝑁 ∈ GoldbachOdd )) |
| 157 | 156 | com12 32 |
. . 3
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁) → ((𝑁 ∈ ℝ* ∧ 7 ≤
𝑁 ∧ 𝑁 < ;13) → 𝑁 ∈ GoldbachOdd )) |
| 158 | 9, 157 | biimtrid 242 |
. 2
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁) → (𝑁 ∈ (7[,);13) → 𝑁 ∈ GoldbachOdd )) |
| 159 | 158 | 3impia 1118 |
1
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 ∈ (7[,);13)) → 𝑁 ∈ GoldbachOdd ) |