Metamath Proof Explorer

Theorem ssfzo12bi

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

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

Proof

Step Hyp Ref Expression
1 df-3an ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) ↔ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) )
2 1 biimpri ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) )
3 2 3adant2 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) )
4 ssfzo12 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿 ) → ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )
5 3 4 syl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )
6 elfzo2 ⊢ ( 𝑥 ∈ ( 𝐾 ..^ 𝐿 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐿 ∈ ℤ ∧ 𝑥 < 𝐿 ) )
7 eluz2 ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) )
8 simprrl ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑀 ∈ ℤ )
9 8 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥 ) ) → 𝑀 ∈ ℤ )
10 simpll ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥 ) ) → 𝑥 ∈ ℤ )
11 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
12 11 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ )
13 12 adantl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑀 ∈ ℝ )
14 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
15 14 adantr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐾 ∈ ℝ )
16 15 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝐾 ∈ ℝ )
17 zre ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
18 17 adantr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑥 ∈ ℝ )
19 letr ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥 ) → 𝑀 ≤ 𝑥 ) )
20 13 16 18 19 syl2an23an ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥 ) → 𝑀 ≤ 𝑥 ) )
21 20 imp ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥 ) ) → 𝑀 ≤ 𝑥 )
22 9 10 21 3jca ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) )
23 22 exp31 ⊢ ( 𝑥 ∈ ℤ → ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥 ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) ) )
24 23 com23 ⊢ ( 𝑥 ∈ ℤ → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥 ) → ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) ) )
25 24 expdimp ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( 𝐾 ≤ 𝑥 → ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) ) )
26 25 impancom ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) → ( 𝑀 ≤ 𝐾 → ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) ) )
27 26 com13 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 ≤ 𝐾 → ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) ) )
28 27 3adant3 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( 𝑀 ≤ 𝐾 → ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) ) )
29 28 com12 ⊢ ( 𝑀 ≤ 𝐾 → ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) ) )
30 29 adantr ⊢ ( ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) → ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) ) )
31 30 impcom ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) )
32 31 com12 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) )
33 32 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) ∧ 𝑥 < 𝐿 ) → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) )
34 33 imp ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) ∧ 𝑥 < 𝐿 ) ∧ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) → ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) )
35 eluz2 ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) )
36 34 35 sylibr ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) ∧ 𝑥 < 𝐿 ) ∧ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
37 simpl2r ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → 𝑁 ∈ ℤ )
38 37 adantl ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) ∧ 𝑥 < 𝐿 ) ∧ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) → 𝑁 ∈ ℤ )
39 17 adantl ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℝ )
40 zre ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
41 40 ad3antlr ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝑥 ∈ ℤ ) → 𝐿 ∈ ℝ )
42 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
43 42 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
44 43 adantl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℝ )
45 44 adantr ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝑥 ∈ ℤ ) → 𝑁 ∈ ℝ )
46 ltletr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑥 < 𝐿 ∧ 𝐿 ≤ 𝑁 ) → 𝑥 < 𝑁 ) )
47 39 41 45 46 syl3anc ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 < 𝐿 ∧ 𝐿 ≤ 𝑁 ) → 𝑥 < 𝑁 ) )
48 47 ex ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑥 ∈ ℤ → ( ( 𝑥 < 𝐿 ∧ 𝐿 ≤ 𝑁 ) → 𝑥 < 𝑁 ) ) )
49 48 com23 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑥 < 𝐿 ∧ 𝐿 ≤ 𝑁 ) → ( 𝑥 ∈ ℤ → 𝑥 < 𝑁 ) ) )
50 49 3adant3 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( ( 𝑥 < 𝐿 ∧ 𝐿 ≤ 𝑁 ) → ( 𝑥 ∈ ℤ → 𝑥 < 𝑁 ) ) )
51 50 expcomd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( 𝐿 ≤ 𝑁 → ( 𝑥 < 𝐿 → ( 𝑥 ∈ ℤ → 𝑥 < 𝑁 ) ) ) )
52 51 adantld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) → ( 𝑥 < 𝐿 → ( 𝑥 ∈ ℤ → 𝑥 < 𝑁 ) ) ) )
53 52 imp ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝑥 < 𝐿 → ( 𝑥 ∈ ℤ → 𝑥 < 𝑁 ) ) )
54 53 com13 ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 < 𝐿 → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → 𝑥 < 𝑁 ) ) )
55 54 adantr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) → ( 𝑥 < 𝐿 → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → 𝑥 < 𝑁 ) ) )
56 55 imp ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) ∧ 𝑥 < 𝐿 ) → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → 𝑥 < 𝑁 ) )
57 56 imp ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) ∧ 𝑥 < 𝐿 ) ∧ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) → 𝑥 < 𝑁 )
58 elfzo2 ⊢ ( 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑥 < 𝑁 ) )
59 36 38 57 58 syl3anbrc ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) ∧ 𝑥 < 𝐿 ) ∧ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) → 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) )
60 59 exp31 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) → ( 𝑥 < 𝐿 → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) ) ) )
61 60 3adant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥 ) → ( 𝑥 < 𝐿 → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) ) ) )
62 7 61 sylbi ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑥 < 𝐿 → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) ) ) )
63 62 imp ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝑥 < 𝐿 ) → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) ) )
64 63 3adant2 ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐿 ∈ ℤ ∧ 𝑥 < 𝐿 ) → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) ) )
65 6 64 sylbi ⊢ ( 𝑥 ∈ ( 𝐾 ..^ 𝐿 ) → ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) ) )
66 65 com12 ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝑥 ∈ ( 𝐾 ..^ 𝐿 ) → 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) ) )
67 66 ssrdv ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) )
68 67 ex ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) → ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) ) )
69 5 68 impbid ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 < 𝐿 ) → ( ( 𝐾 ..^ 𝐿 ) ⊆ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )