Metamath Proof Explorer


Theorem tgoldbachgt

Description: Odd integers greater than ( ; 1 0 ^ ; 2 7 ) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of Helfgott p. 70 , expressed using the set G of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021)

Ref Expression
Hypotheses tgoldbachgt.o
|- O = { z e. ZZ | -. 2 || z }
tgoldbachgt.g
|- G = { z e. O | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ z = ( ( p + q ) + r ) ) }
Assertion tgoldbachgt
|- E. m e. NN ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) )

Proof

Step Hyp Ref Expression
1 tgoldbachgt.o
 |-  O = { z e. ZZ | -. 2 || z }
2 tgoldbachgt.g
 |-  G = { z e. O | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ z = ( ( p + q ) + r ) ) }
3 10nn
 |-  ; 1 0 e. NN
4 2nn0
 |-  2 e. NN0
5 7nn0
 |-  7 e. NN0
6 4 5 deccl
 |-  ; 2 7 e. NN0
7 nnexpcl
 |-  ( ( ; 1 0 e. NN /\ ; 2 7 e. NN0 ) -> ( ; 1 0 ^ ; 2 7 ) e. NN )
8 3 6 7 mp2an
 |-  ( ; 1 0 ^ ; 2 7 ) e. NN
9 8 nnrei
 |-  ( ; 1 0 ^ ; 2 7 ) e. RR
10 9 leidi
 |-  ( ; 1 0 ^ ; 2 7 ) <_ ( ; 1 0 ^ ; 2 7 )
11 simpl
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> n e. O )
12 inss2
 |-  ( O i^i Prime ) C_ Prime
13 prmssnn
 |-  Prime C_ NN
14 12 13 sstri
 |-  ( O i^i Prime ) C_ NN
15 14 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( O i^i Prime ) C_ NN )
16 1 eleq2i
 |-  ( n e. O <-> n e. { z e. ZZ | -. 2 || z } )
17 elrabi
 |-  ( n e. { z e. ZZ | -. 2 || z } -> n e. ZZ )
18 16 17 sylbi
 |-  ( n e. O -> n e. ZZ )
19 18 ad2antrr
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> n e. ZZ )
20 3nn0
 |-  3 e. NN0
21 20 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> 3 e. NN0 )
22 simpr
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) )
23 15 19 21 22 reprf
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> c : ( 0 ..^ 3 ) --> ( O i^i Prime ) )
24 c0ex
 |-  0 e. _V
25 24 tpid1
 |-  0 e. { 0 , 1 , 2 }
26 fzo0to3tp
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
27 25 26 eleqtrri
 |-  0 e. ( 0 ..^ 3 )
28 27 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> 0 e. ( 0 ..^ 3 ) )
29 23 28 ffvelrnd
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 0 ) e. ( O i^i Prime ) )
30 29 elin2d
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 0 ) e. Prime )
31 1ex
 |-  1 e. _V
32 31 tpid2
 |-  1 e. { 0 , 1 , 2 }
33 32 26 eleqtrri
 |-  1 e. ( 0 ..^ 3 )
34 33 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> 1 e. ( 0 ..^ 3 ) )
35 23 34 ffvelrnd
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 1 ) e. ( O i^i Prime ) )
36 35 elin2d
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 1 ) e. Prime )
37 2ex
 |-  2 e. _V
38 37 tpid3
 |-  2 e. { 0 , 1 , 2 }
39 38 26 eleqtrri
 |-  2 e. ( 0 ..^ 3 )
40 39 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> 2 e. ( 0 ..^ 3 ) )
41 23 40 ffvelrnd
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 2 ) e. ( O i^i Prime ) )
42 41 elin2d
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 2 ) e. Prime )
43 29 elin1d
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 0 ) e. O )
44 35 elin1d
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 1 ) e. O )
45 41 elin1d
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 2 ) e. O )
46 43 44 45 3jca
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( ( c ` 0 ) e. O /\ ( c ` 1 ) e. O /\ ( c ` 2 ) e. O ) )
47 26 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( 0 ..^ 3 ) = { 0 , 1 , 2 } )
48 47 sumeq1d
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> sum_ i e. ( 0 ..^ 3 ) ( c ` i ) = sum_ i e. { 0 , 1 , 2 } ( c ` i ) )
49 15 19 21 22 reprsum
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> sum_ i e. ( 0 ..^ 3 ) ( c ` i ) = n )
50 fveq2
 |-  ( i = 0 -> ( c ` i ) = ( c ` 0 ) )
51 fveq2
 |-  ( i = 1 -> ( c ` i ) = ( c ` 1 ) )
52 fveq2
 |-  ( i = 2 -> ( c ` i ) = ( c ` 2 ) )
53 14 29 sseldi
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 0 ) e. NN )
54 53 nncnd
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 0 ) e. CC )
55 14 35 sseldi
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 1 ) e. NN )
56 55 nncnd
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 1 ) e. CC )
57 14 41 sseldi
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 2 ) e. NN )
58 57 nncnd
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( c ` 2 ) e. CC )
59 54 56 58 3jca
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( ( c ` 0 ) e. CC /\ ( c ` 1 ) e. CC /\ ( c ` 2 ) e. CC ) )
60 24 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> 0 e. _V )
61 31 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> 1 e. _V )
62 37 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> 2 e. _V )
63 60 61 62 3jca
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( 0 e. _V /\ 1 e. _V /\ 2 e. _V ) )
64 0ne1
 |-  0 =/= 1
65 64 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> 0 =/= 1 )
66 0ne2
 |-  0 =/= 2
67 66 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> 0 =/= 2 )
68 1ne2
 |-  1 =/= 2
69 68 a1i
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> 1 =/= 2 )
70 50 51 52 59 63 65 67 69 sumtp
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> sum_ i e. { 0 , 1 , 2 } ( c ` i ) = ( ( ( c ` 0 ) + ( c ` 1 ) ) + ( c ` 2 ) ) )
71 48 49 70 3eqtr3d
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> n = ( ( ( c ` 0 ) + ( c ` 1 ) ) + ( c ` 2 ) ) )
72 46 71 jca
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> ( ( ( c ` 0 ) e. O /\ ( c ` 1 ) e. O /\ ( c ` 2 ) e. O ) /\ n = ( ( ( c ` 0 ) + ( c ` 1 ) ) + ( c ` 2 ) ) ) )
73 eleq1
 |-  ( p = ( c ` 0 ) -> ( p e. O <-> ( c ` 0 ) e. O ) )
74 73 3anbi1d
 |-  ( p = ( c ` 0 ) -> ( ( p e. O /\ q e. O /\ r e. O ) <-> ( ( c ` 0 ) e. O /\ q e. O /\ r e. O ) ) )
75 oveq1
 |-  ( p = ( c ` 0 ) -> ( p + q ) = ( ( c ` 0 ) + q ) )
76 75 oveq1d
 |-  ( p = ( c ` 0 ) -> ( ( p + q ) + r ) = ( ( ( c ` 0 ) + q ) + r ) )
77 76 eqeq2d
 |-  ( p = ( c ` 0 ) -> ( n = ( ( p + q ) + r ) <-> n = ( ( ( c ` 0 ) + q ) + r ) ) )
78 74 77 anbi12d
 |-  ( p = ( c ` 0 ) -> ( ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) <-> ( ( ( c ` 0 ) e. O /\ q e. O /\ r e. O ) /\ n = ( ( ( c ` 0 ) + q ) + r ) ) ) )
79 eleq1
 |-  ( q = ( c ` 1 ) -> ( q e. O <-> ( c ` 1 ) e. O ) )
80 79 3anbi2d
 |-  ( q = ( c ` 1 ) -> ( ( ( c ` 0 ) e. O /\ q e. O /\ r e. O ) <-> ( ( c ` 0 ) e. O /\ ( c ` 1 ) e. O /\ r e. O ) ) )
81 oveq2
 |-  ( q = ( c ` 1 ) -> ( ( c ` 0 ) + q ) = ( ( c ` 0 ) + ( c ` 1 ) ) )
82 81 oveq1d
 |-  ( q = ( c ` 1 ) -> ( ( ( c ` 0 ) + q ) + r ) = ( ( ( c ` 0 ) + ( c ` 1 ) ) + r ) )
83 82 eqeq2d
 |-  ( q = ( c ` 1 ) -> ( n = ( ( ( c ` 0 ) + q ) + r ) <-> n = ( ( ( c ` 0 ) + ( c ` 1 ) ) + r ) ) )
84 80 83 anbi12d
 |-  ( q = ( c ` 1 ) -> ( ( ( ( c ` 0 ) e. O /\ q e. O /\ r e. O ) /\ n = ( ( ( c ` 0 ) + q ) + r ) ) <-> ( ( ( c ` 0 ) e. O /\ ( c ` 1 ) e. O /\ r e. O ) /\ n = ( ( ( c ` 0 ) + ( c ` 1 ) ) + r ) ) ) )
85 eleq1
 |-  ( r = ( c ` 2 ) -> ( r e. O <-> ( c ` 2 ) e. O ) )
86 85 3anbi3d
 |-  ( r = ( c ` 2 ) -> ( ( ( c ` 0 ) e. O /\ ( c ` 1 ) e. O /\ r e. O ) <-> ( ( c ` 0 ) e. O /\ ( c ` 1 ) e. O /\ ( c ` 2 ) e. O ) ) )
87 oveq2
 |-  ( r = ( c ` 2 ) -> ( ( ( c ` 0 ) + ( c ` 1 ) ) + r ) = ( ( ( c ` 0 ) + ( c ` 1 ) ) + ( c ` 2 ) ) )
88 87 eqeq2d
 |-  ( r = ( c ` 2 ) -> ( n = ( ( ( c ` 0 ) + ( c ` 1 ) ) + r ) <-> n = ( ( ( c ` 0 ) + ( c ` 1 ) ) + ( c ` 2 ) ) ) )
89 86 88 anbi12d
 |-  ( r = ( c ` 2 ) -> ( ( ( ( c ` 0 ) e. O /\ ( c ` 1 ) e. O /\ r e. O ) /\ n = ( ( ( c ` 0 ) + ( c ` 1 ) ) + r ) ) <-> ( ( ( c ` 0 ) e. O /\ ( c ` 1 ) e. O /\ ( c ` 2 ) e. O ) /\ n = ( ( ( c ` 0 ) + ( c ` 1 ) ) + ( c ` 2 ) ) ) ) )
90 78 84 89 rspc3ev
 |-  ( ( ( ( c ` 0 ) e. Prime /\ ( c ` 1 ) e. Prime /\ ( c ` 2 ) e. Prime ) /\ ( ( ( c ` 0 ) e. O /\ ( c ` 1 ) e. O /\ ( c ` 2 ) e. O ) /\ n = ( ( ( c ` 0 ) + ( c ` 1 ) ) + ( c ` 2 ) ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) )
91 30 36 42 72 90 syl31anc
 |-  ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) )
92 91 adantr
 |-  ( ( ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) /\ T. ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) )
93 8 a1i
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> ( ; 1 0 ^ ; 2 7 ) e. NN )
94 93 nnred
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> ( ; 1 0 ^ ; 2 7 ) e. RR )
95 18 zred
 |-  ( n e. O -> n e. RR )
96 95 adantr
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> n e. RR )
97 simpr
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> ( ; 1 0 ^ ; 2 7 ) < n )
98 94 96 97 ltled
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> ( ; 1 0 ^ ; 2 7 ) <_ n )
99 1 11 98 tgoldbachgtd
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> 0 < ( # ` ( ( O i^i Prime ) ( repr ` 3 ) n ) ) )
100 ovex
 |-  ( ( O i^i Prime ) ( repr ` 3 ) n ) e. _V
101 hashneq0
 |-  ( ( ( O i^i Prime ) ( repr ` 3 ) n ) e. _V -> ( 0 < ( # ` ( ( O i^i Prime ) ( repr ` 3 ) n ) ) <-> ( ( O i^i Prime ) ( repr ` 3 ) n ) =/= (/) ) )
102 100 101 ax-mp
 |-  ( 0 < ( # ` ( ( O i^i Prime ) ( repr ` 3 ) n ) ) <-> ( ( O i^i Prime ) ( repr ` 3 ) n ) =/= (/) )
103 99 102 sylib
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> ( ( O i^i Prime ) ( repr ` 3 ) n ) =/= (/) )
104 103 neneqd
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> -. ( ( O i^i Prime ) ( repr ` 3 ) n ) = (/) )
105 neq0
 |-  ( -. ( ( O i^i Prime ) ( repr ` 3 ) n ) = (/) <-> E. c c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) )
106 104 105 sylib
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> E. c c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) )
107 tru
 |-  T.
108 106 107 jctil
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> ( T. /\ E. c c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) )
109 19.42v
 |-  ( E. c ( T. /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) <-> ( T. /\ E. c c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) )
110 108 109 sylibr
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> E. c ( T. /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) )
111 exancom
 |-  ( E. c ( T. /\ c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) ) <-> E. c ( c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) /\ T. ) )
112 110 111 sylib
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> E. c ( c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) /\ T. ) )
113 df-rex
 |-  ( E. c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) T. <-> E. c ( c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) /\ T. ) )
114 112 113 sylibr
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> E. c e. ( ( O i^i Prime ) ( repr ` 3 ) n ) T. )
115 92 114 r19.29a
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) )
116 2 eleq2i
 |-  ( n e. G <-> n e. { z e. O | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ z = ( ( p + q ) + r ) ) } )
117 eqeq1
 |-  ( z = n -> ( z = ( ( p + q ) + r ) <-> n = ( ( p + q ) + r ) ) )
118 117 anbi2d
 |-  ( z = n -> ( ( ( p e. O /\ q e. O /\ r e. O ) /\ z = ( ( p + q ) + r ) ) <-> ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) ) )
119 118 rexbidv
 |-  ( z = n -> ( E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ z = ( ( p + q ) + r ) ) <-> E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) ) )
120 119 rexbidv
 |-  ( z = n -> ( E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ z = ( ( p + q ) + r ) ) <-> E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) ) )
121 120 rexbidv
 |-  ( z = n -> ( E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ z = ( ( p + q ) + r ) ) <-> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) ) )
122 121 elrab3
 |-  ( n e. O -> ( n e. { z e. O | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ z = ( ( p + q ) + r ) ) } <-> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) ) )
123 116 122 syl5bb
 |-  ( n e. O -> ( n e. G <-> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) ) )
124 123 biimpar
 |-  ( ( n e. O /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ n = ( ( p + q ) + r ) ) ) -> n e. G )
125 11 115 124 syl2anc
 |-  ( ( n e. O /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> n e. G )
126 125 ex
 |-  ( n e. O -> ( ( ; 1 0 ^ ; 2 7 ) < n -> n e. G ) )
127 126 rgen
 |-  A. n e. O ( ( ; 1 0 ^ ; 2 7 ) < n -> n e. G )
128 10 127 pm3.2i
 |-  ( ( ; 1 0 ^ ; 2 7 ) <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. O ( ( ; 1 0 ^ ; 2 7 ) < n -> n e. G ) )
129 breq1
 |-  ( m = ( ; 1 0 ^ ; 2 7 ) -> ( m <_ ( ; 1 0 ^ ; 2 7 ) <-> ( ; 1 0 ^ ; 2 7 ) <_ ( ; 1 0 ^ ; 2 7 ) ) )
130 breq1
 |-  ( m = ( ; 1 0 ^ ; 2 7 ) -> ( m < n <-> ( ; 1 0 ^ ; 2 7 ) < n ) )
131 130 imbi1d
 |-  ( m = ( ; 1 0 ^ ; 2 7 ) -> ( ( m < n -> n e. G ) <-> ( ( ; 1 0 ^ ; 2 7 ) < n -> n e. G ) ) )
132 131 ralbidv
 |-  ( m = ( ; 1 0 ^ ; 2 7 ) -> ( A. n e. O ( m < n -> n e. G ) <-> A. n e. O ( ( ; 1 0 ^ ; 2 7 ) < n -> n e. G ) ) )
133 129 132 anbi12d
 |-  ( m = ( ; 1 0 ^ ; 2 7 ) -> ( ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) ) <-> ( ( ; 1 0 ^ ; 2 7 ) <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. O ( ( ; 1 0 ^ ; 2 7 ) < n -> n e. G ) ) ) )
134 133 rspcev
 |-  ( ( ( ; 1 0 ^ ; 2 7 ) e. NN /\ ( ( ; 1 0 ^ ; 2 7 ) <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. O ( ( ; 1 0 ^ ; 2 7 ) < n -> n e. G ) ) ) -> E. m e. NN ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) ) )
135 8 128 134 mp2an
 |-  E. m e. NN ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) )