Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 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 bgoldbtbnd ( 𝜑 → ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < 𝑀 ) → 𝑛 ∈ GoldbachOdd ) )

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