Metamath Proof Explorer


Theorem gboge9

Description: Any odd Goldbach number is greater than or equal to 9. Because of 9gbo , this bound is strict. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion gboge9 ZGoldbachOdd9Z

Proof

Step Hyp Ref Expression
1 isgbo ZGoldbachOddZOddpqrpOddqOddrOddZ=p+q+r
2 df-3an pqrpqr
3 an6 pqrpOddqOddrOddppOddqqOddrrOdd
4 oddprmuzge3 ppOddp3
5 oddprmuzge3 qqOddq3
6 oddprmuzge3 rrOddr3
7 6p3e9 6+3=9
8 eluzelz p3p
9 eluzelz q3q
10 zaddcl pqp+q
11 8 9 10 syl2an p3q3p+q
12 11 zred p3q3p+q
13 eluzelre r3r
14 12 13 anim12i p3q3r3p+qr
15 14 3impa p3q3r3p+qr
16 6re 6
17 3re 3
18 16 17 pm3.2i 63
19 15 18 jctil p3q3r363p+qr
20 3p3e6 3+3=6
21 eluzelre p3p
22 eluzelre q3q
23 21 22 anim12i p3q3pq
24 17 17 pm3.2i 33
25 23 24 jctil p3q333pq
26 eluzle p33p
27 eluzle q33q
28 26 27 anim12i p3q33p3q
29 le2add 33pq3p3q3+3p+q
30 25 28 29 sylc p3q33+3p+q
31 20 30 eqbrtrrid p3q36p+q
32 31 3adant3 p3q3r36p+q
33 eluzle r33r
34 33 3ad2ant3 p3q3r33r
35 32 34 jca p3q3r36p+q3r
36 le2add 63p+qr6p+q3r6+3p+q+r
37 19 35 36 sylc p3q3r36+3p+q+r
38 7 37 eqbrtrrid p3q3r39p+q+r
39 4 5 6 38 syl3an ppOddqqOddrrOdd9p+q+r
40 3 39 sylbi pqrpOddqOddrOdd9p+q+r
41 2 40 sylanbr pqrpOddqOddrOdd9p+q+r
42 breq2 Z=p+q+r9Z9p+q+r
43 41 42 syl5ibrcom pqrpOddqOddrOddZ=p+q+r9Z
44 43 expimpd pqrpOddqOddrOddZ=p+q+r9Z
45 44 rexlimdva pqrpOddqOddrOddZ=p+q+r9Z
46 45 a1i ZOddpqrpOddqOddrOddZ=p+q+r9Z
47 46 rexlimdvv ZOddpqrpOddqOddrOddZ=p+q+r9Z
48 47 imp ZOddpqrpOddqOddrOddZ=p+q+r9Z
49 1 48 sylbi ZGoldbachOdd9Z