Proof of Theorem ssfzo12
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzolb2 13706 | . . 3
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐾 ∈ (𝐾..^𝐿) ↔ 𝐾 < 𝐿)) | 
| 2 | 1 | biimp3ar 1472 | . 2
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → 𝐾 ∈ (𝐾..^𝐿)) | 
| 3 |  | fzoend 13796 | . . 3
⊢ (𝐾 ∈ (𝐾..^𝐿) → (𝐿 − 1) ∈ (𝐾..^𝐿)) | 
| 4 |  | ssel2 3978 | . . . . . . 7
⊢ (((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ∧ 𝐾 ∈ (𝐾..^𝐿)) → 𝐾 ∈ (𝑀..^𝑁)) | 
| 5 |  | ssel2 3978 | . . . . . . . . . 10
⊢ (((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ∧ (𝐿 − 1) ∈ (𝐾..^𝐿)) → (𝐿 − 1) ∈ (𝑀..^𝑁)) | 
| 6 |  | elfzolt2 13708 | . . . . . . . . . 10
⊢ ((𝐿 − 1) ∈ (𝑀..^𝑁) → (𝐿 − 1) < 𝑁) | 
| 7 |  | simp2 1138 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → 𝐿 ∈ ℤ) | 
| 8 |  | elfzoel2 13698 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑁 ∈ ℤ) | 
| 9 |  | zlem1lt 12669 | . . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁)) | 
| 10 | 7, 8, 9 | syl2anr 597 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (𝑀..^𝑁) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿)) → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁)) | 
| 11 |  | elfzole1 13707 | . . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝐾) | 
| 12 |  | pm3.2 469 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ≤ 𝐾 → (𝐿 ≤ 𝑁 → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | 
| 13 | 11, 12 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝐿 ≤ 𝑁 → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | 
| 14 | 13 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (𝑀..^𝑁) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿)) → (𝐿 ≤ 𝑁 → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | 
| 15 | 10, 14 | sylbird 260 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ (𝑀..^𝑁) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿)) → ((𝐿 − 1) < 𝑁 → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | 
| 16 | 15 | ex 412 | . . . . . . . . . . 11
⊢ (𝐾 ∈ (𝑀..^𝑁) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐿 − 1) < 𝑁 → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))) | 
| 17 | 16 | com13 88 | . . . . . . . . . 10
⊢ ((𝐿 − 1) < 𝑁 → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → (𝐾 ∈ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))) | 
| 18 | 5, 6, 17 | 3syl 18 | . . . . . . . . 9
⊢ (((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ∧ (𝐿 − 1) ∈ (𝐾..^𝐿)) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → (𝐾 ∈ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))) | 
| 19 | 18 | ex 412 | . . . . . . . 8
⊢ ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → ((𝐿 − 1) ∈ (𝐾..^𝐿) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → (𝐾 ∈ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))))) | 
| 20 | 19 | com24 95 | . . . . . . 7
⊢ ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝐾 ∈ (𝑀..^𝑁) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐿 − 1) ∈ (𝐾..^𝐿) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))))) | 
| 21 | 4, 20 | syl5com 31 | . . . . . 6
⊢ (((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ∧ 𝐾 ∈ (𝐾..^𝐿)) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐿 − 1) ∈ (𝐾..^𝐿) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))))) | 
| 22 | 21 | ex 412 | . . . . 5
⊢ ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝐾 ∈ (𝐾..^𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐿 − 1) ∈ (𝐾..^𝐿) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))))) | 
| 23 | 22 | pm2.43a 54 | . . . 4
⊢ ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝐾 ∈ (𝐾..^𝐿) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐿 − 1) ∈ (𝐾..^𝐿) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))))) | 
| 24 | 23 | com14 96 | . . 3
⊢ ((𝐿 − 1) ∈ (𝐾..^𝐿) → (𝐾 ∈ (𝐾..^𝐿) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))))) | 
| 25 | 3, 24 | mpcom 38 | . 2
⊢ (𝐾 ∈ (𝐾..^𝐿) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))) | 
| 26 | 2, 25 | mpcom 38 | 1
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) |