This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 sselid 
 |-  ( ( ( 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 sselid 
 |-  ( ( ( 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 sselid 
 |-  ( ( ( 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 bitrid 
 |-  ( 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 ) )