Theorem ramubcl

Description: If the Ramsey number is upper bounded, then it is an integer. (Contributed by Mario Carneiro, 20-Apr-2015)

	Ref	Expression
Assertion	ramubcl	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐴 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ) ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
2		ltpnf	⊢ ( 𝐴 ∈ ℝ → 𝐴 < +∞ )
3		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
4		pnfxr	⊢ +∞ ∈ ℝ*
5		xrltnle	⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 < +∞ ↔ ¬ +∞ ≤ 𝐴 ) )
6	3 4 5	sylancl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < +∞ ↔ ¬ +∞ ≤ 𝐴 ) )
7	2 6	mpbid	⊢ ( 𝐴 ∈ ℝ → ¬ +∞ ≤ 𝐴 )
8	1 7	syl	⊢ ( 𝐴 ∈ ℕ0 → ¬ +∞ ≤ 𝐴 )
9	8	ad2antrl	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐴 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ) ) → ¬ +∞ ≤ 𝐴 )
10		simprr	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐴 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ) ) → ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 )
11		breq1	⊢ ( ( 𝑀 Ramsey 𝐹 ) = +∞ → ( ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ↔ +∞ ≤ 𝐴 ) )
12	10 11	syl5ibcom	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐴 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ) ) → ( ( 𝑀 Ramsey 𝐹 ) = +∞ → +∞ ≤ 𝐴 ) )
13	9 12	mtod	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐴 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ) ) → ¬ ( 𝑀 Ramsey 𝐹 ) = +∞ )
14		elsni	⊢ ( ( 𝑀 Ramsey 𝐹 ) ∈ { +∞ } → ( 𝑀 Ramsey 𝐹 ) = +∞ )
15	13 14	nsyl	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐴 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ) ) → ¬ ( 𝑀 Ramsey 𝐹 ) ∈ { +∞ } )
16		ramcl2	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) ∈ ( ℕ0 ∪ { +∞ } ) )
17	16	adantr	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐴 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ) ) → ( 𝑀 Ramsey 𝐹 ) ∈ ( ℕ0 ∪ { +∞ } ) )
18		elun	⊢ ( ( 𝑀 Ramsey 𝐹 ) ∈ ( ℕ0 ∪ { +∞ } ) ↔ ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ∨ ( 𝑀 Ramsey 𝐹 ) ∈ { +∞ } ) )
19	17 18	sylib	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐴 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ) ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ∨ ( 𝑀 Ramsey 𝐹 ) ∈ { +∞ } ) )
20	19	ord	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐴 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ) ) → ( ¬ ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 → ( 𝑀 Ramsey 𝐹 ) ∈ { +∞ } ) )
21	15 20	mt3d	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐴 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝐴 ) ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )