bgoldbtbndlem2

	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)$
	bgoldbtbndlem2.s	$⊢ S = X - F (I - 1)$
Assertion	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 (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		bgoldbtbndlem2.s	$⊢ S = X - F (I - 1)$
11		elfzoelz	$⊢ I \in (1 ..^D) \to I \in ℤ$
12		elfzoel2	$⊢ I \in (1 ..^D) \to D \in ℤ$
13		elfzom1b	$⊢ (I \in ℤ \land D \in ℤ) \to (I \in (1 ..^D) \leftrightarrow I - 1 \in (0 ..^D - 1))$
14		fzossrbm1	$⊢ D \in ℤ \to (0 ..^D - 1) \subseteq (0 ..^D)$
15	14	adantl	$⊢ (I \in ℤ \land D \in ℤ) \to (0 ..^D - 1) \subseteq (0 ..^D)$
16	15	sseld	$⊢ (I \in ℤ \land D \in ℤ) \to (I - 1 \in (0 ..^D - 1) \to I - 1 \in (0 ..^D))$
17	13 16	sylbid	$⊢ (I \in ℤ \land D \in ℤ) \to (I \in (1 ..^D) \to I - 1 \in (0 ..^D))$
18	17	com12	$⊢ I \in (1 ..^D) \to ((I \in ℤ \land D \in ℤ) \to I - 1 \in (0 ..^D))$
19	11 12 18	mp2and	$⊢ I \in (1 ..^D) \to I - 1 \in (0 ..^D)$
20		fveq2	$⊢ i = I - 1 \to F (i) = F (I - 1)$
21	20	eleq1d	$⊢ i = I - 1 \to (F (i) \in (ℙ ∖ \{2\}) \leftrightarrow F (I - 1) \in (ℙ ∖ \{2\}))$
22		fvoveq1	$⊢ i = I - 1 \to F (i + 1) = F (I - 1 + 1)$
23	22 20	oveq12d	$⊢ i = I - 1 \to F (i + 1) - F (i) = F (I - 1 + 1) - F (I - 1)$
24	23	breq1d	$⊢ i = I - 1 \to (F (i + 1) - F (i) < N - 4 \leftrightarrow F (I - 1 + 1) - F (I - 1) < N - 4)$
25	23	breq2d	$⊢ i = I - 1 \to (4 < F (i + 1) - F (i) \leftrightarrow 4 < F (I - 1 + 1) - F (I - 1))$
26	21 24 25	3anbi123d	$⊢ i = I - 1 \to ((F (i) \in (ℙ ∖ \{2\}) \land F (i + 1) - F (i) < N - 4 \land 4 < F (i + 1) - F (i)) \leftrightarrow (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1)))$
27	26	rspcv	$⊢ I - 1 \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 - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1)))$
28	19 27	syl	$⊢ I \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 (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1)))$
29	6 28	syl5com	$⊢ φ \to (I \in (1 ..^D) \to (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1)))$
30	29	a1d	$⊢ φ \to (X \in Odd \to (I \in (1 ..^D) \to (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))))$
31	30	3imp	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))$
32		simp2	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to X \in Odd$
33		oddprmALTV	$⊢ F (I - 1) \in (ℙ ∖ \{2\}) \to F (I - 1) \in Odd$
34	33	3ad2ant1	$⊢ (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1)) \to F (I - 1) \in Odd$
35	32 34	anim12i	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \to (X \in Odd \land F (I - 1) \in Odd)$
36	35	adantr	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to (X \in Odd \land F (I - 1) \in Odd)$
37		omoeALTV	$⊢ (X \in Odd \land F (I - 1) \in Odd) \to X - F (I - 1) \in Even$
38	36 37	syl	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to X - F (I - 1) \in Even$
39	10 38	eqeltrid	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to S \in Even$
40	11	zcnd	$⊢ I \in (1 ..^D) \to I \in ℂ$
41	40	3ad2ant3	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to I \in ℂ$
42		npcan1	$⊢ I \in ℂ \to I - 1 + 1 = I$
43	41 42	syl	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to I - 1 + 1 = I$
44	43	fveq2d	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to F (I - 1 + 1) = F (I)$
45	44	oveq1d	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to F (I - 1 + 1) - F (I - 1) = F (I) - F (I - 1)$
46	45	breq1d	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I - 1 + 1) - F (I - 1) < N - 4 \leftrightarrow F (I) - F (I - 1) < N - 4)$
47	46	adantr	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land F (I - 1) \in (ℙ ∖ \{2\})) \to (F (I - 1 + 1) - F (I - 1) < N - 4 \leftrightarrow F (I) - F (I - 1) < N - 4)$
48		eldifi	$⊢ F (I - 1) \in (ℙ ∖ \{2\}) \to F (I - 1) \in ℙ$
49		prmz	$⊢ F (I - 1) \in ℙ \to F (I - 1) \in ℤ$
50		zre	$⊢ F (I - 1) \in ℤ \to F (I - 1) \in ℝ$
51		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\})$
52	51	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\})$
53		fzo0ss1	$⊢ (1 ..^D) \subseteq (0 ..^D)$
54	53	sseli	$⊢ I \in (1 ..^D) \to I \in (0 ..^D)$
55	54	adantl	$⊢ (φ \land I \in (1 ..^D)) \to I \in (0 ..^D)$
56		fveq2	$⊢ i = I \to F (i) = F (I)$
57	56	eleq1d	$⊢ i = I \to (F (i) \in (ℙ ∖ \{2\}) \leftrightarrow F (I) \in (ℙ ∖ \{2\}))$
58	57	rspcv	$⊢ I \in (0 ..^D) \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I) \in (ℙ ∖ \{2\}))$
59	55 58	syl	$⊢ (φ \land I \in (1 ..^D)) \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I) \in (ℙ ∖ \{2\}))$
60	59	ex	$⊢ φ \to (I \in (1 ..^D) \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to F (I) \in (ℙ ∖ \{2\})))$
61	60	com23	$⊢ φ \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to (I \in (1 ..^D) \to F (I) \in (ℙ ∖ \{2\})))$
62	61	a1i	$⊢ X \in Odd \to (φ \to (\forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to (I \in (1 ..^D) \to F (I) \in (ℙ ∖ \{2\}))))$
63	62	com13	$⊢ \forall i \in (0 ..^D) F (i) \in (ℙ ∖ \{2\}) \to (φ \to (X \in Odd \to (I \in (1 ..^D) \to F (I) \in (ℙ ∖ \{2\}))))$
64	52 63	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 (X \in Odd \to (I \in (1 ..^D) \to F (I) \in (ℙ ∖ \{2\}))))$
65	6 64	mpcom	$⊢ φ \to (X \in Odd \to (I \in (1 ..^D) \to F (I) \in (ℙ ∖ \{2\})))$
66	65	3imp	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to F (I) \in (ℙ ∖ \{2\})$
67		eldifi	$⊢ F (I) \in (ℙ ∖ \{2\}) \to F (I) \in ℙ$
68		prmz	$⊢ F (I) \in ℙ \to F (I) \in ℤ$
69		zre	$⊢ F (I) \in ℤ \to F (I) \in ℝ$
70		eluzelz	$⊢ N \in ℤ_{\geq 11} \to N \in ℤ$
71		zre	$⊢ N \in ℤ \to N \in ℝ$
72		oddz	$⊢ X \in Odd \to X \in ℤ$
73	72	zred	$⊢ X \in Odd \to X \in ℝ$
74		simplr	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to X \in ℝ$
75		simprl	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to F (I) \in ℝ$
76		4re	$⊢ 4 \in ℝ$
77	76	a1i	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to 4 \in ℝ$
78	74 75 77	lesubaddd	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to (X - F (I) \leq 4 \leftrightarrow X \leq 4 + F (I))$
79		simpllr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to X \in ℝ$
80		simplrr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to F (I - 1) \in ℝ$
81	79 80	resubcld	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to X - F (I - 1) \in ℝ$
82	76	a1i	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to 4 \in ℝ$
83		simplrl	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to F (I) \in ℝ$
84	82 83	readdcld	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to 4 + F (I) \in ℝ$
85	84 80	resubcld	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to 4 + F (I) - F (I - 1) \in ℝ$
86		simplll	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to N \in ℝ$
87	77 75	readdcld	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to 4 + F (I) \in ℝ$
88		simprr	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to F (I - 1) \in ℝ$
89	74 87 88	lesub1d	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to (X \leq 4 + F (I) \leftrightarrow X - F (I - 1) \leq 4 + F (I) - F (I - 1))$
90	89	biimpa	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land X \leq 4 + F (I)) \to X - F (I - 1) \leq 4 + F (I) - F (I - 1)$
91	90	adantrr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to X - F (I - 1) \leq 4 + F (I) - F (I - 1)$
92		resubcl	$⊢ (F (I) \in ℝ \land F (I - 1) \in ℝ) \to F (I) - F (I - 1) \in ℝ$
93	92	adantl	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to F (I) - F (I - 1) \in ℝ$
94		simpll	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to N \in ℝ$
95		ltaddsub2	$⊢ (4 \in ℝ \land F (I) - F (I - 1) \in ℝ \land N \in ℝ) \to (4 + F (I) - F (I - 1) < N \leftrightarrow F (I) - F (I - 1) < N - 4)$
96	95	bicomd	$⊢ (4 \in ℝ \land F (I) - F (I - 1) \in ℝ \land N \in ℝ) \to (F (I) - F (I - 1) < N - 4 \leftrightarrow 4 + F (I) - F (I - 1) < N)$
97	77 93 94 96	syl3anc	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to (F (I) - F (I - 1) < N - 4 \leftrightarrow 4 + F (I) - F (I - 1) < N)$
98	97	biimpd	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to (F (I) - F (I - 1) < N - 4 \to 4 + F (I) - F (I - 1) < N)$
99	98	adantld	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to ((X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4) \to 4 + F (I) - F (I - 1) < N)$
100	99	imp	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to 4 + F (I) - F (I - 1) < N$
101		4cn	$⊢ 4 \in ℂ$
102	101	a1i	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to 4 \in ℂ$
103	75	recnd	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to F (I) \in ℂ$
104		recn	$⊢ F (I - 1) \in ℝ \to F (I - 1) \in ℂ$
105	104	adantl	$⊢ (F (I) \in ℝ \land F (I - 1) \in ℝ) \to F (I - 1) \in ℂ$
106	105	adantl	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to F (I - 1) \in ℂ$
107	102 103 106	addsubassd	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to 4 + F (I) - F (I - 1) = 4 + F (I) - F (I - 1)$
108	107	breq1d	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to (4 + F (I) - F (I - 1) < N \leftrightarrow 4 + F (I) - F (I - 1) < N)$
109	108	adantr	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to (4 + F (I) - F (I - 1) < N \leftrightarrow 4 + F (I) - F (I - 1) < N)$
110	100 109	mpbird	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to 4 + F (I) - F (I - 1) < N$
111	81 85 86 91 110	lelttrd	$⊢ (((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \land (X \leq 4 + F (I) \land F (I) - F (I - 1) < N - 4)) \to X - F (I - 1) < N$
112	111	exp32	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to (X \leq 4 + F (I) \to (F (I) - F (I - 1) < N - 4 \to X - F (I - 1) < N))$
113	78 112	sylbid	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to (X - F (I) \leq 4 \to (F (I) - F (I - 1) < N - 4 \to X - F (I - 1) < N))$
114	113	com23	$⊢ ((N \in ℝ \land X \in ℝ) \land (F (I) \in ℝ \land F (I - 1) \in ℝ)) \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N))$
115	114	exp32	$⊢ (N \in ℝ \land X \in ℝ) \to (F (I) \in ℝ \to (F (I - 1) \in ℝ \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N))))$
116	73 115	sylan2	$⊢ (N \in ℝ \land X \in Odd) \to (F (I) \in ℝ \to (F (I - 1) \in ℝ \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N))))$
117	116	ex	$⊢ N \in ℝ \to (X \in Odd \to (F (I) \in ℝ \to (F (I - 1) \in ℝ \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N)))))$
118	71 117	syl	$⊢ N \in ℤ \to (X \in Odd \to (F (I) \in ℝ \to (F (I - 1) \in ℝ \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N)))))$
119	2 70 118	3syl	$⊢ φ \to (X \in Odd \to (F (I) \in ℝ \to (F (I - 1) \in ℝ \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N)))))$
120	119	imp	$⊢ (φ \land X \in Odd) \to (F (I) \in ℝ \to (F (I - 1) \in ℝ \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N))))$
121	120	3adant3	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I) \in ℝ \to (F (I - 1) \in ℝ \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N))))$
122	69 121	syl5com	$⊢ F (I) \in ℤ \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I - 1) \in ℝ \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N))))$
123	67 68 122	3syl	$⊢ F (I) \in (ℙ ∖ \{2\}) \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I - 1) \in ℝ \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N))))$
124	66 123	mpcom	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I - 1) \in ℝ \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N)))$
125	50 124	syl5com	$⊢ F (I - 1) \in ℤ \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N)))$
126	48 49 125	3syl	$⊢ F (I - 1) \in (ℙ ∖ \{2\}) \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N)))$
127	126	impcom	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land F (I - 1) \in (ℙ ∖ \{2\})) \to (F (I) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N))$
128	47 127	sylbid	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land F (I - 1) \in (ℙ ∖ \{2\})) \to (F (I - 1 + 1) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N))$
129	128	expcom	$⊢ F (I - 1) \in (ℙ ∖ \{2\}) \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I - 1 + 1) - F (I - 1) < N - 4 \to (X - F (I) \leq 4 \to X - F (I - 1) < N)))$
130	129	com23	$⊢ F (I - 1) \in (ℙ ∖ \{2\}) \to (F (I - 1 + 1) - F (I - 1) < N - 4 \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (X - F (I) \leq 4 \to X - F (I - 1) < N)))$
131	130	imp	$⊢ (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4) \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (X - F (I) \leq 4 \to X - F (I - 1) < N))$
132	131	3adant3	$⊢ (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1)) \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to (X - F (I) \leq 4 \to X - F (I - 1) < N))$
133	132	impcom	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \to (X - F (I) \leq 4 \to X - F (I - 1) < N)$
134	133	com12	$⊢ X - F (I) \leq 4 \to (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \to X - F (I - 1) < N)$
135	134	adantl	$⊢ (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4) \to (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \to X - F (I - 1) < N)$
136	135	impcom	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to X - F (I - 1) < N$
137	10 136	eqbrtrid	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to S < N$
138	76	a1i	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to 4 \in ℝ$
139		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
140		fzoss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 ..^D) \subseteq (0 ..^D)$
141	139 140	mp1i	$⊢ φ \to (1 ..^D) \subseteq (0 ..^D)$
142	141	sselda	$⊢ (φ \land I \in (1 ..^D)) \to I \in (0 ..^D)$
143		fvoveq1	$⊢ i = I \to F (i + 1) = F (I + 1)$
144	143 56	oveq12d	$⊢ i = I \to F (i + 1) - F (i) = F (I + 1) - F (I)$
145	144	breq1d	$⊢ i = I \to (F (i + 1) - F (i) < N - 4 \leftrightarrow F (I + 1) - F (I) < N - 4)$
146	144	breq2d	$⊢ i = I \to (4 < F (i + 1) - F (i) \leftrightarrow 4 < F (I + 1) - F (I))$
147	57 145 146	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)))$
148	147	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)))$
149	142 148	syl	$⊢ (φ \land I \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 (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I)))$
150	68	zred	$⊢ F (I) \in ℙ \to F (I) \in ℝ$
151	67 150	syl	$⊢ F (I) \in (ℙ ∖ \{2\}) \to F (I) \in ℝ$
152	151	3ad2ant1	$⊢ (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I)) \to F (I) \in ℝ$
153	149 152	syl6	$⊢ (φ \land I \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 (I) \in ℝ)$
154	153	ex	$⊢ φ \to (I \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 (I) \in ℝ))$
155	6 154	mpid	$⊢ φ \to (I \in (1 ..^D) \to F (I) \in ℝ)$
156	155	imp	$⊢ (φ \land I \in (1 ..^D)) \to F (I) \in ℝ$
157	156	3adant2	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to F (I) \in ℝ$
158	157	ad2antrr	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to F (I) \in ℝ$
159	49	zred	$⊢ F (I - 1) \in ℙ \to F (I - 1) \in ℝ$
160	48 159	syl	$⊢ F (I - 1) \in (ℙ ∖ \{2\}) \to F (I - 1) \in ℝ$
161	160	3ad2ant1	$⊢ (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1)) \to F (I - 1) \in ℝ$
162	161	ad2antlr	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to F (I - 1) \in ℝ$
163	158 162	resubcld	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to F (I) - F (I - 1) \in ℝ$
164	73	3ad2ant2	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to X \in ℝ$
165		resubcl	$⊢ (X \in ℝ \land F (I - 1) \in ℝ) \to X - F (I - 1) \in ℝ$
166	164 161 165	syl2an	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \to X - F (I - 1) \in ℝ$
167	166	adantr	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to X - F (I - 1) \in ℝ$
168	40 42	syl	$⊢ I \in (1 ..^D) \to I - 1 + 1 = I$
169	168	3ad2ant3	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to I - 1 + 1 = I$
170	169	fveq2d	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to F (I - 1 + 1) = F (I)$
171	170	oveq1d	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to F (I - 1 + 1) - F (I - 1) = F (I) - F (I - 1)$
172	171	breq2d	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (4 < F (I - 1 + 1) - F (I - 1) \leftrightarrow 4 < F (I) - F (I - 1))$
173	172	biimpcd	$⊢ 4 < F (I - 1 + 1) - F (I - 1) \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to 4 < F (I) - F (I - 1))$
174	173	3ad2ant3	$⊢ (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1)) \to ((φ \land X \in Odd \land I \in (1 ..^D)) \to 4 < F (I) - F (I - 1))$
175	174	impcom	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \to 4 < F (I) - F (I - 1)$
176	175	adantr	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to 4 < F (I) - F (I - 1)$
177	164	ad2antrr	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to X \in ℝ$
178		eluzge3nn	$⊢ D \in ℤ_{\geq 3} \to D \in ℕ$
179	4 178	syl	$⊢ φ \to D \in ℕ$
180	179	adantr	$⊢ (φ \land I \in (1 ..^D)) \to D \in ℕ$
181	5	adantr	$⊢ (φ \land I \in (1 ..^D)) \to F \in RePart (D)$
182	139 140	mp1i	$⊢ D \in ℤ_{\geq 3} \to (1 ..^D) \subseteq (0 ..^D)$
183		fzossfz	$⊢ (0 ..^D) \subseteq (0 \dots D)$
184	182 183	sstrdi	$⊢ D \in ℤ_{\geq 3} \to (1 ..^D) \subseteq (0 \dots D)$
185	4 184	syl	$⊢ φ \to (1 ..^D) \subseteq (0 \dots D)$
186	185	sselda	$⊢ (φ \land I \in (1 ..^D)) \to I \in (0 \dots D)$
187	180 181 186	iccpartxr	$⊢ (φ \land I \in (1 ..^D)) \to F (I) \in ℝ^{*}$
188		fzofzp1	$⊢ I \in (0 ..^D) \to I + 1 \in (0 \dots D)$
189	142 188	syl	$⊢ (φ \land I \in (1 ..^D)) \to I + 1 \in (0 \dots D)$
190	180 181 189	iccpartxr	$⊢ (φ \land I \in (1 ..^D)) \to F (I + 1) \in ℝ^{*}$
191	187 190	jca	$⊢ (φ \land I \in (1 ..^D)) \to (F (I) \in ℝ^{} \land F (I + 1) \in ℝ^{})$
192	191	3adant2	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I) \in ℝ^{} \land F (I + 1) \in ℝ^{})$
193		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)))$
194	192 193	syl	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (X \in [F (I), F (I + 1)) \leftrightarrow (X \in ℝ^{*} \land F (I) \leq X \land X < F (I + 1)))$
195		simp2	$⊢ (X \in ℝ^{*} \land F (I) \leq X \land X < F (I + 1)) \to F (I) \leq X$
196	194 195	syl6bi	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (X \in [F (I), F (I + 1)) \to F (I) \leq X)$
197	196	adantrd	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to ((X \in [F (I), F (I + 1)) \land X - F (I) \leq 4) \to F (I) \leq X)$
198	197	adantr	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \to ((X \in [F (I), F (I + 1)) \land X - F (I) \leq 4) \to F (I) \leq X)$
199	198	imp	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to F (I) \leq X$
200	158 177 162 199	lesub1dd	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to F (I) - F (I - 1) \leq X - F (I - 1)$
201	138 163 167 176 200	ltletrd	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to 4 < X - F (I - 1)$
202	201 10	breqtrrdi	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to 4 < S$
203	39 137 202	3jca	$⊢ (((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \land (X \in [F (I), F (I + 1)) \land X - F (I) \leq 4)) \to (S \in Even \land S < N \land 4 < S)$
204	203	ex	$⊢ ((φ \land X \in Odd \land I \in (1 ..^D)) \land (F (I - 1) \in (ℙ ∖ \{2\}) \land F (I - 1 + 1) - F (I - 1) < N - 4 \land 4 < F (I - 1 + 1) - F (I - 1))) \to ((X \in [F (I), F (I + 1)) \land X - F (I) \leq 4) \to (S \in Even \land S < N \land 4 < S))$
205	31 204	mpdan	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to ((X \in [F (I), F (I + 1)) \land X - F (I) \leq 4) \to (S \in Even \land S < N \land 4 < S))$

Metamath Proof Explorer

Theorem bgoldbtbndlem2

Proof