bgoldbtbndlem3

	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 ℝ$
	bgoldbtbndlem3.s	$⊢ S = X - F (I)$
Assertion	bgoldbtbndlem3	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to ((X \in [F (I), F (I + 1)) \land 4 < S) \to (S \in Even \land S < N \land 4 < S))$

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		bgoldbtbndlem3.s	$⊢ S = X - F (I)$
12		fzo0ss1	$⊢ (1 ..^D) \subseteq (0 ..^D)$
13	12	sseli	$⊢ I \in (1 ..^D) \to I \in (0 ..^D)$
14		fveq2	$⊢ i = I \to F (i) = F (I)$
15	14	eleq1d	$⊢ i = I \to (F (i) \in (ℙ ∖ \{2\}) \leftrightarrow F (I) \in (ℙ ∖ \{2\}))$
16		fvoveq1	$⊢ i = I \to F (i + 1) = F (I + 1)$
17	16 14	oveq12d	$⊢ i = I \to F (i + 1) - F (i) = F (I + 1) - F (I)$
18	17	breq1d	$⊢ i = I \to (F (i + 1) - F (i) < N - 4 \leftrightarrow F (I + 1) - F (I) < N - 4)$
19	17	breq2d	$⊢ i = I \to (4 < F (i + 1) - F (i) \leftrightarrow 4 < F (I + 1) - F (I))$
20	15 18 19	3anbi123d	$⊢ i = I \to ((F (i) \in (ℙ ∖ \{2\}) \land F (i + 1) - F (i) < N - 4 \land 4 < F (i + 1) - F (i)) \leftrightarrow (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I)))$
21	20	rspcv	$⊢ I \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 (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I)))$
22	13 6 21	syl2imc	$⊢ φ \to (I \in (1 ..^D) \to (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I)))$
23	22	a1d	$⊢ φ \to (X \in Odd \to (I \in (1 ..^D) \to (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))))$
24	23	3imp	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))$
25		simp2	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to X \in Odd$
26		oddprmALTV	$⊢ F (I) \in (ℙ ∖ \{2\}) \to F (I) \in Odd$
27	26	3ad2ant1	$⊢ (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I)) \to F (I) \in Odd$
28	25 27	anim12i	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \to (X \in Odd \land F (I) \in Odd)$
29	28	adantr	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \land (X \in [F (I), F (I + 1)) \land 4 < S)) \to (X \in Odd \land F (I) \in Odd)$
30		omoeALTV	$⊢ (X \in Odd \land F (I) \in Odd) \to X - F (I) \in Even$
31	29 30	syl	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \land (X \in [F (I), F (I + 1)) \land 4 < S)) \to X - F (I) \in Even$
32	11 31	eqeltrid	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \land (X \in [F (I), F (I + 1)) \land 4 < S)) \to S \in Even$
33		eldifi	$⊢ F (I) \in (ℙ ∖ \{2\}) \to F (I) \in ℙ$
34		prmz	$⊢ F (I) \in ℙ \to F (I) \in ℤ$
35	34	zred	$⊢ F (I) \in ℙ \to F (I) \in ℝ$
36		fzofzp1	$⊢ I \in (1 ..^D) \to I + 1 \in (1 \dots D)$
37		elfzo2	$⊢ I \in (1 ..^D) \leftrightarrow (I \in ℤ_{\geq 1} \land D \in ℤ \land I < D)$
38		1zzd	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ \land I < D) \to 1 \in ℤ$
39		simp2	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ \land I < D) \to D \in ℤ$
40		eluz2	$⊢ I \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land I \in ℤ \land 1 \leq I)$
41		zre	$⊢ 1 \in ℤ \to 1 \in ℝ$
42		zre	$⊢ I \in ℤ \to I \in ℝ$
43		zre	$⊢ D \in ℤ \to D \in ℝ$
44		leltletr	$⊢ (1 \in ℝ \land I \in ℝ \land D \in ℝ) \to ((1 \leq I \land I < D) \to 1 \leq D)$
45	41 42 43 44	syl3an	$⊢ (1 \in ℤ \land I \in ℤ \land D \in ℤ) \to ((1 \leq I \land I < D) \to 1 \leq D)$
46	45	exp5o	$⊢ 1 \in ℤ \to (I \in ℤ \to (D \in ℤ \to (1 \leq I \to (I < D \to 1 \leq D))))$
47	46	com34	$⊢ 1 \in ℤ \to (I \in ℤ \to (1 \leq I \to (D \in ℤ \to (I < D \to 1 \leq D))))$
48	47	3imp	$⊢ (1 \in ℤ \land I \in ℤ \land 1 \leq I) \to (D \in ℤ \to (I < D \to 1 \leq D))$
49	40 48	sylbi	$⊢ I \in ℤ_{\geq 1} \to (D \in ℤ \to (I < D \to 1 \leq D))$
50	49	3imp	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ \land I < D) \to 1 \leq D$
51		eluz2	$⊢ D \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land D \in ℤ \land 1 \leq D)$
52	38 39 50 51	syl3anbrc	$⊢ (I \in ℤ_{\geq 1} \land D \in ℤ \land I < D) \to D \in ℤ_{\geq 1}$
53	37 52	sylbi	$⊢ I \in (1 ..^D) \to D \in ℤ_{\geq 1}$
54		fzisfzounsn	$⊢ D \in ℤ_{\geq 1} \to (1 \dots D) = (1 ..^D) \cup \{D\}$
55	53 54	syl	$⊢ I \in (1 ..^D) \to (1 \dots D) = (1 ..^D) \cup \{D\}$
56	55	eleq2d	$⊢ I \in (1 ..^D) \to (I + 1 \in (1 \dots D) \leftrightarrow I + 1 \in ((1 ..^D) \cup \{D\}))$
57		elun	$⊢ I + 1 \in ((1 ..^D) \cup \{D\}) \leftrightarrow (I + 1 \in (1 ..^D) \lor I + 1 \in \{D\})$
58	56 57	bitrdi	$⊢ I \in (1 ..^D) \to (I + 1 \in (1 \dots D) \leftrightarrow (I + 1 \in (1 ..^D) \lor I + 1 \in \{D\}))$
59		eluz3nn	$⊢ D \in ℤ_{\geq 3} \to D \in ℕ$
60	4 59	syl	$⊢ φ \to D \in ℕ$
61	60	ad2antrl	$⊢ ((I \in (1 ..^D) \land I + 1 \in (1 ..^D)) \land (φ \land X \in Odd)) \to D \in ℕ$
62	5	ad2antrl	$⊢ ((I \in (1 ..^D) \land I + 1 \in (1 ..^D)) \land (φ \land X \in Odd)) \to F \in RePart (D)$
63		simplr	$⊢ ((I \in (1 ..^D) \land I + 1 \in (1 ..^D)) \land (φ \land X \in Odd)) \to I + 1 \in (1 ..^D)$
64	61 62 63	iccpartipre	$⊢ ((I \in (1 ..^D) \land I + 1 \in (1 ..^D)) \land (φ \land X \in Odd)) \to F (I + 1) \in ℝ$
65	64	exp31	$⊢ I \in (1 ..^D) \to (I + 1 \in (1 ..^D) \to ((φ \land X \in Odd) \to F (I + 1) \in ℝ))$
66		elsni	$⊢ I + 1 \in \{D\} \to I + 1 = D$
67	10	ad2antrl	$⊢ (I + 1 = D \land (φ \land X \in Odd)) \to F (D) \in ℝ$
68		fveq2	$⊢ I + 1 = D \to F (I + 1) = F (D)$
69	68	eleq1d	$⊢ I + 1 = D \to (F (I + 1) \in ℝ \leftrightarrow F (D) \in ℝ)$
70	69	adantr	$⊢ (I + 1 = D \land (φ \land X \in Odd)) \to (F (I + 1) \in ℝ \leftrightarrow F (D) \in ℝ)$
71	67 70	mpbird	$⊢ (I + 1 = D \land (φ \land X \in Odd)) \to F (I + 1) \in ℝ$
72	71	ex	$⊢ I + 1 = D \to ((φ \land X \in Odd) \to F (I + 1) \in ℝ)$
73	66 72	syl	$⊢ I + 1 \in \{D\} \to ((φ \land X \in Odd) \to F (I + 1) \in ℝ)$
74	73	a1i	$⊢ I \in (1 ..^D) \to (I + 1 \in \{D\} \to ((φ \land X \in Odd) \to F (I + 1) \in ℝ))$
75	65 74	jaod	$⊢ I \in (1 ..^D) \to ((I + 1 \in (1 ..^D) \lor I + 1 \in \{D\}) \to ((φ \land X \in Odd) \to F (I + 1) \in ℝ))$
76	58 75	sylbid	$⊢ I \in (1 ..^D) \to (I + 1 \in (1 \dots D) \to ((φ \land X \in Odd) \to F (I + 1) \in ℝ))$
77	36 76	mpd	$⊢ I \in (1 ..^D) \to ((φ \land X \in Odd) \to F (I + 1) \in ℝ)$
78	77	com12	$⊢ (φ \land X \in Odd) \to (I \in (1 ..^D) \to F (I + 1) \in ℝ)$
79	78	3impia	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to F (I + 1) \in ℝ$
80		eluzelre	$⊢ N \in ℤ_{\geq 11} \to N \in ℝ$
81	2 80	syl	$⊢ φ \to N \in ℝ$
82		oddz	$⊢ X \in Odd \to X \in ℤ$
83	82	zred	$⊢ X \in Odd \to X \in ℝ$
84		rexr	$⊢ F (I + 1) \in ℝ \to F (I + 1) \in ℝ^{*}$
85		rexr	$⊢ F (I) \in ℝ \to F (I) \in ℝ^{*}$
86	84 85	anim12ci	$⊢ (F (I + 1) \in ℝ \land F (I) \in ℝ) \to (F (I) \in ℝ^{} \land F (I + 1) \in ℝ^{})$
87	86	adantl	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to (F (I) \in ℝ^{} \land F (I + 1) \in ℝ^{})$
88		elico1	$⊢ (F (I) \in ℝ^{} \land F (I + 1) \in ℝ^{}) \to (X \in [F (I), F (I + 1)) \leftrightarrow (X \in ℝ^{*} \land F (I) \leq X \land X < F (I + 1)))$
89	87 88	syl	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to (X \in [F (I), F (I + 1)) \leftrightarrow (X \in ℝ^{*} \land F (I) \leq X \land X < F (I + 1)))$
90		simpllr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to X \in ℝ$
91		simplrl	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to F (I + 1) \in ℝ$
92		simplrr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to F (I) \in ℝ$
93		simpr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to X < F (I + 1)$
94	90 91 92 93	ltsub1dd	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to X - F (I) < F (I + 1) - F (I)$
95		simplr	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to X \in ℝ$
96		simprr	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to F (I) \in ℝ$
97	95 96	resubcld	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to X - F (I) \in ℝ$
98	97	adantr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to X - F (I) \in ℝ$
99	91 92	resubcld	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to F (I + 1) - F (I) \in ℝ$
100		simplll	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to N \in ℝ$
101		4re	$⊢ 4 \in ℝ$
102	101	a1i	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to 4 \in ℝ$
103	100 102	resubcld	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to N - 4 \in ℝ$
104		lttr	$⊢ (X - F (I) \in ℝ \land F (I + 1) - F (I) \in ℝ \land N - 4 \in ℝ) \to ((X - F (I) < F (I + 1) - F (I) \land F (I + 1) - F (I) < N - 4) \to X - F (I) < N - 4)$
105	98 99 103 104	syl3anc	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to ((X - F (I) < F (I + 1) - F (I) \land F (I + 1) - F (I) < N - 4) \to X - F (I) < N - 4)$
106	94 105	mpand	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land X < F (I + 1)) \to (F (I + 1) - F (I) < N - 4 \to X - F (I) < N - 4)$
107	106	impr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land (X < F (I + 1) \land F (I + 1) - F (I) < N - 4)) \to X - F (I) < N - 4$
108		4pos	$⊢ 0 < 4$
109	101	a1i	$⊢ (N \in ℝ \land X \in ℝ) \to 4 \in ℝ$
110		simpl	$⊢ (N \in ℝ \land X \in ℝ) \to N \in ℝ$
111	109 110	ltsubposd	$⊢ (N \in ℝ \land X \in ℝ) \to (0 < 4 \leftrightarrow N - 4 < N)$
112	108 111	mpbii	$⊢ (N \in ℝ \land X \in ℝ) \to N - 4 < N$
113	112	adantr	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to N - 4 < N$
114	113	adantr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land (X < F (I + 1) \land F (I + 1) - F (I) < N - 4)) \to N - 4 < N$
115		simpll	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to N \in ℝ$
116	101	a1i	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to 4 \in ℝ$
117	115 116	resubcld	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to N - 4 \in ℝ$
118		lttr	$⊢ (X - F (I) \in ℝ \land N - 4 \in ℝ \land N \in ℝ) \to ((X - F (I) < N - 4 \land N - 4 < N) \to X - F (I) < N)$
119	97 117 115 118	syl3anc	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to ((X - F (I) < N - 4 \land N - 4 < N) \to X - F (I) < N)$
120	119	adantr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land (X < F (I + 1) \land F (I + 1) - F (I) < N - 4)) \to ((X - F (I) < N - 4 \land N - 4 < N) \to X - F (I) < N)$
121	107 114 120	mp2and	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \land (X < F (I + 1) \land F (I + 1) - F (I) < N - 4)) \to X - F (I) < N$
122	121	exp32	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to (X < F (I + 1) \to (F (I + 1) - F (I) < N - 4 \to X - F (I) < N))$
123	122	com12	$⊢ X < F (I + 1) \to (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to (F (I + 1) - F (I) < N - 4 \to X - F (I) < N))$
124	123	3ad2ant3	$⊢ (X \in ℝ^{*} \land F (I) \leq X \land X < F (I + 1)) \to (((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to (F (I + 1) - F (I) < N - 4 \to X - F (I) < N))$
125	124	com12	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to ((X \in ℝ^{*} \land F (I) \leq X \land X < F (I + 1)) \to (F (I + 1) - F (I) < N - 4 \to X - F (I) < N))$
126	89 125	sylbid	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to (X \in [F (I), F (I + 1)) \to (F (I + 1) - F (I) < N - 4 \to X - F (I) < N))$
127	126	com23	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I + 1) \in ℝ \land F (I) \in ℝ)) \to (F (I + 1) - F (I) < N - 4 \to (X \in [F (I), F (I + 1)) \to X - F (I) < N))$
128	127	exp32	$⊢ (N \in ℝ \land X \in ℝ) \to (F (I + 1) \in ℝ \to (F (I) \in ℝ \to (F (I + 1) - F (I) < N - 4 \to (X \in [F (I), F (I + 1)) \to X - F (I) < N))))$
129	128	com34	$⊢ (N \in ℝ \land X \in ℝ) \to (F (I + 1) \in ℝ \to (F (I + 1) - F (I) < N - 4 \to (F (I) \in ℝ \to (X \in [F (I), F (I + 1)) \to X - F (I) < N))))$
130	81 83 129	syl2an	$⊢ (φ \land X \in Odd) \to (F (I + 1) \in ℝ \to (F (I + 1) - F (I) < N - 4 \to (F (I) \in ℝ \to (X \in [F (I), F (I + 1)) \to X - F (I) < N))))$
131	130	3adant3	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I + 1) \in ℝ \to (F (I + 1) - F (I) < N - 4 \to (F (I) \in ℝ \to (X \in [F (I), F (I + 1)) \to X - F (I) < N))))$
132	79 131	mpd	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I + 1) - F (I) < N - 4 \to (F (I) \in ℝ \to (X \in [F (I), F (I + 1)) \to X - F (I) < N)))$
133	132	com13	$⊢ F (I) \in ℝ \to (F (I + 1) - F (I) < N - 4 \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (X \in [F (I), F (I + 1)) \to X - F (I) < N)))$
134	33 35 133	3syl	$⊢ F (I) \in (ℙ ∖ \{2\}) \to (F (I + 1) - F (I) < N - 4 \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (X \in [F (I), F (I + 1)) \to X - F (I) < N)))$
135	134	imp	$⊢ (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4) \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (X \in [F (I), F (I + 1)) \to X - F (I) < N))$
136	135	3adant3	$⊢ (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I)) \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (X \in [F (I), F (I + 1)) \to X - F (I) < N))$
137	136	impcom	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \to (X \in [F (I), F (I + 1)) \to X - F (I) < N)$
138	137	imp	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \land X \in [F (I), F (I + 1))) \to X - F (I) < N$
139	138	adantrr	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \land (X \in [F (I), F (I + 1)) \land 4 < S)) \to X - F (I) < N$
140	11 139	eqbrtrid	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \land (X \in [F (I), F (I + 1)) \land 4 < S)) \to S < N$
141		simprr	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \land (X \in [F (I), F (I + 1)) \land 4 < S)) \to 4 < S$
142	32 140 141	3jca	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \land (X \in [F (I), F (I + 1)) \land 4 < S)) \to (S \in Even \land S < N \land 4 < S)$
143	142	ex	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I))) \to ((X \in [F (I), F (I + 1)) \land 4 < S) \to (S \in Even \land S < N \land 4 < S))$
144	24 143	mpdan	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to ((X \in [F (I), F (I + 1)) \land 4 < S) \to (S \in Even \land S < N \land 4 < S))$

Metamath Proof Explorer

Theorem bgoldbtbndlem3

Proof