Metamath Proof Explorer


Theorem nnsum4primesoddALTV

Description: If the (strong) ternary Goldbach conjecture is valid, then every odd integer greater than 7 is the sum of 3 primes. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion nnsum4primesoddALTV
|- ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> ( ( N e. ( ZZ>= ` 8 ) /\ N e. Odd ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )

Proof

Step Hyp Ref Expression
1 breq2
 |-  ( m = N -> ( 7 < m <-> 7 < N ) )
2 eleq1
 |-  ( m = N -> ( m e. GoldbachOdd <-> N e. GoldbachOdd ) )
3 1 2 imbi12d
 |-  ( m = N -> ( ( 7 < m -> m e. GoldbachOdd ) <-> ( 7 < N -> N e. GoldbachOdd ) ) )
4 3 rspcv
 |-  ( N e. Odd -> ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> ( 7 < N -> N e. GoldbachOdd ) ) )
5 4 adantl
 |-  ( ( N e. ( ZZ>= ` 8 ) /\ N e. Odd ) -> ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> ( 7 < N -> N e. GoldbachOdd ) ) )
6 eluz2
 |-  ( N e. ( ZZ>= ` 8 ) <-> ( 8 e. ZZ /\ N e. ZZ /\ 8 <_ N ) )
7 7lt8
 |-  7 < 8
8 7re
 |-  7 e. RR
9 8 a1i
 |-  ( N e. ZZ -> 7 e. RR )
10 8re
 |-  8 e. RR
11 10 a1i
 |-  ( N e. ZZ -> 8 e. RR )
12 zre
 |-  ( N e. ZZ -> N e. RR )
13 ltletr
 |-  ( ( 7 e. RR /\ 8 e. RR /\ N e. RR ) -> ( ( 7 < 8 /\ 8 <_ N ) -> 7 < N ) )
14 9 11 12 13 syl3anc
 |-  ( N e. ZZ -> ( ( 7 < 8 /\ 8 <_ N ) -> 7 < N ) )
15 7 14 mpani
 |-  ( N e. ZZ -> ( 8 <_ N -> 7 < N ) )
16 15 imp
 |-  ( ( N e. ZZ /\ 8 <_ N ) -> 7 < N )
17 16 3adant1
 |-  ( ( 8 e. ZZ /\ N e. ZZ /\ 8 <_ N ) -> 7 < N )
18 6 17 sylbi
 |-  ( N e. ( ZZ>= ` 8 ) -> 7 < N )
19 18 adantr
 |-  ( ( N e. ( ZZ>= ` 8 ) /\ N e. Odd ) -> 7 < N )
20 pm2.27
 |-  ( 7 < N -> ( ( 7 < N -> N e. GoldbachOdd ) -> N e. GoldbachOdd ) )
21 19 20 syl
 |-  ( ( N e. ( ZZ>= ` 8 ) /\ N e. Odd ) -> ( ( 7 < N -> N e. GoldbachOdd ) -> N e. GoldbachOdd ) )
22 isgbo
 |-  ( N e. GoldbachOdd <-> ( N e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ N = ( ( p + q ) + r ) ) ) )
23 1ex
 |-  1 e. _V
24 2ex
 |-  2 e. _V
25 3ex
 |-  3 e. _V
26 vex
 |-  p e. _V
27 vex
 |-  q e. _V
28 vex
 |-  r e. _V
29 1ne2
 |-  1 =/= 2
30 1re
 |-  1 e. RR
31 1lt3
 |-  1 < 3
32 30 31 ltneii
 |-  1 =/= 3
33 2re
 |-  2 e. RR
34 2lt3
 |-  2 < 3
35 33 34 ltneii
 |-  2 =/= 3
36 23 24 25 26 27 28 29 32 35 ftp
 |-  { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } : { 1 , 2 , 3 } --> { p , q , r }
37 36 a1i
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } : { 1 , 2 , 3 } --> { p , q , r } )
38 1p2e3
 |-  ( 1 + 2 ) = 3
39 38 eqcomi
 |-  3 = ( 1 + 2 )
40 39 oveq2i
 |-  ( 1 ... 3 ) = ( 1 ... ( 1 + 2 ) )
41 1z
 |-  1 e. ZZ
42 fztp
 |-  ( 1 e. ZZ -> ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
43 41 42 ax-mp
 |-  ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
44 eqid
 |-  1 = 1
45 id
 |-  ( 1 = 1 -> 1 = 1 )
46 1p1e2
 |-  ( 1 + 1 ) = 2
47 46 a1i
 |-  ( 1 = 1 -> ( 1 + 1 ) = 2 )
48 38 a1i
 |-  ( 1 = 1 -> ( 1 + 2 ) = 3 )
49 45 47 48 tpeq123d
 |-  ( 1 = 1 -> { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 } )
50 44 49 ax-mp
 |-  { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 }
51 40 43 50 3eqtri
 |-  ( 1 ... 3 ) = { 1 , 2 , 3 }
52 51 feq2i
 |-  ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } : ( 1 ... 3 ) --> { p , q , r } <-> { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } : { 1 , 2 , 3 } --> { p , q , r } )
53 37 52 sylibr
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } : ( 1 ... 3 ) --> { p , q , r } )
54 df-3an
 |-  ( ( p e. Prime /\ q e. Prime /\ r e. Prime ) <-> ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) )
55 26 27 28 tpss
 |-  ( ( p e. Prime /\ q e. Prime /\ r e. Prime ) <-> { p , q , r } C_ Prime )
56 54 55 sylbb1
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> { p , q , r } C_ Prime )
57 53 56 fssd
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } : ( 1 ... 3 ) --> Prime )
58 prmex
 |-  Prime e. _V
59 ovex
 |-  ( 1 ... 3 ) e. _V
60 58 59 pm3.2i
 |-  ( Prime e. _V /\ ( 1 ... 3 ) e. _V )
61 elmapg
 |-  ( ( Prime e. _V /\ ( 1 ... 3 ) e. _V ) -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } e. ( Prime ^m ( 1 ... 3 ) ) <-> { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } : ( 1 ... 3 ) --> Prime ) )
62 60 61 mp1i
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } e. ( Prime ^m ( 1 ... 3 ) ) <-> { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } : ( 1 ... 3 ) --> Prime ) )
63 57 62 mpbird
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } e. ( Prime ^m ( 1 ... 3 ) ) )
64 fveq1
 |-  ( f = { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } -> ( f ` k ) = ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) )
65 64 sumeq2sdv
 |-  ( f = { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } -> sum_ k e. ( 1 ... 3 ) ( f ` k ) = sum_ k e. ( 1 ... 3 ) ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) )
66 65 eqeq2d
 |-  ( f = { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } -> ( ( ( p + q ) + r ) = sum_ k e. ( 1 ... 3 ) ( f ` k ) <-> ( ( p + q ) + r ) = sum_ k e. ( 1 ... 3 ) ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) ) )
67 66 adantl
 |-  ( ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) /\ f = { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ) -> ( ( ( p + q ) + r ) = sum_ k e. ( 1 ... 3 ) ( f ` k ) <-> ( ( p + q ) + r ) = sum_ k e. ( 1 ... 3 ) ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) ) )
68 51 a1i
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( 1 ... 3 ) = { 1 , 2 , 3 } )
69 68 sumeq1d
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> sum_ k e. ( 1 ... 3 ) ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) = sum_ k e. { 1 , 2 , 3 } ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) )
70 fveq2
 |-  ( k = 1 -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) = ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` 1 ) )
71 23 26 fvtp1
 |-  ( ( 1 =/= 2 /\ 1 =/= 3 ) -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` 1 ) = p )
72 29 32 71 mp2an
 |-  ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` 1 ) = p
73 70 72 eqtrdi
 |-  ( k = 1 -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) = p )
74 fveq2
 |-  ( k = 2 -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) = ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` 2 ) )
75 24 27 fvtp2
 |-  ( ( 1 =/= 2 /\ 2 =/= 3 ) -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` 2 ) = q )
76 29 35 75 mp2an
 |-  ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` 2 ) = q
77 74 76 eqtrdi
 |-  ( k = 2 -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) = q )
78 fveq2
 |-  ( k = 3 -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) = ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` 3 ) )
79 25 28 fvtp3
 |-  ( ( 1 =/= 3 /\ 2 =/= 3 ) -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` 3 ) = r )
80 32 35 79 mp2an
 |-  ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` 3 ) = r
81 78 80 eqtrdi
 |-  ( k = 3 -> ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) = r )
82 prmz
 |-  ( p e. Prime -> p e. ZZ )
83 82 zcnd
 |-  ( p e. Prime -> p e. CC )
84 prmz
 |-  ( q e. Prime -> q e. ZZ )
85 84 zcnd
 |-  ( q e. Prime -> q e. CC )
86 prmz
 |-  ( r e. Prime -> r e. ZZ )
87 86 zcnd
 |-  ( r e. Prime -> r e. CC )
88 83 85 87 3anim123i
 |-  ( ( p e. Prime /\ q e. Prime /\ r e. Prime ) -> ( p e. CC /\ q e. CC /\ r e. CC ) )
89 88 3expa
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( p e. CC /\ q e. CC /\ r e. CC ) )
90 2z
 |-  2 e. ZZ
91 3z
 |-  3 e. ZZ
92 41 90 91 3pm3.2i
 |-  ( 1 e. ZZ /\ 2 e. ZZ /\ 3 e. ZZ )
93 92 a1i
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( 1 e. ZZ /\ 2 e. ZZ /\ 3 e. ZZ ) )
94 29 a1i
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> 1 =/= 2 )
95 32 a1i
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> 1 =/= 3 )
96 35 a1i
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> 2 =/= 3 )
97 73 77 81 89 93 94 95 96 sumtp
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> sum_ k e. { 1 , 2 , 3 } ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) = ( ( p + q ) + r ) )
98 69 97 eqtr2d
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( ( p + q ) + r ) = sum_ k e. ( 1 ... 3 ) ( { <. 1 , p >. , <. 2 , q >. , <. 3 , r >. } ` k ) )
99 63 67 98 rspcedvd
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) ( ( p + q ) + r ) = sum_ k e. ( 1 ... 3 ) ( f ` k ) )
100 eqeq1
 |-  ( N = ( ( p + q ) + r ) -> ( N = sum_ k e. ( 1 ... 3 ) ( f ` k ) <-> ( ( p + q ) + r ) = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
101 100 rexbidv
 |-  ( N = ( ( p + q ) + r ) -> ( E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) <-> E. f e. ( Prime ^m ( 1 ... 3 ) ) ( ( p + q ) + r ) = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
102 99 101 syl5ibrcom
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( N = ( ( p + q ) + r ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
103 102 adantld
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ N = ( ( p + q ) + r ) ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
104 103 rexlimdva
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ N = ( ( p + q ) + r ) ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
105 104 rexlimivv
 |-  ( E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ N = ( ( p + q ) + r ) ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) )
106 105 adantl
 |-  ( ( N e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ N = ( ( p + q ) + r ) ) ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) )
107 22 106 sylbi
 |-  ( N e. GoldbachOdd -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) )
108 107 a1i
 |-  ( ( N e. ( ZZ>= ` 8 ) /\ N e. Odd ) -> ( N e. GoldbachOdd -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
109 5 21 108 3syld
 |-  ( ( N e. ( ZZ>= ` 8 ) /\ N e. Odd ) -> ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
110 109 com12
 |-  ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> ( ( N e. ( ZZ>= ` 8 ) /\ N e. Odd ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )