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