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

Metamath Proof Explorer

Theorem nnsum3primesprm

Description: Every prime is "the sum of at most 3" (actually one - the prime itself) primes. (Contributed by AV, 2-Aug-2020) (Proof shortened by AV, 17-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 1nn ⊢ 1 ∈ ℕ
2 1zzd ⊢ ( 𝑃 ∈ ℙ → 1 ∈ ℤ )
3 id ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℙ )
4 2 3 fsnd ⊢ ( 𝑃 ∈ ℙ → { ⟨ 1 , 𝑃 ⟩ } : { 1 } ⟶ ℙ )
5 prmex ⊢ ℙ ∈ V
6 snex ⊢ { 1 } ∈ V
7 5 6 elmap ⊢ ( { ⟨ 1 , 𝑃 ⟩ } ∈ ( ℙ ↑m { 1 } ) ↔ { ⟨ 1 , 𝑃 ⟩ } : { 1 } ⟶ ℙ )
8 4 7 sylibr ⊢ ( 𝑃 ∈ ℙ → { ⟨ 1 , 𝑃 ⟩ } ∈ ( ℙ ↑m { 1 } ) )
9 1re ⊢ 1 ∈ ℝ
10 simpl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ { 1 } ) → 𝑃 ∈ ℙ )
11 fvsng ⊢ ( ( 1 ∈ ℝ ∧ 𝑃 ∈ ℙ ) → ( { ⟨ 1 , 𝑃 ⟩ } ‘ 1 ) = 𝑃 )
12 9 10 11 sylancr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ { 1 } ) → ( { ⟨ 1 , 𝑃 ⟩ } ‘ 1 ) = 𝑃 )
13 12 sumeq2dv ⊢ ( 𝑃 ∈ ℙ → Σ 𝑘 ∈ { 1 } ( { ⟨ 1 , 𝑃 ⟩ } ‘ 1 ) = Σ 𝑘 ∈ { 1 } 𝑃 )
14 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
15 14 zcnd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
16 eqidd ⊢ ( 𝑘 = 1 → 𝑃 = 𝑃 )
17 16 sumsn ⊢ ( ( 1 ∈ ℝ ∧ 𝑃 ∈ ℂ ) → Σ 𝑘 ∈ { 1 } 𝑃 = 𝑃 )
18 9 15 17 sylancr ⊢ ( 𝑃 ∈ ℙ → Σ 𝑘 ∈ { 1 } 𝑃 = 𝑃 )
19 13 18 eqtr2d ⊢ ( 𝑃 ∈ ℙ → 𝑃 = Σ 𝑘 ∈ { 1 } ( { ⟨ 1 , 𝑃 ⟩ } ‘ 1 ) )
20 1le3 ⊢ 1 ≤ 3
21 19 20 jctil ⊢ ( 𝑃 ∈ ℙ → ( 1 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ { 1 } ( { ⟨ 1 , 𝑃 ⟩ } ‘ 1 ) ) )
22 simpl ⊢ ( ( 𝑓 = { ⟨ 1 , 𝑃 ⟩ } ∧ 𝑘 ∈ { 1 } ) → 𝑓 = { ⟨ 1 , 𝑃 ⟩ } )
23 elsni ⊢ ( 𝑘 ∈ { 1 } → 𝑘 = 1 )
24 23 adantl ⊢ ( ( 𝑓 = { ⟨ 1 , 𝑃 ⟩ } ∧ 𝑘 ∈ { 1 } ) → 𝑘 = 1 )
25 22 24 fveq12d ⊢ ( ( 𝑓 = { ⟨ 1 , 𝑃 ⟩ } ∧ 𝑘 ∈ { 1 } ) → ( 𝑓 ‘ 𝑘 ) = ( { ⟨ 1 , 𝑃 ⟩ } ‘ 1 ) )
26 25 sumeq2dv ⊢ ( 𝑓 = { ⟨ 1 , 𝑃 ⟩ } → Σ 𝑘 ∈ { 1 } ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ { 1 } ( { ⟨ 1 , 𝑃 ⟩ } ‘ 1 ) )
27 26 eqeq2d ⊢ ( 𝑓 = { ⟨ 1 , 𝑃 ⟩ } → ( 𝑃 = Σ 𝑘 ∈ { 1 } ( 𝑓 ‘ 𝑘 ) ↔ 𝑃 = Σ 𝑘 ∈ { 1 } ( { ⟨ 1 , 𝑃 ⟩ } ‘ 1 ) ) )
28 27 anbi2d ⊢ ( 𝑓 = { ⟨ 1 , 𝑃 ⟩ } → ( ( 1 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ { 1 } ( 𝑓 ‘ 𝑘 ) ) ↔ ( 1 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ { 1 } ( { ⟨ 1 , 𝑃 ⟩ } ‘ 1 ) ) ) )
29 28 rspcev ⊢ ( ( { ⟨ 1 , 𝑃 ⟩ } ∈ ( ℙ ↑m { 1 } ) ∧ ( 1 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ { 1 } ( { ⟨ 1 , 𝑃 ⟩ } ‘ 1 ) ) ) → ∃ 𝑓 ∈ ( ℙ ↑m { 1 } ) ( 1 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ { 1 } ( 𝑓 ‘ 𝑘 ) ) )
30 8 21 29 syl2anc ⊢ ( 𝑃 ∈ ℙ → ∃ 𝑓 ∈ ( ℙ ↑m { 1 } ) ( 1 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ { 1 } ( 𝑓 ‘ 𝑘 ) ) )
31 oveq2 ⊢ ( 𝑑 = 1 → ( 1 ... 𝑑 ) = ( 1 ... 1 ) )
32 1z ⊢ 1 ∈ ℤ
33 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
34 32 33 ax-mp ⊢ ( 1 ... 1 ) = { 1 }
35 31 34 eqtrdi ⊢ ( 𝑑 = 1 → ( 1 ... 𝑑 ) = { 1 } )
36 35 oveq2d ⊢ ( 𝑑 = 1 → ( ℙ ↑m ( 1 ... 𝑑 ) ) = ( ℙ ↑m { 1 } ) )
37 breq1 ⊢ ( 𝑑 = 1 → ( 𝑑 ≤ 3 ↔ 1 ≤ 3 ) )
38 35 sumeq1d ⊢ ( 𝑑 = 1 → Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ { 1 } ( 𝑓 ‘ 𝑘 ) )
39 38 eqeq2d ⊢ ( 𝑑 = 1 → ( 𝑃 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ↔ 𝑃 = Σ 𝑘 ∈ { 1 } ( 𝑓 ‘ 𝑘 ) ) )
40 37 39 anbi12d ⊢ ( 𝑑 = 1 → ( ( 𝑑 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 1 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ { 1 } ( 𝑓 ‘ 𝑘 ) ) ) )
41 36 40 rexeqbidv ⊢ ( 𝑑 = 1 → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 } ) ( 1 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ { 1 } ( 𝑓 ‘ 𝑘 ) ) ) )
42 41 rspcev ⊢ ( ( 1 ∈ ℕ ∧ ∃ 𝑓 ∈ ( ℙ ↑m { 1 } ) ( 1 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ { 1 } ( 𝑓 ‘ 𝑘 ) ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
43 1 30 42 sylancr ⊢ ( 𝑃 ∈ ℙ → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑃 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )