Step | Hyp | Ref
| Expression |
1 | | breq2 5044 |
. . . . . 6
⊢ (𝑚 = 𝑁 → (7 < 𝑚 ↔ 7 < 𝑁)) |
2 | | eleq1 2821 |
. . . . . 6
⊢ (𝑚 = 𝑁 → (𝑚 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd )) |
3 | 1, 2 | imbi12d 348 |
. . . . 5
⊢ (𝑚 = 𝑁 → ((7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ↔ (7 < 𝑁 → 𝑁 ∈ GoldbachOdd ))) |
4 | 3 | rspcv 3524 |
. . . 4
⊢ (𝑁 ∈ Odd →
(∀𝑚 ∈ Odd (7
< 𝑚 → 𝑚 ∈ GoldbachOdd ) → (7
< 𝑁 → 𝑁 ∈ GoldbachOdd
))) |
5 | 4 | adantl 485 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘8) ∧ 𝑁 ∈ Odd ) → (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → (7 < 𝑁 → 𝑁 ∈ GoldbachOdd ))) |
6 | | eluz2 12342 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘8) ↔ (8 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 8 ≤
𝑁)) |
7 | | 7lt8 11920 |
. . . . . . . . 9
⊢ 7 <
8 |
8 | | 7re 11821 |
. . . . . . . . . . 11
⊢ 7 ∈
ℝ |
9 | 8 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 7 ∈
ℝ) |
10 | | 8re 11824 |
. . . . . . . . . . 11
⊢ 8 ∈
ℝ |
11 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 8 ∈
ℝ) |
12 | | zre 12078 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
13 | | ltletr 10822 |
. . . . . . . . . 10
⊢ ((7
∈ ℝ ∧ 8 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((7 < 8 ∧ 8
≤ 𝑁) → 7 < 𝑁)) |
14 | 9, 11, 12, 13 | syl3anc 1372 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → ((7 <
8 ∧ 8 ≤ 𝑁) → 7
< 𝑁)) |
15 | 7, 14 | mpani 696 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (8 ≤
𝑁 → 7 < 𝑁)) |
16 | 15 | imp 410 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 8 ≤
𝑁) → 7 < 𝑁) |
17 | 16 | 3adant1 1131 |
. . . . . 6
⊢ ((8
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 8 ≤ 𝑁) → 7 < 𝑁) |
18 | 6, 17 | sylbi 220 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘8) → 7 < 𝑁) |
19 | 18 | adantr 484 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘8) ∧ 𝑁 ∈ Odd ) → 7 < 𝑁) |
20 | | pm2.27 42 |
. . . 4
⊢ (7 <
𝑁 → ((7 < 𝑁 → 𝑁 ∈ GoldbachOdd ) → 𝑁 ∈ GoldbachOdd
)) |
21 | 19, 20 | syl 17 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘8) ∧ 𝑁 ∈ Odd ) → ((7 < 𝑁 → 𝑁 ∈ GoldbachOdd ) → 𝑁 ∈ GoldbachOdd
)) |
22 | | isgbo 44786 |
. . . . 5
⊢ (𝑁 ∈ GoldbachOdd ↔
(𝑁 ∈ Odd ∧
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
∃𝑟 ∈ ℙ
((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑁 = ((𝑝 + 𝑞) + 𝑟)))) |
23 | | 1ex 10727 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
V |
24 | | 2ex 11805 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
V |
25 | | 3ex 11810 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
V |
26 | | vex 3404 |
. . . . . . . . . . . . . . . 16
⊢ 𝑝 ∈ V |
27 | | vex 3404 |
. . . . . . . . . . . . . . . 16
⊢ 𝑞 ∈ V |
28 | | vex 3404 |
. . . . . . . . . . . . . . . 16
⊢ 𝑟 ∈ V |
29 | | 1ne2 11936 |
. . . . . . . . . . . . . . . 16
⊢ 1 ≠
2 |
30 | | 1re 10731 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ |
31 | | 1lt3 11901 |
. . . . . . . . . . . . . . . . 17
⊢ 1 <
3 |
32 | 30, 31 | ltneii 10843 |
. . . . . . . . . . . . . . . 16
⊢ 1 ≠
3 |
33 | | 2re 11802 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
34 | | 2lt3 11900 |
. . . . . . . . . . . . . . . . 17
⊢ 2 <
3 |
35 | 33, 34 | ltneii 10843 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≠
3 |
36 | 23, 24, 25, 26, 27, 28, 29, 32, 35 | ftp 6941 |
. . . . . . . . . . . . . . 15
⊢ {〈1,
𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}:{1, 2, 3}⟶{𝑝, 𝑞, 𝑟} |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) →
{〈1, 𝑝〉, 〈2,
𝑞〉, 〈3, 𝑟〉}:{1, 2, 3}⟶{𝑝, 𝑞, 𝑟}) |
38 | | 1p2e3 11871 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 + 2) =
3 |
39 | 38 | eqcomi 2748 |
. . . . . . . . . . . . . . . . 17
⊢ 3 = (1 +
2) |
40 | 39 | oveq2i 7193 |
. . . . . . . . . . . . . . . 16
⊢ (1...3) =
(1...(1 + 2)) |
41 | | 1z 12105 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ |
42 | | fztp 13066 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
ℤ → (1...(1 + 2)) = {1, (1 + 1), (1 + 2)}) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (1...(1 +
2)) = {1, (1 + 1), (1 + 2)} |
44 | | eqid 2739 |
. . . . . . . . . . . . . . . . 17
⊢ 1 =
1 |
45 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 = 1
→ 1 = 1) |
46 | | 1p1e2 11853 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 + 1) =
2 |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 = 1
→ (1 + 1) = 2) |
48 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 = 1
→ (1 + 2) = 3) |
49 | 45, 47, 48 | tpeq123d 4649 |
. . . . . . . . . . . . . . . . 17
⊢ (1 = 1
→ {1, (1 + 1), (1 + 2)} = {1, 2, 3}) |
50 | 44, 49 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ {1, (1 +
1), (1 + 2)} = {1, 2, 3} |
51 | 40, 43, 50 | 3eqtri 2766 |
. . . . . . . . . . . . . . 15
⊢ (1...3) =
{1, 2, 3} |
52 | 51 | feq2i 6506 |
. . . . . . . . . . . . . 14
⊢
({〈1, 𝑝〉,
〈2, 𝑞〉, 〈3,
𝑟〉}:(1...3)⟶{𝑝, 𝑞, 𝑟} ↔ {〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}:{1, 2, 3}⟶{𝑝, 𝑞, 𝑟}) |
53 | 37, 52 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) →
{〈1, 𝑝〉, 〈2,
𝑞〉, 〈3, 𝑟〉}:(1...3)⟶{𝑝, 𝑞, 𝑟}) |
54 | | df-3an 1090 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ) ↔ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈
ℙ)) |
55 | 26, 27, 28 | tpss 4733 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ) ↔ {𝑝, 𝑞, 𝑟} ⊆ ℙ) |
56 | 54, 55 | sylbb1 240 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → {𝑝, 𝑞, 𝑟} ⊆ ℙ) |
57 | 53, 56 | fssd 6532 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) →
{〈1, 𝑝〉, 〈2,
𝑞〉, 〈3, 𝑟〉}:(1...3)⟶ℙ) |
58 | | prmex 16130 |
. . . . . . . . . . . . . 14
⊢ ℙ
∈ V |
59 | | ovex 7215 |
. . . . . . . . . . . . . 14
⊢ (1...3)
∈ V |
60 | 58, 59 | pm3.2i 474 |
. . . . . . . . . . . . 13
⊢ (ℙ
∈ V ∧ (1...3) ∈ V) |
61 | | elmapg 8462 |
. . . . . . . . . . . . 13
⊢ ((ℙ
∈ V ∧ (1...3) ∈ V) → ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉} ∈ (ℙ ↑m
(1...3)) ↔ {〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}:(1...3)⟶ℙ)) |
62 | 60, 61 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) →
({〈1, 𝑝〉,
〈2, 𝑞〉, 〈3,
𝑟〉} ∈ (ℙ
↑m (1...3)) ↔ {〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}:(1...3)⟶ℙ)) |
63 | 57, 62 | mpbird 260 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) →
{〈1, 𝑝〉, 〈2,
𝑞〉, 〈3, 𝑟〉} ∈ (ℙ
↑m (1...3))) |
64 | | fveq1 6685 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = {〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉} → (𝑓‘𝑘) = ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘)) |
65 | 64 | sumeq2sdv 15166 |
. . . . . . . . . . . . 13
⊢ (𝑓 = {〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉} → Σ𝑘 ∈ (1...3)(𝑓‘𝑘) = Σ𝑘 ∈ (1...3)({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘)) |
66 | 65 | eqeq2d 2750 |
. . . . . . . . . . . 12
⊢ (𝑓 = {〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉} → (((𝑝 + 𝑞) + 𝑟) = Σ𝑘 ∈ (1...3)(𝑓‘𝑘) ↔ ((𝑝 + 𝑞) + 𝑟) = Σ𝑘 ∈ (1...3)({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘))) |
67 | 66 | adantl 485 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) ∧ 𝑓 = {〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}) → (((𝑝 + 𝑞) + 𝑟) = Σ𝑘 ∈ (1...3)(𝑓‘𝑘) ↔ ((𝑝 + 𝑞) + 𝑟) = Σ𝑘 ∈ (1...3)({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘))) |
68 | 51 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → (1...3)
= {1, 2, 3}) |
69 | 68 | sumeq1d 15163 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) →
Σ𝑘 ∈
(1...3)({〈1, 𝑝〉,
〈2, 𝑞〉, 〈3,
𝑟〉}‘𝑘) = Σ𝑘 ∈ {1, 2, 3} ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘)) |
70 | | fveq2 6686 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘) = ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘1)) |
71 | 23, 26 | fvtp1 6979 |
. . . . . . . . . . . . . . 15
⊢ ((1 ≠
2 ∧ 1 ≠ 3) → ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘1) = 𝑝) |
72 | 29, 32, 71 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
({〈1, 𝑝〉,
〈2, 𝑞〉, 〈3,
𝑟〉}‘1) = 𝑝 |
73 | 70, 72 | eqtrdi 2790 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘) = 𝑝) |
74 | | fveq2 6686 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 2 → ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘) = ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘2)) |
75 | 24, 27 | fvtp2 6980 |
. . . . . . . . . . . . . . 15
⊢ ((1 ≠
2 ∧ 2 ≠ 3) → ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘2) = 𝑞) |
76 | 29, 35, 75 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
({〈1, 𝑝〉,
〈2, 𝑞〉, 〈3,
𝑟〉}‘2) = 𝑞 |
77 | 74, 76 | eqtrdi 2790 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 2 → ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘) = 𝑞) |
78 | | fveq2 6686 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 3 → ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘) = ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘3)) |
79 | 25, 28 | fvtp3 6981 |
. . . . . . . . . . . . . . 15
⊢ ((1 ≠
3 ∧ 2 ≠ 3) → ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘3) = 𝑟) |
80 | 32, 35, 79 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
({〈1, 𝑝〉,
〈2, 𝑞〉, 〈3,
𝑟〉}‘3) = 𝑟 |
81 | 78, 80 | eqtrdi 2790 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 3 → ({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘) = 𝑟) |
82 | | prmz 16128 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
83 | 82 | zcnd 12181 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℂ) |
84 | | prmz 16128 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
85 | 84 | zcnd 12181 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℂ) |
86 | | prmz 16128 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ ℙ → 𝑟 ∈
ℤ) |
87 | 86 | zcnd 12181 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ ℙ → 𝑟 ∈
ℂ) |
88 | 83, 85, 87 | 3anim123i 1152 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ) → (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ ∧ 𝑟 ∈
ℂ)) |
89 | 88 | 3expa 1119 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ ∧ 𝑟 ∈
ℂ)) |
90 | | 2z 12107 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
91 | | 3z 12108 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℤ |
92 | 41, 90, 91 | 3pm3.2i 1340 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℤ ∧ 2 ∈ ℤ ∧ 3 ∈ ℤ) |
93 | 92 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → (1
∈ ℤ ∧ 2 ∈ ℤ ∧ 3 ∈ ℤ)) |
94 | 29 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → 1 ≠
2) |
95 | 32 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → 1 ≠
3) |
96 | 35 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → 2 ≠
3) |
97 | 73, 77, 81, 89, 93, 94, 95, 96 | sumtp 15209 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) →
Σ𝑘 ∈ {1, 2, 3}
({〈1, 𝑝〉,
〈2, 𝑞〉, 〈3,
𝑟〉}‘𝑘) = ((𝑝 + 𝑞) + 𝑟)) |
98 | 69, 97 | eqtr2d 2775 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → ((𝑝 + 𝑞) + 𝑟) = Σ𝑘 ∈ (1...3)({〈1, 𝑝〉, 〈2, 𝑞〉, 〈3, 𝑟〉}‘𝑘)) |
99 | 63, 67, 98 | rspcedvd 3532 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) →
∃𝑓 ∈ (ℙ
↑m (1...3))((𝑝 + 𝑞) + 𝑟) = Σ𝑘 ∈ (1...3)(𝑓‘𝑘)) |
100 | | eqeq1 2743 |
. . . . . . . . . . 11
⊢ (𝑁 = ((𝑝 + 𝑞) + 𝑟) → (𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘) ↔ ((𝑝 + 𝑞) + 𝑟) = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
101 | 100 | rexbidv 3208 |
. . . . . . . . . 10
⊢ (𝑁 = ((𝑝 + 𝑞) + 𝑟) → (∃𝑓 ∈ (ℙ ↑m
(1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘) ↔ ∃𝑓 ∈ (ℙ ↑m
(1...3))((𝑝 + 𝑞) + 𝑟) = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
102 | 99, 101 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → (𝑁 = ((𝑝 + 𝑞) + 𝑟) → ∃𝑓 ∈ (ℙ ↑m
(1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
103 | 102 | adantld 494 |
. . . . . . . 8
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑁 = ((𝑝 + 𝑞) + 𝑟)) → ∃𝑓 ∈ (ℙ ↑m
(1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
104 | 103 | rexlimdva 3195 |
. . . . . . 7
⊢ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) →
(∃𝑟 ∈ ℙ
((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑁 = ((𝑝 + 𝑞) + 𝑟)) → ∃𝑓 ∈ (ℙ ↑m
(1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
105 | 104 | rexlimivv 3203 |
. . . . . 6
⊢
(∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ ∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 𝑁 = ((𝑝 + 𝑞) + 𝑟)) → ∃𝑓 ∈ (ℙ ↑m
(1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘)) |
106 | 105 | adantl 485 |
. . . . 5
⊢ ((𝑁 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑁 = ((𝑝 + 𝑞) + 𝑟))) → ∃𝑓 ∈ (ℙ ↑m
(1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘)) |
107 | 22, 106 | sylbi 220 |
. . . 4
⊢ (𝑁 ∈ GoldbachOdd →
∃𝑓 ∈ (ℙ
↑m (1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘)) |
108 | 107 | a1i 11 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘8) ∧ 𝑁 ∈ Odd ) → (𝑁 ∈ GoldbachOdd → ∃𝑓 ∈ (ℙ
↑m (1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
109 | 5, 21, 108 | 3syld 60 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘8) ∧ 𝑁 ∈ Odd ) → (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ∃𝑓 ∈ (ℙ
↑m (1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
110 | 109 | com12 32 |
1
⊢
(∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) →
((𝑁 ∈
(ℤ≥‘8) ∧ 𝑁 ∈ Odd ) → ∃𝑓 ∈ (ℙ
↑m (1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |