This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elincfzoext

Description: Membership of an increased integer in a correspondingly extended half-open range of integers. (Contributed by AV, 30-Apr-2020)

Ref Expression
Assertion elincfzoext ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 + 𝐼 ) ∈ ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 elfzole1 ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ 𝑍 )
2 elfzoelz ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑍 ∈ ℤ )
3 2 zred ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑍 ∈ ℝ )
4 3 adantr ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑀 ≤ 𝑍 ) → 𝑍 ∈ ℝ )
5 nn0addge1 ⊢ ( ( 𝑍 ∈ ℝ ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ≤ ( 𝑍 + 𝐼 ) )
6 4 5 sylan ⊢ ( ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑀 ≤ 𝑍 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ≤ ( 𝑍 + 𝐼 ) )
7 elfzoel1 ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℤ )
8 7 zred ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℝ )
9 8 adantr ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
10 3 adantr ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ∈ ℝ )
11 nn0re ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ )
12 11 adantl ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℝ )
13 10 12 readdcld ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 + 𝐼 ) ∈ ℝ )
14 letr ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑍 ∈ ℝ ∧ ( 𝑍 + 𝐼 ) ∈ ℝ ) → ( ( 𝑀 ≤ 𝑍 ∧ 𝑍 ≤ ( 𝑍 + 𝐼 ) ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) )
15 9 10 13 14 syl3anc ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝑀 ≤ 𝑍 ∧ 𝑍 ≤ ( 𝑍 + 𝐼 ) ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) )
16 15 exp4b ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐼 ∈ ℕ0 → ( 𝑀 ≤ 𝑍 → ( 𝑍 ≤ ( 𝑍 + 𝐼 ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) ) ) )
17 16 com23 ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝑍 → ( 𝐼 ∈ ℕ0 → ( 𝑍 ≤ ( 𝑍 + 𝐼 ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) ) ) )
18 17 imp31 ⊢ ( ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑀 ≤ 𝑍 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 ≤ ( 𝑍 + 𝐼 ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) )
19 6 18 mpd ⊢ ( ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑀 ≤ 𝑍 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) )
20 19 exp31 ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝑍 → ( 𝐼 ∈ ℕ0 → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) ) )
21 1 20 mpd ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐼 ∈ ℕ0 → 𝑀 ≤ ( 𝑍 + 𝐼 ) ) )
22 21 imp ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑀 ≤ ( 𝑍 + 𝐼 ) )
23 elfzoel2 ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
24 23 zred ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℝ )
25 24 adantr ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
26 elfzolt2 ⊢ ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑍 < 𝑁 )
27 26 adantr ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 < 𝑁 )
28 10 25 12 27 ltadd1dd ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 + 𝐼 ) < ( 𝑁 + 𝐼 ) )
29 2 adantr ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑍 ∈ ℤ )
30 nn0z ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℤ )
31 30 adantl ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℤ )
32 29 31 zaddcld ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 + 𝐼 ) ∈ ℤ )
33 7 adantr ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
34 23 adantr ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
35 34 31 zaddcld ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑁 + 𝐼 ) ∈ ℤ )
36 elfzo ⊢ ( ( ( 𝑍 + 𝐼 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑁 + 𝐼 ) ∈ ℤ ) → ( ( 𝑍 + 𝐼 ) ∈ ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) ↔ ( 𝑀 ≤ ( 𝑍 + 𝐼 ) ∧ ( 𝑍 + 𝐼 ) < ( 𝑁 + 𝐼 ) ) ) )
37 32 33 35 36 syl3anc ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝑍 + 𝐼 ) ∈ ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) ↔ ( 𝑀 ≤ ( 𝑍 + 𝐼 ) ∧ ( 𝑍 + 𝐼 ) < ( 𝑁 + 𝐼 ) ) ) )
38 22 28 37 mpbir2and ⊢ ( ( 𝑍 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑍 + 𝐼 ) ∈ ( 𝑀 ..^ ( 𝑁 + 𝐼 ) ) )