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 ) ) |