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	2 70 71 117	4syl	$⊢ φ \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	118	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))))$
120	119	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))))$
121	69 120	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))))$
122	67 68 121	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))))$
123	66 122	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)))$
124	50 123	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)))$
125	48 49 124	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)))$
126	125	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))$
127	47 126	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))$
128	127	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)))$
129	128	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)))$
130	129	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))$
131	130	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))$
132	131	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)$
133	132	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)$
134	133	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)$
135	134	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$
136	10 135	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$
137	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 ℝ$
138		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
139		fzoss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 ..^D) \subseteq (0 ..^D)$
140	138 139	mp1i	$⊢ φ \to (1 ..^D) \subseteq (0 ..^D)$
141	140	sselda	$⊢ (φ \land I \in (1 ..^D)) \to I \in (0 ..^D)$
142		fvoveq1	$⊢ i = I \to F (i + 1) = F (I + 1)$
143	142 56	oveq12d	$⊢ i = I \to F (i + 1) - F (i) = F (I + 1) - F (I)$
144	143	breq1d	$⊢ i = I \to (F (i + 1) - F (i) < N - 4 \leftrightarrow F (I + 1) - F (I) < N - 4)$
145	143	breq2d	$⊢ i = I \to (4 < F (i + 1) - F (i) \leftrightarrow 4 < F (I + 1) - F (I))$
146	57 144 145	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)))$
147	146	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)))$
148	141 147	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)))$
149	68	zred	$⊢ F (I) \in ℙ \to F (I) \in ℝ$
150	67 149	syl	$⊢ F (I) \in (ℙ ∖ \{2\}) \to F (I) \in ℝ$
151	150	3ad2ant1	$⊢ (F (I) \in (ℙ ∖ \{2\}) \land F (I + 1) - F (I) < N - 4 \land 4 < F (I + 1) - F (I)) \to F (I) \in ℝ$
152	148 151	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 ℝ)$
153	152	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 ℝ))$
154	6 153	mpid	$⊢ φ \to (I \in (1 ..^D) \to F (I) \in ℝ)$
155	154	imp	$⊢ (φ \land I \in (1 ..^D)) \to F (I) \in ℝ$
156	155	3adant2	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to F (I) \in ℝ$
157	156	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 ℝ$
158	49	zred	$⊢ F (I - 1) \in ℙ \to F (I - 1) \in ℝ$
159	48 158	syl	$⊢ F (I - 1) \in (ℙ ∖ \{2\}) \to F (I - 1) \in ℝ$
160	159	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 ℝ$
161	160	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 ℝ$
162	157 161	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 ℝ$
163	73	3ad2ant2	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to X \in ℝ$
164		resubcl	$⊢ (X \in ℝ \land F (I - 1) \in ℝ) \to X - F (I - 1) \in ℝ$
165	163 160 164	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 ℝ$
166	165	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 ℝ$
167	40 42	syl	$⊢ I \in (1 ..^D) \to I - 1 + 1 = I$
168	167	3ad2ant3	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to I - 1 + 1 = I$
169	168	fveq2d	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to F (I - 1 + 1) = F (I)$
170	169	oveq1d	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to F (I - 1 + 1) - F (I - 1) = F (I) - F (I - 1)$
171	170	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))$
172	171	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))$
173	172	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))$
174	173	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)$
175	174	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)$
176	163	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 ℝ$
177		eluz3nn	$⊢ D \in ℤ_{\geq 3} \to D \in ℕ$
178	4 177	syl	$⊢ φ \to D \in ℕ$
179	178	adantr	$⊢ (φ \land I \in (1 ..^D)) \to D \in ℕ$
180	5	adantr	$⊢ (φ \land I \in (1 ..^D)) \to F \in RePart (D)$
181	138 139	mp1i	$⊢ D \in ℤ_{\geq 3} \to (1 ..^D) \subseteq (0 ..^D)$
182		fzossfz	$⊢ (0 ..^D) \subseteq (0 \dots D)$
183	181 182	sstrdi	$⊢ D \in ℤ_{\geq 3} \to (1 ..^D) \subseteq (0 \dots D)$
184	4 183	syl	$⊢ φ \to (1 ..^D) \subseteq (0 \dots D)$
185	184	sselda	$⊢ (φ \land I \in (1 ..^D)) \to I \in (0 \dots D)$
186	179 180 185	iccpartxr	$⊢ (φ \land I \in (1 ..^D)) \to F (I) \in ℝ^{*}$
187		fzofzp1	$⊢ I \in (0 ..^D) \to I + 1 \in (0 \dots D)$
188	141 187	syl	$⊢ (φ \land I \in (1 ..^D)) \to I + 1 \in (0 \dots D)$
189	179 180 188	iccpartxr	$⊢ (φ \land I \in (1 ..^D)) \to F (I + 1) \in ℝ^{*}$
190	186 189	jca	$⊢ (φ \land I \in (1 ..^D)) \to (F (I) \in ℝ^{} \land F (I + 1) \in ℝ^{})$
191	190	3adant2	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (F (I) \in ℝ^{} \land F (I + 1) \in ℝ^{})$
192		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)))$
193	191 192	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)))$
194		simp2	$⊢ (X \in ℝ^{*} \land F (I) \leq X \land X < F (I + 1)) \to F (I) \leq X$
195	193 194	biimtrdi	$⊢ (φ \land X \in Odd \land I \in (1 ..^D)) \to (X \in [F (I), F (I + 1)) \to F (I) \leq X)$
196	195	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)$
197	196	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)$
198	197	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$
199	157 176 161 198	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)$
200	137 162 166 175 199	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)$
201	200 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$
202	39 136 201	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)$
203	202	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))$
204	31 203	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