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	imbitrrdi	⊢ ( ( ( 𝑁 ∈ ℕ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 ..^ 𝑁 ) → 𝐵 ≤ 𝐴 ) ) )