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 ... 𝑑 ) ( 𝑓𝑘 ) )