nnsum4primesevenALTV

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

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

Proof

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

Metamath Proof Explorer

Theorem nnsum4primesevenALTV

Proof