Metamath Proof Explorer

Theorem bgoldbtbndlem4

Description: Lemma 4 for bgoldbtbnd . (Contributed by AV, 1-Aug-2020)

Ref Expression
Hypotheses bgoldbtbnd.m ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 1 ) )
bgoldbtbnd.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 1 ) )
bgoldbtbnd.b ⊢ ( 𝜑 → ∀ 𝑛 ∈ Even ( ( 4 < 𝑛 ∧ 𝑛 < 𝑁 ) → 𝑛 ∈ GoldbachEven ) )
bgoldbtbnd.d ⊢ ( 𝜑 → 𝐷 ∈ ( ℤ≥ ‘ 3 ) )
bgoldbtbnd.f ⊢ ( 𝜑 → 𝐹 ∈ ( RePart ‘ 𝐷 ) )
bgoldbtbnd.i ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝐷 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ) )
bgoldbtbnd.0 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 7 )
bgoldbtbnd.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = 1 3 )
bgoldbtbnd.l ⊢ ( 𝜑 → 𝑀 < ( 𝐹 ‘ 𝐷 ) )
bgoldbtbnd.r ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐷 ) ∈ ℝ )
Assertion bgoldbtbndlem4 ( ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ 𝑋 ∈ Odd ) → ( ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑋 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )

Proof

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