Proof of Theorem stgoldbwt
Step | Hyp | Ref
| Expression |
1 | | pm3.35 609 |
. . . . . 6
⊢ ((7 <
𝑛 ∧ (7 < 𝑛 → 𝑛 ∈ GoldbachOddALTV )) → 𝑛 ∈ GoldbachOddALTV
) |
2 | | gboagbo 40178 |
. . . . . . 7
⊢ (𝑛 ∈ GoldbachOddALTV →
𝑛 ∈ GoldbachOdd
) |
3 | 2 | a1d 25 |
. . . . . 6
⊢ (𝑛 ∈ GoldbachOddALTV →
(5 < 𝑛 → 𝑛 ∈ GoldbachOdd
)) |
4 | 1, 3 | syl 17 |
. . . . 5
⊢ ((7 <
𝑛 ∧ (7 < 𝑛 → 𝑛 ∈ GoldbachOddALTV )) → (5 <
𝑛 → 𝑛 ∈ GoldbachOdd )) |
5 | 4 | ex 449 |
. . . 4
⊢ (7 <
𝑛 → ((7 < 𝑛 → 𝑛 ∈ GoldbachOddALTV ) → (5 <
𝑛 → 𝑛 ∈ GoldbachOdd ))) |
6 | 5 | a1d 25 |
. . 3
⊢ (7 <
𝑛 → (𝑛 ∈ Odd → ((7 <
𝑛 → 𝑛 ∈ GoldbachOddALTV ) → (5 <
𝑛 → 𝑛 ∈ GoldbachOdd )))) |
7 | | oddz 40082 |
. . . . . . . 8
⊢ (𝑛 ∈ Odd → 𝑛 ∈
ℤ) |
8 | 7 | zred 11358 |
. . . . . . 7
⊢ (𝑛 ∈ Odd → 𝑛 ∈
ℝ) |
9 | | 7re 10980 |
. . . . . . . 8
⊢ 7 ∈
ℝ |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝑛 ∈ Odd → 7 ∈
ℝ) |
11 | 8, 10 | lenltd 10062 |
. . . . . 6
⊢ (𝑛 ∈ Odd → (𝑛 ≤ 7 ↔ ¬ 7 <
𝑛)) |
12 | 8, 10 | leloed 10059 |
. . . . . . . 8
⊢ (𝑛 ∈ Odd → (𝑛 ≤ 7 ↔ (𝑛 < 7 ∨ 𝑛 = 7))) |
13 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ Odd ∧ 5 < 𝑛) → 𝑛 ∈ ℤ) |
14 | | 6nn 11066 |
. . . . . . . . . . . . . . . . 17
⊢ 6 ∈
ℕ |
15 | 14 | nnzi 11278 |
. . . . . . . . . . . . . . . 16
⊢ 6 ∈
ℤ |
16 | 13, 15 | jctir 559 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ Odd ∧ 5 < 𝑛) → (𝑛 ∈ ℤ ∧ 6 ∈
ℤ)) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 < 7 ∧ (𝑛 ∈ Odd ∧ 5 < 𝑛)) → (𝑛 ∈ ℤ ∧ 6 ∈
ℤ)) |
18 | | df-7 10961 |
. . . . . . . . . . . . . . . . 17
⊢ 7 = (6 +
1) |
19 | 18 | breq2i 4591 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 < 7 ↔ 𝑛 < (6 + 1)) |
20 | 19 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 < 7 → 𝑛 < (6 + 1)) |
21 | | df-6 10960 |
. . . . . . . . . . . . . . . 16
⊢ 6 = (5 +
1) |
22 | | 5nn 11065 |
. . . . . . . . . . . . . . . . . . 19
⊢ 5 ∈
ℕ |
23 | 22 | nnzi 11278 |
. . . . . . . . . . . . . . . . . 18
⊢ 5 ∈
ℤ |
24 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . . 18
⊢ ((5
∈ ℤ ∧ 𝑛
∈ ℤ) → (5 < 𝑛 ↔ (5 + 1) ≤ 𝑛)) |
25 | 23, 7, 24 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ Odd → (5 < 𝑛 ↔ (5 + 1) ≤ 𝑛)) |
26 | 25 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ Odd ∧ 5 < 𝑛) → (5 + 1) ≤ 𝑛) |
27 | 21, 26 | syl5eqbr 4618 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ Odd ∧ 5 < 𝑛) → 6 ≤ 𝑛) |
28 | 20, 27 | anim12ci 589 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 < 7 ∧ (𝑛 ∈ Odd ∧ 5 < 𝑛)) → (6 ≤ 𝑛 ∧ 𝑛 < (6 + 1))) |
29 | | zgeltp1eq 39943 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℤ ∧ 6 ∈
ℤ) → ((6 ≤ 𝑛
∧ 𝑛 < (6 + 1))
→ 𝑛 =
6)) |
30 | 17, 28, 29 | sylc 63 |
. . . . . . . . . . . . 13
⊢ ((𝑛 < 7 ∧ (𝑛 ∈ Odd ∧ 5 < 𝑛)) → 𝑛 = 6) |
31 | 30 | orcd 406 |
. . . . . . . . . . . 12
⊢ ((𝑛 < 7 ∧ (𝑛 ∈ Odd ∧ 5 < 𝑛)) → (𝑛 = 6 ∨ 𝑛 = 7)) |
32 | 31 | ex 449 |
. . . . . . . . . . 11
⊢ (𝑛 < 7 → ((𝑛 ∈ Odd ∧ 5 < 𝑛) → (𝑛 = 6 ∨ 𝑛 = 7))) |
33 | | olc 398 |
. . . . . . . . . . . 12
⊢ (𝑛 = 7 → (𝑛 = 6 ∨ 𝑛 = 7)) |
34 | 33 | a1d 25 |
. . . . . . . . . . 11
⊢ (𝑛 = 7 → ((𝑛 ∈ Odd ∧ 5 < 𝑛) → (𝑛 = 6 ∨ 𝑛 = 7))) |
35 | 32, 34 | jaoi 393 |
. . . . . . . . . 10
⊢ ((𝑛 < 7 ∨ 𝑛 = 7) → ((𝑛 ∈ Odd ∧ 5 < 𝑛) → (𝑛 = 6 ∨ 𝑛 = 7))) |
36 | 35 | expd 451 |
. . . . . . . . 9
⊢ ((𝑛 < 7 ∨ 𝑛 = 7) → (𝑛 ∈ Odd → (5 < 𝑛 → (𝑛 = 6 ∨ 𝑛 = 7)))) |
37 | 36 | com12 32 |
. . . . . . . 8
⊢ (𝑛 ∈ Odd → ((𝑛 < 7 ∨ 𝑛 = 7) → (5 < 𝑛 → (𝑛 = 6 ∨ 𝑛 = 7)))) |
38 | 12, 37 | sylbid 229 |
. . . . . . 7
⊢ (𝑛 ∈ Odd → (𝑛 ≤ 7 → (5 < 𝑛 → (𝑛 = 6 ∨ 𝑛 = 7)))) |
39 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑛 = 6 → (𝑛 ∈ Odd ↔ 6 ∈ Odd
)) |
40 | | 6even 40158 |
. . . . . . . . . . 11
⊢ 6 ∈
Even |
41 | | evennodd 40094 |
. . . . . . . . . . . 12
⊢ (6 ∈
Even → ¬ 6 ∈ Odd ) |
42 | 41 | pm2.21d 117 |
. . . . . . . . . . 11
⊢ (6 ∈
Even → (6 ∈ Odd → 𝑛 ∈ GoldbachOdd )) |
43 | 40, 42 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝑛 = 6 → (6 ∈ Odd →
𝑛 ∈ GoldbachOdd
)) |
44 | 39, 43 | sylbid 229 |
. . . . . . . . 9
⊢ (𝑛 = 6 → (𝑛 ∈ Odd → 𝑛 ∈ GoldbachOdd )) |
45 | | 7gbo 40194 |
. . . . . . . . . . 11
⊢ 7 ∈
GoldbachOdd |
46 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑛 = 7 → (𝑛 ∈ GoldbachOdd ↔ 7 ∈
GoldbachOdd )) |
47 | 45, 46 | mpbiri 247 |
. . . . . . . . . 10
⊢ (𝑛 = 7 → 𝑛 ∈ GoldbachOdd ) |
48 | 47 | a1d 25 |
. . . . . . . . 9
⊢ (𝑛 = 7 → (𝑛 ∈ Odd → 𝑛 ∈ GoldbachOdd )) |
49 | 44, 48 | jaoi 393 |
. . . . . . . 8
⊢ ((𝑛 = 6 ∨ 𝑛 = 7) → (𝑛 ∈ Odd → 𝑛 ∈ GoldbachOdd )) |
50 | 49 | com12 32 |
. . . . . . 7
⊢ (𝑛 ∈ Odd → ((𝑛 = 6 ∨ 𝑛 = 7) → 𝑛 ∈ GoldbachOdd )) |
51 | 38, 50 | syl6d 73 |
. . . . . 6
⊢ (𝑛 ∈ Odd → (𝑛 ≤ 7 → (5 < 𝑛 → 𝑛 ∈ GoldbachOdd ))) |
52 | 11, 51 | sylbird 249 |
. . . . 5
⊢ (𝑛 ∈ Odd → (¬ 7 <
𝑛 → (5 < 𝑛 → 𝑛 ∈ GoldbachOdd ))) |
53 | 52 | com12 32 |
. . . 4
⊢ (¬ 7
< 𝑛 → (𝑛 ∈ Odd → (5 < 𝑛 → 𝑛 ∈ GoldbachOdd ))) |
54 | 53 | a1dd 48 |
. . 3
⊢ (¬ 7
< 𝑛 → (𝑛 ∈ Odd → ((7 <
𝑛 → 𝑛 ∈ GoldbachOddALTV ) → (5 <
𝑛 → 𝑛 ∈ GoldbachOdd )))) |
55 | 6, 54 | pm2.61i 175 |
. 2
⊢ (𝑛 ∈ Odd → ((7 <
𝑛 → 𝑛 ∈ GoldbachOddALTV ) → (5 <
𝑛 → 𝑛 ∈ GoldbachOdd ))) |
56 | 55 | ralimia 2934 |
1
⊢
(∀𝑛 ∈
Odd (7 < 𝑛 → 𝑛 ∈ GoldbachOddALTV ) →
∀𝑛 ∈ Odd (5
< 𝑛 → 𝑛 ∈ GoldbachOdd
)) |