Proof of Theorem sgoldbeven3prm
| Step | Hyp | Ref
| Expression |
| 1 | | sbgoldbb 47769 |
. 2
⊢
(∀𝑛 ∈
Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) →
∀𝑛 ∈ Even (2
< 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |
| 2 | | 2p2e4 12401 |
. . . . 5
⊢ (2 + 2) =
4 |
| 3 | | evenz 47617 |
. . . . . . . 8
⊢ (𝑁 ∈ Even → 𝑁 ∈
ℤ) |
| 4 | 3 | zred 12722 |
. . . . . . 7
⊢ (𝑁 ∈ Even → 𝑁 ∈
ℝ) |
| 5 | | 4lt6 12448 |
. . . . . . . 8
⊢ 4 <
6 |
| 6 | | 4re 12350 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
| 7 | | 6re 12356 |
. . . . . . . . 9
⊢ 6 ∈
ℝ |
| 8 | | ltletr 11353 |
. . . . . . . . 9
⊢ ((4
∈ ℝ ∧ 6 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((4 < 6 ∧ 6
≤ 𝑁) → 4 < 𝑁)) |
| 9 | 6, 7, 8 | mp3an12 1453 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ → ((4 <
6 ∧ 6 ≤ 𝑁) → 4
< 𝑁)) |
| 10 | 5, 9 | mpani 696 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ → (6 ≤
𝑁 → 4 < 𝑁)) |
| 11 | 4, 10 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ Even → (6 ≤
𝑁 → 4 < 𝑁)) |
| 12 | 11 | imp 406 |
. . . . 5
⊢ ((𝑁 ∈ Even ∧ 6 ≤ 𝑁) → 4 < 𝑁) |
| 13 | 2, 12 | eqbrtrid 5178 |
. . . 4
⊢ ((𝑁 ∈ Even ∧ 6 ≤ 𝑁) → (2 + 2) < 𝑁) |
| 14 | | 2re 12340 |
. . . . . 6
⊢ 2 ∈
ℝ |
| 15 | 14 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ Even ∧ 6 ≤ 𝑁) → 2 ∈
ℝ) |
| 16 | 4 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ Even ∧ 6 ≤ 𝑁) → 𝑁 ∈ ℝ) |
| 17 | 15, 15, 16 | ltaddsub2d 11864 |
. . . 4
⊢ ((𝑁 ∈ Even ∧ 6 ≤ 𝑁) → ((2 + 2) < 𝑁 ↔ 2 < (𝑁 − 2))) |
| 18 | 13, 17 | mpbid 232 |
. . 3
⊢ ((𝑁 ∈ Even ∧ 6 ≤ 𝑁) → 2 < (𝑁 − 2)) |
| 19 | | 2evenALTV 47679 |
. . . . . 6
⊢ 2 ∈
Even |
| 20 | | emee 47693 |
. . . . . 6
⊢ ((𝑁 ∈ Even ∧ 2 ∈ Even
) → (𝑁 − 2)
∈ Even ) |
| 21 | 19, 20 | mpan2 691 |
. . . . 5
⊢ (𝑁 ∈ Even → (𝑁 − 2) ∈ Even
) |
| 22 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑛 = (𝑁 − 2) → (2 < 𝑛 ↔ 2 < (𝑁 − 2))) |
| 23 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑛 = (𝑁 − 2) → (𝑛 = (𝑝 + 𝑞) ↔ (𝑁 − 2) = (𝑝 + 𝑞))) |
| 24 | 23 | 2rexbidv 3222 |
. . . . . . . 8
⊢ (𝑛 = (𝑁 − 2) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) ↔ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑁 − 2) = (𝑝 + 𝑞))) |
| 25 | 22, 24 | imbi12d 344 |
. . . . . . 7
⊢ (𝑛 = (𝑁 − 2) → ((2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) ↔ (2 < (𝑁 − 2) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑁 − 2) = (𝑝 + 𝑞)))) |
| 26 | 25 | rspcv 3618 |
. . . . . 6
⊢ ((𝑁 − 2) ∈ Even →
(∀𝑛 ∈ Even (2
< 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → (2 < (𝑁 − 2) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑁 − 2) = (𝑝 + 𝑞)))) |
| 27 | | 2prm 16729 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℙ |
| 28 | 27 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Even ∧ (𝑁 − 2) = (𝑝 + 𝑞)) → 2 ∈ ℙ) |
| 29 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 2 → ((𝑝 + 𝑞) + 𝑟) = ((𝑝 + 𝑞) + 2)) |
| 30 | 29 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑟 = 2 → (𝑁 = ((𝑝 + 𝑞) + 𝑟) ↔ 𝑁 = ((𝑝 + 𝑞) + 2))) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Even ∧ (𝑁 − 2) = (𝑝 + 𝑞)) ∧ 𝑟 = 2) → (𝑁 = ((𝑝 + 𝑞) + 𝑟) ↔ 𝑁 = ((𝑝 + 𝑞) + 2))) |
| 32 | 3 | zcnd 12723 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ Even → 𝑁 ∈
ℂ) |
| 33 | | 2cnd 12344 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ Even → 2 ∈
ℂ) |
| 34 | | npcan 11517 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑁 −
2) + 2) = 𝑁) |
| 35 | 34 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → 𝑁 = ((𝑁 − 2) +
2)) |
| 36 | 32, 33, 35 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ Even → 𝑁 = ((𝑁 − 2) + 2)) |
| 37 | 36 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Even ∧ (𝑁 − 2) = (𝑝 + 𝑞)) → 𝑁 = ((𝑁 − 2) + 2)) |
| 38 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Even ∧ (𝑁 − 2) = (𝑝 + 𝑞)) → (𝑁 − 2) = (𝑝 + 𝑞)) |
| 39 | 38 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Even ∧ (𝑁 − 2) = (𝑝 + 𝑞)) → ((𝑁 − 2) + 2) = ((𝑝 + 𝑞) + 2)) |
| 40 | 37, 39 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Even ∧ (𝑁 − 2) = (𝑝 + 𝑞)) → 𝑁 = ((𝑝 + 𝑞) + 2)) |
| 41 | 28, 31, 40 | rspcedvd 3624 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Even ∧ (𝑁 − 2) = (𝑝 + 𝑞)) → ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟)) |
| 42 | 41 | ex 412 |
. . . . . . . . 9
⊢ (𝑁 ∈ Even → ((𝑁 − 2) = (𝑝 + 𝑞) → ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟))) |
| 43 | 42 | reximdv 3170 |
. . . . . . . 8
⊢ (𝑁 ∈ Even →
(∃𝑞 ∈ ℙ
(𝑁 − 2) = (𝑝 + 𝑞) → ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟))) |
| 44 | 43 | reximdv 3170 |
. . . . . . 7
⊢ (𝑁 ∈ Even →
(∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
(𝑁 − 2) = (𝑝 + 𝑞) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟))) |
| 45 | 44 | imim2d 57 |
. . . . . 6
⊢ (𝑁 ∈ Even → ((2 <
(𝑁 − 2) →
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
(𝑁 − 2) = (𝑝 + 𝑞)) → (2 < (𝑁 − 2) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟)))) |
| 46 | 26, 45 | syl9r 78 |
. . . . 5
⊢ (𝑁 ∈ Even → ((𝑁 − 2) ∈ Even →
(∀𝑛 ∈ Even (2
< 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → (2 < (𝑁 − 2) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟))))) |
| 47 | 21, 46 | mpd 15 |
. . . 4
⊢ (𝑁 ∈ Even →
(∀𝑛 ∈ Even (2
< 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → (2 < (𝑁 − 2) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟)))) |
| 48 | 47 | adantr 480 |
. . 3
⊢ ((𝑁 ∈ Even ∧ 6 ≤ 𝑁) → (∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → (2 < (𝑁 − 2) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟)))) |
| 49 | 18, 48 | mpid 44 |
. 2
⊢ ((𝑁 ∈ Even ∧ 6 ≤ 𝑁) → (∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟))) |
| 50 | 1, 49 | syl5com 31 |
1
⊢
(∀𝑛 ∈
Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) →
((𝑁 ∈ Even ∧ 6
≤ 𝑁) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟))) |