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