Metamath Proof Explorer

Theorem tgblthelfgott

Description: The ternary Goldbach conjecture is valid for all odd numbers less than 8.8 x 10^30 (actually 8.875694 x 10^30, see section 1.2.2 in Helfgott p. 4, using bgoldbachlt , ax-hgprmladder and bgoldbtbnd . (Contributed by AV, 4-Aug-2020) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion tgblthelfgott 
|- ( ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> N e. GoldbachOdd )

Proof

Step Hyp Ref Expression
1 ax-hgprmladder 
 |-  E. d e. ( ZZ>= ` 3 ) E. f e. ( RePart ` d ) ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) )
2 1nn0 
 |-  1 e. NN0
3 1nn 
 |-  1 e. NN
4 2 3 decnncl 
 |-  ; 1 1 e. NN
5 4 nnzi 
 |-  ; 1 1 e. ZZ
6 8nn0 
 |-  8 e. NN0
7 8nn 
 |-  8 e. NN
8 6 7 decnncl 
 |-  ; 8 8 e. NN
9 10nn 
 |-  ; 1 0 e. NN
10 2nn0 
 |-  2 e. NN0
11 9nn 
 |-  9 e. NN
12 10 11 decnncl 
 |-  ; 2 9 e. NN
13 12 nnnn0i 
 |-  ; 2 9 e. NN0
14 nnexpcl 
 |-  ( ( ; 1 0 e. NN /\ ; 2 9 e. NN0 ) -> ( ; 1 0 ^ ; 2 9 ) e. NN )
15 9 13 14 mp2an 
 |-  ( ; 1 0 ^ ; 2 9 ) e. NN
16 8 15 nnmulcli 
 |-  ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN
17 16 nnzi 
 |-  ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. ZZ
18 1re 
 |-  1 e. RR
19 8 nnrei 
 |-  ; 8 8 e. RR
20 18 19 pm3.2i 
 |-  ( 1 e. RR /\ ; 8 8 e. RR )
21 0le1 
 |-  0 <_ 1
22 1lt10 
 |-  1 < ; 1 0
23 7 6 2 22 declti 
 |-  1 < ; 8 8
24 21 23 pm3.2i 
 |-  ( 0 <_ 1 /\ 1 < ; 8 8 )
25 nnexpcl 
 |-  ( ( ; 1 0 e. NN /\ 1 e. NN0 ) -> ( ; 1 0 ^ 1 ) e. NN )
26 9 2 25 mp2an 
 |-  ( ; 1 0 ^ 1 ) e. NN
27 26 nnrei 
 |-  ( ; 1 0 ^ 1 ) e. RR
28 15 nnrei 
 |-  ( ; 1 0 ^ ; 2 9 ) e. RR
29 27 28 pm3.2i 
 |-  ( ( ; 1 0 ^ 1 ) e. RR /\ ( ; 1 0 ^ ; 2 9 ) e. RR )
30 0re 
 |-  0 e. RR
31 10re 
 |-  ; 1 0 e. RR
32 10pos 
 |-  0 < ; 1 0
33 30 31 32 ltleii 
 |-  0 <_ ; 1 0
34 9 nncni 
 |-  ; 1 0 e. CC
35 exp1 
 |-  ( ; 1 0 e. CC -> ( ; 1 0 ^ 1 ) = ; 1 0 )
36 34 35 ax-mp 
 |-  ( ; 1 0 ^ 1 ) = ; 1 0
37 33 36 breqtrri 
 |-  0 <_ ( ; 1 0 ^ 1 )
38 1z 
 |-  1 e. ZZ
39 12 nnzi 
 |-  ; 2 9 e. ZZ
40 31 38 39 3pm3.2i 
 |-  ( ; 1 0 e. RR /\ 1 e. ZZ /\ ; 2 9 e. ZZ )
41 2nn 
 |-  2 e. NN
42 9nn0 
 |-  9 e. NN0
43 41 42 2 22 declti 
 |-  1 < ; 2 9
44 22 43 pm3.2i 
 |-  ( 1 < ; 1 0 /\ 1 < ; 2 9 )
45 ltexp2a 
 |-  ( ( ( ; 1 0 e. RR /\ 1 e. ZZ /\ ; 2 9 e. ZZ ) /\ ( 1 < ; 1 0 /\ 1 < ; 2 9 ) ) -> ( ; 1 0 ^ 1 ) < ( ; 1 0 ^ ; 2 9 ) )
46 40 44 45 mp2an 
 |-  ( ; 1 0 ^ 1 ) < ( ; 1 0 ^ ; 2 9 )
47 37 46 pm3.2i 
 |-  ( 0 <_ ( ; 1 0 ^ 1 ) /\ ( ; 1 0 ^ 1 ) < ( ; 1 0 ^ ; 2 9 ) )
48 ltmul12a 
 |-  ( ( ( ( 1 e. RR /\ ; 8 8 e. RR ) /\ ( 0 <_ 1 /\ 1 < ; 8 8 ) ) /\ ( ( ( ; 1 0 ^ 1 ) e. RR /\ ( ; 1 0 ^ ; 2 9 ) e. RR ) /\ ( 0 <_ ( ; 1 0 ^ 1 ) /\ ( ; 1 0 ^ 1 ) < ( ; 1 0 ^ ; 2 9 ) ) ) ) -> ( 1 x. ( ; 1 0 ^ 1 ) ) < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
49 20 24 29 47 48 mp4an 
 |-  ( 1 x. ( ; 1 0 ^ 1 ) ) < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) )
50 26 nnzi 
 |-  ( ; 1 0 ^ 1 ) e. ZZ
51 zmulcl 
 |-  ( ( 1 e. ZZ /\ ( ; 1 0 ^ 1 ) e. ZZ ) -> ( 1 x. ( ; 1 0 ^ 1 ) ) e. ZZ )
52 38 50 51 mp2an 
 |-  ( 1 x. ( ; 1 0 ^ 1 ) ) e. ZZ
53 zltp1le 
 |-  ( ( ( 1 x. ( ; 1 0 ^ 1 ) ) e. ZZ /\ ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. ZZ ) -> ( ( 1 x. ( ; 1 0 ^ 1 ) ) < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) <-> ( ( 1 x. ( ; 1 0 ^ 1 ) ) + 1 ) <_ ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) )
54 52 17 53 mp2an 
 |-  ( ( 1 x. ( ; 1 0 ^ 1 ) ) < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) <-> ( ( 1 x. ( ; 1 0 ^ 1 ) ) + 1 ) <_ ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
55 1t10e1p1e11 
 |-  ; 1 1 = ( ( 1 x. ( ; 1 0 ^ 1 ) ) + 1 )
56 55 eqcomi 
 |-  ( ( 1 x. ( ; 1 0 ^ 1 ) ) + 1 ) = ; 1 1
57 56 breq1i 
 |-  ( ( ( 1 x. ( ; 1 0 ^ 1 ) ) + 1 ) <_ ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) <-> ; 1 1 <_ ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
58 54 57 bitri 
 |-  ( ( 1 x. ( ; 1 0 ^ 1 ) ) < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) <-> ; 1 1 <_ ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
59 49 58 mpbi 
 |-  ; 1 1 <_ ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) )
60 eluz2 
 |-  ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. ( ZZ>= ` ; 1 1 ) <-> ( ; 1 1 e. ZZ /\ ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. ZZ /\ ; 1 1 <_ ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) )
61 5 17 59 60 mpbir3an 
 |-  ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. ( ZZ>= ` ; 1 1 )
62 61 a1i 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. ( ZZ>= ` ; 1 1 ) )
63 4nn 
 |-  4 e. NN
64 2 7 decnncl 
 |-  ; 1 8 e. NN
65 64 nnnn0i 
 |-  ; 1 8 e. NN0
66 nnexpcl 
 |-  ( ( ; 1 0 e. NN /\ ; 1 8 e. NN0 ) -> ( ; 1 0 ^ ; 1 8 ) e. NN )
67 9 65 66 mp2an 
 |-  ( ; 1 0 ^ ; 1 8 ) e. NN
68 63 67 nnmulcli 
 |-  ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN
69 68 nnzi 
 |-  ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. ZZ
70 4re 
 |-  4 e. RR
71 18 70 pm3.2i 
 |-  ( 1 e. RR /\ 4 e. RR )
72 1lt4 
 |-  1 < 4
73 21 72 pm3.2i 
 |-  ( 0 <_ 1 /\ 1 < 4 )
74 67 nnrei 
 |-  ( ; 1 0 ^ ; 1 8 ) e. RR
75 27 74 pm3.2i 
 |-  ( ( ; 1 0 ^ 1 ) e. RR /\ ( ; 1 0 ^ ; 1 8 ) e. RR )
76 64 nnzi 
 |-  ; 1 8 e. ZZ
77 31 38 76 3pm3.2i 
 |-  ( ; 1 0 e. RR /\ 1 e. ZZ /\ ; 1 8 e. ZZ )
78 3 6 2 22 declti 
 |-  1 < ; 1 8
79 22 78 pm3.2i 
 |-  ( 1 < ; 1 0 /\ 1 < ; 1 8 )
80 ltexp2a 
 |-  ( ( ( ; 1 0 e. RR /\ 1 e. ZZ /\ ; 1 8 e. ZZ ) /\ ( 1 < ; 1 0 /\ 1 < ; 1 8 ) ) -> ( ; 1 0 ^ 1 ) < ( ; 1 0 ^ ; 1 8 ) )
81 77 79 80 mp2an 
 |-  ( ; 1 0 ^ 1 ) < ( ; 1 0 ^ ; 1 8 )
82 37 81 pm3.2i 
 |-  ( 0 <_ ( ; 1 0 ^ 1 ) /\ ( ; 1 0 ^ 1 ) < ( ; 1 0 ^ ; 1 8 ) )
83 ltmul12a 
 |-  ( ( ( ( 1 e. RR /\ 4 e. RR ) /\ ( 0 <_ 1 /\ 1 < 4 ) ) /\ ( ( ( ; 1 0 ^ 1 ) e. RR /\ ( ; 1 0 ^ ; 1 8 ) e. RR ) /\ ( 0 <_ ( ; 1 0 ^ 1 ) /\ ( ; 1 0 ^ 1 ) < ( ; 1 0 ^ ; 1 8 ) ) ) ) -> ( 1 x. ( ; 1 0 ^ 1 ) ) < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) )
84 71 73 75 82 83 mp4an 
 |-  ( 1 x. ( ; 1 0 ^ 1 ) ) < ( 4 x. ( ; 1 0 ^ ; 1 8 ) )
85 4z 
 |-  4 e. ZZ
86 67 nnzi 
 |-  ( ; 1 0 ^ ; 1 8 ) e. ZZ
87 zmulcl 
 |-  ( ( 4 e. ZZ /\ ( ; 1 0 ^ ; 1 8 ) e. ZZ ) -> ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. ZZ )
88 85 86 87 mp2an 
 |-  ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. ZZ
89 zltp1le 
 |-  ( ( ( 1 x. ( ; 1 0 ^ 1 ) ) e. ZZ /\ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. ZZ ) -> ( ( 1 x. ( ; 1 0 ^ 1 ) ) < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <-> ( ( 1 x. ( ; 1 0 ^ 1 ) ) + 1 ) <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) )
90 52 88 89 mp2an 
 |-  ( ( 1 x. ( ; 1 0 ^ 1 ) ) < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <-> ( ( 1 x. ( ; 1 0 ^ 1 ) ) + 1 ) <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) )
91 56 breq1i 
 |-  ( ( ( 1 x. ( ; 1 0 ^ 1 ) ) + 1 ) <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <-> ; 1 1 <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) )
92 90 91 bitri 
 |-  ( ( 1 x. ( ; 1 0 ^ 1 ) ) < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <-> ; 1 1 <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) )
93 84 92 mpbi 
 |-  ; 1 1 <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) )
94 eluz2 
 |-  ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. ( ZZ>= ` ; 1 1 ) <-> ( ; 1 1 e. ZZ /\ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. ZZ /\ ; 1 1 <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) )
95 5 69 93 94 mpbir3an 
 |-  ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. ( ZZ>= ` ; 1 1 )
96 95 a1i 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. ( ZZ>= ` ; 1 1 ) )
97 simpl 
 |-  ( ( n e. Even /\ ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) -> n e. Even )
98 simprl 
 |-  ( ( n e. Even /\ ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) -> 4 < n )
99 evenz 
 |-  ( n e. Even -> n e. ZZ )
100 99 zred 
 |-  ( n e. Even -> n e. RR )
101 68 nnrei 
 |-  ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. RR
102 ltle 
 |-  ( ( n e. RR /\ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. RR ) -> ( n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> n <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) )
103 100 101 102 sylancl 
 |-  ( n e. Even -> ( n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> n <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) )
104 103 a1d 
 |-  ( n e. Even -> ( 4 < n -> ( n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> n <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) )
105 104 imp32 
 |-  ( ( n e. Even /\ ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) -> n <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) )
106 ax-bgbltosilva 
 |-  ( ( n e. Even /\ 4 < n /\ n <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven )
107 97 98 105 106 syl3anc 
 |-  ( ( n e. Even /\ ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) -> n e. GoldbachEven )
108 107 ex 
 |-  ( n e. Even -> ( ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven ) )
109 108 a1i 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> ( n e. Even -> ( ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven ) ) )
110 109 ralrimiv 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> A. n e. Even ( ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven ) )
111 simpl 
 |-  ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) -> d e. ( ZZ>= ` 3 ) )
112 111 ad2antrr 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> d e. ( ZZ>= ` 3 ) )
113 simpr 
 |-  ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) -> f e. ( RePart ` d ) )
114 113 ad2antrr 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> f e. ( RePart ` d ) )
115 simpr 
 |-  ( ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) -> A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) )
116 115 ad2antlr 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) )
117 simpl1 
 |-  ( ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) -> ( f ` 0 ) = 7 )
118 117 ad2antlr 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> ( f ` 0 ) = 7 )
119 simpl2 
 |-  ( ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) -> ( f ` 1 ) = ; 1 3 )
120 119 ad2antlr 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> ( f ` 1 ) = ; 1 3 )
121 6 11 decnncl 
 |-  ; 8 9 e. NN
122 121 nnrei 
 |-  ; 8 9 e. RR
123 15 nngt0i 
 |-  0 < ( ; 1 0 ^ ; 2 9 )
124 28 123 pm3.2i 
 |-  ( ( ; 1 0 ^ ; 2 9 ) e. RR /\ 0 < ( ; 1 0 ^ ; 2 9 ) )
125 19 122 124 3pm3.2i 
 |-  ( ; 8 8 e. RR /\ ; 8 9 e. RR /\ ( ( ; 1 0 ^ ; 2 9 ) e. RR /\ 0 < ( ; 1 0 ^ ; 2 9 ) ) )
126 8lt9 
 |-  8 < 9
127 6 6 11 126 declt 
 |-  ; 8 8 < ; 8 9
128 ltmul1a 
 |-  ( ( ( ; 8 8 e. RR /\ ; 8 9 e. RR /\ ( ( ; 1 0 ^ ; 2 9 ) e. RR /\ 0 < ( ; 1 0 ^ ; 2 9 ) ) ) /\ ; 8 8 < ; 8 9 ) -> ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) < ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) )
129 125 127 128 mp2an 
 |-  ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) < ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) )
130 breq2 
 |-  ( ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) -> ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) < ( f ` d ) <-> ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) < ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) )
131 129 130 mpbiri 
 |-  ( ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) -> ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) < ( f ` d ) )
132 131 3ad2ant3 
 |-  ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) < ( f ` d ) )
133 132 adantr 
 |-  ( ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) -> ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) < ( f ` d ) )
134 133 ad2antlr 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) < ( f ` d ) )
135 121 15 nnmulcli 
 |-  ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN
136 135 nnrei 
 |-  ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) e. RR
137 eleq1 
 |-  ( ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) -> ( ( f ` d ) e. RR <-> ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) e. RR ) )
138 136 137 mpbiri 
 |-  ( ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) -> ( f ` d ) e. RR )
139 138 3ad2ant3 
 |-  ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> ( f ` d ) e. RR )
140 139 adantr 
 |-  ( ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) -> ( f ` d ) e. RR )
141 140 ad2antlr 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> ( f ` d ) e. RR )
142 62 96 110 112 114 116 118 120 134 141 bgoldbtbnd 
 |-  ( ( ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) /\ ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) ) /\ ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) )
143 142 exp31 
 |-  ( ( d e. ( ZZ>= ` 3 ) /\ f e. ( RePart ` d ) ) -> ( ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) -> ( ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) ) ) )
144 143 rexlimivv 
 |-  ( E. d e. ( ZZ>= ` 3 ) E. f e. ( RePart ` d ) ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) -> ( ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) ) )
145 breq2 
 |-  ( n = N -> ( 7 < n <-> 7 < N ) )
146 breq1 
 |-  ( n = N -> ( n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) <-> N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) )
147 145 146 anbi12d 
 |-  ( n = N -> ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) <-> ( 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) )
148 eleq1 
 |-  ( n = N -> ( n e. GoldbachOdd <-> N e. GoldbachOdd ) )
149 147 148 imbi12d 
 |-  ( n = N -> ( ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) <-> ( ( 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> N e. GoldbachOdd ) ) )
150 149 rspcv 
 |-  ( N e. Odd -> ( A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) -> ( ( 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> N e. GoldbachOdd ) ) )
151 150 com23 
 |-  ( N e. Odd -> ( ( 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> ( A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) -> N e. GoldbachOdd ) ) )
152 151 3impib 
 |-  ( ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> ( A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) -> N e. GoldbachOdd ) )
153 144 152 sylcom 
 |-  ( E. d e. ( ZZ>= ` 3 ) E. f e. ( RePart ` d ) ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) ) /\ A. i e. ( 0 ..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) ) -> ( ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> N e. GoldbachOdd ) )
154 1 153 ax-mp 
 |-  ( ( N e. Odd /\ 7 < N /\ N < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> N e. GoldbachOdd )