Step | Hyp | Ref
| Expression |
1 | | simplll 794 |
. . . . 5
⊢
((((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
∧ 𝑜 ∈
GoldbachOddALTV ) ∧ 𝑁 =
(𝑜 + 3)) →
∀𝑚 ∈ Odd (7
< 𝑚 → 𝑚 ∈ GoldbachOddALTV
)) |
2 | | 8nn 11068 |
. . . . . . . . . 10
⊢ 8 ∈
ℕ |
3 | 2 | nnzi 11278 |
. . . . . . . . 9
⊢ 8 ∈
ℤ |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ 8 ∈ ℤ) |
5 | | 3z 11287 |
. . . . . . . . 9
⊢ 3 ∈
ℤ |
6 | 5 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ 3 ∈ ℤ) |
7 | 4, 6 | zaddcld 11362 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ (8 + 3) ∈ ℤ) |
8 | | eluzelz 11573 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ 𝑁 ∈
ℤ) |
9 | | eluz2 11569 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘;12)
↔ (;12 ∈ ℤ ∧
𝑁 ∈ ℤ ∧
;12 ≤ 𝑁)) |
10 | | 8p4e12 11490 |
. . . . . . . . . . . . . 14
⊢ (8 + 4) =
;12 |
11 | 10 | breq1i 4590 |
. . . . . . . . . . . . 13
⊢ ((8 + 4)
≤ 𝑁 ↔ ;12 ≤ 𝑁) |
12 | | 1nn0 11185 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 |
13 | | 2nn 11062 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
14 | | 1lt2 11071 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
2 |
15 | 12, 12, 13, 14 | declt 11406 |
. . . . . . . . . . . . . . 15
⊢ ;11 < ;12 |
16 | | 8p3e11 11488 |
. . . . . . . . . . . . . . 15
⊢ (8 + 3) =
;11 |
17 | 15, 16, 10 | 3brtr4i 4613 |
. . . . . . . . . . . . . 14
⊢ (8 + 3)
< (8 + 4) |
18 | | 8re 10982 |
. . . . . . . . . . . . . . . . 17
⊢ 8 ∈
ℝ |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → 8 ∈
ℝ) |
20 | | 3re 10971 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℝ |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → 3 ∈
ℝ) |
22 | 19, 21 | readdcld 9948 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → (8 + 3)
∈ ℝ) |
23 | | 4re 10974 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
ℝ |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → 4 ∈
ℝ) |
25 | 19, 24 | readdcld 9948 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → (8 + 4)
∈ ℝ) |
26 | | zre 11258 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
27 | | ltleletr 10009 |
. . . . . . . . . . . . . . 15
⊢ (((8 + 3)
∈ ℝ ∧ (8 + 4) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((8 + 3) < (8 +
4) ∧ (8 + 4) ≤ 𝑁)
→ (8 + 3) ≤ 𝑁)) |
28 | 22, 25, 26, 27 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → (((8 + 3)
< (8 + 4) ∧ (8 + 4) ≤ 𝑁) → (8 + 3) ≤ 𝑁)) |
29 | 17, 28 | mpani 708 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → ((8 + 4)
≤ 𝑁 → (8 + 3) ≤
𝑁)) |
30 | 11, 29 | syl5bir 232 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (;12 ≤ 𝑁 → (8 + 3) ≤ 𝑁)) |
31 | 30 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ;12 ≤ 𝑁) → (8 + 3) ≤ 𝑁) |
32 | 31 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((;12 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ;12 ≤ 𝑁) → (8 + 3) ≤ 𝑁) |
33 | 9, 32 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ (8 + 3) ≤ 𝑁) |
34 | | eluz2 11569 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘(8 + 3)) ↔ ((8 + 3) ∈ ℤ ∧
𝑁 ∈ ℤ ∧ (8 +
3) ≤ 𝑁)) |
35 | 7, 8, 33, 34 | syl3anbrc 1239 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ 𝑁 ∈
(ℤ≥‘(8 + 3))) |
36 | | eluzsub 11593 |
. . . . . . . 8
⊢ ((8
∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(8 +
3))) → (𝑁 − 3)
∈ (ℤ≥‘8)) |
37 | 4, 6, 35, 36 | syl3anc 1318 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ (𝑁 − 3) ∈
(ℤ≥‘8)) |
38 | 37 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ (𝑁 − 3) ∈
(ℤ≥‘8)) |
39 | 38 | ad3antlr 763 |
. . . . 5
⊢
((((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
∧ 𝑜 ∈
GoldbachOddALTV ) ∧ 𝑁 =
(𝑜 + 3)) → (𝑁 − 3) ∈
(ℤ≥‘8)) |
40 | | 3odd 40155 |
. . . . . . . . . . . 12
⊢ 3 ∈
Odd |
41 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ 3 ∈ Odd ) |
42 | 41 | anim1i 590 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ (3 ∈ Odd ∧ 𝑁 ∈ Even )) |
43 | 42 | adantl 481 |
. . . . . . . . 9
⊢
((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
→ (3 ∈ Odd ∧ 𝑁 ∈ Even )) |
44 | 43 | ancomd 466 |
. . . . . . . 8
⊢
((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
→ (𝑁 ∈ Even ∧
3 ∈ Odd )) |
45 | 44 | adantr 480 |
. . . . . . 7
⊢
(((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
∧ 𝑜 ∈
GoldbachOddALTV ) → (𝑁
∈ Even ∧ 3 ∈ Odd )) |
46 | 45 | adantr 480 |
. . . . . 6
⊢
((((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
∧ 𝑜 ∈
GoldbachOddALTV ) ∧ 𝑁 =
(𝑜 + 3)) → (𝑁 ∈ Even ∧ 3 ∈ Odd
)) |
47 | | emoo 40151 |
. . . . . 6
⊢ ((𝑁 ∈ Even ∧ 3 ∈ Odd
) → (𝑁 − 3)
∈ Odd ) |
48 | 46, 47 | syl 17 |
. . . . 5
⊢
((((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
∧ 𝑜 ∈
GoldbachOddALTV ) ∧ 𝑁 =
(𝑜 + 3)) → (𝑁 − 3) ∈ Odd
) |
49 | | nnsum4primesoddALTV 40213 |
. . . . . 6
⊢
(∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) →
(((𝑁 − 3) ∈
(ℤ≥‘8) ∧ (𝑁 − 3) ∈ Odd ) → ∃𝑔 ∈ (ℙ
↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘))) |
50 | 49 | imp 444 |
. . . . 5
⊢
((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
((𝑁 − 3) ∈
(ℤ≥‘8) ∧ (𝑁 − 3) ∈ Odd )) →
∃𝑔 ∈ (ℙ
↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) |
51 | 1, 39, 48, 50 | syl12anc 1316 |
. . . 4
⊢
((((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
∧ 𝑜 ∈
GoldbachOddALTV ) ∧ 𝑁 =
(𝑜 + 3)) →
∃𝑔 ∈ (ℙ
↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) |
52 | | elmapi 7765 |
. . . . . . . . 9
⊢ (𝑔 ∈ (ℙ
↑𝑚 (1...3)) → 𝑔:(1...3)⟶ℙ) |
53 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → 𝑔:(1...3)⟶ℙ) |
54 | | 4z 11288 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℤ |
55 | | fzonel 12352 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬ 4
∈ (1..^4) |
56 | | fzoval 12340 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ∈
ℤ → (1..^4) = (1...(4 − 1))) |
57 | 54, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1..^4) =
(1...(4 − 1)) |
58 | | 4cn 10975 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 4 ∈
ℂ |
59 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℂ |
60 | | 3cn 10972 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 ∈
ℂ |
61 | | 3p1e4 11030 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (3 + 1) =
4 |
62 | | subadd2 10164 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((4
∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ) → ((4
− 1) = 3 ↔ (3 + 1) = 4)) |
63 | 61, 62 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((4
∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ) → (4 −
1) = 3) |
64 | 58, 59, 60, 63 | mp3an 1416 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4
− 1) = 3 |
65 | 64 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1...(4
− 1)) = (1...3) |
66 | 57, 65 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1..^4) =
(1...3) |
67 | 66 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1...3) =
(1..^4) |
68 | 67 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (4 ∈
(1...3) ↔ 4 ∈ (1..^4)) |
69 | 55, 68 | mtbir 312 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ 4
∈ (1...3) |
70 | 54, 69 | pm3.2i 470 |
. . . . . . . . . . . . . . . . 17
⊢ (4 ∈
ℤ ∧ ¬ 4 ∈ (1...3)) |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → (4 ∈
ℤ ∧ ¬ 4 ∈ (1...3))) |
72 | | 3prm 15244 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℙ |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → 3 ∈
ℙ) |
74 | | fsnunf 6356 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:(1...3)⟶ℙ ∧ (4
∈ ℤ ∧ ¬ 4 ∈ (1...3)) ∧ 3 ∈ ℙ) →
(𝑔 ∪ {〈4,
3〉}):((1...3) ∪ {4})⟶ℙ) |
75 | 53, 71, 73, 74 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {〈4,
3〉}):((1...3) ∪ {4})⟶ℙ) |
76 | | fzval3 12404 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 ∈
ℤ → (1...4) = (1..^(4 + 1))) |
77 | 54, 76 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (1...4) =
(1..^(4 + 1)) |
78 | | 1z 11284 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℤ |
79 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ |
80 | | 1lt4 11076 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
4 |
81 | 79, 23, 80 | ltleii 10039 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ≤
4 |
82 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . 19
⊢ (4 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 4 ∈
ℤ ∧ 1 ≤ 4)) |
83 | 78, 54, 81, 82 | mpbir3an 1237 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
(ℤ≥‘1) |
84 | | fzosplitsn 12442 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 ∈
(ℤ≥‘1) → (1..^(4 + 1)) = ((1..^4) ∪
{4})) |
85 | 83, 84 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (1..^(4 +
1)) = ((1..^4) ∪ {4}) |
86 | 66 | uneq1i 3725 |
. . . . . . . . . . . . . . . . 17
⊢ ((1..^4)
∪ {4}) = ((1...3) ∪ {4}) |
87 | 77, 85, 86 | 3eqtri 2636 |
. . . . . . . . . . . . . . . 16
⊢ (1...4) =
((1...3) ∪ {4}) |
88 | 87 | feq2i 5950 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∪ {〈4,
3〉}):(1...4)⟶ℙ ↔ (𝑔 ∪ {〈4, 3〉}):((1...3) ∪
{4})⟶ℙ) |
89 | 75, 88 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {〈4,
3〉}):(1...4)⟶ℙ) |
90 | | prmex 15229 |
. . . . . . . . . . . . . . . 16
⊢ ℙ
∈ V |
91 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ (1...4)
∈ V |
92 | 90, 91 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (ℙ
∈ V ∧ (1...4) ∈ V) |
93 | | elmapg 7757 |
. . . . . . . . . . . . . . 15
⊢ ((ℙ
∈ V ∧ (1...4) ∈ V) → ((𝑔 ∪ {〈4, 3〉}) ∈ (ℙ
↑𝑚 (1...4)) ↔ (𝑔 ∪ {〈4,
3〉}):(1...4)⟶ℙ)) |
94 | 92, 93 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4, 3〉})
∈ (ℙ ↑𝑚 (1...4)) ↔ (𝑔 ∪ {〈4,
3〉}):(1...4)⟶ℙ)) |
95 | 89, 94 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {〈4, 3〉})
∈ (ℙ ↑𝑚 (1...4))) |
96 | 95 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (𝑔 ∪ {〈4, 3〉}) ∈ (ℙ
↑𝑚 (1...4))) |
97 | | fveq1 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑔 ∪ {〈4, 3〉}) → (𝑓‘𝑘) = ((𝑔 ∪ {〈4, 3〉})‘𝑘)) |
98 | 97 | sumeq2sdv 14282 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑔 ∪ {〈4, 3〉}) →
Σ𝑘 ∈
(1...4)(𝑓‘𝑘) = Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4, 3〉})‘𝑘)) |
99 | 98 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑔 ∪ {〈4, 3〉}) → (𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘) ↔ 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4, 3〉})‘𝑘))) |
100 | 99 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) ∧ 𝑓 = (𝑔 ∪ {〈4, 3〉})) → (𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘) ↔ 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4, 3〉})‘𝑘))) |
101 | 83 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → 4 ∈
(ℤ≥‘1)) |
102 | 87 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...4) ↔ 𝑘 ∈ ((1...3) ∪
{4})) |
103 | | elun 3715 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((1...3) ∪ {4})
↔ (𝑘 ∈ (1...3)
∨ 𝑘 ∈
{4})) |
104 | | velsn 4141 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ {4} ↔ 𝑘 = 4) |
105 | 104 | orbi2i 540 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ (1...3) ∨ 𝑘 ∈ {4}) ↔ (𝑘 ∈ (1...3) ∨ 𝑘 = 4)) |
106 | 102, 103,
105 | 3bitri 285 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (1...4) ↔ (𝑘 ∈ (1...3) ∨ 𝑘 = 4)) |
107 | | elfz2 12204 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (1...3) ↔ ((1
∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (1 ≤ 𝑘 ∧ 𝑘 ≤ 3))) |
108 | 20, 23 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (3 ∈
ℝ ∧ 4 ∈ ℝ) |
109 | | 3lt4 11074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 3 <
4 |
110 | | ltnle 9996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((3
∈ ℝ ∧ 4 ∈ ℝ) → (3 < 4 ↔ ¬ 4 ≤
3)) |
111 | 109, 110 | mpbii 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((3
∈ ℝ ∧ 4 ∈ ℝ) → ¬ 4 ≤ 3) |
112 | 108, 111 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ¬ 4
≤ 3 |
113 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 = 4 → (𝑘 ≤ 3 ↔ 4 ≤ 3)) |
114 | 113 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (4 =
𝑘 → (𝑘 ≤ 3 ↔ 4 ≤
3)) |
115 | 112, 114 | mtbiri 316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (4 =
𝑘 → ¬ 𝑘 ≤ 3) |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ ℤ → (4 =
𝑘 → ¬ 𝑘 ≤ 3)) |
117 | 116 | necon2ad 2797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ ℤ → (𝑘 ≤ 3 → 4 ≠ 𝑘)) |
118 | 117 | adantld 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ℤ → ((1 ≤
𝑘 ∧ 𝑘 ≤ 3) → 4 ≠ 𝑘)) |
119 | 118 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((1
∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((1 ≤ 𝑘 ∧ 𝑘 ≤ 3) → 4 ≠ 𝑘)) |
120 | 119 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((1
∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (1 ≤ 𝑘 ∧ 𝑘 ≤ 3)) → 4 ≠ 𝑘) |
121 | 107, 120 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ (1...3) → 4 ≠
𝑘) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
4 ≠ 𝑘) |
123 | | fvunsn 6350 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ≠
𝑘 → ((𝑔 ∪ {〈4,
3〉})‘𝑘) = (𝑔‘𝑘)) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
((𝑔 ∪ {〈4,
3〉})‘𝑘) = (𝑔‘𝑘)) |
125 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:(1...3)⟶ℙ ∧
𝑘 ∈ (1...3)) →
(𝑔‘𝑘) ∈ ℙ) |
126 | 125 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
(𝑔‘𝑘) ∈ ℙ) |
127 | | prmz 15227 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔‘𝑘) ∈ ℙ → (𝑔‘𝑘) ∈ ℤ) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
(𝑔‘𝑘) ∈ ℤ) |
129 | 128 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
(𝑔‘𝑘) ∈ ℂ) |
130 | 124, 129 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) →
((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ) |
131 | 130 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...3) → (𝑔:(1...3)⟶ℙ →
((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
132 | 131 | adantld 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...3) → ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
133 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 4 → ((𝑔 ∪ {〈4, 3〉})‘𝑘) = ((𝑔 ∪ {〈4,
3〉})‘4)) |
134 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:(1...3)⟶ℙ → 4
∈ ℤ) |
135 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:(1...3)⟶ℙ → 3
∈ ℤ) |
136 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑔:(1...3)⟶ℙ →
dom 𝑔 =
(1...3)) |
137 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑔 = (1...3) → (4
∈ dom 𝑔 ↔ 4
∈ (1...3))) |
138 | 69, 137 | mtbiri 316 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (dom
𝑔 = (1...3) → ¬ 4
∈ dom 𝑔) |
139 | 136, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:(1...3)⟶ℙ →
¬ 4 ∈ dom 𝑔) |
140 | | fsnunfv 6358 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((4
∈ ℤ ∧ 3 ∈ ℤ ∧ ¬ 4 ∈ dom 𝑔) → ((𝑔 ∪ {〈4, 3〉})‘4) =
3) |
141 | 134, 135,
139, 140 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔:(1...3)⟶ℙ →
((𝑔 ∪ {〈4,
3〉})‘4) = 3) |
142 | 141 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4,
3〉})‘4) = 3) |
143 | 133, 142 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 = 4 ∧ (𝑁 ∈ (ℤ≥‘;12) ∧ 𝑔:(1...3)⟶ℙ)) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) =
3) |
144 | 143, 60 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 = 4 ∧ (𝑁 ∈ (ℤ≥‘;12) ∧ 𝑔:(1...3)⟶ℙ)) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ) |
145 | 144 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 4 → ((𝑁 ∈ (ℤ≥‘;12) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
146 | 132, 145 | jaoi 393 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ (1...3) ∨ 𝑘 = 4) → ((𝑁 ∈ (ℤ≥‘;12) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
147 | 146 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑘 ∈ (1...3) ∨ 𝑘 = 4) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
148 | 106, 147 | syl5bi 231 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → (𝑘 ∈ (1...4) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ)) |
149 | 148 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...4)) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) ∈
ℂ) |
150 | 101, 149,
133 | fsumm1 14324 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4,
3〉})‘𝑘) =
(Σ𝑘 ∈ (1...(4
− 1))((𝑔 ∪
{〈4, 3〉})‘𝑘) + ((𝑔 ∪ {〈4,
3〉})‘4))) |
151 | 150 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4, 3〉})‘𝑘) = (Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘) +
((𝑔 ∪ {〈4,
3〉})‘4))) |
152 | 64 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 3 = (4
− 1) |
153 | 152 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1...3) =
(1...(4 − 1)) |
154 | 153 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → (1...3) =
(1...(4 − 1))) |
155 | 121 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → 4 ≠
𝑘) |
156 | 155, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → ((𝑔 ∪ {〈4,
3〉})‘𝑘) = (𝑔‘𝑘)) |
157 | 156 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → (𝑔‘𝑘) = ((𝑔 ∪ {〈4, 3〉})‘𝑘)) |
158 | 154, 157 | sumeq12dv 14284 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → Σ𝑘 ∈ (1...3)(𝑔‘𝑘) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘)) |
159 | 158 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) ↔ (𝑁 − 3) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘))) |
160 | 159 | biimpa 500 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (𝑁 − 3) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘)) |
161 | 160 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘) = (𝑁 − 3)) |
162 | 161 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {〈4,
3〉})‘𝑘) +
((𝑔 ∪ {〈4,
3〉})‘4)) = ((𝑁
− 3) + ((𝑔 ∪
{〈4, 3〉})‘4))) |
163 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → 4 ∈
ℤ) |
164 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → 3 ∈
ℤ) |
165 | 139 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ¬ 4
∈ dom 𝑔) |
166 | 163, 164,
165, 140 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {〈4,
3〉})‘4) = 3) |
167 | 166 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + ((𝑔 ∪ {〈4,
3〉})‘4)) = ((𝑁
− 3) + 3)) |
168 | | eluzelcn 11575 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ 𝑁 ∈
ℂ) |
169 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ 3 ∈ ℂ) |
170 | 168, 169 | npcand 10275 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ ((𝑁 − 3) + 3)
= 𝑁) |
171 | 170 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + 3) = 𝑁) |
172 | 167, 171 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + ((𝑔 ∪ {〈4,
3〉})‘4)) = 𝑁) |
173 | 172 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → ((𝑁 − 3) + ((𝑔 ∪ {〈4, 3〉})‘4)) = 𝑁) |
174 | 151, 162,
173 | 3eqtrrd 2649 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {〈4, 3〉})‘𝑘)) |
175 | 96, 100, 174 | rspcedvd 3289 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → ∃𝑓 ∈ (ℙ ↑𝑚
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)) |
176 | 175 | ex 449 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |
177 | 176 | expcom 450 |
. . . . . . . . 9
⊢ (𝑔:(1...3)⟶ℙ →
(𝑁 ∈
(ℤ≥‘;12)
→ ((𝑁 − 3) =
Σ𝑘 ∈
(1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ
↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))) |
178 | 52, 177 | syl 17 |
. . . . . . . 8
⊢ (𝑔 ∈ (ℙ
↑𝑚 (1...3)) → (𝑁 ∈ (ℤ≥‘;12) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))) |
179 | 178 | com12 32 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ (𝑔 ∈ (ℙ
↑𝑚 (1...3)) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))) |
180 | 179 | rexlimdv 3012 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ (∃𝑔 ∈
(ℙ ↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |
181 | 180 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ (∃𝑔 ∈
(ℙ ↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |
182 | 181 | ad3antlr 763 |
. . . 4
⊢
((((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
∧ 𝑜 ∈
GoldbachOddALTV ) ∧ 𝑁 =
(𝑜 + 3)) →
(∃𝑔 ∈ (ℙ
↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚
(1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |
183 | 51, 182 | mpd 15 |
. . 3
⊢
((((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
∧ 𝑜 ∈
GoldbachOddALTV ) ∧ 𝑁 =
(𝑜 + 3)) →
∃𝑓 ∈ (ℙ
↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)) |
184 | | evengpoap3 40215 |
. . . 4
⊢
(∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) →
((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ ∃𝑜 ∈
GoldbachOddALTV 𝑁 = (𝑜 + 3))) |
185 | 184 | imp 444 |
. . 3
⊢
((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
→ ∃𝑜 ∈
GoldbachOddALTV 𝑁 = (𝑜 + 3)) |
186 | 183, 185 | r19.29a 3060 |
. 2
⊢
((∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ∧
(𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ))
→ ∃𝑓 ∈
(ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)) |
187 | 186 | ex 449 |
1
⊢
(∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) →
((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ ∃𝑓 ∈
(ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) |