| Step | Hyp | Ref
| Expression |
| 1 | | evengpop3 47785 |
. . . 4
⊢
(∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) →
((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3))) |
| 2 | 1 | imp 406 |
. . 3
⊢
((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3)) |
| 3 | | simplll 775 |
. . . . . 6
⊢
((((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → ∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW )) |
| 4 | | 6nn 12355 |
. . . . . . . . . . 11
⊢ 6 ∈
ℕ |
| 5 | 4 | nnzi 12641 |
. . . . . . . . . 10
⊢ 6 ∈
ℤ |
| 6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘9) → 6 ∈ ℤ) |
| 7 | | 3z 12650 |
. . . . . . . . . 10
⊢ 3 ∈
ℤ |
| 8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘9) → 3 ∈ ℤ) |
| 9 | | 6p3e9 12426 |
. . . . . . . . . . . . 13
⊢ (6 + 3) =
9 |
| 10 | 9 | eqcomi 2746 |
. . . . . . . . . . . 12
⊢ 9 = (6 +
3) |
| 11 | 10 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(ℤ≥‘9) = (ℤ≥‘(6 +
3)) |
| 12 | 11 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘9) ↔ 𝑁 ∈ (ℤ≥‘(6 +
3))) |
| 13 | 12 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘9) → 𝑁 ∈ (ℤ≥‘(6 +
3))) |
| 14 | | eluzsub 12908 |
. . . . . . . . 9
⊢ ((6
∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(6 +
3))) → (𝑁 − 3)
∈ (ℤ≥‘6)) |
| 15 | 6, 8, 13, 14 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘9) → (𝑁 − 3) ∈
(ℤ≥‘6)) |
| 16 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (𝑁 − 3) ∈
(ℤ≥‘6)) |
| 17 | 16 | ad3antlr 731 |
. . . . . 6
⊢
((((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → (𝑁 − 3) ∈
(ℤ≥‘6)) |
| 18 | | 3odd 47695 |
. . . . . . . . . . . . 13
⊢ 3 ∈
Odd |
| 19 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘9) → 3 ∈ Odd ) |
| 20 | 19 | anim1i 615 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (3 ∈ Odd ∧
𝑁 ∈ Even
)) |
| 21 | 20 | adantl 481 |
. . . . . . . . . 10
⊢
((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) → (3 ∈ Odd ∧
𝑁 ∈ Even
)) |
| 22 | 21 | ancomd 461 |
. . . . . . . . 9
⊢
((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) → (𝑁 ∈ Even ∧ 3 ∈ Odd
)) |
| 23 | 22 | adantr 480 |
. . . . . . . 8
⊢
(((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) → (𝑁 ∈ Even ∧ 3 ∈ Odd
)) |
| 24 | 23 | adantr 480 |
. . . . . . 7
⊢
((((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → (𝑁 ∈ Even ∧ 3 ∈ Odd
)) |
| 25 | | emoo 47691 |
. . . . . . 7
⊢ ((𝑁 ∈ Even ∧ 3 ∈ Odd
) → (𝑁 − 3)
∈ Odd ) |
| 26 | 24, 25 | syl 17 |
. . . . . 6
⊢
((((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → (𝑁 − 3) ∈ Odd ) |
| 27 | | nnsum4primesodd 47783 |
. . . . . . 7
⊢
(∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) →
(((𝑁 − 3) ∈
(ℤ≥‘6) ∧ (𝑁 − 3) ∈ Odd ) → ∃𝑔 ∈ (ℙ
↑m (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘))) |
| 28 | 27 | imp 406 |
. . . . . 6
⊢
((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
((𝑁 − 3) ∈
(ℤ≥‘6) ∧ (𝑁 − 3) ∈ Odd )) →
∃𝑔 ∈ (ℙ
↑m (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) |
| 29 | 3, 17, 26, 28 | syl12anc 837 |
. . . . 5
⊢
((((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → ∃𝑔 ∈ (ℙ ↑m
(1...3))(𝑁 − 3) =
Σ𝑘 ∈
(1...3)(𝑔‘𝑘)) |
| 30 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 𝑔:(1...3)⟶ℙ) |
| 31 | | 4z 12651 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℤ |
| 32 | | fzonel 13713 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬ 4
∈ (1..^4) |
| 33 | | fzoval 13700 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ∈
ℤ → (1..^4) = (1...(4 − 1))) |
| 34 | 31, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1..^4) =
(1...(4 − 1)) |
| 35 | | 4cn 12351 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 4 ∈
ℂ |
| 36 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℂ |
| 37 | | 3cn 12347 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 3 ∈
ℂ |
| 38 | 35, 36, 37 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (4 ∈
ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ) |
| 39 | | 3p1e4 12411 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (3 + 1) =
4 |
| 40 | | subadd2 11512 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((4
∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ) → ((4
− 1) = 3 ↔ (3 + 1) = 4)) |
| 41 | 39, 40 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((4
∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ) → (4 −
1) = 3) |
| 42 | 38, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4
− 1) = 3 |
| 43 | 42 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1...(4
− 1)) = (1...3) |
| 44 | 34, 43 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1..^4) =
(1...3) |
| 45 | 44 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1...3) =
(1..^4) |
| 46 | 45 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (4 ∈
(1...3) ↔ 4 ∈ (1..^4)) |
| 47 | 32, 46 | mtbir 323 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ 4
∈ (1...3) |
| 48 | 31, 47 | pm3.2i 470 |
. . . . . . . . . . . . . . . . 17
⊢ (4 ∈
ℤ ∧ ¬ 4 ∈ (1...3)) |
| 49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (4 ∈
ℤ ∧ ¬ 4 ∈ (1...3))) |
| 50 | | 3prm 16731 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℙ |
| 51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 3 ∈
ℙ) |
| 52 | | fsnunf 7205 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:(1...3)⟶ℙ ∧ (4
∈ ℤ ∧ ¬ 4 ∈ (1...3)) ∧ 3 ∈ ℙ) →
(𝑔 ∪ {〈4,
3〉}):((1...3) ∪ {4})⟶ℙ) |
| 53 | 30, 49, 51, 52 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {〈4,
3〉}):((1...3) ∪ {4})⟶ℙ) |
| 54 | | fzval3 13773 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 ∈
ℤ → (1...4) = (1..^(4 + 1))) |
| 55 | 31, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (1...4) =
(1..^(4 + 1)) |
| 56 | | 1z 12647 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℤ |
| 57 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ |
| 58 | | 4re 12350 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 4 ∈
ℝ |
| 59 | | 1lt4 12442 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
4 |
| 60 | 57, 58, 59 | ltleii 11384 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ≤
4 |
| 61 | | eluz2 12884 |
. . . . . . . . . . . . . . . . . . 19
⊢ (4 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 4 ∈
ℤ ∧ 1 ≤ 4)) |
| 62 | 56, 31, 60, 61 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
(ℤ≥‘1) |
| 63 | | fzosplitsn 13814 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 ∈
(ℤ≥‘1) → (1..^(4 + 1)) = ((1..^4) ∪
{4})) |
| 64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (1..^(4 +
1)) = ((1..^4) ∪ {4}) |
| 65 | 44 | uneq1i 4164 |
. . . . . . . . . . . . . . . . 17
⊢ ((1..^4)
∪ {4}) = ((1...3) ∪ {4}) |
| 66 | 55, 64, 65 | 3eqtri 2769 |
. . . . . . . . . . . . . . . 16
⊢ (1...4) =
((1...3) ∪ {4}) |
| 67 | 66 | feq2i 6728 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∪ {〈4,
3〉}):(1...4)⟶ℙ ↔ (𝑔 ∪ {〈4, 3〉}):((1...3) ∪
{4})⟶ℙ) |
| 68 | 53, 67 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {〈4,
3〉}):(1...4)⟶ℙ) |
| 69 | | prmex 16714 |
. . . . . . . . . . . . . . . 16
⊢ ℙ
∈ V |
| 70 | | ovex 7464 |
. . . . . . . . . . . . . . . 16
⊢ (1...4)
∈ V |
| 71 | 69, 70 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (ℙ
∈ V ∧ (1...4) ∈ V) |
| 72 | | elmapg 8879 |
. . . . . . . . . . . . . . 15
⊢ ((ℙ
∈ V ∧ (1...4) ∈ V) → ((𝑔 ∪ {〈4, 3〉}) ∈ (ℙ
↑m (1...4)) ↔ (𝑔 ∪ {〈4,
3〉}):(1...4)⟶ℙ)) |
| 73 | 71, 72 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4, 3〉})
∈ (ℙ ↑m (1...4)) ↔ (𝑔 ∪ {〈4,
3〉}):(1...4)⟶ℙ)) |
| 74 | 68, 73 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {〈4, 3〉})
∈ (ℙ ↑m (1...4))) |
| 75 | 74 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (𝑔 ∪ {〈4, 3〉}) ∈ (ℙ
↑m (1...4))) |
| 76 | | fveq1 6905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∪ {〈4, 3〉}) → (𝑓‘𝑘) = ((𝑔 ∪ {〈4, 3〉})‘𝑘)) |
| 77 | 76 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 = (𝑔 ∪ {〈4, 3〉}) ∧ 𝑘 ∈ (1...4)) → (𝑓‘𝑘) = ((𝑔 ∪ {〈4, 3〉})‘𝑘)) |
| 78 | 77 | sumeq2dv 15738 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑔 ∪ {〈4, 3〉}) →
Σ𝑘 ∈
(1...4)(𝑓‘𝑘) = Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4, 3〉})‘𝑘)) |
| 79 | 78 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑔 ∪ {〈4, 3〉}) → (𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘) ↔ 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4, 3〉})‘𝑘))) |
| 80 | 79 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) ∧ 𝑓 = (𝑔 ∪ {〈4, 3〉})) → (𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘) ↔ 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4, 3〉})‘𝑘))) |
| 81 | 62 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 4 ∈
(ℤ≥‘1)) |
| 82 | 66 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...4) ↔ 𝑘 ∈ ((1...3) ∪
{4})) |
| 83 | | elun 4153 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((1...3) ∪ {4})
↔ (𝑘 ∈ (1...3)
∨ 𝑘 ∈
{4})) |
| 84 | | velsn 4642 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ {4} ↔ 𝑘 = 4) |
| 85 | 84 | orbi2i 913 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ (1...3) ∨ 𝑘 ∈ {4}) ↔ (𝑘 ∈ (1...3) ∨ 𝑘 = 4)) |
| 86 | 82, 83, 85 | 3bitri 297 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (1...4) ↔ (𝑘 ∈ (1...3) ∨ 𝑘 = 4)) |
| 87 | | elfz2 13554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (1...3) ↔ ((1
∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (1 ≤ 𝑘 ∧ 𝑘 ≤ 3))) |
| 88 | | 3re 12346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 3 ∈
ℝ |
| 89 | 88, 58 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (3 ∈
ℝ ∧ 4 ∈ ℝ) |
| 90 | | 3lt4 12440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 3 <
4 |
| 91 | | ltnle 11340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((3
∈ ℝ ∧ 4 ∈ ℝ) → (3 < 4 ↔ ¬ 4 ≤
3)) |
| 92 | 90, 91 | mpbii 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((3
∈ ℝ ∧ 4 ∈ ℝ) → ¬ 4 ≤ 3) |
| 93 | 89, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ¬ 4
≤ 3 |
| 94 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 = 4 → (𝑘 ≤ 3 ↔ 4 ≤ 3)) |
| 95 | 94 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (4 =
𝑘 → (𝑘 ≤ 3 ↔ 4 ≤
3)) |
| 96 | 93, 95 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (4 =
𝑘 → ¬ 𝑘 ≤ 3) |
| 97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ ℤ → (4 =
𝑘 → ¬ 𝑘 ≤ 3)) |
| 98 | 97 | necon2ad 2955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ ℤ → (𝑘 ≤ 3 → 4 ≠ 𝑘)) |
| 99 | 98 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ℤ → ((1 ≤
𝑘 ∧ 𝑘 ≤ 3) → 4 ≠ 𝑘)) |
| 100 | 99 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((1
∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((1 ≤ 𝑘 ∧ 𝑘 ≤ 3) → 4 ≠ 𝑘)) |
| 101 | 100 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((1
∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (1 ≤ 𝑘 ∧ 𝑘 ≤ 3)) → 4 ≠ 𝑘) |
| 102 | 87, 101 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ (1...3) → 4 ≠
𝑘) |
| 103 | 102 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
4 ≠ 𝑘) |
| 104 | | fvunsn 7199 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ≠
𝑘 → ((𝑔 ∪ {〈4,
3〉})‘𝑘) = (𝑔‘𝑘)) |
| 105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
((𝑔 ∪ {〈4,
3〉})‘𝑘) = (𝑔‘𝑘)) |
| 106 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:(1...3)⟶ℙ ∧
𝑘 ∈ (1...3)) →
(𝑔‘𝑘) ∈ ℙ) |
| 107 | 106 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
(𝑔‘𝑘) ∈ ℙ) |
| 108 | | prmz 16712 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔‘𝑘) ∈ ℙ → (𝑔‘𝑘) ∈ ℤ) |
| 109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
(𝑔‘𝑘) ∈ ℤ) |
| 110 | 109 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
(𝑔‘𝑘) ∈ ℂ) |
| 111 | 105, 110 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ) |
| 112 | 111 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...3) → (𝑔:(1...3)⟶ℙ →
((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
| 113 | 112 | adantld 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...3) → ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
| 114 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 4 → ((𝑔 ∪ {〈4, 3〉})‘𝑘) = ((𝑔 ∪ {〈4,
3〉})‘4)) |
| 115 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:(1...3)⟶ℙ → 4
∈ ℤ) |
| 116 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:(1...3)⟶ℙ → 3
∈ ℤ) |
| 117 | | fdm 6745 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑔:(1...3)⟶ℙ →
dom 𝑔 =
(1...3)) |
| 118 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑔 = (1...3) → (4
∈ dom 𝑔 ↔ 4
∈ (1...3))) |
| 119 | 47, 118 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (dom
𝑔 = (1...3) → ¬ 4
∈ dom 𝑔) |
| 120 | 117, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:(1...3)⟶ℙ →
¬ 4 ∈ dom 𝑔) |
| 121 | | fsnunfv 7207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((4
∈ ℤ ∧ 3 ∈ ℤ ∧ ¬ 4 ∈ dom 𝑔) → ((𝑔 ∪ {〈4, 3〉})‘4) =
3) |
| 122 | 115, 116,
120, 121 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔:(1...3)⟶ℙ →
((𝑔 ∪ {〈4,
3〉})‘4) = 3) |
| 123 | 122 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4,
3〉})‘4) = 3) |
| 124 | 114, 123 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 = 4 ∧ (𝑁 ∈ (ℤ≥‘9)
∧ 𝑔:(1...3)⟶ℙ)) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) =
3) |
| 125 | 124, 37 | eqeltrdi 2849 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 = 4 ∧ (𝑁 ∈ (ℤ≥‘9)
∧ 𝑔:(1...3)⟶ℙ)) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ) |
| 126 | 125 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 4 → ((𝑁 ∈ (ℤ≥‘9)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
| 127 | 113, 126 | jaoi 858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ (1...3) ∨ 𝑘 = 4) → ((𝑁 ∈ (ℤ≥‘9)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
| 128 | 127 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑘 ∈ (1...3) ∨ 𝑘 = 4) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
| 129 | 86, 128 | biimtrid 242 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑘 ∈ (1...4) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
| 130 | 129 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...4)) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ) |
| 131 | 81, 130, 114 | fsumm1 15787 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4,
3〉})‘𝑘) =
(Σ𝑘 ∈ (1...(4
− 1))((𝑔 ∪
{〈4, 3〉})‘𝑘) + ((𝑔 ∪ {〈4,
3〉})‘4))) |
| 132 | 131 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4, 3〉})‘𝑘) = (Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘) +
((𝑔 ∪ {〈4,
3〉})‘4))) |
| 133 | 42 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 3 = (4
− 1) |
| 134 | 133 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1...3) =
(1...(4 − 1)) |
| 135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (1...3) =
(1...(4 − 1))) |
| 136 | 102 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → 4 ≠
𝑘) |
| 137 | 136, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) = (𝑔‘𝑘)) |
| 138 | 137 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → (𝑔‘𝑘) = ((𝑔 ∪ {〈4, 3〉})‘𝑘)) |
| 139 | 135, 138 | sumeq12dv 15742 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → Σ𝑘 ∈ (1...3)(𝑔‘𝑘) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘)) |
| 140 | 139 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) ↔ (𝑁 − 3) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘))) |
| 141 | 140 | biimpa 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (𝑁 − 3) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘)) |
| 142 | 141 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘) = (𝑁 − 3)) |
| 143 | 142 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘) +
((𝑔 ∪ {〈4,
3〉})‘4)) = ((𝑁
− 3) + ((𝑔 ∪
{〈4, 3〉})‘4))) |
| 144 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 4 ∈
ℤ) |
| 145 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 3 ∈
ℤ) |
| 146 | 120 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ¬ 4
∈ dom 𝑔) |
| 147 | 144, 145,
146, 121 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4,
3〉})‘4) = 3) |
| 148 | 147 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + ((𝑔 ∪ {〈4,
3〉})‘4)) = ((𝑁
− 3) + 3)) |
| 149 | | eluzelcn 12890 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘9) → 𝑁 ∈ ℂ) |
| 150 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘9) → 3 ∈ ℂ) |
| 151 | 149, 150 | npcand 11624 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘9) → ((𝑁 − 3) + 3) = 𝑁) |
| 152 | 151 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + 3) = 𝑁) |
| 153 | 148, 152 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + ((𝑔 ∪ {〈4,
3〉})‘4)) = 𝑁) |
| 154 | 153 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → ((𝑁 − 3) + ((𝑔 ∪ {〈4, 3〉})‘4)) = 𝑁) |
| 155 | 132, 143,
154 | 3eqtrrd 2782 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4, 3〉})‘𝑘)) |
| 156 | 75, 80, 155 | rspcedvd 3624 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → ∃𝑓 ∈ (ℙ ↑m
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)) |
| 157 | 156 | ex 412 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑m
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |
| 158 | 157 | expcom 413 |
. . . . . . . . 9
⊢ (𝑔:(1...3)⟶ℙ →
(𝑁 ∈
(ℤ≥‘9) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑m
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))) |
| 159 | | elmapi 8889 |
. . . . . . . . 9
⊢ (𝑔 ∈ (ℙ
↑m (1...3)) → 𝑔:(1...3)⟶ℙ) |
| 160 | 158, 159 | syl11 33 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘9) → (𝑔 ∈ (ℙ ↑m (1...3))
→ ((𝑁 − 3) =
Σ𝑘 ∈
(1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ
↑m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))) |
| 161 | 160 | rexlimdv 3153 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘9) → (∃𝑔 ∈ (ℙ ↑m
(1...3))(𝑁 − 3) =
Σ𝑘 ∈
(1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ
↑m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |
| 162 | 161 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (∃𝑔 ∈ (ℙ
↑m (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑m
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |
| 163 | 162 | ad3antlr 731 |
. . . . 5
⊢
((((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → (∃𝑔 ∈ (ℙ ↑m
(1...3))(𝑁 − 3) =
Σ𝑘 ∈
(1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ
↑m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |
| 164 | 29, 163 | mpd 15 |
. . . 4
⊢
((((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → ∃𝑓 ∈ (ℙ ↑m
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)) |
| 165 | 164 | rexlimdva2 3157 |
. . 3
⊢
((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) → (∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3) → ∃𝑓 ∈ (ℙ ↑m
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |
| 166 | 2, 165 | mpd 15 |
. 2
⊢
((∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧
(𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even )) → ∃𝑓 ∈ (ℙ
↑m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)) |
| 167 | 166 | ex 412 |
1
⊢
(∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) →
((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ
↑m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |