bgoldbtbndlem4

	Ref	Expression
Hypotheses	bgoldbtbnd.m	$⊢ φ \to M \in ℤ_{\geq 11}$
	bgoldbtbnd.n	$⊢ φ \to N \in ℤ_{\geq 11}$
	bgoldbtbnd.b	$⊢ φ \to \forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven)$
	bgoldbtbnd.d	$⊢ φ \to D \in ℤ_{\geq 3}$
	bgoldbtbnd.f	$⊢ φ \to F \in RePart (D)$
	bgoldbtbnd.i	$⊢ φ \to \forall i \in (0 ..^D) (F (i) \in (ℙ ∖ \{2\}) \land F (i + 1) - F (i) < N - 4 \land 4 < F (i + 1) - F (i))$
	bgoldbtbnd.0	$⊢ φ \to F (0) = 7$
	bgoldbtbnd.1	$⊢ φ \to F (1) = 13$
	bgoldbtbnd.l	$⊢ φ \to M < F (D)$
	bgoldbtbnd.r	$⊢ φ \to F (D) \in ℝ$
Assertion	bgoldbtbndlem4	$⊢ ((φ \land I \in (1 ..^D)) \land X \in Odd) \to ((X \in [F (I), F (I + 1)) \land X - F (I) \leq 4) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))$

Proof

Step	Hyp	Ref	Expression
1		bgoldbtbnd.m	$⊢ φ \to M \in ℤ_{\geq 11}$
2		bgoldbtbnd.n	$⊢ φ \to N \in ℤ_{\geq 11}$
3		bgoldbtbnd.b	$⊢ φ \to \forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven)$
4		bgoldbtbnd.d	$⊢ φ \to D \in ℤ_{\geq 3}$
5		bgoldbtbnd.f	$⊢ φ \to F \in RePart (D)$
6		bgoldbtbnd.i	$⊢ φ \to \forall i \in (0 ..^D) (F (i) \in (ℙ ∖ \{2\}) \land F (i + 1) - F (i) < N - 4 \land 4 < F (i + 1) - F (i))$
7		bgoldbtbnd.0	$⊢ φ \to F (0) = 7$
8		bgoldbtbnd.1	$⊢ φ \to F (1) = 13$
9		bgoldbtbnd.l	$⊢ φ \to M < F (D)$
10		bgoldbtbnd.r	$⊢ φ \to F (D) \in ℝ$
11		simpll	$⊢ ((φ \land I \in (1 ..^D)) \land X \in Odd) \to φ$
12		simpr	$⊢ ((φ \land I \in (1 ..^D)) \land X \in Odd) \to X \in Odd$
13		simplr	$⊢ ((φ \land I \in (1 ..^D)) \land X \in Odd) \to I \in (1 ..^D)$
14		eqid	$⊢ X - F (I - 1) = X - F (I - 1)$
15	1 2 3 4 5 6 7 8 9 14	bgoldbtbndlem2	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to ((X \in [F (I), F (I + 1)) \land X - F (I) \leq 4) \to (X - F (I - 1) \in Even \land X - F (I - 1) < N \land 4 < X - F (I - 1)))$
16	11 12 13 15	syl3anc	$⊢ ((φ \land I \in (1 ..^D)) \land X \in Odd) \to ((X \in [F (I), F (I + 1)) \land X - F (I) \leq 4) \to (X - F (I - 1) \in Even \land X - F (I - 1) < N \land 4 < X - F (I - 1)))$
17		breq2	$⊢ n = m \to (4 < n \leftrightarrow 4 < m)$
18		breq1	$⊢ n = m \to (n < N \leftrightarrow m < N)$
19	17 18	anbi12d	$⊢ n = m \to ((4 < n \land n < N) \leftrightarrow (4 < m \land m < N))$
20		eleq1	$⊢ n = m \to (n \in GoldbachEven \leftrightarrow m \in GoldbachEven)$
21	19 20	imbi12d	$⊢ n = m \to (((4 < n \land n < N) \to n \in GoldbachEven) \leftrightarrow ((4 < m \land m < N) \to m \in GoldbachEven))$
22	21	cbvralvw	$⊢ \forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \leftrightarrow \forall m \in Even ((4 < m \land m < N) \to m \in GoldbachEven)$
23		breq2	$⊢ m = X - F (I - 1) \to (4 < m \leftrightarrow 4 < X - F (I - 1))$
24		breq1	$⊢ m = X - F (I - 1) \to (m < N \leftrightarrow X - F (I - 1) < N)$
25	23 24	anbi12d	$⊢ m = X - F (I - 1) \to ((4 < m \land m < N) \leftrightarrow (4 < X - F (I - 1) \land X - F (I - 1) < N))$
26		eleq1	$⊢ m = X - F (I - 1) \to (m \in GoldbachEven \leftrightarrow X - F (I - 1) \in GoldbachEven)$
27	25 26	imbi12d	$⊢ m = X - F (I - 1) \to (((4 < m \land m < N) \to m \in GoldbachEven) \leftrightarrow ((4 < X - F (I - 1) \land X - F (I - 1) < N) \to X - F (I - 1) \in GoldbachEven))$
28	27	rspcv	$⊢ X - F (I - 1) \in Even \to (\forall m \in Even ((4 < m \land m < N) \to m \in GoldbachEven) \to ((4 < X - F (I - 1) \land X - F (I - 1) < N) \to X - F (I - 1) \in GoldbachEven))$
29	22 28	biimtrid	$⊢ X - F (I - 1) \in Even \to (\forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \to ((4 < X - F (I - 1) \land X - F (I - 1) < N) \to X - F (I - 1) \in GoldbachEven))$
30		id	$⊢ ((4 < X - F (I - 1) \land X - F (I - 1) < N) \to X - F (I - 1) \in GoldbachEven) \to ((4 < X - F (I - 1) \land X - F (I - 1) < N) \to X - F (I - 1) \in GoldbachEven)$
31		isgbe	$⊢ X - F (I - 1) \in GoldbachEven \leftrightarrow (X - F (I - 1) \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q))$
32		simp1	$⊢ (F (i) \in (ℙ ∖ \{2\}) \land F (i + 1) - F (i) < N - 4 \land 4 < F (i + 1) - F (i)) \to F (i) \in (ℙ ∖ \{2\})$
33	32	ralimi	$⊢ \forall i \in (0 ..^D) (F (i) \in (ℙ ∖ \{2\}) \land F (i + 1) - F (i) < N - 4 \land 4 < F (i + 1) - F (i)) \to \forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\})$
34		elfzo1	$⊢ I \in (1 ..^D) \leftrightarrow (I \in ℕ \land D \in ℕ \land I < D)$
35		nnm1nn0	$⊢ I \in ℕ \to I - 1 \in ℕ_{0}$
36	35	3ad2ant1	$⊢ (I \in ℕ \land D \in ℕ \land I < D) \to I - 1 \in ℕ_{0}$
37	34 36	sylbi	$⊢ I \in (1 ..^D) \to I - 1 \in ℕ_{0}$
38	37	a1i	$⊢ D \in ℤ_{\geq 3} \to (I \in (1 ..^D) \to I - 1 \in ℕ_{0})$
39		eluz3nn	$⊢ D \in ℤ_{\geq 3} \to D \in ℕ$
40	39	a1d	$⊢ D \in ℤ_{\geq 3} \to (I \in (1 ..^D) \to D \in ℕ)$
41		elfzo2	$⊢ I \in (1 ..^D) \leftrightarrow (I \in ℤ_{\geq 1} \land D \in ℤ \land I < D)$
42		eluzelre	$⊢ I \in ℤ_{\geq 1} \to I \in ℝ$
43	42	adantr	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ) \to I \in ℝ$
44	43	ltm1d	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ) \to I - 1 < I$
45		1red	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ) \to 1 \in ℝ$
46	43 45	resubcld	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ) \to I - 1 \in ℝ$
47		zre	$⊢ D \in ℤ \to D \in ℝ$
48	47	adantl	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ) \to D \in ℝ$
49		lttr	$⊢ (I - 1 \in ℝ \land I \in ℝ \land D \in ℝ) \to ((I - 1 < I \land I < D) \to I - 1 < D)$
50	46 43 48 49	syl3anc	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ) \to ((I - 1 < I \land I < D) \to I - 1 < D)$
51	44 50	mpand	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ) \to (I < D \to I - 1 < D)$
52	51	3impia	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ \land I < D) \to I - 1 < D$
53	41 52	sylbi	$⊢ I \in (1 ..^D) \to I - 1 < D$
54	53	a1i	$⊢ D \in ℤ_{\geq 3} \to (I \in (1 ..^D) \to I - 1 < D)$
55	38 40 54	3jcad	$⊢ D \in ℤ_{\geq 3} \to (I \in (1 ..^D) \to (I - 1 \in ℕ_{0} \land D \in ℕ \land I - 1 < D))$
56	4 55	syl	$⊢ φ \to (I \in (1 ..^D) \to (I - 1 \in ℕ_{0} \land D \in ℕ \land I - 1 < D))$
57	56	imp	$⊢ (φ \land I \in (1 ..^D)) \to (I - 1 \in ℕ_{0} \land D \in ℕ \land I - 1 < D)$
58		elfzo0	$⊢ I - 1 \in (0 ..^D) \leftrightarrow (I - 1 \in ℕ_{0} \land D \in ℕ \land I - 1 < D)$
59	57 58	sylibr	$⊢ (φ \land I \in (1 ..^D)) \to I - 1 \in (0 ..^D)$
60		fveq2	$⊢ i = I - 1 \to F (i) = F (I - 1)$
61	60	eleq1d	$⊢ i = I - 1 \to (F (i) \in (ℙ ∖ \{2\}) \leftrightarrow F (I - 1) \in (ℙ ∖ \{2\}))$
62	61	rspcv	$⊢ I - 1 \in (0 ..^D) \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I - 1) \in (ℙ ∖ \{2\}))$
63	59 62	syl	$⊢ (φ \land I \in (1 ..^D)) \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I - 1) \in (ℙ ∖ \{2\}))$
64		eldifi	$⊢ F (I - 1) \in (ℙ ∖ \{2\}) \to F (I - 1) \in ℙ$
65	63 64	syl6	$⊢ (φ \land I \in (1 ..^D)) \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I - 1) \in ℙ)$
66	65	expcom	$⊢ I \in (1 ..^D) \to (φ \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I - 1) \in ℙ))$
67	66	com13	$⊢ \forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to (φ \to (I \in (1 ..^D) \to F (I - 1) \in ℙ))$
68	33 67	syl	$⊢ \forall i \in (0 ..^D) (F (i) \in (ℙ ∖ \{2\}) \land F (i + 1) - F (i) < N - 4 \land 4 < F (i + 1) - F (i)) \to (φ \to (I \in (1 ..^D) \to F (I - 1) \in ℙ))$
69	6 68	mpcom	$⊢ φ \to (I \in (1 ..^D) \to F (I - 1) \in ℙ)$
70	69	adantl	$⊢ (X - F (I - 1) \in Even \land φ) \to (I \in (1 ..^D) \to F (I - 1) \in ℙ)$
71	70	imp	$⊢ ((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \to F (I - 1) \in ℙ$
72	71	ad2antrr	$⊢ ((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \to F (I - 1) \in ℙ$
73	72	ad2antrr	$⊢ ((((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q)) \to F (I - 1) \in ℙ$
74		eleq1	$⊢ r = F (I - 1) \to (r \in Odd \leftrightarrow F (I - 1) \in Odd)$
75	74	3anbi3d	$⊢ r = F (I - 1) \to ((p \in Odd \land q \in Odd \land r \in Odd) \leftrightarrow (p \in Odd \land q \in Odd \land F (I - 1) \in Odd))$
76		oveq2	$⊢ r = F (I - 1) \to p + q + r = p + q + F (I - 1)$
77	76	eqeq2d	$⊢ r = F (I - 1) \to (X = p + q + r \leftrightarrow X = p + q + F (I - 1))$
78	75 77	anbi12d	$⊢ r = F (I - 1) \to (((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r) \leftrightarrow ((p \in Odd \land q \in Odd \land F (I - 1) \in Odd) \land X = p + q + F (I - 1)))$
79	78	adantl	$⊢ (((((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q)) \land r = F (I - 1)) \to (((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r) \leftrightarrow ((p \in Odd \land q \in Odd \land F (I - 1) \in Odd) \land X = p + q + F (I - 1)))$
80		oddprmALTV	$⊢ F (I - 1) \in (ℙ ∖ \{2\}) \to F (I - 1) \in Odd$
81	63 80	syl6	$⊢ (φ \land I \in (1 ..^D)) \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I - 1) \in Odd)$
82	81	expcom	$⊢ I \in (1 ..^D) \to (φ \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I - 1) \in Odd))$
83	82	com13	$⊢ \forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to (φ \to (I \in (1 ..^D) \to F (I - 1) \in Odd))$
84	33 83	syl	$⊢ \forall i \in (0 ..^D) (F (i) \in (ℙ ∖ \{2\}) \land F (i + 1) - F (i) < N - 4 \land 4 < F (i + 1) - F (i)) \to (φ \to (I \in (1 ..^D) \to F (I - 1) \in Odd))$
85	6 84	mpcom	$⊢ φ \to (I \in (1 ..^D) \to F (I - 1) \in Odd)$
86	85	adantl	$⊢ (X - F (I - 1) \in Even \land φ) \to (I \in (1 ..^D) \to F (I - 1) \in Odd)$
87	86	imp	$⊢ ((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \to F (I - 1) \in Odd$
88	87	ad3antrrr	$⊢ (((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \to F (I - 1) \in Odd$
89		3simpa	$⊢ (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q) \to (p \in Odd \land q \in Odd)$
90	88 89	anim12ci	$⊢ ((((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q)) \to ((p \in Odd \land q \in Odd) \land F (I - 1) \in Odd)$
91		df-3an	$⊢ (p \in Odd \land q \in Odd \land F (I - 1) \in Odd) \leftrightarrow ((p \in Odd \land q \in Odd) \land F (I - 1) \in Odd)$
92	90 91	sylibr	$⊢ ((((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q)) \to (p \in Odd \land q \in Odd \land F (I - 1) \in Odd)$
93		oddz	$⊢ X \in Odd \to X \in ℤ$
94	93	zcnd	$⊢ X \in Odd \to X \in ℂ$
95	94	adantl	$⊢ (((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \to X \in ℂ$
96	95	ad2antrr	$⊢ (((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \to X \in ℂ$
97	96	adantl	$⊢ ((p \in Odd \land q \in Odd) \land (((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ)) \to X \in ℂ$
98		prmz	$⊢ F (I - 1) \in ℙ \to F (I - 1) \in ℤ$
99	98	zcnd	$⊢ F (I - 1) \in ℙ \to F (I - 1) \in ℂ$
100	64 99	syl	$⊢ F (I - 1) \in (ℙ ∖ \{2\}) \to F (I - 1) \in ℂ$
101	63 100	syl6	$⊢ (φ \land I \in (1 ..^D)) \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I - 1) \in ℂ)$
102	101	expcom	$⊢ I \in (1 ..^D) \to (φ \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I - 1) \in ℂ))$
103	102	com13	$⊢ \forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to (φ \to (I \in (1 ..^D) \to F (I - 1) \in ℂ))$
104	33 103	syl	$⊢ \forall i \in (0 ..^D) (F (i) \in (ℙ ∖ \{2\}) \land F (i + 1) - F (i) < N - 4 \land 4 < F (i + 1) - F (i)) \to (φ \to (I \in (1 ..^D) \to F (I - 1) \in ℂ))$
105	6 104	mpcom	$⊢ φ \to (I \in (1 ..^D) \to F (I - 1) \in ℂ)$
106	105	adantl	$⊢ (X - F (I - 1) \in Even \land φ) \to (I \in (1 ..^D) \to F (I - 1) \in ℂ)$
107	106	imp	$⊢ ((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \to F (I - 1) \in ℂ$
108	107	ad3antrrr	$⊢ (((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \to F (I - 1) \in ℂ$
109	108	adantl	$⊢ ((p \in Odd \land q \in Odd) \land (((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ)) \to F (I - 1) \in ℂ$
110	97 109	npcand	$⊢ ((p \in Odd \land q \in Odd) \land (((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ)) \to X - F (I - 1) + F (I - 1) = X$
111		oveq1	$⊢ X - F (I - 1) = p + q \to X - F (I - 1) + F (I - 1) = p + q + F (I - 1)$
112	110 111	sylan9req	$⊢ (((p \in Odd \land q \in Odd) \land (((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ)) \land X - F (I - 1) = p + q) \to X = p + q + F (I - 1)$
113	112	exp31	$⊢ (p \in Odd \land q \in Odd) \to ((((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \to (X - F (I - 1) = p + q \to X = p + q + F (I - 1)))$
114	113	com23	$⊢ (p \in Odd \land q \in Odd) \to (X - F (I - 1) = p + q \to ((((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \to X = p + q + F (I - 1)))$
115	114	3impia	$⊢ (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q) \to ((((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \to X = p + q + F (I - 1))$
116	115	impcom	$⊢ ((((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q)) \to X = p + q + F (I - 1)$
117	92 116	jca	$⊢ ((((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q)) \to ((p \in Odd \land q \in Odd \land F (I - 1) \in Odd) \land X = p + q + F (I - 1))$
118	73 79 117	rspcedvd	$⊢ ((((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q)) \to \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r)$
119	118	ex	$⊢ (((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \land q \in ℙ) \to ((p \in Odd \land q \in Odd \land X - F (I - 1) = p + q) \to \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))$
120	119	reximdva	$⊢ ((((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \land p \in ℙ) \to (\exists q \in ℙ (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q) \to \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))$
121	120	reximdva	$⊢ (((X - F (I - 1) \in Even \land φ) \land I \in (1 ..^D)) \land X \in Odd) \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))$
122	121	exp41	$⊢ X - F (I - 1) \in Even \to (φ \to (I \in (1 ..^D) \to (X \in Odd \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r)))))$
123	122	com25	$⊢ X - F (I - 1) \in Even \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q) \to (I \in (1 ..^D) \to (X \in Odd \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r)))))$
124	123	imp	$⊢ (X - F (I - 1) \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land X - F (I - 1) = p + q)) \to (I \in (1 ..^D) \to (X \in Odd \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))))$
125	31 124	sylbi	$⊢ X - F (I - 1) \in GoldbachEven \to (I \in (1 ..^D) \to (X \in Odd \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))))$
126	125	a1d	$⊢ X - F (I - 1) \in GoldbachEven \to (X - F (I - 1) \in Even \to (I \in (1 ..^D) \to (X \in Odd \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r)))))$
127	30 126	syl6com	$⊢ (4 < X - F (I - 1) \land X - F (I - 1) < N) \to (((4 < X - F (I - 1) \land X - F (I - 1) < N) \to X - F (I - 1) \in GoldbachEven) \to (X - F (I - 1) \in Even \to (I \in (1 ..^D) \to (X \in Odd \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))))))$
128	127	ancoms	$⊢ (X - F (I - 1) < N \land 4 < X - F (I - 1)) \to (((4 < X - F (I - 1) \land X - F (I - 1) < N) \to X - F (I - 1) \in GoldbachEven) \to (X - F (I - 1) \in Even \to (I \in (1 ..^D) \to (X \in Odd \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))))))$
129	128	com13	$⊢ X - F (I - 1) \in Even \to (((4 < X - F (I - 1) \land X - F (I - 1) < N) \to X - F (I - 1) \in GoldbachEven) \to ((X - F (I - 1) < N \land 4 < X - F (I - 1)) \to (I \in (1 ..^D) \to (X \in Odd \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))))))$
130	29 129	syld	$⊢ X - F (I - 1) \in Even \to (\forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \to ((X - F (I - 1) < N \land 4 < X - F (I - 1)) \to (I \in (1 ..^D) \to (X \in Odd \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))))))$
131	130	com23	$⊢ X - F (I - 1) \in Even \to ((X - F (I - 1) < N \land 4 < X - F (I - 1)) \to (\forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \to (I \in (1 ..^D) \to (X \in Odd \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))))))$
132	131	3impib	$⊢ (X - F (I - 1) \in Even \land X - F (I - 1) < N \land 4 < X - F (I - 1)) \to (\forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \to (I \in (1 ..^D) \to (X \in Odd \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r)))))$
133	132	com15	$⊢ φ \to (\forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \to (I \in (1 ..^D) \to (X \in Odd \to ((X - F (I - 1) \in Even \land X - F (I - 1) < N \land 4 < X - F (I - 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r)))))$
134	3 133	mpd	$⊢ φ \to (I \in (1 ..^D) \to (X \in Odd \to ((X - F (I - 1) \in Even \land X - F (I - 1) < N \land 4 < X - F (I - 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))))$
135	134	imp31	$⊢ ((φ \land I \in (1 ..^D)) \land X \in Odd) \to ((X - F (I - 1) \in Even \land X - F (I - 1) < N \land 4 < X - F (I - 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))$
136	16 135	syld	$⊢ ((φ \land I \in (1 ..^D)) \land X \in Odd) \to ((X \in [F (I), F (I + 1)) \land X - F (I) \leq 4) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land X = p + q + r))$

Metamath Proof Explorer

Theorem bgoldbtbndlem4

Proof