Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ) |
2 |
|
simp3 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝐼 ∈ ℤ ) |
3 |
|
simp1 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑀 ∈ ℤ ) |
4 |
2 3
|
ifcld |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ ) |
5 |
4
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ ) |
6 |
|
elfzelz |
⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℤ ) |
7 |
6
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ℤ ) |
8 |
4
|
zred |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℝ ) |
9 |
8
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℝ ) |
10 |
|
zre |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ ) |
11 |
10
|
3ad2ant1 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑀 ∈ ℝ ) |
12 |
11
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℝ ) |
13 |
6
|
zred |
⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℝ ) |
14 |
13
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ℝ ) |
15 |
|
zre |
⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ ) |
16 |
10 15
|
anim12i |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ ) ) |
17 |
16
|
ancomd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ) |
18 |
17
|
3adant2 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ) |
19 |
18
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ) |
20 |
|
min2 |
⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑀 ) |
21 |
19 20
|
syl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑀 ) |
22 |
|
elfzle1 |
⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ≤ 𝑘 ) |
23 |
22
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ≤ 𝑘 ) |
24 |
9 12 14 21 23
|
letrd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑘 ) |
25 |
|
eluz2 |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ) ↔ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑘 ) ) |
26 |
5 7 24 25
|
syl3anbrc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ) ) |
27 |
|
simp2 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑁 ∈ ℤ ) |
28 |
27 2
|
ifcld |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ ) |
29 |
28
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ ) |
30 |
|
zre |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ ) |
31 |
30
|
3ad2ant2 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑁 ∈ ℝ ) |
32 |
31
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ℝ ) |
33 |
28
|
zred |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℝ ) |
34 |
33
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℝ ) |
35 |
|
elfzle2 |
⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ≤ 𝑁 ) |
36 |
35
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ≤ 𝑁 ) |
37 |
30 15
|
anim12i |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ ) ) |
38 |
37
|
3adant1 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ ) ) |
39 |
38
|
ancomd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) |
40 |
|
max2 |
⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) |
41 |
39 40
|
syl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑁 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) |
42 |
41
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) |
43 |
14 32 34 36 42
|
letrd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) |
44 |
|
eluz2 |
⊢ ( if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ( ℤ≥ ‘ 𝑘 ) ↔ ( 𝑘 ∈ ℤ ∧ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ ∧ 𝑘 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) |
45 |
7 29 43 44
|
syl3anbrc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) |
46 |
|
elfzuzb |
⊢ ( 𝑘 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ) ∧ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) ) |
47 |
26 45 46
|
sylanbrc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) |
48 |
47
|
ex |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) ) |
49 |
48
|
ssrdv |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) |
50 |
49
|
adantl |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑀 ... 𝑁 ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) |
51 |
1 50
|
sstrd |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝑆 ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) |
52 |
4
|
adantl |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ ) |
53 |
28
|
adantl |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ ) |
54 |
2
|
adantl |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝐼 ∈ ℤ ) |
55 |
52 53 54
|
3jca |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ ∧ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) |
56 |
16
|
3adant2 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ ) ) |
57 |
56
|
adantl |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ ) ) |
58 |
57
|
ancomd |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ) |
59 |
|
min1 |
⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝐼 ) |
60 |
58 59
|
syl |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝐼 ) |
61 |
38
|
adantl |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ ) ) |
62 |
61
|
ancomd |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) |
63 |
|
max1 |
⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝐼 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) |
64 |
62 63
|
syl |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝐼 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) |
65 |
60 64
|
jca |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝐼 ∧ 𝐼 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) |
66 |
|
elfz2 |
⊢ ( 𝐼 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ↔ ( ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ ∧ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝐼 ∧ 𝐼 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) ) |
67 |
55 65 66
|
sylanbrc |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝐼 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) |
68 |
67
|
snssd |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → { 𝐼 } ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) |
69 |
51 68
|
unssd |
⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑆 ∪ { 𝐼 } ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) |