# Metamath Proof Explorer

## Theorem ramz

Description: The Ramsey number when F is the zero function. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion ramz
`|- ( ( M e. NN0 /\ R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 )`

### Proof

Step Hyp Ref Expression
1 elnn0
` |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )`
2 n0
` |-  ( R =/= (/) <-> E. c c e. R )`
3 simpll
` |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> M e. NN )`
4 simplr
` |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> R e. V )`
5 0nn0
` |-  0 e. NN0`
6 5 fconst6
` |-  ( R X. { 0 } ) : R --> NN0`
7 6 a1i
` |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> ( R X. { 0 } ) : R --> NN0 )`
8 simpr
` |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> c e. R )`
9 fvconst2g
` |-  ( ( 0 e. NN0 /\ c e. R ) -> ( ( R X. { 0 } ) ` c ) = 0 )`
10 5 8 9 sylancr
` |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> ( ( R X. { 0 } ) ` c ) = 0 )`
11 ramz2
` |-  ( ( ( M e. NN /\ R e. V /\ ( R X. { 0 } ) : R --> NN0 ) /\ ( c e. R /\ ( ( R X. { 0 } ) ` c ) = 0 ) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 )`
12 3 4 7 8 10 11 syl32anc
` |-  ( ( ( M e. NN /\ R e. V ) /\ c e. R ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 )`
13 12 ex
` |-  ( ( M e. NN /\ R e. V ) -> ( c e. R -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )`
14 13 exlimdv
` |-  ( ( M e. NN /\ R e. V ) -> ( E. c c e. R -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )`
15 2 14 syl5bi
` |-  ( ( M e. NN /\ R e. V ) -> ( R =/= (/) -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )`
16 15 expimpd
` |-  ( M e. NN -> ( ( R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )`
17 simpl
` |-  ( ( R e. V /\ R =/= (/) ) -> R e. V )`
18 simpr
` |-  ( ( R e. V /\ R =/= (/) ) -> R =/= (/) )`
19 6 a1i
` |-  ( ( R e. V /\ R =/= (/) ) -> ( R X. { 0 } ) : R --> NN0 )`
20 0z
` |-  0 e. ZZ`
21 elsni
` |-  ( y e. { 0 } -> y = 0 )`
22 0le0
` |-  0 <_ 0`
23 21 22 eqbrtrdi
` |-  ( y e. { 0 } -> y <_ 0 )`
24 23 rgen
` |-  A. y e. { 0 } y <_ 0`
25 rnxp
` |-  ( R =/= (/) -> ran ( R X. { 0 } ) = { 0 } )`
` |-  ( ( R e. V /\ R =/= (/) ) -> ran ( R X. { 0 } ) = { 0 } )`
27 26 raleqdv
` |-  ( ( R e. V /\ R =/= (/) ) -> ( A. y e. ran ( R X. { 0 } ) y <_ 0 <-> A. y e. { 0 } y <_ 0 ) )`
28 24 27 mpbiri
` |-  ( ( R e. V /\ R =/= (/) ) -> A. y e. ran ( R X. { 0 } ) y <_ 0 )`
29 brralrspcev
` |-  ( ( 0 e. ZZ /\ A. y e. ran ( R X. { 0 } ) y <_ 0 ) -> E. x e. ZZ A. y e. ran ( R X. { 0 } ) y <_ x )`
30 20 28 29 sylancr
` |-  ( ( R e. V /\ R =/= (/) ) -> E. x e. ZZ A. y e. ran ( R X. { 0 } ) y <_ x )`
31 0ram
` |-  ( ( ( R e. V /\ R =/= (/) /\ ( R X. { 0 } ) : R --> NN0 ) /\ E. x e. ZZ A. y e. ran ( R X. { 0 } ) y <_ x ) -> ( 0 Ramsey ( R X. { 0 } ) ) = sup ( ran ( R X. { 0 } ) , RR , < ) )`
32 17 18 19 30 31 syl31anc
` |-  ( ( R e. V /\ R =/= (/) ) -> ( 0 Ramsey ( R X. { 0 } ) ) = sup ( ran ( R X. { 0 } ) , RR , < ) )`
33 26 supeq1d
` |-  ( ( R e. V /\ R =/= (/) ) -> sup ( ran ( R X. { 0 } ) , RR , < ) = sup ( { 0 } , RR , < ) )`
34 ltso
` |-  < Or RR`
35 0re
` |-  0 e. RR`
36 supsn
` |-  ( ( < Or RR /\ 0 e. RR ) -> sup ( { 0 } , RR , < ) = 0 )`
37 34 35 36 mp2an
` |-  sup ( { 0 } , RR , < ) = 0`
38 37 a1i
` |-  ( ( R e. V /\ R =/= (/) ) -> sup ( { 0 } , RR , < ) = 0 )`
39 32 33 38 3eqtrd
` |-  ( ( R e. V /\ R =/= (/) ) -> ( 0 Ramsey ( R X. { 0 } ) ) = 0 )`
40 oveq1
` |-  ( M = 0 -> ( M Ramsey ( R X. { 0 } ) ) = ( 0 Ramsey ( R X. { 0 } ) ) )`
41 40 eqeq1d
` |-  ( M = 0 -> ( ( M Ramsey ( R X. { 0 } ) ) = 0 <-> ( 0 Ramsey ( R X. { 0 } ) ) = 0 ) )`
42 39 41 syl5ibr
` |-  ( M = 0 -> ( ( R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )`
43 16 42 jaoi
` |-  ( ( M e. NN \/ M = 0 ) -> ( ( R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )`
44 1 43 sylbi
` |-  ( M e. NN0 -> ( ( R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 ) )`
45 44 3impib
` |-  ( ( M e. NN0 /\ R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 )`