This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfzouz2

Description: The upper bound of a half-open range is greater than or equal to an element of the range. (Contributed by Mario Carneiro, 29-Sep-2015)

		Ref	Expression
	Assertion	elfzouz2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ( ℤ_≥ ‘ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ℤ )
2		elfzoel2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
3		elfzolt2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 < 𝑁 )
4		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
5		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
6		ltle	⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐾 < 𝑁 → 𝐾 ≤ 𝑁 ) )
7	4 5 6	syl2an	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 → 𝐾 ≤ 𝑁 ) )
8	1 2 7	syl2anc	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 < 𝑁 → 𝐾 ≤ 𝑁 ) )
9	3 8	mpd	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ≤ 𝑁 )
10		eluz2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝐾 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) )
11	1 2 9 10	syl3anbrc	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ( ℤ_≥ ‘ 𝐾 ) )