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