nnsum4primeseven

Description: If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of 4 primes. (Contributed by AV, 25-Jul-2020)

		Ref	Expression
	Assertion	nnsum4primeseven	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to ((N \in ℤ_{\geq 9} \land N \in Even) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k))$

Proof

Step	Hyp	Ref	Expression
1		evengpop3	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to ((N \in ℤ_{\geq 9} \land N \in Even) \to \exists o \in GoldbachOddW N = o + 3)$
2	1	imp	$⊢ (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \to \exists o \in GoldbachOddW N = o + 3$
3		simplll	$⊢ (((\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \land o \in GoldbachOddW) \land N = o + 3) \to \forall m \in Odd (5 < m \to m \in GoldbachOddW)$
4		6nn	$⊢ 6 \in ℕ$
5	4	nnzi	$⊢ 6 \in ℤ$
6	5	a1i	$⊢ N \in ℤ_{\geq 9} \to 6 \in ℤ$
7		3z	$⊢ 3 \in ℤ$
8	7	a1i	$⊢ N \in ℤ_{\geq 9} \to 3 \in ℤ$
9		6p3e9	$⊢ 6 + 3 = 9$
10	9	eqcomi	$⊢ 9 = 6 + 3$
11	10	fveq2i	$⊢ ℤ_{\geq 9} = ℤ_{\geq (6 + 3)}$
12	11	eleq2i	$⊢ N \in ℤ_{\geq 9} \leftrightarrow N \in ℤ_{\geq (6 + 3)}$
13	12	biimpi	$⊢ N \in ℤ_{\geq 9} \to N \in ℤ_{\geq (6 + 3)}$
14		eluzsub	$⊢ (6 \in ℤ \land 3 \in ℤ \land N \in ℤ_{\geq (6 + 3)}) \to N - 3 \in ℤ_{\geq 6}$
15	6 8 13 14	syl3anc	$⊢ N \in ℤ_{\geq 9} \to N - 3 \in ℤ_{\geq 6}$
16	15	adantr	$⊢ (N \in ℤ_{\geq 9} \land N \in Even) \to N - 3 \in ℤ_{\geq 6}$
17	16	ad3antlr	$⊢ (((\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \land o \in GoldbachOddW) \land N = o + 3) \to N - 3 \in ℤ_{\geq 6}$
18		3odd	$⊢ 3 \in Odd$
19	18	a1i	$⊢ N \in ℤ_{\geq 9} \to 3 \in Odd$
20	19	anim1i	$⊢ (N \in ℤ_{\geq 9} \land N \in Even) \to (3 \in Odd \land N \in Even)$
21	20	adantl	$⊢ (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \to (3 \in Odd \land N \in Even)$
22	21	ancomd	$⊢ (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \to (N \in Even \land 3 \in Odd)$
23	22	adantr	$⊢ ((\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \land o \in GoldbachOddW) \to (N \in Even \land 3 \in Odd)$
24	23	adantr	$⊢ (((\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \land o \in GoldbachOddW) \land N = o + 3) \to (N \in Even \land 3 \in Odd)$
25		emoo	$⊢ (N \in Even \land 3 \in Odd) \to N - 3 \in Odd$
26	24 25	syl	$⊢ (((\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \land o \in GoldbachOddW) \land N = o + 3) \to N - 3 \in Odd$
27		nnsum4primesodd	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to ((N - 3 \in ℤ_{\geq 6} \land N - 3 \in Odd) \to \exists g \in (ℙ^{(1 \dots 3)}) N - 3 = \sum_{k = 1}^{3} g (k))$
28	27	imp	$⊢ (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N - 3 \in ℤ_{\geq 6} \land N - 3 \in Odd)) \to \exists g \in (ℙ^{(1 \dots 3)}) N - 3 = \sum_{k = 1}^{3} g (k)$
29	3 17 26 28	syl12anc	$⊢ (((\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \land o \in GoldbachOddW) \land N = o + 3) \to \exists g \in (ℙ^{(1 \dots 3)}) N - 3 = \sum_{k = 1}^{3} g (k)$
30		simpr	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to g : (1 \dots 3) ⟶ ℙ$
31		4z	$⊢ 4 \in ℤ$
32		fzonel	$⊢ \neg 4 \in (1 ..^4)$
33		fzoval	$⊢ 4 \in ℤ \to (1 ..^4) = (1 \dots 4 - 1)$
34	31 33	ax-mp	$⊢ (1 ..^4) = (1 \dots 4 - 1)$
35		4cn	$⊢ 4 \in ℂ$
36		ax-1cn	$⊢ 1 \in ℂ$
37		3cn	$⊢ 3 \in ℂ$
38	35 36 37	3pm3.2i	$⊢ (4 \in ℂ \land 1 \in ℂ \land 3 \in ℂ)$
39		3p1e4	$⊢ 3 + 1 = 4$
40		subadd2	$⊢ (4 \in ℂ \land 1 \in ℂ \land 3 \in ℂ) \to (4 - 1 = 3 \leftrightarrow 3 + 1 = 4)$
41	39 40	mpbiri	$⊢ (4 \in ℂ \land 1 \in ℂ \land 3 \in ℂ) \to 4 - 1 = 3$
42	38 41	ax-mp	$⊢ 4 - 1 = 3$
43	42	oveq2i	$⊢ (1 \dots 4 - 1) = (1 \dots 3)$
44	34 43	eqtri	$⊢ (1 ..^4) = (1 \dots 3)$
45	44	eqcomi	$⊢ (1 \dots 3) = (1 ..^4)$
46	45	eleq2i	$⊢ 4 \in (1 \dots 3) \leftrightarrow 4 \in (1 ..^4)$
47	32 46	mtbir	$⊢ \neg 4 \in (1 \dots 3)$
48	31 47	pm3.2i	$⊢ (4 \in ℤ \land \neg 4 \in (1 \dots 3))$
49	48	a1i	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (4 \in ℤ \land \neg 4 \in (1 \dots 3))$
50		3prm	$⊢ 3 \in ℙ$
51	50	a1i	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to 3 \in ℙ$
52		fsnunf	$⊢ (g : (1 \dots 3) ⟶ ℙ \land (4 \in ℤ \land \neg 4 \in (1 \dots 3)) \land 3 \in ℙ) \to (g \cup \{⟨4, 3⟩\}) : (1 \dots 3) \cup \{4\} ⟶ ℙ$
53	30 49 51 52	syl3anc	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (g \cup \{⟨4, 3⟩\}) : (1 \dots 3) \cup \{4\} ⟶ ℙ$
54		fzval3	$⊢ 4 \in ℤ \to (1 \dots 4) = (1 ..^4 + 1)$
55	31 54	ax-mp	$⊢ (1 \dots 4) = (1 ..^4 + 1)$
56		1z	$⊢ 1 \in ℤ$
57		1re	$⊢ 1 \in ℝ$
58		4re	$⊢ 4 \in ℝ$
59		1lt4	$⊢ 1 < 4$
60	57 58 59	ltleii	$⊢ 1 \leq 4$
61		eluz2	$⊢ 4 \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land 4 \in ℤ \land 1 \leq 4)$
62	56 31 60 61	mpbir3an	$⊢ 4 \in ℤ_{\geq 1}$
63		fzosplitsn	$⊢ 4 \in ℤ_{\geq 1} \to (1 ..^4 + 1) = (1 ..^4) \cup \{4\}$
64	62 63	ax-mp	$⊢ (1 ..^4 + 1) = (1 ..^4) \cup \{4\}$
65	44	uneq1i	$⊢ (1 ..^4) \cup \{4\} = (1 \dots 3) \cup \{4\}$
66	55 64 65	3eqtri	$⊢ (1 \dots 4) = (1 \dots 3) \cup \{4\}$
67	66	feq2i	$⊢ (g \cup \{⟨4, 3⟩\}) : (1 \dots 4) ⟶ ℙ \leftrightarrow (g \cup \{⟨4, 3⟩\}) : (1 \dots 3) \cup \{4\} ⟶ ℙ$
68	53 67	sylibr	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (g \cup \{⟨4, 3⟩\}) : (1 \dots 4) ⟶ ℙ$
69		prmex	$⊢ ℙ \in V$
70		ovex	$⊢ (1 \dots 4) \in V$
71	69 70	pm3.2i	$⊢ (ℙ \in V \land (1 \dots 4) \in V)$
72		elmapg	$⊢ (ℙ \in V \land (1 \dots 4) \in V) \to (g \cup \{⟨4, 3⟩\} \in (ℙ^{(1 \dots 4)}) \leftrightarrow (g \cup \{⟨4, 3⟩\}) : (1 \dots 4) ⟶ ℙ)$
73	71 72	mp1i	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (g \cup \{⟨4, 3⟩\} \in (ℙ^{(1 \dots 4)}) \leftrightarrow (g \cup \{⟨4, 3⟩\}) : (1 \dots 4) ⟶ ℙ)$
74	68 73	mpbird	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to g \cup \{⟨4, 3⟩\} \in (ℙ^{(1 \dots 4)})$
75	74	adantr	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land N - 3 = \sum_{k = 1}^{3} g (k)) \to g \cup \{⟨4, 3⟩\} \in (ℙ^{(1 \dots 4)})$
76		fveq1	$⊢ f = g \cup \{⟨4, 3⟩\} \to f (k) = (g \cup \{⟨4, 3⟩\}) (k)$
77	76	adantr	$⊢ (f = g \cup \{⟨4, 3⟩\} \land k \in (1 \dots 4)) \to f (k) = (g \cup \{⟨4, 3⟩\}) (k)$
78	77	sumeq2dv	$⊢ f = g \cup \{⟨4, 3⟩\} \to \sum_{k = 1}^{4} f (k) = \sum_{k = 1}^{4} (g \cup \{⟨4, 3⟩\}) (k)$
79	78	eqeq2d	$⊢ f = g \cup \{⟨4, 3⟩\} \to (N = \sum_{k = 1}^{4} f (k) \leftrightarrow N = \sum_{k = 1}^{4} (g \cup \{⟨4, 3⟩\}) (k))$
80	79	adantl	$⊢ (((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land N - 3 = \sum_{k = 1}^{3} g (k)) \land f = g \cup \{⟨4, 3⟩\}) \to (N = \sum_{k = 1}^{4} f (k) \leftrightarrow N = \sum_{k = 1}^{4} (g \cup \{⟨4, 3⟩\}) (k))$
81	62	a1i	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to 4 \in ℤ_{\geq 1}$
82	66	eleq2i	$⊢ k \in (1 \dots 4) \leftrightarrow k \in ((1 \dots 3) \cup \{4\})$
83		elun	$⊢ k \in ((1 \dots 3) \cup \{4\}) \leftrightarrow (k \in (1 \dots 3) \lor k \in \{4\})$
84		velsn	$⊢ k \in \{4\} \leftrightarrow k = 4$
85	84	orbi2i	$⊢ (k \in (1 \dots 3) \lor k \in \{4\}) \leftrightarrow (k \in (1 \dots 3) \lor k = 4)$
86	82 83 85	3bitri	$⊢ k \in (1 \dots 4) \leftrightarrow (k \in (1 \dots 3) \lor k = 4)$
87		elfz2	$⊢ k \in (1 \dots 3) \leftrightarrow ((1 \in ℤ \land 3 \in ℤ \land k \in ℤ) \land (1 \leq k \land k \leq 3))$
88		3re	$⊢ 3 \in ℝ$
89	88 58	pm3.2i	$⊢ (3 \in ℝ \land 4 \in ℝ)$
90		3lt4	$⊢ 3 < 4$
91		ltnle	$⊢ (3 \in ℝ \land 4 \in ℝ) \to (3 < 4 \leftrightarrow \neg 4 \leq 3)$
92	90 91	mpbii	$⊢ (3 \in ℝ \land 4 \in ℝ) \to \neg 4 \leq 3$
93	89 92	ax-mp	$⊢ \neg 4 \leq 3$
94		breq1	$⊢ k = 4 \to (k \leq 3 \leftrightarrow 4 \leq 3)$
95	94	eqcoms	$⊢ 4 = k \to (k \leq 3 \leftrightarrow 4 \leq 3)$
96	93 95	mtbiri	$⊢ 4 = k \to \neg k \leq 3$
97	96	a1i	$⊢ k \in ℤ \to (4 = k \to \neg k \leq 3)$
98	97	necon2ad	$⊢ k \in ℤ \to (k \leq 3 \to 4 \neq k)$
99	98	adantld	$⊢ k \in ℤ \to ((1 \leq k \land k \leq 3) \to 4 \neq k)$
100	99	3ad2ant3	$⊢ (1 \in ℤ \land 3 \in ℤ \land k \in ℤ) \to ((1 \leq k \land k \leq 3) \to 4 \neq k)$
101	100	imp	$⊢ ((1 \in ℤ \land 3 \in ℤ \land k \in ℤ) \land (1 \leq k \land k \leq 3)) \to 4 \neq k$
102	87 101	sylbi	$⊢ k \in (1 \dots 3) \to 4 \neq k$
103	102	adantr	$⊢ (k \in (1 \dots 3) \land g : (1 \dots 3) ⟶ ℙ) \to 4 \neq k$
104		fvunsn	$⊢ 4 \neq k \to (g \cup \{⟨4, 3⟩\}) (k) = g (k)$
105	103 104	syl	$⊢ (k \in (1 \dots 3) \land g : (1 \dots 3) ⟶ ℙ) \to (g \cup \{⟨4, 3⟩\}) (k) = g (k)$
106		ffvelrn	$⊢ (g : (1 \dots 3) ⟶ ℙ \land k \in (1 \dots 3)) \to g (k) \in ℙ$
107	106	ancoms	$⊢ (k \in (1 \dots 3) \land g : (1 \dots 3) ⟶ ℙ) \to g (k) \in ℙ$
108		prmz	$⊢ g (k) \in ℙ \to g (k) \in ℤ$
109	107 108	syl	$⊢ (k \in (1 \dots 3) \land g : (1 \dots 3) ⟶ ℙ) \to g (k) \in ℤ$
110	109	zcnd	$⊢ (k \in (1 \dots 3) \land g : (1 \dots 3) ⟶ ℙ) \to g (k) \in ℂ$
111	105 110	eqeltrd	$⊢ (k \in (1 \dots 3) \land g : (1 \dots 3) ⟶ ℙ) \to (g \cup \{⟨4, 3⟩\}) (k) \in ℂ$
112	111	ex	$⊢ k \in (1 \dots 3) \to (g : (1 \dots 3) ⟶ ℙ \to (g \cup \{⟨4, 3⟩\}) (k) \in ℂ)$
113	112	adantld	$⊢ k \in (1 \dots 3) \to ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (g \cup \{⟨4, 3⟩\}) (k) \in ℂ)$
114		fveq2	$⊢ k = 4 \to (g \cup \{⟨4, 3⟩\}) (k) = (g \cup \{⟨4, 3⟩\}) (4)$
115	31	a1i	$⊢ g : (1 \dots 3) ⟶ ℙ \to 4 \in ℤ$
116	7	a1i	$⊢ g : (1 \dots 3) ⟶ ℙ \to 3 \in ℤ$
117		fdm	$⊢ g : (1 \dots 3) ⟶ ℙ \to dom g = (1 \dots 3)$
118		eleq2	$⊢ dom g = (1 \dots 3) \to (4 \in dom g \leftrightarrow 4 \in (1 \dots 3))$
119	47 118	mtbiri	$⊢ dom g = (1 \dots 3) \to \neg 4 \in dom g$
120	117 119	syl	$⊢ g : (1 \dots 3) ⟶ ℙ \to \neg 4 \in dom g$
121		fsnunfv	$⊢ (4 \in ℤ \land 3 \in ℤ \land \neg 4 \in dom g) \to (g \cup \{⟨4, 3⟩\}) (4) = 3$
122	115 116 120 121	syl3anc	$⊢ g : (1 \dots 3) ⟶ ℙ \to (g \cup \{⟨4, 3⟩\}) (4) = 3$
123	122	adantl	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (g \cup \{⟨4, 3⟩\}) (4) = 3$
124	114 123	sylan9eq	$⊢ (k = 4 \land (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ)) \to (g \cup \{⟨4, 3⟩\}) (k) = 3$
125	124 37	eqeltrdi	$⊢ (k = 4 \land (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ)) \to (g \cup \{⟨4, 3⟩\}) (k) \in ℂ$
126	125	ex	$⊢ k = 4 \to ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (g \cup \{⟨4, 3⟩\}) (k) \in ℂ)$
127	113 126	jaoi	$⊢ (k \in (1 \dots 3) \lor k = 4) \to ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (g \cup \{⟨4, 3⟩\}) (k) \in ℂ)$
128	127	com12	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to ((k \in (1 \dots 3) \lor k = 4) \to (g \cup \{⟨4, 3⟩\}) (k) \in ℂ)$
129	86 128	syl5bi	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (k \in (1 \dots 4) \to (g \cup \{⟨4, 3⟩\}) (k) \in ℂ)$
130	129	imp	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land k \in (1 \dots 4)) \to (g \cup \{⟨4, 3⟩\}) (k) \in ℂ$
131	81 130 114	fsumm1	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to \sum_{k = 1}^{4} (g \cup \{⟨4, 3⟩\}) (k) = \sum_{k = 1}^{4 - 1} (g \cup \{⟨4, 3⟩\}) (k) + (g \cup \{⟨4, 3⟩\}) (4)$
132	131	adantr	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land N - 3 = \sum_{k = 1}^{3} g (k)) \to \sum_{k = 1}^{4} (g \cup \{⟨4, 3⟩\}) (k) = \sum_{k = 1}^{4 - 1} (g \cup \{⟨4, 3⟩\}) (k) + (g \cup \{⟨4, 3⟩\}) (4)$
133	42	eqcomi	$⊢ 3 = 4 - 1$
134	133	oveq2i	$⊢ (1 \dots 3) = (1 \dots 4 - 1)$
135	134	a1i	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (1 \dots 3) = (1 \dots 4 - 1)$
136	102	adantl	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land k \in (1 \dots 3)) \to 4 \neq k$
137	136 104	syl	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land k \in (1 \dots 3)) \to (g \cup \{⟨4, 3⟩\}) (k) = g (k)$
138	137	eqcomd	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land k \in (1 \dots 3)) \to g (k) = (g \cup \{⟨4, 3⟩\}) (k)$
139	135 138	sumeq12dv	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to \sum_{k = 1}^{3} g (k) = \sum_{k = 1}^{4 - 1} (g \cup \{⟨4, 3⟩\}) (k)$
140	139	eqeq2d	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (N - 3 = \sum_{k = 1}^{3} g (k) \leftrightarrow N - 3 = \sum_{k = 1}^{4 - 1} (g \cup \{⟨4, 3⟩\}) (k))$
141	140	biimpa	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land N - 3 = \sum_{k = 1}^{3} g (k)) \to N - 3 = \sum_{k = 1}^{4 - 1} (g \cup \{⟨4, 3⟩\}) (k)$
142	141	eqcomd	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land N - 3 = \sum_{k = 1}^{3} g (k)) \to \sum_{k = 1}^{4 - 1} (g \cup \{⟨4, 3⟩\}) (k) = N - 3$
143	142	oveq1d	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land N - 3 = \sum_{k = 1}^{3} g (k)) \to \sum_{k = 1}^{4 - 1} (g \cup \{⟨4, 3⟩\}) (k) + (g \cup \{⟨4, 3⟩\}) (4) = N - 3 + (g \cup \{⟨4, 3⟩\}) (4)$
144	31	a1i	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to 4 \in ℤ$
145	7	a1i	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to 3 \in ℤ$
146	120	adantl	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to \neg 4 \in dom g$
147	144 145 146 121	syl3anc	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (g \cup \{⟨4, 3⟩\}) (4) = 3$
148	147	oveq2d	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to N - 3 + (g \cup \{⟨4, 3⟩\}) (4) = N - 3 + 3$
149		eluzelcn	$⊢ N \in ℤ_{\geq 9} \to N \in ℂ$
150	37	a1i	$⊢ N \in ℤ_{\geq 9} \to 3 \in ℂ$
151	149 150	npcand	$⊢ N \in ℤ_{\geq 9} \to N - 3 + 3 = N$
152	151	adantr	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to N - 3 + 3 = N$
153	148 152	eqtrd	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to N - 3 + (g \cup \{⟨4, 3⟩\}) (4) = N$
154	153	adantr	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land N - 3 = \sum_{k = 1}^{3} g (k)) \to N - 3 + (g \cup \{⟨4, 3⟩\}) (4) = N$
155	132 143 154	3eqtrrd	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land N - 3 = \sum_{k = 1}^{3} g (k)) \to N = \sum_{k = 1}^{4} (g \cup \{⟨4, 3⟩\}) (k)$
156	75 80 155	rspcedvd	$⊢ ((N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \land N - 3 = \sum_{k = 1}^{3} g (k)) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k)$
157	156	ex	$⊢ (N \in ℤ_{\geq 9} \land g : (1 \dots 3) ⟶ ℙ) \to (N - 3 = \sum_{k = 1}^{3} g (k) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k))$
158	157	expcom	$⊢ g : (1 \dots 3) ⟶ ℙ \to (N \in ℤ_{\geq 9} \to (N - 3 = \sum_{k = 1}^{3} g (k) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k)))$
159		elmapi	$⊢ g \in (ℙ^{(1 \dots 3)}) \to g : (1 \dots 3) ⟶ ℙ$
160	158 159	syl11	$⊢ N \in ℤ_{\geq 9} \to (g \in (ℙ^{(1 \dots 3)}) \to (N - 3 = \sum_{k = 1}^{3} g (k) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k)))$
161	160	rexlimdv	$⊢ N \in ℤ_{\geq 9} \to (\exists g \in (ℙ^{(1 \dots 3)}) N - 3 = \sum_{k = 1}^{3} g (k) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k))$
162	161	adantr	$⊢ (N \in ℤ_{\geq 9} \land N \in Even) \to (\exists g \in (ℙ^{(1 \dots 3)}) N - 3 = \sum_{k = 1}^{3} g (k) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k))$
163	162	ad3antlr	$⊢ (((\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \land o \in GoldbachOddW) \land N = o + 3) \to (\exists g \in (ℙ^{(1 \dots 3)}) N - 3 = \sum_{k = 1}^{3} g (k) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k))$
164	29 163	mpd	$⊢ (((\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \land o \in GoldbachOddW) \land N = o + 3) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k)$
165	164	rexlimdva2	$⊢ (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \to (\exists o \in GoldbachOddW N = o + 3 \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k))$
166	2 165	mpd	$⊢ (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land (N \in ℤ_{\geq 9} \land N \in Even)) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k)$
167	166	ex	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to ((N \in ℤ_{\geq 9} \land N \in Even) \to \exists f \in (ℙ^{(1 \dots 4)}) N = \sum_{k = 1}^{4} f (k))$

Metamath Proof Explorer

Theorem nnsum4primeseven

Proof