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