This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnsum3primes4

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

Ref Expression
Assertion nnsum3primes4 ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 1ne2 ⊢ 1 ≠ 2
3 1ex ⊢ 1 ∈ V
4 2ex ⊢ 2 ∈ V
5 3 4 4 4 fpr ⊢ ( 1 ≠ 2 → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } : { 1 , 2 } ⟶ { 2 , 2 } )
6 2prm ⊢ 2 ∈ ℙ
7 6 6 pm3.2i ⊢ ( 2 ∈ ℙ ∧ 2 ∈ ℙ )
8 4 4 prss ⊢ ( ( 2 ∈ ℙ ∧ 2 ∈ ℙ ) ↔ { 2 , 2 } ⊆ ℙ )
9 7 8 mpbi ⊢ { 2 , 2 } ⊆ ℙ
10 fss ⊢ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } : { 1 , 2 } ⟶ { 2 , 2 } ∧ { 2 , 2 } ⊆ ℙ ) → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } : { 1 , 2 } ⟶ ℙ )
11 9 10 mpan2 ⊢ ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } : { 1 , 2 } ⟶ { 2 , 2 } → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } : { 1 , 2 } ⟶ ℙ )
12 2 5 11 mp2b ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } : { 1 , 2 } ⟶ ℙ
13 prmex ⊢ ℙ ∈ V
14 prex ⊢ { 1 , 2 } ∈ V
15 13 14 elmap ⊢ ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( ℙ ↑m { 1 , 2 } ) ↔ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } : { 1 , 2 } ⟶ ℙ )
16 12 15 mpbir ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( ℙ ↑m { 1 , 2 } )
17 2re ⊢ 2 ∈ ℝ
18 3re ⊢ 3 ∈ ℝ
19 2lt3 ⊢ 2 < 3
20 17 18 19 ltleii ⊢ 2 ≤ 3
21 2cn ⊢ 2 ∈ ℂ
22 fveq2 ⊢ ( 𝑘 = 1 → ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 1 ) )
23 3 4 fvpr1 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 1 ) = 2 )
24 2 23 ax-mp ⊢ ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 1 ) = 2
25 22 24 eqtrdi ⊢ ( 𝑘 = 1 → ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) = 2 )
26 fveq2 ⊢ ( 𝑘 = 2 → ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 2 ) )
27 4 4 fvpr2 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 2 ) = 2 )
28 2 27 ax-mp ⊢ ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 2 ) = 2
29 26 28 eqtrdi ⊢ ( 𝑘 = 2 → ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) = 2 )
30 id ⊢ ( 2 ∈ ℂ → 2 ∈ ℂ )
31 30 ancri ⊢ ( 2 ∈ ℂ → ( 2 ∈ ℂ ∧ 2 ∈ ℂ ) )
32 3 jctl ⊢ ( 2 ∈ ℂ → ( 1 ∈ V ∧ 2 ∈ ℂ ) )
33 2 a1i ⊢ ( 2 ∈ ℂ → 1 ≠ 2 )
34 25 29 31 32 33 sumpr ⊢ ( 2 ∈ ℂ → Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) = ( 2 + 2 ) )
35 21 34 ax-mp ⊢ Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) = ( 2 + 2 )
36 2p2e4 ⊢ ( 2 + 2 ) = 4
37 35 36 eqtr2i ⊢ 4 = Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 )
38 20 37 pm3.2i ⊢ ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) )
39 fveq1 ⊢ ( 𝑓 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } → ( 𝑓 ‘ 𝑘 ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) )
40 39 sumeq2sdv ⊢ ( 𝑓 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } → Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) )
41 40 eqeq2d ⊢ ( 𝑓 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } → ( 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ↔ 4 = Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) ) )
42 41 anbi2d ⊢ ( 𝑓 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } → ( ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ↔ ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) ) ) )
43 42 rspcev ⊢ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( ℙ ↑m { 1 , 2 } ) ∧ ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑘 ) ) ) → ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) )
44 16 38 43 mp2an ⊢ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) )
45 oveq2 ⊢ ( 𝑑 = 2 → ( 1 ... 𝑑 ) = ( 1 ... 2 ) )
46 df-2 ⊢ 2 = ( 1 + 1 )
47 46 oveq2i ⊢ ( 1 ... 2 ) = ( 1 ... ( 1 + 1 ) )
48 1z ⊢ 1 ∈ ℤ
49 fzpr ⊢ ( 1 ∈ ℤ → ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } )
50 48 49 ax-mp ⊢ ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) }
51 1p1e2 ⊢ ( 1 + 1 ) = 2
52 51 preq2i ⊢ { 1 , ( 1 + 1 ) } = { 1 , 2 }
53 50 52 eqtri ⊢ ( 1 ... ( 1 + 1 ) ) = { 1 , 2 }
54 47 53 eqtri ⊢ ( 1 ... 2 ) = { 1 , 2 }
55 45 54 eqtrdi ⊢ ( 𝑑 = 2 → ( 1 ... 𝑑 ) = { 1 , 2 } )
56 55 oveq2d ⊢ ( 𝑑 = 2 → ( ℙ ↑m ( 1 ... 𝑑 ) ) = ( ℙ ↑m { 1 , 2 } ) )
57 breq1 ⊢ ( 𝑑 = 2 → ( 𝑑 ≤ 3 ↔ 2 ≤ 3 ) )
58 55 sumeq1d ⊢ ( 𝑑 = 2 → Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) )
59 58 eqeq2d ⊢ ( 𝑑 = 2 → ( 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ↔ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) )
60 57 59 anbi12d ⊢ ( 𝑑 = 2 → ( ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) )
61 56 60 rexeqbidv ⊢ ( 𝑑 = 2 → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) )
62 61 rspcev ⊢ ( ( 2 ∈ ℕ ∧ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
63 1 44 62 mp2an ⊢ ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) )