Theorem nnsum3primes4 38920

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

Assertion

Ref	Expression
nnsum3primes4	|- E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) )

Distinct variable group:   f, d, k

Proof of Theorem nnsum3primes4

Step	Hyp	Ref	Expression
1		2nn 10795	. 2 |- 2 e. NN
2		1ne2 10850	. . . . 5 |- 1 =/= 2
3		1ex 9663	. . . . . 6 |- 1 e. _V
4		2ex 10708	. . . . . 6 |- 2 e. _V
5	3, 4, 4, 4	fpr 6095	. . . . 5 |- ( 1 =/= 2 -> { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> { 2 , 2 } )
6		2prm 14688	. . . . . . . 8 |- 2 e. Prime
7	6, 6	pm3.2i 461	. . . . . . 7 |- ( 2 e. Prime /\ 2 e. Prime )
8	4, 4	prss 4138	. . . . . . 7 |- ( ( 2 e. Prime /\ 2 e. Prime ) <-> { 2 , 2 } C_ Prime )
9	7, 8	mpbi 213	. . . . . 6 |- { 2 , 2 } C_ Prime
10		fss 5759	. . . . . 6 |- ( ( { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> { 2 , 2 } /\ { 2 , 2 } C_ Prime ) -> { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> Prime )
11	9, 10	mpan2 682	. . . . 5 |- ( { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> { 2 , 2 } -> { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> Prime )
12	2, 5, 11	mp2b 10	. . . 4 |- { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> Prime
13		prmex 14676	. . . . 5 |- Prime e. _V
14		prex 4655	. . . . 5 |- { 1 , 2 } e. _V
15	13, 14	elmap 7525	. . . 4 |- ( { <. 1 , 2 >. , <. 2 , 2 >. } e. ( Prime ^m { 1 , 2 } ) <-> { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> Prime )
16	12, 15	mpbir 214	. . 3 |- { <. 1 , 2 >. , <. 2 , 2 >. } e. ( Prime ^m { 1 , 2 } )
17		2re 10706	. . . . 5 |- 2 e. RR
18		3re 10710	. . . . 5 |- 3 e. RR
19		2lt3 10805	. . . . 5 |- 2 < 3
20	17, 18, 19	ltleii 9782	. . . 4 |- 2 <_ 3
21		2cn 10707	. . . . . 6 |- 2 e. CC
22		fveq2 5887	. . . . . . . 8 |- ( k = 1 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 1 ) )
23	3, 4	fvpr1 6130	. . . . . . . . 9 |- ( 1 =/= 2 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 1 ) = 2 )
24	2, 23	ax-mp 5	. . . . . . . 8 |- ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 1 ) = 2
25	22, 24	syl6eq 2511	. . . . . . 7 |- ( k = 1 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = 2 )
26		fveq2 5887	. . . . . . . 8 |- ( k = 2 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 2 ) )
27	4, 4	fvpr2 6131	. . . . . . . . 9 |- ( 1 =/= 2 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 2 ) = 2 )
28	2, 27	ax-mp 5	. . . . . . . 8 |- ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 2 ) = 2
29	26, 28	syl6eq 2511	. . . . . . 7 |- ( k = 2 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = 2 )
30		id 22	. . . . . . . 8 |- ( 2 e. CC -> 2 e. CC )
31	30	ancri 559	. . . . . . 7 |- ( 2 e. CC -> ( 2 e. CC /\ 2 e. CC ) )
32	3	jctl 548	. . . . . . 7 |- ( 2 e. CC -> ( 1 e. _V /\ 2 e. CC ) )
33	2	a1i 11	. . . . . . 7 |- ( 2 e. CC -> 1 =/= 2 )
34	25, 29, 31, 32, 33	sumpr 13857	. . . . . 6 |- ( 2 e. CC -> sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = ( 2 + 2 ) )
35	21, 34	ax-mp 5	. . . . 5 |- sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = ( 2 + 2 )
36		2p2e4 10755	. . . . 5 |- ( 2 + 2 ) = 4
37	35, 36	eqtr2i 2484	. . . 4 |- 4 = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k )
38	20, 37	pm3.2i 461	. . 3 |- ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) )
39		fveq1 5886	. . . . . . 7 |- ( f = { <. 1 , 2 >. , <. 2 , 2 >. } -> ( f ` k ) = ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) )
40	39	sumeq2sdv 13818	. . . . . 6 |- ( f = { <. 1 , 2 >. , <. 2 , 2 >. } -> sum_ k e. { 1 , 2 } ( f ` k ) = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) )
41	40	eqeq2d 2471	. . . . 5 |- ( f = { <. 1 , 2 >. , <. 2 , 2 >. } -> ( 4 = sum_ k e. { 1 , 2 } ( f ` k ) <-> 4 = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) ) )
42	41	anbi2d 715	. . . 4 |- ( f = { <. 1 , 2 >. , <. 2 , 2 >. } -> ( ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) <-> ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) ) ) )
43	42	rspcev 3161	. . 3 |- ( ( { <. 1 , 2 >. , <. 2 , 2 >. } e. ( Prime ^m { 1 , 2 } ) /\ ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) ) ) -> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) )
44	16, 38, 43	mp2an 683	. 2 |- E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) )
45		oveq2 6322	. . . . . 6 |- ( d = 2 -> ( 1 ... d ) = ( 1 ... 2 ) )
46		df-2 10695	. . . . . . . 8 |- 2 = ( 1 + 1 )
47	46	oveq2i 6325	. . . . . . 7 |- ( 1 ... 2 ) = ( 1 ... ( 1 + 1 ) )
48		1z 10995	. . . . . . . . 9 |- 1 e. ZZ
49		fzpr 11879	. . . . . . . . 9 |- ( 1 e. ZZ -> ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } )
50	48, 49	ax-mp 5	. . . . . . . 8 |- ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) }
51		1p1e2 10750	. . . . . . . . 9 |- ( 1 + 1 ) = 2
52	51	preq2i 4067	. . . . . . . 8 |- { 1 , ( 1 + 1 ) } = { 1 , 2 }
53	50, 52	eqtri 2483	. . . . . . 7 |- ( 1 ... ( 1 + 1 ) ) = { 1 , 2 }
54	47, 53	eqtri 2483	. . . . . 6 |- ( 1 ... 2 ) = { 1 , 2 }
55	45, 54	syl6eq 2511	. . . . 5 |- ( d = 2 -> ( 1 ... d ) = { 1 , 2 } )
56	55	oveq2d 6330	. . . 4 |- ( d = 2 -> ( Prime ^m ( 1 ... d ) ) = ( Prime ^m { 1 , 2 } ) )
57		breq1 4418	. . . . 5 |- ( d = 2 -> ( d <_ 3 <-> 2 <_ 3 ) )
58	55	sumeq1d 13815	. . . . . 6 |- ( d = 2 -> sum_ k e. ( 1 ... d ) ( f ` k ) = sum_ k e. { 1 , 2 } ( f ` k ) )
59	58	eqeq2d 2471	. . . . 5 |- ( d = 2 -> ( 4 = sum_ k e. ( 1 ... d ) ( f ` k ) <-> 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) )
60	57, 59	anbi12d 722	. . . 4 |- ( d = 2 -> ( ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) ) )
61	56, 60	rexeqbidv 3013	. . 3 |- ( d = 2 -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) ) )
62	61	rspcev 3161	. 2 |- ( ( 2 e. NN /\ E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
63	1, 44, 62	mp2an 683	1 |- E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) )

Syntax hints:   /\ wa 375   = wceq 1454   e. wcel 1897   =/= wne 2632   E.wrex 2749   _Vcvv 3056   C_ wss 3415   {cpr 3981   <.cop 3985   class class class wbr 4415   -->wf 5596   ` cfv 5600  (class class class)co 6314   ^m cmap 7497   CCcc 9562   1c1 9565   + caddc 9567   <_ cle 9701   NNcn 10636   2c2 10686   3c3 10687   4c4 10688   ZZcz 10965   ...cfz 11812   sum_csu 13800   Primecprime 14670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-inf2 8171  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641  ax-pre-sup 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-fal 1460  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-2o 7208  df-oadd 7211  df-er 7388  df-map 7499  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-sup 7981  df-oi 8050  df-card 8398  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-div 10297  df-nn 10637  df-2 10695  df-3 10696  df-4 10697  df-n0 10898  df-z 10966  df-uz 11188  df-rp 11331  df-fz 11813  df-fzo 11946  df-seq 12245  df-exp 12304  df-hash 12547  df-cj 13210  df-re 13211  df-im 13212  df-sqrt 13346  df-abs 13347  df-clim 13600  df-sum 13801  df-dvds 14354  df-prm 14671

This theorem is referenced by:  nnsum4primes4  38921  nnsum3primesle9  38926