Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . 3
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → 𝑆 ⊆ (𝑀...𝑁)) |
2 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝐼 ∈
ℤ) |
3 | | simp1 1137 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝑀 ∈
ℤ) |
4 | 2, 3 | ifcld 4470 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℤ) |
5 | 4 | adantr 484 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℤ) |
6 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝑁 ∈
ℤ) |
7 | 6, 2 | ifcld 4470 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ) |
8 | 7 | adantr 484 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ) |
9 | | elfzelz 13010 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ) |
10 | 9 | adantl 485 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ ℤ) |
11 | 4 | zred 12180 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℝ) |
12 | 11 | adantr 484 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℝ) |
13 | | zre 12078 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
14 | 13 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝑀 ∈
ℝ) |
15 | 14 | adantr 484 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℝ) |
16 | 9 | zred 12180 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ) |
17 | 16 | adantl 485 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ ℝ) |
18 | | zre 12078 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ ℤ → 𝐼 ∈
ℝ) |
19 | 13, 18 | anim12i 616 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑀 ∈ ℝ ∧ 𝐼 ∈
ℝ)) |
20 | 19 | ancomd 465 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝐼 ∈ ℝ ∧ 𝑀 ∈
ℝ)) |
21 | 20 | 3adant2 1132 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝐼 ∈ ℝ ∧ 𝑀 ∈
ℝ)) |
22 | 21 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ)) |
23 | | min2 12678 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝑀) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝑀) |
25 | | elfzle1 13013 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑘) |
26 | 25 | adantl 485 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑀 ≤ 𝑘) |
27 | 12, 15, 17, 24, 26 | letrd 10887 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝑘) |
28 | | zre 12078 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
29 | 28 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝑁 ∈
ℝ) |
30 | 29 | adantr 484 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ) |
31 | 7 | zred 12180 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℝ) |
32 | 31 | adantr 484 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℝ) |
33 | | elfzle2 13014 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ≤ 𝑁) |
34 | 33 | adantl 485 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ≤ 𝑁) |
35 | 28, 18 | anim12i 616 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑁 ∈ ℝ ∧ 𝐼 ∈
ℝ)) |
36 | 35 | 3adant1 1131 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑁 ∈ ℝ ∧ 𝐼 ∈
ℝ)) |
37 | 36 | ancomd 465 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝐼 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
38 | | max2 12675 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → 𝑁 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
40 | 39 | adantr 484 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑁 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
41 | 17, 30, 32, 34, 40 | letrd 10887 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
42 | 5, 8, 10, 27, 41 | elfzd 13001 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
43 | 42 | ex 416 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))) |
44 | 43 | ssrdv 3893 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑀...𝑁) ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
45 | 44 | adantl 485 |
. . 3
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑀...𝑁) ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
46 | 1, 45 | sstrd 3897 |
. 2
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → 𝑆 ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
47 | 4 | adantl 485 |
. . . 4
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ∈ ℤ) |
48 | 7 | adantl 485 |
. . . 4
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℤ) |
49 | 2 | adantl 485 |
. . . 4
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → 𝐼 ∈ ℤ) |
50 | 19 | 3adant2 1132 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑀 ∈ ℝ ∧ 𝐼 ∈
ℝ)) |
51 | 50 | adantl 485 |
. . . . . 6
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
52 | 51 | ancomd 465 |
. . . . 5
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ)) |
53 | | min1 12677 |
. . . . 5
⊢ ((𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝐼) |
54 | 52, 53 | syl 17 |
. . . 4
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → if(𝐼 ≤ 𝑀, 𝐼, 𝑀) ≤ 𝐼) |
55 | 36 | adantl 485 |
. . . . . 6
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
56 | 55 | ancomd 465 |
. . . . 5
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
57 | | max1 12673 |
. . . . 5
⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝐼 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
58 | 56, 57 | syl 17 |
. . . 4
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → 𝐼 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
59 | 47, 48, 49, 54, 58 | elfzd 13001 |
. . 3
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → 𝐼 ∈ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
60 | 59 | snssd 4707 |
. 2
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → {𝐼} ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
61 | 46, 60 | unssd 4086 |
1
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑆 ∪ {𝐼}) ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |