Proof of Theorem ssfzunsn
Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. . 3
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → 𝑆 ⊆ (𝑀...𝑁)) |
2 | | simpl 472 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(ℤ≥‘𝑀)) → 𝑁 ∈ ℤ) |
3 | | eluzelz 11573 |
. . . . . . . 8
⊢ (𝐼 ∈
(ℤ≥‘𝑀) → 𝐼 ∈ ℤ) |
4 | 3 | adantl 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(ℤ≥‘𝑀)) → 𝐼 ∈ ℤ) |
5 | 2, 4 | ifcld 4081 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(ℤ≥‘𝑀)) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ) |
6 | | zre 11258 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
7 | | eluzelre 11574 |
. . . . . . . . 9
⊢ (𝐼 ∈
(ℤ≥‘𝑀) → 𝐼 ∈ ℝ) |
8 | 6, 7 | anim12i 588 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(ℤ≥‘𝑀)) → (𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
9 | 8 | ancomd 466 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(ℤ≥‘𝑀)) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
10 | | max2 11892 |
. . . . . . 7
⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(ℤ≥‘𝑀)) → 𝑁 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
12 | | eluz2 11569 |
. . . . . 6
⊢ (if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ (ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ ∧ 𝑁 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
13 | 2, 5, 11, 12 | syl3anbrc 1239 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(ℤ≥‘𝑀)) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ (ℤ≥‘𝑁)) |
14 | | fzss2 12252 |
. . . . 5
⊢ (if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ (ℤ≥‘𝑁) → (𝑀...𝑁) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
15 | 13, 14 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(ℤ≥‘𝑀)) → (𝑀...𝑁) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
16 | 15 | 3adant1 1072 |
. . 3
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝑀...𝑁) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
17 | 1, 16 | sstrd 3578 |
. 2
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → 𝑆 ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
18 | | eluzel2 11568 |
. . . . . 6
⊢ (𝐼 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
19 | 18 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℤ) |
20 | 5 | 3adant1 1072 |
. . . . 5
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ) |
21 | 3 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → 𝐼 ∈ ℤ) |
22 | 19, 20, 21 | 3jca 1235 |
. . . 4
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝑀 ∈ ℤ ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ ∧ 𝐼 ∈ ℤ)) |
23 | | eluzle 11576 |
. . . . . 6
⊢ (𝐼 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝐼) |
24 | 23 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → 𝑀 ≤ 𝐼) |
25 | 8 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
26 | 25 | ancomd 466 |
. . . . . 6
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
27 | | max1 11890 |
. . . . . 6
⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝐼 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
28 | 26, 27 | syl 17 |
. . . . 5
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → 𝐼 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
29 | 24, 28 | jca 553 |
. . . 4
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
30 | | elfz2 12204 |
. . . 4
⊢ (𝐼 ∈ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) ↔ ((𝑀 ∈ ℤ ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))) |
31 | 22, 29, 30 | sylanbrc 695 |
. . 3
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → 𝐼 ∈ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
32 | 31 | snssd 4281 |
. 2
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → {𝐼} ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
33 | 17, 32 | unssd 3751 |
1
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝑆 ∪ {𝐼}) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |