Metamath Proof Explorer


Theorem nnsum3primesgbe

Description: Any even Goldbach number is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020)

Ref Expression
Assertion nnsum3primesgbe ( 𝑁 ∈ GoldbachEven → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 isgbe ( 𝑁 ∈ GoldbachEven ↔ ( 𝑁 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) )
2 2nn 2 ∈ ℕ
3 2 a1i ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → 2 ∈ ℕ )
4 oveq2 ( 𝑑 = 2 → ( 1 ... 𝑑 ) = ( 1 ... 2 ) )
5 df-2 2 = ( 1 + 1 )
6 5 oveq2i ( 1 ... 2 ) = ( 1 ... ( 1 + 1 ) )
7 1z 1 ∈ ℤ
8 fzpr ( 1 ∈ ℤ → ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } )
9 7 8 ax-mp ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) }
10 1p1e2 ( 1 + 1 ) = 2
11 10 preq2i { 1 , ( 1 + 1 ) } = { 1 , 2 }
12 6 9 11 3eqtri ( 1 ... 2 ) = { 1 , 2 }
13 4 12 eqtrdi ( 𝑑 = 2 → ( 1 ... 𝑑 ) = { 1 , 2 } )
14 13 oveq2d ( 𝑑 = 2 → ( ℙ ↑m ( 1 ... 𝑑 ) ) = ( ℙ ↑m { 1 , 2 } ) )
15 breq1 ( 𝑑 = 2 → ( 𝑑 ≤ 3 ↔ 2 ≤ 3 ) )
16 13 sumeq1d ( 𝑑 = 2 → Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) )
17 16 eqeq2d ( 𝑑 = 2 → ( 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ↔ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ) )
18 15 17 anbi12d ( 𝑑 = 2 → ( ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ↔ ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ) ) )
19 14 18 rexeqbidv ( 𝑑 = 2 → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ) ) )
20 19 adantl ( ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) ∧ 𝑑 = 2 ) → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ) ) )
21 1ne2 1 ≠ 2
22 1ex 1 ∈ V
23 2ex 2 ∈ V
24 vex 𝑝 ∈ V
25 vex 𝑞 ∈ V
26 22 23 24 25 fpr ( 1 ≠ 2 → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } : { 1 , 2 } ⟶ { 𝑝 , 𝑞 } )
27 21 26 mp1i ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } : { 1 , 2 } ⟶ { 𝑝 , 𝑞 } )
28 prssi ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → { 𝑝 , 𝑞 } ⊆ ℙ )
29 27 28 fssd ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } : { 1 , 2 } ⟶ ℙ )
30 prmex ℙ ∈ V
31 prex { 1 , 2 } ∈ V
32 30 31 pm3.2i ( ℙ ∈ V ∧ { 1 , 2 } ∈ V )
33 elmapg ( ( ℙ ∈ V ∧ { 1 , 2 } ∈ V ) → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ∈ ( ℙ ↑m { 1 , 2 } ) ↔ { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } : { 1 , 2 } ⟶ ℙ ) )
34 32 33 mp1i ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ∈ ( ℙ ↑m { 1 , 2 } ) ↔ { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } : { 1 , 2 } ⟶ ℙ ) )
35 29 34 mpbird ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ∈ ( ℙ ↑m { 1 , 2 } ) )
36 fveq1 ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } → ( 𝑓𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) )
37 36 adantr ( ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ∧ 𝑘 ∈ { 1 , 2 } ) → ( 𝑓𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) )
38 37 sumeq2dv ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } → Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) )
39 38 eqeq1d ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } → ( Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) ↔ Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) )
40 39 anbi2d ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } → ( ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) ) ↔ ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
41 40 adantl ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ) → ( ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) ) ↔ ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
42 prmz ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
43 prmz ( 𝑞 ∈ ℙ → 𝑞 ∈ ℤ )
44 fveq2 ( 𝑘 = 1 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 1 ) )
45 22 24 fvpr1 ( 1 ≠ 2 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 1 ) = 𝑝 )
46 21 45 ax-mp ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 1 ) = 𝑝
47 44 46 eqtrdi ( 𝑘 = 1 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = 𝑝 )
48 fveq2 ( 𝑘 = 2 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 2 ) )
49 23 25 fvpr2 ( 1 ≠ 2 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 2 ) = 𝑞 )
50 21 49 ax-mp ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 2 ) = 𝑞
51 48 50 eqtrdi ( 𝑘 = 2 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = 𝑞 )
52 zcn ( 𝑝 ∈ ℤ → 𝑝 ∈ ℂ )
53 zcn ( 𝑞 ∈ ℤ → 𝑞 ∈ ℂ )
54 52 53 anim12i ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ ) )
55 7 2 pm3.2i ( 1 ∈ ℤ ∧ 2 ∈ ℕ )
56 55 a1i ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 1 ∈ ℤ ∧ 2 ∈ ℕ ) )
57 21 a1i ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → 1 ≠ 2 )
58 47 51 54 56 57 sumpr ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) )
59 42 43 58 syl2an ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) )
60 2re 2 ∈ ℝ
61 3re 3 ∈ ℝ
62 2lt3 2 < 3
63 60 61 62 ltleii 2 ≤ 3
64 59 63 jctil ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) )
65 35 41 64 rspcedvd ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) ) )
66 65 adantr ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) ) )
67 eqeq1 ( 𝑁 = ( 𝑝 + 𝑞 ) → ( 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ↔ ( 𝑝 + 𝑞 ) = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ) )
68 eqcom ( ( 𝑝 + 𝑞 ) = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ↔ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) )
69 67 68 bitrdi ( 𝑁 = ( 𝑝 + 𝑞 ) → ( 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ↔ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) ) )
70 69 anbi2d ( 𝑁 = ( 𝑝 + 𝑞 ) → ( ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ) ↔ ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
71 70 rexbidv ( 𝑁 = ( 𝑝 + 𝑞 ) → ( ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
72 71 3ad2ant3 ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) → ( ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
73 72 adantl ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ( ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
74 66 73 mpbird ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓𝑘 ) ) )
75 3 20 74 rspcedvd ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )
76 75 a1d ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ( 𝑁 ∈ Even → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
77 76 ex ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) → ( 𝑁 ∈ Even → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) ) )
78 77 rexlimivv ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) → ( 𝑁 ∈ Even → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
79 78 impcom ( ( 𝑁 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )
80 1 79 sylbi ( 𝑁 ∈ GoldbachEven → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )