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

Metamath Proof Explorer

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 ⊢ ( 𝑁 ∈ ℤ → ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑅 ) ∧ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐾 ∈ ( 𝑁 ..^ 𝑅 ) ) )