Step |
Hyp |
Ref |
Expression |
1 |
|
elfzofz |
⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐴 ∈ ( 𝑀 ... 𝑁 ) ) |
2 |
|
elfzolt2 |
⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐴 < 𝑁 ) |
3 |
1 2
|
jca |
⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) ) |
4 |
|
elfzuz |
⊢ ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) → 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
5 |
4
|
adantr |
⊢ ( ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) → 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
6 |
|
elfzel2 |
⊢ ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ ) |
7 |
6
|
adantr |
⊢ ( ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) → 𝑁 ∈ ℤ ) |
8 |
|
simpr |
⊢ ( ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) → 𝐴 < 𝑁 ) |
9 |
|
elfzo2 |
⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) ) |
10 |
5 7 8 9
|
syl3anbrc |
⊢ ( ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) → 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) ) |
11 |
3 10
|
impbii |
⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) ) |