bgoldbtbnd

Description: If the binary Goldbach conjecture is valid up to an integer N , and there is a series ("ladder") of primes with a difference of at most N up to an integer M , then the strong ternary Goldbach conjecture is valid up to M , see section 1.2.2 in Helfgott p. 4 with N = 4 x 10^18, taken from OeSilva, and M = 8.875 x 10^30. (Contributed by AV, 1-Aug-2020)

	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	bgoldbtbnd	$⊢ φ \to \forall n \in Odd ((7 < n \land n < M) \to n \in GoldbachOdd)$

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		simprl	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to n \in Odd$
12		eluzge3nn	$⊢ D \in ℤ_{\geq 3} \to D \in ℕ$
13	4 12	syl	$⊢ φ \to D \in ℕ$
14		iccelpart	$⊢ D \in ℕ \to \forall f \in RePart (D) (n \in [f (0), f (D)) \to \exists j \in (0 ..^D) n \in [f (j), f (j + 1)))$
15	13 14	syl	$⊢ φ \to \forall f \in RePart (D) (n \in [f (0), f (D)) \to \exists j \in (0 ..^D) n \in [f (j), f (j + 1)))$
16		fveq1	$⊢ f = F \to f (0) = F (0)$
17		fveq1	$⊢ f = F \to f (D) = F (D)$
18	16 17	oveq12d	$⊢ f = F \to [f (0), f (D)) = [F (0), F (D))$
19	18	eleq2d	$⊢ f = F \to (n \in [f (0), f (D)) \leftrightarrow n \in [F (0), F (D)))$
20		fveq1	$⊢ f = F \to f (j) = F (j)$
21		fveq1	$⊢ f = F \to f (j + 1) = F (j + 1)$
22	20 21	oveq12d	$⊢ f = F \to [f (j), f (j + 1)) = [F (j), F (j + 1))$
23	22	eleq2d	$⊢ f = F \to (n \in [f (j), f (j + 1)) \leftrightarrow n \in [F (j), F (j + 1)))$
24	23	rexbidv	$⊢ f = F \to (\exists j \in (0 ..^D) n \in [f (j), f (j + 1)) \leftrightarrow \exists j \in (0 ..^D) n \in [F (j), F (j + 1)))$
25	19 24	imbi12d	$⊢ f = F \to ((n \in [f (0), f (D)) \to \exists j \in (0 ..^D) n \in [f (j), f (j + 1))) \leftrightarrow (n \in [F (0), F (D)) \to \exists j \in (0 ..^D) n \in [F (j), F (j + 1))))$
26	25	rspcv	$⊢ F \in RePart (D) \to (\forall f \in RePart (D) (n \in [f (0), f (D)) \to \exists j \in (0 ..^D) n \in [f (j), f (j + 1))) \to (n \in [F (0), F (D)) \to \exists j \in (0 ..^D) n \in [F (j), F (j + 1))))$
27	5 26	syl	$⊢ φ \to (\forall f \in RePart (D) (n \in [f (0), f (D)) \to \exists j \in (0 ..^D) n \in [f (j), f (j + 1))) \to (n \in [F (0), F (D)) \to \exists j \in (0 ..^D) n \in [F (j), F (j + 1))))$
28		oddz	$⊢ n \in Odd \to n \in ℤ$
29	28	zred	$⊢ n \in Odd \to n \in ℝ$
30	29	rexrd	$⊢ n \in Odd \to n \in ℝ^{*}$
31	30	ad2antrl	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to n \in ℝ^{*}$
32		7re	$⊢ 7 \in ℝ$
33		ltle	$⊢ (7 \in ℝ \land n \in ℝ) \to (7 < n \to 7 \leq n)$
34	32 29 33	sylancr	$⊢ n \in Odd \to (7 < n \to 7 \leq n)$
35	34	com12	$⊢ 7 < n \to (n \in Odd \to 7 \leq n)$
36	35	adantr	$⊢ (7 < n \land n < M) \to (n \in Odd \to 7 \leq n)$
37	36	impcom	$⊢ (n \in Odd \land (7 < n \land n < M)) \to 7 \leq n$
38	37	adantl	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to 7 \leq n$
39		eluzelre	$⊢ M \in ℤ_{\geq 11} \to M \in ℝ$
40	39	rexrd	$⊢ M \in ℤ_{\geq 11} \to M \in ℝ^{*}$
41	1 40	syl	$⊢ φ \to M \in ℝ^{*}$
42	41	adantr	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to M \in ℝ^{*}$
43	10	rexrd	$⊢ φ \to F (D) \in ℝ^{*}$
44	43	adantr	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to F (D) \in ℝ^{*}$
45		simprrr	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to n < M$
46	9	adantr	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to M < F (D)$
47	31 42 44 45 46	xrlttrd	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to n < F (D)$
48	7	oveq1d	$⊢ φ \to [F (0), F (D)) = [7, F (D))$
49	48	eleq2d	$⊢ φ \to (n \in [F (0), F (D)) \leftrightarrow n \in [7, F (D)))$
50	49	adantr	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to (n \in [F (0), F (D)) \leftrightarrow n \in [7, F (D)))$
51	32	rexri	$⊢ 7 \in ℝ^{*}$
52		elico1	$⊢ (7 \in ℝ^{} \land F (D) \in ℝ^{}) \to (n \in [7, F (D)) \leftrightarrow (n \in ℝ^{*} \land 7 \leq n \land n < F (D)))$
53	51 44 52	sylancr	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to (n \in [7, F (D)) \leftrightarrow (n \in ℝ^{*} \land 7 \leq n \land n < F (D)))$
54	50 53	bitrd	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to (n \in [F (0), F (D)) \leftrightarrow (n \in ℝ^{*} \land 7 \leq n \land n < F (D)))$
55	31 38 47 54	mpbir3and	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to n \in [F (0), F (D))$
56		fzo0sn0fzo1	$⊢ D \in ℕ \to (0 ..^D) = \{0\} \cup (1 ..^D)$
57	56	eleq2d	$⊢ D \in ℕ \to (j \in (0 ..^D) \leftrightarrow j \in (\{0\} \cup (1 ..^D)))$
58		elun	$⊢ j \in (\{0\} \cup (1 ..^D)) \leftrightarrow (j \in \{0\} \lor j \in (1 ..^D))$
59	57 58	bitrdi	$⊢ D \in ℕ \to (j \in (0 ..^D) \leftrightarrow (j \in \{0\} \lor j \in (1 ..^D)))$
60	13 59	syl	$⊢ φ \to (j \in (0 ..^D) \leftrightarrow (j \in \{0\} \lor j \in (1 ..^D)))$
61	60	adantr	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to (j \in (0 ..^D) \leftrightarrow (j \in \{0\} \lor j \in (1 ..^D)))$
62		velsn	$⊢ j \in \{0\} \leftrightarrow j = 0$
63		fveq2	$⊢ j = 0 \to F (j) = F (0)$
64		fv0p1e1	$⊢ j = 0 \to F (j + 1) = F (1)$
65	63 64	oveq12d	$⊢ j = 0 \to [F (j), F (j + 1)) = [F (0), F (1))$
66	7 8	oveq12d	$⊢ φ \to [F (0), F (1)) = [7, 13)$
67	66	adantr	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to [F (0), F (1)) = [7, 13)$
68	65 67	sylan9eq	$⊢ (j = 0 \land (φ \land (n \in Odd \land (7 < n \land n < M)))) \to [F (j), F (j + 1)) = [7, 13)$
69	68	eleq2d	$⊢ (j = 0 \land (φ \land (n \in Odd \land (7 < n \land n < M)))) \to (n \in [F (j), F (j + 1)) \leftrightarrow n \in [7, 13))$
70	11	adantr	$⊢ ((φ \land (n \in Odd \land (7 < n \land n < M))) \land n \in [7, 13)) \to n \in Odd$
71		simprrl	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to 7 < n$
72	71	adantr	$⊢ ((φ \land (n \in Odd \land (7 < n \land n < M))) \land n \in [7, 13)) \to 7 < n$
73		simpr	$⊢ ((φ \land (n \in Odd \land (7 < n \land n < M))) \land n \in [7, 13)) \to n \in [7, 13)$
74		bgoldbtbndlem1	$⊢ (n \in Odd \land 7 < n \land n \in [7, 13)) \to n \in GoldbachOdd$
75	70 72 73 74	syl3anc	$⊢ ((φ \land (n \in Odd \land (7 < n \land n < M))) \land n \in [7, 13)) \to n \in GoldbachOdd$
76		isgbo	$⊢ n \in GoldbachOdd \leftrightarrow (n \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
77	75 76	sylib	$⊢ ((φ \land (n \in Odd \land (7 < n \land n < M))) \land n \in [7, 13)) \to (n \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
78	77	simprd	$⊢ ((φ \land (n \in Odd \land (7 < n \land n < M))) \land n \in [7, 13)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)$
79	78	ex	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to (n \in [7, 13) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
80	79	adantl	$⊢ (j = 0 \land (φ \land (n \in Odd \land (7 < n \land n < M)))) \to (n \in [7, 13) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
81	69 80	sylbid	$⊢ (j = 0 \land (φ \land (n \in Odd \land (7 < n \land n < M)))) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
82	81	ex	$⊢ j = 0 \to ((φ \land (n \in Odd \land (7 < n \land n < M))) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
83	62 82	sylbi	$⊢ j \in \{0\} \to ((φ \land (n \in Odd \land (7 < n \land n < M))) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
84		fzo0ss1	$⊢ (1 ..^D) \subseteq (0 ..^D)$
85	84	sseli	$⊢ j \in (1 ..^D) \to j \in (0 ..^D)$
86		fveq2	$⊢ i = j \to F (i) = F (j)$
87	86	eleq1d	$⊢ i = j \to (F (i) \in (ℙ ∖ \{2\}) \leftrightarrow F (j) \in (ℙ ∖ \{2\}))$
88		fvoveq1	$⊢ i = j \to F (i + 1) = F (j + 1)$
89	88 86	oveq12d	$⊢ i = j \to F (i + 1) - F (i) = F (j + 1) - F (j)$
90	89	breq1d	$⊢ i = j \to (F (i + 1) - F (i) < N - 4 \leftrightarrow F (j + 1) - F (j) < N - 4)$
91	89	breq2d	$⊢ i = j \to (4 < F (i + 1) - F (i) \leftrightarrow 4 < F (j + 1) - F (j))$
92	87 90 91	3anbi123d	$⊢ i = j \to ((F (i) \in (ℙ ∖ \{2\}) \land F (i + 1) - F (i) < N - 4 \land 4 < F (i + 1) - F (i)) \leftrightarrow (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))$
93	92	rspcv	$⊢ j \in (0 ..^D) \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)) \to (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))$
94	85 93	syl	$⊢ j \in (1 ..^D) \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)) \to (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))$
95	6 94	mpan9	$⊢ (φ \land j \in (1 ..^D)) \to (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))$
96	1 2 3 4 5 6 7 8 9 10	bgoldbtbndlem4	$⊢ ((φ \land j \in (1 ..^D)) \land n \in Odd) \to ((n \in [F (j), F (j + 1)) \land n - F (j) \leq 4) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
97	96	ad2ant2r	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to ((n \in [F (j), F (j + 1)) \land n - F (j) \leq 4) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
98	97	expcomd	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to (n - F (j) \leq 4 \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
99		simplll	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to φ$
100		simprl	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to n \in Odd$
101		simpllr	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to j \in (1 ..^D)$
102		eqid	$⊢ n - F (j) = n - F (j)$
103	1 2 3 4 5 6 7 8 9 10 102	bgoldbtbndlem3	$⊢ (φ \land n \in Odd \land j \in (1 ..^D)) \to ((n \in [F (j), F (j + 1)) \land 4 < n - F (j)) \to (n - F (j) \in Even \land n - F (j) < N \land 4 < n - F (j)))$
104	99 100 101 103	syl3anc	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to ((n \in [F (j), F (j + 1)) \land 4 < n - F (j)) \to (n - F (j) \in Even \land n - F (j) < N \land 4 < n - F (j)))$
105		breq2	$⊢ n = m \to (4 < n \leftrightarrow 4 < m)$
106		breq1	$⊢ n = m \to (n < N \leftrightarrow m < N)$
107	105 106	anbi12d	$⊢ n = m \to ((4 < n \land n < N) \leftrightarrow (4 < m \land m < N))$
108		eleq1	$⊢ n = m \to (n \in GoldbachEven \leftrightarrow m \in GoldbachEven)$
109	107 108	imbi12d	$⊢ n = m \to (((4 < n \land n < N) \to n \in GoldbachEven) \leftrightarrow ((4 < m \land m < N) \to m \in GoldbachEven))$
110	109	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)$
111		breq2	$⊢ m = n - F (j) \to (4 < m \leftrightarrow 4 < n - F (j))$
112		breq1	$⊢ m = n - F (j) \to (m < N \leftrightarrow n - F (j) < N)$
113	111 112	anbi12d	$⊢ m = n - F (j) \to ((4 < m \land m < N) \leftrightarrow (4 < n - F (j) \land n - F (j) < N))$
114		eleq1	$⊢ m = n - F (j) \to (m \in GoldbachEven \leftrightarrow n - F (j) \in GoldbachEven)$
115	113 114	imbi12d	$⊢ m = n - F (j) \to (((4 < m \land m < N) \to m \in GoldbachEven) \leftrightarrow ((4 < n - F (j) \land n - F (j) < N) \to n - F (j) \in GoldbachEven))$
116	115	rspcv	$⊢ n - F (j) \in Even \to (\forall m \in Even ((4 < m \land m < N) \to m \in GoldbachEven) \to ((4 < n - F (j) \land n - F (j) < N) \to n - F (j) \in GoldbachEven))$
117	110 116	syl5bi	$⊢ n - F (j) \in Even \to (\forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \to ((4 < n - F (j) \land n - F (j) < N) \to n - F (j) \in GoldbachEven))$
118		pm3.35	$⊢ ((4 < n - F (j) \land n - F (j) < N) \land ((4 < n - F (j) \land n - F (j) < N) \to n - F (j) \in GoldbachEven)) \to n - F (j) \in GoldbachEven$
119		isgbe	$⊢ n - F (j) \in GoldbachEven \leftrightarrow (n - F (j) \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n - F (j) = p + q))$
120		eldifi	$⊢ F (j) \in (ℙ ∖ \{2\}) \to F (j) \in ℙ$
121	120	3ad2ant1	$⊢ (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)) \to F (j) \in ℙ$
122	121	adantl	$⊢ (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to F (j) \in ℙ$
123	122	ad5antlr	$⊢ ((((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land n - F (j) = p + q)) \to F (j) \in ℙ$
124		eleq1	$⊢ r = F (j) \to (r \in Odd \leftrightarrow F (j) \in Odd)$
125	124	3anbi3d	$⊢ r = F (j) \to ((p \in Odd \land q \in Odd \land r \in Odd) \leftrightarrow (p \in Odd \land q \in Odd \land F (j) \in Odd))$
126		oveq2	$⊢ r = F (j) \to p + q + r = p + q + F (j)$
127	126	eqeq2d	$⊢ r = F (j) \to (n = p + q + r \leftrightarrow n = p + q + F (j))$
128	125 127	anbi12d	$⊢ r = F (j) \to (((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r) \leftrightarrow ((p \in Odd \land q \in Odd \land F (j) \in Odd) \land n = p + q + F (j)))$
129	128	adantl	$⊢ (((((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land n - F (j) = p + q)) \land r = F (j)) \to (((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r) \leftrightarrow ((p \in Odd \land q \in Odd \land F (j) \in Odd) \land n = p + q + F (j)))$
130		oddprmALTV	$⊢ F (j) \in (ℙ ∖ \{2\}) \to F (j) \in Odd$
131	130	3ad2ant1	$⊢ (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)) \to F (j) \in Odd$
132	131	adantl	$⊢ (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to F (j) \in Odd$
133	132	ad4antlr	$⊢ (((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \to F (j) \in Odd$
134		3simpa	$⊢ (p \in Odd \land q \in Odd \land n - F (j) = p + q) \to (p \in Odd \land q \in Odd)$
135	133 134	anim12ci	$⊢ ((((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land n - F (j) = p + q)) \to ((p \in Odd \land q \in Odd) \land F (j) \in Odd)$
136		df-3an	$⊢ (p \in Odd \land q \in Odd \land F (j) \in Odd) \leftrightarrow ((p \in Odd \land q \in Odd) \land F (j) \in Odd)$
137	135 136	sylibr	$⊢ ((((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land n - F (j) = p + q)) \to (p \in Odd \land q \in Odd \land F (j) \in Odd)$
138	28	zcnd	$⊢ n \in Odd \to n \in ℂ$
139	138	ad2antrl	$⊢ (((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \to n \in ℂ$
140		prmz	$⊢ F (j) \in ℙ \to F (j) \in ℤ$
141	140	zcnd	$⊢ F (j) \in ℙ \to F (j) \in ℂ$
142	120 141	syl	$⊢ F (j) \in (ℙ ∖ \{2\}) \to F (j) \in ℂ$
143	142	3ad2ant1	$⊢ (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)) \to F (j) \in ℂ$
144	143	adantl	$⊢ (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to F (j) \in ℂ$
145	144	ad2antlr	$⊢ (((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \to F (j) \in ℂ$
146	139 145	npcand	$⊢ (((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \to n - F (j) + F (j) = n$
147	146	adantr	$⊢ ((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \to n - F (j) + F (j) = n$
148	147	ad2antrl	$⊢ ((p \in Odd \land q \in Odd) \land (((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ)) \to n - F (j) + F (j) = n$
149		oveq1	$⊢ n - F (j) = p + q \to n - F (j) + F (j) = p + q + F (j)$
150	148 149	sylan9req	$⊢ (((p \in Odd \land q \in Odd) \land (((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ)) \land n - F (j) = p + q) \to n = p + q + F (j)$
151	150	exp31	$⊢ (p \in Odd \land q \in Odd) \to ((((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \to (n - F (j) = p + q \to n = p + q + F (j)))$
152	151	com23	$⊢ (p \in Odd \land q \in Odd) \to (n - F (j) = p + q \to ((((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \to n = p + q + F (j)))$
153	152	3impia	$⊢ (p \in Odd \land q \in Odd \land n - F (j) = p + q) \to ((((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \to n = p + q + F (j))$
154	153	impcom	$⊢ ((((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land n - F (j) = p + q)) \to n = p + q + F (j)$
155	137 154	jca	$⊢ ((((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land n - F (j) = p + q)) \to ((p \in Odd \land q \in Odd \land F (j) \in Odd) \land n = p + q + F (j))$
156	123 129 155	rspcedvd	$⊢ ((((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land n - F (j) = p + q)) \to \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)$
157	156	ex	$⊢ (((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \land q \in ℙ) \to ((p \in Odd \land q \in Odd \land n - F (j) = p + q) \to \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
158	157	reximdva	$⊢ ((((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \land p \in ℙ) \to (\exists q \in ℙ (p \in Odd \land q \in Odd \land n - F (j) = p + q) \to \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
159	158	reximdva	$⊢ (((n - F (j) \in Even \land φ) \land (j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)))) \land (n \in Odd \land (7 < n \land n < M))) \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n - F (j) = p + q) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
160	159	exp41	$⊢ n - F (j) \in Even \to (φ \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n - F (j) = p + q) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))))$
161	160	com25	$⊢ n - F (j) \in Even \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n - F (j) = p + q) \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))))$
162	161	imp	$⊢ (n - F (j) \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n - F (j) = p + q)) \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))))$
163	119 162	sylbi	$⊢ n - F (j) \in GoldbachEven \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))))$
164	163	a1d	$⊢ n - F (j) \in GoldbachEven \to (n - F (j) \in Even \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))))$
165	118 164	syl	$⊢ ((4 < n - F (j) \land n - F (j) < N) \land ((4 < n - F (j) \land n - F (j) < N) \to n - F (j) \in GoldbachEven)) \to (n - F (j) \in Even \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))))$
166	165	ex	$⊢ (4 < n - F (j) \land n - F (j) < N) \to (((4 < n - F (j) \land n - F (j) < N) \to n - F (j) \in GoldbachEven) \to (n - F (j) \in Even \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))))))$
167	166	ancoms	$⊢ (n - F (j) < N \land 4 < n - F (j)) \to (((4 < n - F (j) \land n - F (j) < N) \to n - F (j) \in GoldbachEven) \to (n - F (j) \in Even \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))))))$
168	167	com13	$⊢ n - F (j) \in Even \to (((4 < n - F (j) \land n - F (j) < N) \to n - F (j) \in GoldbachEven) \to ((n - F (j) < N \land 4 < n - F (j)) \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))))))$
169	117 168	syld	$⊢ n - F (j) \in Even \to (\forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \to ((n - F (j) < N \land 4 < n - F (j)) \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))))))$
170	169	com23	$⊢ n - F (j) \in Even \to ((n - F (j) < N \land 4 < n - F (j)) \to (\forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))))))$
171	170	3impib	$⊢ (n - F (j) \in Even \land n - F (j) < N \land 4 < n - F (j)) \to (\forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (φ \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))))$
172	171	com15	$⊢ φ \to (\forall n \in Even ((4 < n \land n < N) \to n \in GoldbachEven) \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to ((n - F (j) \in Even \land n - F (j) < N \land 4 < n - F (j)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))))$
173	3 172	mpd	$⊢ φ \to ((j \in (1 ..^D) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to ((n - F (j) \in Even \land n - F (j) < N \land 4 < n - F (j)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))))$
174	173	impl	$⊢ ((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to ((n - F (j) \in Even \land n - F (j) < N \land 4 < n - F (j)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
175	174	imp	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to ((n - F (j) \in Even \land n - F (j) < N \land 4 < n - F (j)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
176	104 175	syld	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to ((n \in [F (j), F (j + 1)) \land 4 < n - F (j)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
177	176	expcomd	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to (4 < n - F (j) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
178	29	ad2antrl	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to n \in ℝ$
179	140	zred	$⊢ F (j) \in ℙ \to F (j) \in ℝ$
180	120 179	syl	$⊢ F (j) \in (ℙ ∖ \{2\}) \to F (j) \in ℝ$
181	180	3ad2ant1	$⊢ (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j)) \to F (j) \in ℝ$
182	181	ad2antlr	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to F (j) \in ℝ$
183	178 182	resubcld	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to n - F (j) \in ℝ$
184		4re	$⊢ 4 \in ℝ$
185		lelttric	$⊢ (n - F (j) \in ℝ \land 4 \in ℝ) \to (n - F (j) \leq 4 \lor 4 < n - F (j))$
186	183 184 185	sylancl	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to (n - F (j) \leq 4 \lor 4 < n - F (j))$
187	98 177 186	mpjaod	$⊢ (((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \land (n \in Odd \land (7 < n \land n < M))) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
188	187	ex	$⊢ ((φ \land j \in (1 ..^D)) \land (F (j) \in (ℙ ∖ \{2\}) \land F (j + 1) - F (j) < N - 4 \land 4 < F (j + 1) - F (j))) \to ((n \in Odd \land (7 < n \land n < M)) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
189	95 188	mpdan	$⊢ (φ \land j \in (1 ..^D)) \to ((n \in Odd \land (7 < n \land n < M)) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
190	189	expcom	$⊢ j \in (1 ..^D) \to (φ \to ((n \in Odd \land (7 < n \land n < M)) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))))$
191	190	impd	$⊢ j \in (1 ..^D) \to ((φ \land (n \in Odd \land (7 < n \land n < M))) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
192	83 191	jaoi	$⊢ (j \in \{0\} \lor j \in (1 ..^D)) \to ((φ \land (n \in Odd \land (7 < n \land n < M))) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
193	192	com12	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to ((j \in \{0\} \lor j \in (1 ..^D)) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
194	61 193	sylbid	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to (j \in (0 ..^D) \to (n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
195	194	rexlimdv	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to (\exists j \in (0 ..^D) n \in [F (j), F (j + 1)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
196	55 195	embantd	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to ((n \in [F (0), F (D)) \to \exists j \in (0 ..^D) n \in [F (j), F (j + 1))) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
197	196	ex	$⊢ φ \to ((n \in Odd \land (7 < n \land n < M)) \to ((n \in [F (0), F (D)) \to \exists j \in (0 ..^D) n \in [F (j), F (j + 1))) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
198	197	com23	$⊢ φ \to ((n \in [F (0), F (D)) \to \exists j \in (0 ..^D) n \in [F (j), F (j + 1))) \to ((n \in Odd \land (7 < n \land n < M)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
199	27 198	syld	$⊢ φ \to (\forall f \in RePart (D) (n \in [f (0), f (D)) \to \exists j \in (0 ..^D) n \in [f (j), f (j + 1))) \to ((n \in Odd \land (7 < n \land n < M)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)))$
200	15 199	mpd	$⊢ φ \to ((n \in Odd \land (7 < n \land n < M)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
201	200	imp	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r)$
202	11 201	jca	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to (n \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land n = p + q + r))$
203	202 76	sylibr	$⊢ (φ \land (n \in Odd \land (7 < n \land n < M))) \to n \in GoldbachOdd$
204	203	exp32	$⊢ φ \to (n \in Odd \to ((7 < n \land n < M) \to n \in GoldbachOdd))$
205	204	ralrimiv	$⊢ φ \to \forall n \in Odd ((7 < n \land n < M) \to n \in GoldbachOdd)$

Metamath Proof Explorer

Theorem bgoldbtbnd

Proof