Metamath Proof Explorer

Theorem ssfzoulel

Description: If a half-open integer range is a subset of a half-open range of nonnegative integers, but its lower bound is greater than or equal to the upper bound of the containing range, or its upper bound is less than or equal to 0, then its upper bound is less than or equal to its lower bound (and therefore it is actually empty). (Contributed by Alexander van der Vekens, 24-May-2018)

Ref Expression
Assertion ssfzoulel ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ 𝑁 ) → 𝐵 ≤ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → 𝐴 ∈ ℤ )
2 simpl3 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → 𝐵 ∈ ℤ )
3 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
4 zre ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
5 ltnle ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) )
6 3 4 5 syl2an ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) )
7 6 3adant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) )
8 7 biimpar ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → 𝐴 < 𝐵 )
9 ssfzo12 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ 𝑁 ) → ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁 ) ) )
10 1 2 8 9 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ 𝑁 ) → ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁 ) ) )
11 4 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℝ )
12 0red ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 0 ∈ ℝ )
13 3 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℝ )
14 letr ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ≤ 0 ∧ 0 ≤ 𝐴 ) → 𝐵 ≤ 𝐴 ) )
15 11 12 13 14 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐵 ≤ 0 ∧ 0 ≤ 𝐴 ) → 𝐵 ≤ 𝐴 ) )
16 15 expcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 0 ≤ 𝐴 → ( 𝐵 ≤ 0 → 𝐵 ≤ 𝐴 ) ) )
17 16 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 0 ≤ 𝐴 ) → ( 𝐵 ≤ 0 → 𝐵 ≤ 𝐴 ) )
18 17 con3d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 0 ≤ 𝐴 ) → ( ¬ 𝐵 ≤ 𝐴 → ¬ 𝐵 ≤ 0 ) )
19 18 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 0 ≤ 𝐴 → ( ¬ 𝐵 ≤ 𝐴 → ¬ 𝐵 ≤ 0 ) ) )
20 19 3adant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 0 ≤ 𝐴 → ( ¬ 𝐵 ≤ 𝐴 → ¬ 𝐵 ≤ 0 ) ) )
21 20 com23 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ¬ 𝐵 ≤ 𝐴 → ( 0 ≤ 𝐴 → ¬ 𝐵 ≤ 0 ) ) )
22 21 imp ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( 0 ≤ 𝐴 → ¬ 𝐵 ≤ 0 ) )
23 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
24 4 23 3 3anim123i ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
25 24 3coml ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
26 letr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ≤ 𝑁 ∧ 𝑁 ≤ 𝐴 ) → 𝐵 ≤ 𝐴 ) )
27 25 26 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐵 ≤ 𝑁 ∧ 𝑁 ≤ 𝐴 ) → 𝐵 ≤ 𝐴 ) )
28 27 expdimp ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐵 ≤ 𝑁 ) → ( 𝑁 ≤ 𝐴 → 𝐵 ≤ 𝐴 ) )
29 28 con3d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐵 ≤ 𝑁 ) → ( ¬ 𝐵 ≤ 𝐴 → ¬ 𝑁 ≤ 𝐴 ) )
30 29 impancom ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( 𝐵 ≤ 𝑁 → ¬ 𝑁 ≤ 𝐴 ) )
31 22 30 anim12d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁 ) → ( ¬ 𝐵 ≤ 0 ∧ ¬ 𝑁 ≤ 𝐴 ) ) )
32 ioran ⊢ ( ¬ ( 𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ↔ ( ¬ 𝑁 ≤ 𝐴 ∧ ¬ 𝐵 ≤ 0 ) )
33 32 biancomi ⊢ ( ¬ ( 𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ↔ ( ¬ 𝐵 ≤ 0 ∧ ¬ 𝑁 ≤ 𝐴 ) )
34 31 33 syl6ibr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁 ) → ¬ ( 𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) )
35 10 34 syld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ 𝑁 ) → ¬ ( 𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) )
36 35 con2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( ( 𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ¬ ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ 𝑁 ) ) )
37 36 impancom ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) → ( ¬ 𝐵 ≤ 𝐴 → ¬ ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ 𝑁 ) ) )
38 37 con4d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0 ) ) → ( ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ 𝑁 ) → 𝐵 ≤ 𝐴 ) )
39 38 ex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0 ) → ( ( 𝐴 ..^ 𝐵 ) ⊆ ( 0 ..^ 𝑁 ) → 𝐵 ≤ 𝐴 ) ) )