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 m Odd 7 < m m GoldbachOdd N 8 N Odd f 1 3 N = k = 1 3 f k

Proof

Step Hyp Ref Expression
1 breq2 m = N 7 < m 7 < N
2 eleq1 m = N m GoldbachOdd N GoldbachOdd
3 1 2 imbi12d m = N 7 < m m GoldbachOdd 7 < N N GoldbachOdd
4 3 rspcv N Odd m Odd 7 < m m GoldbachOdd 7 < N N GoldbachOdd
5 4 adantl N 8 N Odd m Odd 7 < m m GoldbachOdd 7 < N N GoldbachOdd
6 eluz2 N 8 8 N 8 N
7 7lt8 7 < 8
8 7re 7
9 8 a1i N 7
10 8re 8
11 10 a1i N 8
12 zre N N
13 ltletr 7 8 N 7 < 8 8 N 7 < N
14 9 11 12 13 syl3anc N 7 < 8 8 N 7 < N
15 7 14 mpani N 8 N 7 < N
16 15 imp N 8 N 7 < N
17 16 3adant1 8 N 8 N 7 < N
18 6 17 sylbi N 8 7 < N
19 18 adantr N 8 N Odd 7 < N
20 pm2.27 7 < N 7 < N N GoldbachOdd N GoldbachOdd
21 19 20 syl N 8 N Odd 7 < N N GoldbachOdd N GoldbachOdd
22 isgbo N GoldbachOdd N Odd p q r p Odd q Odd r Odd N = p + q + r
23 1ex 1 V
24 2ex 2 V
25 3ex 3 V
26 vex p V
27 vex q V
28 vex r V
29 1ne2 1 2
30 1re 1
31 1lt3 1 < 3
32 30 31 ltneii 1 3
33 2re 2
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 q r 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
42 fztp 1 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 q r 1 p 2 q 3 r : 1 3 p q r
54 df-3an p q r p q r
55 26 27 28 tpss p q r p q r
56 54 55 sylbb1 p q r p q r
57 53 56 fssd p q r 1 p 2 q 3 r : 1 3
58 prmex V
59 ovex 1 3 V
60 58 59 pm3.2i V 1 3 V
61 elmapg V 1 3 V 1 p 2 q 3 r 1 3 1 p 2 q 3 r : 1 3
62 60 61 mp1i p q r 1 p 2 q 3 r 1 3 1 p 2 q 3 r : 1 3
63 57 62 mpbird p q r 1 p 2 q 3 r 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 k = 1 3 f k = k = 1 3 1 p 2 q 3 r k
66 65 eqeq2d f = 1 p 2 q 3 r p + q + r = k = 1 3 f k p + q + r = k = 1 3 1 p 2 q 3 r k
67 66 adantl p q r f = 1 p 2 q 3 r p + q + r = k = 1 3 f k p + q + r = k = 1 3 1 p 2 q 3 r k
68 51 a1i p q r 1 3 = 1 2 3
69 68 sumeq1d p q r k = 1 3 1 p 2 q 3 r k = k 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 p
83 82 zcnd p p
84 prmz q q
85 84 zcnd q q
86 prmz r r
87 86 zcnd r r
88 83 85 87 3anim123i p q r p q r
89 88 3expa p q r p q r
90 2z 2
91 3z 3
92 41 90 91 3pm3.2i 1 2 3
93 92 a1i p q r 1 2 3
94 29 a1i p q r 1 2
95 32 a1i p q r 1 3
96 35 a1i p q r 2 3
97 73 77 81 89 93 94 95 96 sumtp p q r k 1 2 3 1 p 2 q 3 r k = p + q + r
98 69 97 eqtr2d p q r p + q + r = k = 1 3 1 p 2 q 3 r k
99 63 67 98 rspcedvd p q r f 1 3 p + q + r = k = 1 3 f k
100 eqeq1 N = p + q + r N = k = 1 3 f k p + q + r = k = 1 3 f k
101 100 rexbidv N = p + q + r f 1 3 N = k = 1 3 f k f 1 3 p + q + r = k = 1 3 f k
102 99 101 syl5ibrcom p q r N = p + q + r f 1 3 N = k = 1 3 f k
103 102 adantld p q r p Odd q Odd r Odd N = p + q + r f 1 3 N = k = 1 3 f k
104 103 rexlimdva p q r p Odd q Odd r Odd N = p + q + r f 1 3 N = k = 1 3 f k
105 104 rexlimivv p q r p Odd q Odd r Odd N = p + q + r f 1 3 N = k = 1 3 f k
106 105 adantl N Odd p q r p Odd q Odd r Odd N = p + q + r f 1 3 N = k = 1 3 f k
107 22 106 sylbi N GoldbachOdd f 1 3 N = k = 1 3 f k
108 107 a1i N 8 N Odd N GoldbachOdd f 1 3 N = k = 1 3 f k
109 5 21 108 3syld N 8 N Odd m Odd 7 < m m GoldbachOdd f 1 3 N = k = 1 3 f k
110 109 com12 m Odd 7 < m m GoldbachOdd N 8 N Odd f 1 3 N = k = 1 3 f k