Metamath Proof Explorer

Theorem bgoldbtbndlem4

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

Ref Expression
Hypotheses bgoldbtbnd.m 
|- ( ph -> M e. ( ZZ>= ` ; 1 1 ) )
bgoldbtbnd.n 
|- ( ph -> N e. ( ZZ>= ` ; 1 1 ) )
bgoldbtbnd.b 
|- ( ph -> A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) )
bgoldbtbnd.d 
|- ( ph -> D e. ( ZZ>= ` 3 ) )
bgoldbtbnd.f 
|- ( ph -> F e. ( RePart ` D ) )
bgoldbtbnd.i 
|- ( ph -> A. i e. ( 0 ..^ D ) ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) )
bgoldbtbnd.0 
|- ( ph -> ( F ` 0 ) = 7 )
bgoldbtbnd.1 
|- ( ph -> ( F ` 1 ) = ; 1 3 )
bgoldbtbnd.l 
|- ( ph -> M < ( F ` D ) )
bgoldbtbnd.r 
|- ( ph -> ( F ` D ) e. RR )
Assertion bgoldbtbndlem4 
|- ( ( ( ph /\ I e. ( 1 ..^ D ) ) /\ X e. Odd ) -> ( ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ X = ( ( p + q ) + r ) ) ) )

Proof

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