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	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (A \in ℕ_{0} \land M Ramsey F \leq A)) \to M Ramsey F \in ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
2		ltpnf	$⊢ A \in ℝ \to A < +∞$
3		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
4		pnfxr	$⊢ +∞ \in ℝ^{*}$
5		xrltnle	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to (A < +∞ \leftrightarrow \neg +∞ \leq A)$
6	3 4 5	sylancl	$⊢ A \in ℝ \to (A < +∞ \leftrightarrow \neg +∞ \leq A)$
7	2 6	mpbid	$⊢ A \in ℝ \to \neg +∞ \leq A$
8	1 7	syl	$⊢ A \in ℕ_{0} \to \neg +∞ \leq A$
9	8	ad2antrl	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (A \in ℕ_{0} \land M Ramsey F \leq A)) \to \neg +∞ \leq A$
10		simprr	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (A \in ℕ_{0} \land M Ramsey F \leq A)) \to M Ramsey F \leq A$
11		breq1	$⊢ M Ramsey F = +∞ \to (M Ramsey F \leq A \leftrightarrow +∞ \leq A)$
12	10 11	syl5ibcom	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (A \in ℕ_{0} \land M Ramsey F \leq A)) \to (M Ramsey F = +∞ \to +∞ \leq A)$
13	9 12	mtod	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (A \in ℕ_{0} \land M Ramsey F \leq A)) \to \neg M Ramsey F = +∞$
14		elsni	$⊢ M Ramsey F \in \{+∞\} \to M Ramsey F = +∞$
15	13 14	nsyl	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (A \in ℕ_{0} \land M Ramsey F \leq A)) \to \neg M Ramsey F \in \{+∞\}$
16		ramcl2	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to M Ramsey F \in (ℕ_{0} \cup \{+∞\})$
17	16	adantr	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (A \in ℕ_{0} \land M Ramsey F \leq A)) \to M Ramsey F \in (ℕ_{0} \cup \{+∞\})$
18		elun	$⊢ M Ramsey F \in (ℕ_{0} \cup \{+∞\}) \leftrightarrow (M Ramsey F \in ℕ_{0} \lor M Ramsey F \in \{+∞\})$
19	17 18	sylib	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (A \in ℕ_{0} \land M Ramsey F \leq A)) \to (M Ramsey F \in ℕ_{0} \lor M Ramsey F \in \{+∞\})$
20	19	ord	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (A \in ℕ_{0} \land M Ramsey F \leq A)) \to (\neg M Ramsey F \in ℕ_{0} \to M Ramsey F \in \{+∞\})$
21	15 20	mt3d	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (A \in ℕ_{0} \land M Ramsey F \leq A)) \to M Ramsey F \in ℕ_{0}$

Metamath Proof Explorer

Theorem ramubcl

Proof