Proof of Theorem stgoldbwt
| Step | Hyp | Ref
| Expression |
| 1 | | pm3.35 803 |
. . . . . 6
⊢ ((7 <
𝑛 ∧ (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )) → 𝑛 ∈ GoldbachOdd
) |
| 2 | | gbogbow 47743 |
. . . . . . 7
⊢ (𝑛 ∈ GoldbachOdd → 𝑛 ∈ GoldbachOddW
) |
| 3 | 2 | a1d 25 |
. . . . . 6
⊢ (𝑛 ∈ GoldbachOdd → (5
< 𝑛 → 𝑛 ∈ GoldbachOddW
)) |
| 4 | 1, 3 | syl 17 |
. . . . 5
⊢ ((7 <
𝑛 ∧ (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )) → (5 < 𝑛 → 𝑛 ∈ GoldbachOddW )) |
| 5 | 4 | ex 412 |
. . . 4
⊢ (7 <
𝑛 → ((7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → (5 < 𝑛 → 𝑛 ∈ GoldbachOddW ))) |
| 6 | 5 | a1d 25 |
. . 3
⊢ (7 <
𝑛 → (𝑛 ∈ Odd → ((7 <
𝑛 → 𝑛 ∈ GoldbachOdd ) → (5 < 𝑛 → 𝑛 ∈ GoldbachOddW )))) |
| 7 | | oddz 47618 |
. . . . . . . 8
⊢ (𝑛 ∈ Odd → 𝑛 ∈
ℤ) |
| 8 | 7 | zred 12722 |
. . . . . . 7
⊢ (𝑛 ∈ Odd → 𝑛 ∈
ℝ) |
| 9 | | 7re 12359 |
. . . . . . . 8
⊢ 7 ∈
ℝ |
| 10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝑛 ∈ Odd → 7 ∈
ℝ) |
| 11 | 8, 10 | lenltd 11407 |
. . . . . 6
⊢ (𝑛 ∈ Odd → (𝑛 ≤ 7 ↔ ¬ 7 <
𝑛)) |
| 12 | 8, 10 | leloed 11404 |
. . . . . . . 8
⊢ (𝑛 ∈ Odd → (𝑛 ≤ 7 ↔ (𝑛 < 7 ∨ 𝑛 = 7))) |
| 13 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ Odd ∧ 5 < 𝑛) → 𝑛 ∈ ℤ) |
| 14 | | 6nn 12355 |
. . . . . . . . . . . . . . . . 17
⊢ 6 ∈
ℕ |
| 15 | 14 | nnzi 12641 |
. . . . . . . . . . . . . . . 16
⊢ 6 ∈
ℤ |
| 16 | 13, 15 | jctir 520 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ Odd ∧ 5 < 𝑛) → (𝑛 ∈ ℤ ∧ 6 ∈
ℤ)) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 < 7 ∧ (𝑛 ∈ Odd ∧ 5 < 𝑛)) → (𝑛 ∈ ℤ ∧ 6 ∈
ℤ)) |
| 18 | | df-7 12334 |
. . . . . . . . . . . . . . . . 17
⊢ 7 = (6 +
1) |
| 19 | 18 | breq2i 5151 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 < 7 ↔ 𝑛 < (6 + 1)) |
| 20 | 19 | biimpi 216 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 < 7 → 𝑛 < (6 + 1)) |
| 21 | | df-6 12333 |
. . . . . . . . . . . . . . . 16
⊢ 6 = (5 +
1) |
| 22 | | 5nn 12352 |
. . . . . . . . . . . . . . . . . . 19
⊢ 5 ∈
ℕ |
| 23 | 22 | nnzi 12641 |
. . . . . . . . . . . . . . . . . 18
⊢ 5 ∈
ℤ |
| 24 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . . 18
⊢ ((5
∈ ℤ ∧ 𝑛
∈ ℤ) → (5 < 𝑛 ↔ (5 + 1) ≤ 𝑛)) |
| 25 | 23, 7, 24 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ Odd → (5 < 𝑛 ↔ (5 + 1) ≤ 𝑛)) |
| 26 | 25 | biimpa 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ Odd ∧ 5 < 𝑛) → (5 + 1) ≤ 𝑛) |
| 27 | 21, 26 | eqbrtrid 5178 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ Odd ∧ 5 < 𝑛) → 6 ≤ 𝑛) |
| 28 | 20, 27 | anim12ci 614 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 < 7 ∧ (𝑛 ∈ Odd ∧ 5 < 𝑛)) → (6 ≤ 𝑛 ∧ 𝑛 < (6 + 1))) |
| 29 | | zgeltp1eq 47321 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℤ ∧ 6 ∈
ℤ) → ((6 ≤ 𝑛
∧ 𝑛 < (6 + 1))
→ 𝑛 =
6)) |
| 30 | 17, 28, 29 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((𝑛 < 7 ∧ (𝑛 ∈ Odd ∧ 5 < 𝑛)) → 𝑛 = 6) |
| 31 | 30 | orcd 874 |
. . . . . . . . . . . 12
⊢ ((𝑛 < 7 ∧ (𝑛 ∈ Odd ∧ 5 < 𝑛)) → (𝑛 = 6 ∨ 𝑛 = 7)) |
| 32 | 31 | ex 412 |
. . . . . . . . . . 11
⊢ (𝑛 < 7 → ((𝑛 ∈ Odd ∧ 5 < 𝑛) → (𝑛 = 6 ∨ 𝑛 = 7))) |
| 33 | | olc 869 |
. . . . . . . . . . . 12
⊢ (𝑛 = 7 → (𝑛 = 6 ∨ 𝑛 = 7)) |
| 34 | 33 | a1d 25 |
. . . . . . . . . . 11
⊢ (𝑛 = 7 → ((𝑛 ∈ Odd ∧ 5 < 𝑛) → (𝑛 = 6 ∨ 𝑛 = 7))) |
| 35 | 32, 34 | jaoi 858 |
. . . . . . . . . 10
⊢ ((𝑛 < 7 ∨ 𝑛 = 7) → ((𝑛 ∈ Odd ∧ 5 < 𝑛) → (𝑛 = 6 ∨ 𝑛 = 7))) |
| 36 | 35 | expd 415 |
. . . . . . . . 9
⊢ ((𝑛 < 7 ∨ 𝑛 = 7) → (𝑛 ∈ Odd → (5 < 𝑛 → (𝑛 = 6 ∨ 𝑛 = 7)))) |
| 37 | 36 | com12 32 |
. . . . . . . 8
⊢ (𝑛 ∈ Odd → ((𝑛 < 7 ∨ 𝑛 = 7) → (5 < 𝑛 → (𝑛 = 6 ∨ 𝑛 = 7)))) |
| 38 | 12, 37 | sylbid 240 |
. . . . . . 7
⊢ (𝑛 ∈ Odd → (𝑛 ≤ 7 → (5 < 𝑛 → (𝑛 = 6 ∨ 𝑛 = 7)))) |
| 39 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑛 = 6 → (𝑛 ∈ Odd ↔ 6 ∈ Odd
)) |
| 40 | | 6even 47698 |
. . . . . . . . . . 11
⊢ 6 ∈
Even |
| 41 | | evennodd 47630 |
. . . . . . . . . . . 12
⊢ (6 ∈
Even → ¬ 6 ∈ Odd ) |
| 42 | 41 | pm2.21d 121 |
. . . . . . . . . . 11
⊢ (6 ∈
Even → (6 ∈ Odd → 𝑛 ∈ GoldbachOddW )) |
| 43 | 40, 42 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝑛 = 6 → (6 ∈ Odd →
𝑛 ∈ GoldbachOddW
)) |
| 44 | 39, 43 | sylbid 240 |
. . . . . . . . 9
⊢ (𝑛 = 6 → (𝑛 ∈ Odd → 𝑛 ∈ GoldbachOddW )) |
| 45 | | 7gbow 47759 |
. . . . . . . . . . 11
⊢ 7 ∈
GoldbachOddW |
| 46 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑛 = 7 → (𝑛 ∈ GoldbachOddW ↔ 7 ∈
GoldbachOddW )) |
| 47 | 45, 46 | mpbiri 258 |
. . . . . . . . . 10
⊢ (𝑛 = 7 → 𝑛 ∈ GoldbachOddW ) |
| 48 | 47 | a1d 25 |
. . . . . . . . 9
⊢ (𝑛 = 7 → (𝑛 ∈ Odd → 𝑛 ∈ GoldbachOddW )) |
| 49 | 44, 48 | jaoi 858 |
. . . . . . . 8
⊢ ((𝑛 = 6 ∨ 𝑛 = 7) → (𝑛 ∈ Odd → 𝑛 ∈ GoldbachOddW )) |
| 50 | 49 | com12 32 |
. . . . . . 7
⊢ (𝑛 ∈ Odd → ((𝑛 = 6 ∨ 𝑛 = 7) → 𝑛 ∈ GoldbachOddW )) |
| 51 | 38, 50 | syl6d 75 |
. . . . . 6
⊢ (𝑛 ∈ Odd → (𝑛 ≤ 7 → (5 < 𝑛 → 𝑛 ∈ GoldbachOddW ))) |
| 52 | 11, 51 | sylbird 260 |
. . . . 5
⊢ (𝑛 ∈ Odd → (¬ 7 <
𝑛 → (5 < 𝑛 → 𝑛 ∈ GoldbachOddW ))) |
| 53 | 52 | com12 32 |
. . . 4
⊢ (¬ 7
< 𝑛 → (𝑛 ∈ Odd → (5 < 𝑛 → 𝑛 ∈ GoldbachOddW ))) |
| 54 | 53 | a1dd 50 |
. . 3
⊢ (¬ 7
< 𝑛 → (𝑛 ∈ Odd → ((7 <
𝑛 → 𝑛 ∈ GoldbachOdd ) → (5 < 𝑛 → 𝑛 ∈ GoldbachOddW )))) |
| 55 | 6, 54 | pm2.61i 182 |
. 2
⊢ (𝑛 ∈ Odd → ((7 <
𝑛 → 𝑛 ∈ GoldbachOdd ) → (5 < 𝑛 → 𝑛 ∈ GoldbachOddW ))) |
| 56 | 55 | ralimia 3080 |
1
⊢
(∀𝑛 ∈
Odd (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) →
∀𝑛 ∈ Odd (5
< 𝑛 → 𝑛 ∈ GoldbachOddW
)) |