Proof of Theorem sbgoldbalt
| Step | Hyp | Ref
| Expression |
| 1 | | 2z 12649 |
. . . . . 6
⊢ 2 ∈
ℤ |
| 2 | | evenz 47617 |
. . . . . 6
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℤ) |
| 3 | | zltp1le 12667 |
. . . . . 6
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛)) |
| 4 | 1, 2, 3 | sylancr 587 |
. . . . 5
⊢ (𝑛 ∈ Even → (2 <
𝑛 ↔ (2 + 1) ≤ 𝑛)) |
| 5 | | 2p1e3 12408 |
. . . . . . 7
⊢ (2 + 1) =
3 |
| 6 | 5 | breq1i 5150 |
. . . . . 6
⊢ ((2 + 1)
≤ 𝑛 ↔ 3 ≤ 𝑛) |
| 7 | | 3re 12346 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
| 8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ Even → 3 ∈
ℝ) |
| 9 | 2 | zred 12722 |
. . . . . . . 8
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℝ) |
| 10 | 8, 9 | leloed 11404 |
. . . . . . 7
⊢ (𝑛 ∈ Even → (3 ≤
𝑛 ↔ (3 < 𝑛 ∨ 3 = 𝑛))) |
| 11 | | 3z 12650 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℤ |
| 12 | | zltp1le 12667 |
. . . . . . . . . . . 12
⊢ ((3
∈ ℤ ∧ 𝑛
∈ ℤ) → (3 < 𝑛 ↔ (3 + 1) ≤ 𝑛)) |
| 13 | 11, 2, 12 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ Even → (3 <
𝑛 ↔ (3 + 1) ≤ 𝑛)) |
| 14 | | 3p1e4 12411 |
. . . . . . . . . . . . 13
⊢ (3 + 1) =
4 |
| 15 | 14 | breq1i 5150 |
. . . . . . . . . . . 12
⊢ ((3 + 1)
≤ 𝑛 ↔ 4 ≤ 𝑛) |
| 16 | | 4re 12350 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℝ |
| 17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ Even → 4 ∈
ℝ) |
| 18 | 17, 9 | leloed 11404 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ Even → (4 ≤
𝑛 ↔ (4 < 𝑛 ∨ 4 = 𝑛))) |
| 19 | | pm3.35 803 |
. . . . . . . . . . . . . . . . . 18
⊢ ((4 <
𝑛 ∧ (4 < 𝑛 → 𝑛 ∈ GoldbachEven )) → 𝑛 ∈ GoldbachEven
) |
| 20 | | isgbe 47738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ GoldbachEven ↔
(𝑛 ∈ Even ∧
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
(𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞)))) |
| 21 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞)) → 𝑛 = (𝑝 + 𝑞)) |
| 22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ Even ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞)) → 𝑛 = (𝑝 + 𝑞))) |
| 23 | 22 | reximdva 3168 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ Even ∧ 𝑝 ∈ ℙ) →
(∃𝑞 ∈ ℙ
(𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞)) → ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |
| 24 | 23 | reximdva 3168 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ Even →
(∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
(𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |
| 25 | 24 | imp 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) |
| 26 | 20, 25 | sylbi 217 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ GoldbachEven →
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
𝑛 = (𝑝 + 𝑞)) |
| 27 | 26 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ GoldbachEven →
(𝑛 ∈ Even →
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
𝑛 = (𝑝 + 𝑞))) |
| 28 | 19, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((4 <
𝑛 ∧ (4 < 𝑛 → 𝑛 ∈ GoldbachEven )) → (𝑛 ∈ Even → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |
| 29 | 28 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ (4 <
𝑛 → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑛 ∈ Even → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 30 | 29 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ (4 <
𝑛 → (𝑛 ∈ Even → ((4 <
𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 31 | | 2prm 16729 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℙ |
| 32 | | 2p2e4 12401 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 + 2) =
4 |
| 33 | 32 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 = (2 +
2) |
| 34 | | rspceov 7480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℙ ∧ 2 ∈ ℙ ∧ 4 = (2 + 2)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 4 = (𝑝 + 𝑞)) |
| 35 | 31, 31, 33, 34 | mp3an 1463 |
. . . . . . . . . . . . . . . . . 18
⊢
∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ 4 = (𝑝 + 𝑞) |
| 36 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (4 =
𝑛 → (4 = (𝑝 + 𝑞) ↔ 𝑛 = (𝑝 + 𝑞))) |
| 37 | 36 | 2rexbidv 3222 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 =
𝑛 → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 4 = (𝑝 + 𝑞) ↔ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |
| 38 | 35, 37 | mpbii 233 |
. . . . . . . . . . . . . . . . 17
⊢ (4 =
𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) |
| 39 | 38 | a1d 25 |
. . . . . . . . . . . . . . . 16
⊢ (4 =
𝑛 → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |
| 40 | 39 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ (4 =
𝑛 → (𝑛 ∈ Even → ((4 <
𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 41 | 30, 40 | jaoi 858 |
. . . . . . . . . . . . . 14
⊢ ((4 <
𝑛 ∨ 4 = 𝑛) → (𝑛 ∈ Even → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 42 | 41 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ Even → ((4 <
𝑛 ∨ 4 = 𝑛) → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 43 | 18, 42 | sylbid 240 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ Even → (4 ≤
𝑛 → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 44 | 15, 43 | biimtrid 242 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ Even → ((3 + 1)
≤ 𝑛 → ((4 <
𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 45 | 13, 44 | sylbid 240 |
. . . . . . . . . 10
⊢ (𝑛 ∈ Even → (3 <
𝑛 → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 46 | 45 | com12 32 |
. . . . . . . . 9
⊢ (3 <
𝑛 → (𝑛 ∈ Even → ((4 <
𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 47 | | 3odd 47695 |
. . . . . . . . . . . 12
⊢ 3 ∈
Odd |
| 48 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (3 =
𝑛 → (3 ∈ Odd
↔ 𝑛 ∈ Odd
)) |
| 49 | 47, 48 | mpbii 233 |
. . . . . . . . . . 11
⊢ (3 =
𝑛 → 𝑛 ∈ Odd ) |
| 50 | | oddneven 47631 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ Odd → ¬ 𝑛 ∈ Even ) |
| 51 | 49, 50 | syl 17 |
. . . . . . . . . 10
⊢ (3 =
𝑛 → ¬ 𝑛 ∈ Even ) |
| 52 | 51 | pm2.21d 121 |
. . . . . . . . 9
⊢ (3 =
𝑛 → (𝑛 ∈ Even → ((4 <
𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 53 | 46, 52 | jaoi 858 |
. . . . . . . 8
⊢ ((3 <
𝑛 ∨ 3 = 𝑛) → (𝑛 ∈ Even → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 54 | 53 | com12 32 |
. . . . . . 7
⊢ (𝑛 ∈ Even → ((3 <
𝑛 ∨ 3 = 𝑛) → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 55 | 10, 54 | sylbid 240 |
. . . . . 6
⊢ (𝑛 ∈ Even → (3 ≤
𝑛 → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 56 | 6, 55 | biimtrid 242 |
. . . . 5
⊢ (𝑛 ∈ Even → ((2 + 1)
≤ 𝑛 → ((4 <
𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 57 | 4, 56 | sylbid 240 |
. . . 4
⊢ (𝑛 ∈ Even → (2 <
𝑛 → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 58 | 57 | com23 86 |
. . 3
⊢ (𝑛 ∈ Even → ((4 <
𝑛 → 𝑛 ∈ GoldbachEven ) → (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 59 | | 2lt4 12441 |
. . . . . . . 8
⊢ 2 <
4 |
| 60 | | 2re 12340 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
| 61 | 60 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ Even → 2 ∈
ℝ) |
| 62 | | lttr 11337 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ 4 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((2 < 4 ∧ 4
< 𝑛) → 2 < 𝑛)) |
| 63 | 61, 17, 9, 62 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝑛 ∈ Even → ((2 < 4
∧ 4 < 𝑛) → 2
< 𝑛)) |
| 64 | 59, 63 | mpani 696 |
. . . . . . 7
⊢ (𝑛 ∈ Even → (4 <
𝑛 → 2 < 𝑛)) |
| 65 | 64 | imp 406 |
. . . . . 6
⊢ ((𝑛 ∈ Even ∧ 4 < 𝑛) → 2 < 𝑛) |
| 66 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑛 ∈ Even ∧ 4 < 𝑛) ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → 𝑛 ∈ Even ) |
| 67 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ Even ∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) |
| 68 | 67 | anim1i 615 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ Even ∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑛 ∈ Even
∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑛 = (𝑝 + 𝑞)) → (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) |
| 70 | | simpll 767 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ Even ∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑛 ∈ Even ∧ 4 < 𝑛)) |
| 71 | 70 | anim1i 615 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑛 ∈ Even
∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑛 = (𝑝 + 𝑞)) → ((𝑛 ∈ Even ∧ 4 < 𝑛) ∧ 𝑛 = (𝑝 + 𝑞))) |
| 72 | | df-3an 1089 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 = (𝑝 + 𝑞)) ↔ ((𝑛 ∈ Even ∧ 4 < 𝑛) ∧ 𝑛 = (𝑝 + 𝑞))) |
| 73 | 71, 72 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑛 ∈ Even
∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑛 = (𝑝 + 𝑞)) → (𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 = (𝑝 + 𝑞))) |
| 74 | | sbgoldbaltlem2 47767 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) → ((𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 = (𝑝 + 𝑞)) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ))) |
| 75 | 69, 73, 74 | sylc 65 |
. . . . . . . . . . . . . 14
⊢
(((((𝑛 ∈ Even
∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑛 = (𝑝 + 𝑞)) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd )) |
| 76 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝑛 ∈ Even
∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑛 = (𝑝 + 𝑞)) → 𝑛 = (𝑝 + 𝑞)) |
| 77 | | df-3an 1089 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞)) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ 𝑛 = (𝑝 + 𝑞))) |
| 78 | 75, 76, 77 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢
(((((𝑛 ∈ Even
∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑛 = (𝑝 + 𝑞)) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞))) |
| 79 | 78 | ex 412 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ Even ∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑛 = (𝑝 + 𝑞) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞)))) |
| 80 | 79 | reximdva 3168 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ Even ∧ 4 < 𝑛) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) → ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞)))) |
| 81 | 80 | reximdva 3168 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ Even ∧ 4 < 𝑛) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞)))) |
| 82 | 81 | imp 406 |
. . . . . . . . 9
⊢ (((𝑛 ∈ Even ∧ 4 < 𝑛) ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞))) |
| 83 | 66, 82 | jca 511 |
. . . . . . . 8
⊢ (((𝑛 ∈ Even ∧ 4 < 𝑛) ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → (𝑛 ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞)))) |
| 84 | 83 | ex 412 |
. . . . . . 7
⊢ ((𝑛 ∈ Even ∧ 4 < 𝑛) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) → (𝑛 ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = (𝑝 + 𝑞))))) |
| 85 | 84, 20 | imbitrrdi 252 |
. . . . . 6
⊢ ((𝑛 ∈ Even ∧ 4 < 𝑛) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) → 𝑛 ∈ GoldbachEven )) |
| 86 | 65, 85 | embantd 59 |
. . . . 5
⊢ ((𝑛 ∈ Even ∧ 4 < 𝑛) → ((2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → 𝑛 ∈ GoldbachEven )) |
| 87 | 86 | ex 412 |
. . . 4
⊢ (𝑛 ∈ Even → (4 <
𝑛 → ((2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → 𝑛 ∈ GoldbachEven ))) |
| 88 | 87 | com23 86 |
. . 3
⊢ (𝑛 ∈ Even → ((2 <
𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → (4 < 𝑛 → 𝑛 ∈ GoldbachEven ))) |
| 89 | 58, 88 | impbid 212 |
. 2
⊢ (𝑛 ∈ Even → ((4 <
𝑛 → 𝑛 ∈ GoldbachEven ) ↔ (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
| 90 | 89 | ralbiia 3091 |
1
⊢
(∀𝑛 ∈
Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔
∀𝑛 ∈ Even (2
< 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |