Theorem elfzonelfzo

Description: If an element of a half-open integer range is not contained in the lower subrange, it must be in the upper subrange. (Contributed by Alexander van der Vekens, 30-Mar-2018)

	Ref	Expression
Assertion	elfzonelfzo	⊢ ( 𝑁 ∈ ℤ → ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐾 ∈ ( 𝑁 ..^ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzo2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑅 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) )
2		simpr	⊢ ( ( ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
3		eluzelz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ℤ )
4	3	3ad2ant1	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) → 𝐾 ∈ ℤ )
5	4	ad2antrr	⊢ ( ( ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ )
6		eluzelre	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ℝ )
7		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
8		ltnle	⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐾 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐾 ) )
9	6 7 8	syl2an	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐾 ) )
10		id	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
11	10	3expa	⊢ ( ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝑁 ) → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
12		elfzo2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
13	11 12	sylibr	⊢ ( ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝑁 ) → 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) )
14	13	ex	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 → 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) )
15	9 14	sylbird	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑁 ≤ 𝐾 → 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) )
16	15	con1d	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ≤ 𝐾 ) )
17	16	ex	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 ∈ ℤ → ( ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ≤ 𝐾 ) ) )
18	17	com23	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁 ∈ ℤ → 𝑁 ≤ 𝐾 ) ) )
19	18	3ad2ant1	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) → ( ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁 ∈ ℤ → 𝑁 ≤ 𝐾 ) ) )
20	19	imp31	⊢ ( ( ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ≤ 𝐾 )
21		eluz2	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ≤ 𝐾 ) )
22	2 5 20 21	syl3anbrc	⊢ ( ( ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) )
23		simpll2	⊢ ( ( ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → 𝑅 ∈ ℤ )
24		simpll3	⊢ ( ( ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → 𝐾 < 𝑅 )
25		elfzo2	⊢ ( 𝐾 ∈ ( 𝑁 ..^ 𝑅 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) )
26	22 23 24 25	syl3anbrc	⊢ ( ( ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ( 𝑁 ..^ 𝑅 ) )
27	26	ex	⊢ ( ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑁 ∈ ℤ → 𝐾 ∈ ( 𝑁 ..^ 𝑅 ) ) )
28	1 27	sylanb	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑁 ∈ ℤ → 𝐾 ∈ ( 𝑁 ..^ 𝑅 ) ) )
29	28	com12	⊢ ( 𝑁 ∈ ℤ → ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐾 ∈ ( 𝑁 ..^ 𝑅 ) ) )