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 
|- ( Z e. GoldbachOdd -> 9 <_ Z )

Proof

Step Hyp Ref Expression
1 isgbo 
 |-  ( Z e. GoldbachOdd <-> ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) ) )
2 df-3an 
 |-  ( ( p e. Prime /\ q e. Prime /\ r e. Prime ) <-> ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) )
3 an6 
 |-  ( ( ( p e. Prime /\ q e. Prime /\ r e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ r e. Odd ) ) <-> ( ( p e. Prime /\ p e. Odd ) /\ ( q e. Prime /\ q e. Odd ) /\ ( r e. Prime /\ r e. Odd ) ) )
4 oddprmuzge3 
 |-  ( ( p e. Prime /\ p e. Odd ) -> p e. ( ZZ>= ` 3 ) )
5 oddprmuzge3 
 |-  ( ( q e. Prime /\ q e. Odd ) -> q e. ( ZZ>= ` 3 ) )
6 oddprmuzge3 
 |-  ( ( r e. Prime /\ r e. Odd ) -> r e. ( ZZ>= ` 3 ) )
7 6p3e9 
 |-  ( 6 + 3 ) = 9
8 eluzelz 
 |-  ( p e. ( ZZ>= ` 3 ) -> p e. ZZ )
9 eluzelz 
 |-  ( q e. ( ZZ>= ` 3 ) -> q e. ZZ )
10 zaddcl 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> ( p + q ) e. ZZ )
11 8 9 10 syl2an 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) ) -> ( p + q ) e. ZZ )
12 11 zred 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) ) -> ( p + q ) e. RR )
13 eluzelre 
 |-  ( r e. ( ZZ>= ` 3 ) -> r e. RR )
14 12 13 anim12i 
 |-  ( ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) ) /\ r e. ( ZZ>= ` 3 ) ) -> ( ( p + q ) e. RR /\ r e. RR ) )
15 14 3impa 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) /\ r e. ( ZZ>= ` 3 ) ) -> ( ( p + q ) e. RR /\ r e. RR ) )
16 6re 
 |-  6 e. RR
17 3re 
 |-  3 e. RR
18 16 17 pm3.2i 
 |-  ( 6 e. RR /\ 3 e. RR )
19 15 18 jctil 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) /\ r e. ( ZZ>= ` 3 ) ) -> ( ( 6 e. RR /\ 3 e. RR ) /\ ( ( p + q ) e. RR /\ r e. RR ) ) )
20 3p3e6 
 |-  ( 3 + 3 ) = 6
21 eluzelre 
 |-  ( p e. ( ZZ>= ` 3 ) -> p e. RR )
22 eluzelre 
 |-  ( q e. ( ZZ>= ` 3 ) -> q e. RR )
23 21 22 anim12i 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) ) -> ( p e. RR /\ q e. RR ) )
24 17 17 pm3.2i 
 |-  ( 3 e. RR /\ 3 e. RR )
25 23 24 jctil 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) ) -> ( ( 3 e. RR /\ 3 e. RR ) /\ ( p e. RR /\ q e. RR ) ) )
26 eluzle 
 |-  ( p e. ( ZZ>= ` 3 ) -> 3 <_ p )
27 eluzle 
 |-  ( q e. ( ZZ>= ` 3 ) -> 3 <_ q )
28 26 27 anim12i 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) ) -> ( 3 <_ p /\ 3 <_ q ) )
29 le2add 
 |-  ( ( ( 3 e. RR /\ 3 e. RR ) /\ ( p e. RR /\ q e. RR ) ) -> ( ( 3 <_ p /\ 3 <_ q ) -> ( 3 + 3 ) <_ ( p + q ) ) )
30 25 28 29 sylc 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) ) -> ( 3 + 3 ) <_ ( p + q ) )
31 20 30 eqbrtrrid 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) ) -> 6 <_ ( p + q ) )
32 31 3adant3 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) /\ r e. ( ZZ>= ` 3 ) ) -> 6 <_ ( p + q ) )
33 eluzle 
 |-  ( r e. ( ZZ>= ` 3 ) -> 3 <_ r )
34 33 3ad2ant3 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) /\ r e. ( ZZ>= ` 3 ) ) -> 3 <_ r )
35 32 34 jca 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) /\ r e. ( ZZ>= ` 3 ) ) -> ( 6 <_ ( p + q ) /\ 3 <_ r ) )
36 le2add 
 |-  ( ( ( 6 e. RR /\ 3 e. RR ) /\ ( ( p + q ) e. RR /\ r e. RR ) ) -> ( ( 6 <_ ( p + q ) /\ 3 <_ r ) -> ( 6 + 3 ) <_ ( ( p + q ) + r ) ) )
37 19 35 36 sylc 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) /\ r e. ( ZZ>= ` 3 ) ) -> ( 6 + 3 ) <_ ( ( p + q ) + r ) )
38 7 37 eqbrtrrid 
 |-  ( ( p e. ( ZZ>= ` 3 ) /\ q e. ( ZZ>= ` 3 ) /\ r e. ( ZZ>= ` 3 ) ) -> 9 <_ ( ( p + q ) + r ) )
39 4 5 6 38 syl3an 
 |-  ( ( ( p e. Prime /\ p e. Odd ) /\ ( q e. Prime /\ q e. Odd ) /\ ( r e. Prime /\ r e. Odd ) ) -> 9 <_ ( ( p + q ) + r ) )
40 3 39 sylbi 
 |-  ( ( ( p e. Prime /\ q e. Prime /\ r e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ r e. Odd ) ) -> 9 <_ ( ( p + q ) + r ) )
41 2 40 sylanbr 
 |-  ( ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ r e. Odd ) ) -> 9 <_ ( ( p + q ) + r ) )
42 breq2 
 |-  ( Z = ( ( p + q ) + r ) -> ( 9 <_ Z <-> 9 <_ ( ( p + q ) + r ) ) )
43 41 42 syl5ibrcom 
 |-  ( ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ r e. Odd ) ) -> ( Z = ( ( p + q ) + r ) -> 9 <_ Z ) )
44 43 expimpd 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) -> 9 <_ Z ) )
45 44 rexlimdva 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) -> 9 <_ Z ) )
46 45 a1i 
 |-  ( Z e. Odd -> ( ( p e. Prime /\ q e. Prime ) -> ( E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) -> 9 <_ Z ) ) )
47 46 rexlimdvv 
 |-  ( Z e. Odd -> ( E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) -> 9 <_ Z ) )
48 47 imp 
 |-  ( ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) ) -> 9 <_ Z )
49 1 48 sylbi 
 |-  ( Z e. GoldbachOdd -> 9 <_ Z )