Metamath Proof Explorer

Theorem stgoldbwt

Description: If the strong ternary Goldbach conjecture is valid, then the weak ternary Goldbach conjecture holds, too. (Contributed by AV, 27-Jul-2020)

Ref Expression
Assertion stgoldbwt 
|- ( A. n e. Odd ( 7 < n -> n e. GoldbachOdd ) -> A. n e. Odd ( 5 < n -> n e. GoldbachOddW ) )

Proof

Step Hyp Ref Expression
1 pm3.35 
 |-  ( ( 7 < n /\ ( 7 < n -> n e. GoldbachOdd ) ) -> n e. GoldbachOdd )
2 gbogbow 
 |-  ( n e. GoldbachOdd -> n e. GoldbachOddW )
3 2 a1d 
 |-  ( n e. GoldbachOdd -> ( 5 < n -> n e. GoldbachOddW ) )
4 1 3 syl 
 |-  ( ( 7 < n /\ ( 7 < n -> n e. GoldbachOdd ) ) -> ( 5 < n -> n e. GoldbachOddW ) )
5 4 ex 
 |-  ( 7 < n -> ( ( 7 < n -> n e. GoldbachOdd ) -> ( 5 < n -> n e. GoldbachOddW ) ) )
6 5 a1d 
 |-  ( 7 < n -> ( n e. Odd -> ( ( 7 < n -> n e. GoldbachOdd ) -> ( 5 < n -> n e. GoldbachOddW ) ) ) )
7 oddz 
 |-  ( n e. Odd -> n e. ZZ )
8 7 zred 
 |-  ( n e. Odd -> n e. RR )
9 7re 
 |-  7 e. RR
10 9 a1i 
 |-  ( n e. Odd -> 7 e. RR )
11 8 10 lenltd 
 |-  ( n e. Odd -> ( n <_ 7 <-> -. 7 < n ) )
12 8 10 leloed 
 |-  ( n e. Odd -> ( n <_ 7 <-> ( n < 7 \/ n = 7 ) ) )
13 7 adantr 
 |-  ( ( n e. Odd /\ 5 < n ) -> n e. ZZ )
14 6nn 
 |-  6 e. NN
15 14 nnzi 
 |-  6 e. ZZ
16 13 15 jctir 
 |-  ( ( n e. Odd /\ 5 < n ) -> ( n e. ZZ /\ 6 e. ZZ ) )
17 16 adantl 
 |-  ( ( n < 7 /\ ( n e. Odd /\ 5 < n ) ) -> ( n e. ZZ /\ 6 e. ZZ ) )
18 df-7 
 |-  7 = ( 6 + 1 )
19 18 breq2i 
 |-  ( n < 7 <-> n < ( 6 + 1 ) )
20 19 biimpi 
 |-  ( n < 7 -> n < ( 6 + 1 ) )
21 df-6 
 |-  6 = ( 5 + 1 )
22 5nn 
 |-  5 e. NN
23 22 nnzi 
 |-  5 e. ZZ
24 zltp1le 
 |-  ( ( 5 e. ZZ /\ n e. ZZ ) -> ( 5 < n <-> ( 5 + 1 ) <_ n ) )
25 23 7 24 sylancr 
 |-  ( n e. Odd -> ( 5 < n <-> ( 5 + 1 ) <_ n ) )
26 25 biimpa 
 |-  ( ( n e. Odd /\ 5 < n ) -> ( 5 + 1 ) <_ n )
27 21 26 eqbrtrid 
 |-  ( ( n e. Odd /\ 5 < n ) -> 6 <_ n )
28 20 27 anim12ci 
 |-  ( ( n < 7 /\ ( n e. Odd /\ 5 < n ) ) -> ( 6 <_ n /\ n < ( 6 + 1 ) ) )
29 zgeltp1eq 
 |-  ( ( n e. ZZ /\ 6 e. ZZ ) -> ( ( 6 <_ n /\ n < ( 6 + 1 ) ) -> n = 6 ) )
30 17 28 29 sylc 
 |-  ( ( n < 7 /\ ( n e. Odd /\ 5 < n ) ) -> n = 6 )
31 30 orcd 
 |-  ( ( n < 7 /\ ( n e. Odd /\ 5 < n ) ) -> ( n = 6 \/ n = 7 ) )
32 31 ex 
 |-  ( n < 7 -> ( ( n e. Odd /\ 5 < n ) -> ( n = 6 \/ n = 7 ) ) )
33 olc 
 |-  ( n = 7 -> ( n = 6 \/ n = 7 ) )
34 33 a1d 
 |-  ( n = 7 -> ( ( n e. Odd /\ 5 < n ) -> ( n = 6 \/ n = 7 ) ) )
35 32 34 jaoi 
 |-  ( ( n < 7 \/ n = 7 ) -> ( ( n e. Odd /\ 5 < n ) -> ( n = 6 \/ n = 7 ) ) )
36 35 expd 
 |-  ( ( n < 7 \/ n = 7 ) -> ( n e. Odd -> ( 5 < n -> ( n = 6 \/ n = 7 ) ) ) )
37 36 com12 
 |-  ( n e. Odd -> ( ( n < 7 \/ n = 7 ) -> ( 5 < n -> ( n = 6 \/ n = 7 ) ) ) )
38 12 37 sylbid 
 |-  ( n e. Odd -> ( n <_ 7 -> ( 5 < n -> ( n = 6 \/ n = 7 ) ) ) )
39 eleq1 
 |-  ( n = 6 -> ( n e. Odd <-> 6 e. Odd ) )
40 6even 
 |-  6 e. Even
41 evennodd 
 |-  ( 6 e. Even -> -. 6 e. Odd )
42 41 pm2.21d 
 |-  ( 6 e. Even -> ( 6 e. Odd -> n e. GoldbachOddW ) )
43 40 42 mp1i 
 |-  ( n = 6 -> ( 6 e. Odd -> n e. GoldbachOddW ) )
44 39 43 sylbid 
 |-  ( n = 6 -> ( n e. Odd -> n e. GoldbachOddW ) )
45 7gbow 
 |-  7 e. GoldbachOddW
46 eleq1 
 |-  ( n = 7 -> ( n e. GoldbachOddW <-> 7 e. GoldbachOddW ) )
47 45 46 mpbiri 
 |-  ( n = 7 -> n e. GoldbachOddW )
48 47 a1d 
 |-  ( n = 7 -> ( n e. Odd -> n e. GoldbachOddW ) )
49 44 48 jaoi 
 |-  ( ( n = 6 \/ n = 7 ) -> ( n e. Odd -> n e. GoldbachOddW ) )
50 49 com12 
 |-  ( n e. Odd -> ( ( n = 6 \/ n = 7 ) -> n e. GoldbachOddW ) )
51 38 50 syl6d 
 |-  ( n e. Odd -> ( n <_ 7 -> ( 5 < n -> n e. GoldbachOddW ) ) )
52 11 51 sylbird 
 |-  ( n e. Odd -> ( -. 7 < n -> ( 5 < n -> n e. GoldbachOddW ) ) )
53 52 com12 
 |-  ( -. 7 < n -> ( n e. Odd -> ( 5 < n -> n e. GoldbachOddW ) ) )
54 53 a1dd 
 |-  ( -. 7 < n -> ( n e. Odd -> ( ( 7 < n -> n e. GoldbachOdd ) -> ( 5 < n -> n e. GoldbachOddW ) ) ) )
55 6 54 pm2.61i 
 |-  ( n e. Odd -> ( ( 7 < n -> n e. GoldbachOdd ) -> ( 5 < n -> n e. GoldbachOddW ) ) )
56 55 ralimia 
 |-  ( A. n e. Odd ( 7 < n -> n e. GoldbachOdd ) -> A. n e. Odd ( 5 < n -> n e. GoldbachOddW ) )