Metamath Proof Explorer

Theorem ssfzo12

Description: Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018)

Ref Expression
Assertion ssfzo12 ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 fzolb2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐾 ∈ ( 𝐾 ..^ 𝐿 ) ↔ 𝐾 < 𝐿 ) )
2 1 biimp3ar ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → 𝐾 ∈ ( 𝐾 ..^ 𝐿 ) )
3 fzoend ⊢ ( 𝐾 ∈ ( 𝐾 ..^ 𝐿 ) → ( 𝐿 − 1 ) ∈ ( 𝐾 ..^ 𝐿 ) )
4 ssel2 ⊢ ( ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ∈ ( 𝐾 ..^ 𝐿 ) ) → 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) )
5 ssel2 ⊢ ( ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝐿 − 1 ) ∈ ( 𝐾 ..^ 𝐿 ) ) → ( 𝐿 − 1 ) ∈ ( 𝑀 ..^ 𝑁 ) )
6 elfzolt2 ⊢ ( ( 𝐿 − 1 ) ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐿 − 1 ) < 𝑁 )
7 simp2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → 𝐿 ∈ ℤ )
8 elfzoel2 ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
9 zlem1lt ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ≤ 𝑁 ↔ ( 𝐿 − 1 ) < 𝑁 ) )
10 7 8 9 syl2anr ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) ) → ( 𝐿 ≤ 𝑁 ↔ ( 𝐿 − 1 ) < 𝑁 ) )
11 elfzole1 ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ 𝐾 )
12 pm3.2 ⊢ ( 𝑀 ≤ 𝐾 → ( 𝐿 ≤ 𝑁 → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )
13 11 12 syl ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐿 ≤ 𝑁 → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )
14 13 adantr ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) ) → ( 𝐿 ≤ 𝑁 → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )
15 10 14 sylbird ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) ) → ( ( 𝐿 − 1 ) < 𝑁 → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )
16 15 ex ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( ( 𝐿 − 1 ) < 𝑁 → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
17 16 com13 ⊢ ( ( 𝐿 − 1 ) < 𝑁 → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
18 5 6 17 3syl ⊢ ( ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝐿 − 1 ) ∈ ( 𝐾 ..^ 𝐿 ) ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
19 18 ex ⊢ ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( ( 𝐿 − 1 ) ∈ ( 𝐾 ..^ 𝐿 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) )
20 19 com24 ⊢ ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( ( 𝐿 − 1 ) ∈ ( 𝐾 ..^ 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) )
21 4 20 syl5com ⊢ ( ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ∈ ( 𝐾 ..^ 𝐿 ) ) → ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( ( 𝐿 − 1 ) ∈ ( 𝐾 ..^ 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) )
22 21 ex ⊢ ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 ∈ ( 𝐾 ..^ 𝐿 ) → ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( ( 𝐿 − 1 ) ∈ ( 𝐾 ..^ 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) ) )
23 22 pm2.43a ⊢ ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 ∈ ( 𝐾 ..^ 𝐿 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( ( 𝐿 − 1 ) ∈ ( 𝐾 ..^ 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) )
24 23 com14 ⊢ ( ( 𝐿 − 1 ) ∈ ( 𝐾 ..^ 𝐿 ) → ( 𝐾 ∈ ( 𝐾 ..^ 𝐿 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) )
25 3 24 mpcom ⊢ ( 𝐾 ∈ ( 𝐾 ..^ 𝐿 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
26 2 25 mpcom ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )