Step | Hyp | Ref
| Expression |
1 | | df-3an 1088 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) ↔ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝐾 < 𝐿)) |
2 | 1 | biimpri 227 |
. . . 4
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝐾 < 𝐿) → (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿)) |
3 | 2 | 3adant2 1130 |
. . 3
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿)) |
4 | | ssfzo12 13478 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) |
5 | 3, 4 | syl 17 |
. 2
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) |
6 | | elfzo2 13389 |
. . . . . 6
⊢ (𝑥 ∈ (𝐾..^𝐿) ↔ (𝑥 ∈ (ℤ≥‘𝐾) ∧ 𝐿 ∈ ℤ ∧ 𝑥 < 𝐿)) |
7 | | eluz2 12587 |
. . . . . . . . 9
⊢ (𝑥 ∈
(ℤ≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥)) |
8 | | simprrl 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℤ ∧ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑀 ∈
ℤ) |
9 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ ℤ ∧ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥)) → 𝑀 ∈ ℤ) |
10 | | simpll 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ ℤ ∧ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥)) → 𝑥 ∈ ℤ) |
11 | | zre 12323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
12 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℝ) |
13 | 12 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑀 ∈
ℝ) |
14 | | zre 12323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐾 ∈
ℝ) |
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝐾 ∈
ℝ) |
17 | | zre 12323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℝ) |
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ ℤ ∧ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑥 ∈
ℝ) |
19 | | letr 11069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥) → 𝑀 ≤ 𝑥)) |
20 | 13, 16, 18, 19 | syl2an23an 1422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℤ ∧ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) →
((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥) → 𝑀 ≤ 𝑥)) |
21 | 20 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ ℤ ∧ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥)) → 𝑀 ≤ 𝑥) |
22 | 9, 10, 21 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ ℤ ∧ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥)) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)) |
23 | 22 | exp31 420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℤ → (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)))) |
24 | 23 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℤ → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑥) → (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)))) |
25 | 24 | expdimp 453 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝐾) → (𝐾 ≤ 𝑥 → (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)))) |
26 | 25 | impancom 452 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) → (𝑀 ≤ 𝐾 → (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)))) |
27 | 26 | com13 88 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ≤ 𝐾 → ((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)))) |
28 | 27 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → (𝑀 ≤ 𝐾 → ((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)))) |
29 | 28 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ≤ 𝐾 → (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)))) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁) → (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)))) |
31 | 30 | impcom 408 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → ((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥))) |
32 | 31 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥))) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) ∧ 𝑥 < 𝐿) → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥))) |
34 | 33 | imp 407 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) ∧ 𝑥 < 𝐿) ∧ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) → (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)) |
35 | | eluz2 12587 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)) |
36 | 34, 35 | sylibr 233 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) ∧ 𝑥 < 𝐿) ∧ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) → 𝑥 ∈ (ℤ≥‘𝑀)) |
37 | | simpl2r 1226 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → 𝑁 ∈ ℤ) |
38 | 37 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) ∧ 𝑥 < 𝐿) ∧ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) → 𝑁 ∈ ℤ) |
39 | 17 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℝ) |
40 | | zre 12323 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) |
41 | 40 | ad3antlr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → 𝐿 ∈
ℝ) |
42 | | zre 12323 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℝ) |
44 | 43 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈
ℝ) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → 𝑁 ∈
ℝ) |
46 | | ltletr 11067 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑥 < 𝐿 ∧ 𝐿 ≤ 𝑁) → 𝑥 < 𝑁)) |
47 | 39, 41, 45, 46 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → ((𝑥 < 𝐿 ∧ 𝐿 ≤ 𝑁) → 𝑥 < 𝑁)) |
48 | 47 | ex 413 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 ∈ ℤ → ((𝑥 < 𝐿 ∧ 𝐿 ≤ 𝑁) → 𝑥 < 𝑁))) |
49 | 48 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 < 𝐿 ∧ 𝐿 ≤ 𝑁) → (𝑥 ∈ ℤ → 𝑥 < 𝑁))) |
50 | 49 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝑥 < 𝐿 ∧ 𝐿 ≤ 𝑁) → (𝑥 ∈ ℤ → 𝑥 < 𝑁))) |
51 | 50 | expcomd 417 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → (𝐿 ≤ 𝑁 → (𝑥 < 𝐿 → (𝑥 ∈ ℤ → 𝑥 < 𝑁)))) |
52 | 51 | adantld 491 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁) → (𝑥 < 𝐿 → (𝑥 ∈ ℤ → 𝑥 < 𝑁)))) |
53 | 52 | imp 407 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → (𝑥 < 𝐿 → (𝑥 ∈ ℤ → 𝑥 < 𝑁))) |
54 | 53 | com13 88 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → (𝑥 < 𝐿 → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → 𝑥 < 𝑁))) |
55 | 54 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) → (𝑥 < 𝐿 → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → 𝑥 < 𝑁))) |
56 | 55 | imp 407 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) ∧ 𝑥 < 𝐿) → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → 𝑥 < 𝑁)) |
57 | 56 | imp 407 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) ∧ 𝑥 < 𝐿) ∧ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) → 𝑥 < 𝑁) |
58 | | elfzo2 13389 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑀..^𝑁) ↔ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑥 < 𝑁)) |
59 | 36, 38, 57, 58 | syl3anbrc 1342 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) ∧ 𝑥 < 𝐿) ∧ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) → 𝑥 ∈ (𝑀..^𝑁)) |
60 | 59 | exp31 420 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) → (𝑥 < 𝐿 → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → 𝑥 ∈ (𝑀..^𝑁)))) |
61 | 60 | 3adant1 1129 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥) → (𝑥 < 𝐿 → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → 𝑥 ∈ (𝑀..^𝑁)))) |
62 | 7, 61 | sylbi 216 |
. . . . . . . 8
⊢ (𝑥 ∈
(ℤ≥‘𝐾) → (𝑥 < 𝐿 → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → 𝑥 ∈ (𝑀..^𝑁)))) |
63 | 62 | imp 407 |
. . . . . . 7
⊢ ((𝑥 ∈
(ℤ≥‘𝐾) ∧ 𝑥 < 𝐿) → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → 𝑥 ∈ (𝑀..^𝑁))) |
64 | 63 | 3adant2 1130 |
. . . . . 6
⊢ ((𝑥 ∈
(ℤ≥‘𝐾) ∧ 𝐿 ∈ ℤ ∧ 𝑥 < 𝐿) → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → 𝑥 ∈ (𝑀..^𝑁))) |
65 | 6, 64 | sylbi 216 |
. . . . 5
⊢ (𝑥 ∈ (𝐾..^𝐿) → ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → 𝑥 ∈ (𝑀..^𝑁))) |
66 | 65 | com12 32 |
. . . 4
⊢ ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → (𝑥 ∈ (𝐾..^𝐿) → 𝑥 ∈ (𝑀..^𝑁))) |
67 | 66 | ssrdv 3932 |
. . 3
⊢ ((((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) ∧ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)) → (𝐾..^𝐿) ⊆ (𝑀..^𝑁)) |
68 | 67 | ex 413 |
. 2
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁) → (𝐾..^𝐿) ⊆ (𝑀..^𝑁))) |
69 | 5, 68 | impbid 211 |
1
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) |