Metamath Proof Explorer

Theorem elfzonlteqm1

Description: If an element of a half-open integer range is not less than the upper bound of the range decreased by 1, it must be equal to the upper bound of the range decreased by 1. (Contributed by AV, 3-Nov-2018)

Ref Expression
Assertion elfzonlteqm1 ( ( 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ ¬ 𝐴 < ( 𝐵 − 1 ) ) → 𝐴 = ( 𝐵 − 1 ) )

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 elfzo0 ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) ↔ ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) )
3 elnnuz ⊢ ( 𝐵 ∈ ℕ ↔ 𝐵 ∈ ( ℤ≥ ‘ 1 ) )
4 3 biimpi ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ( ℤ≥ ‘ 1 ) )
5 0p1e1 ⊢ ( 0 + 1 ) = 1
6 5 a1i ⊢ ( 𝐵 ∈ ℕ → ( 0 + 1 ) = 1 )
7 6 fveq2d ⊢ ( 𝐵 ∈ ℕ → ( ℤ≥ ‘ ( 0 + 1 ) ) = ( ℤ≥ ‘ 1 ) )
8 4 7 eleqtrrd ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
9 8 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
10 2 9 sylbi ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → 𝐵 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
11 fzosplitsnm1 ⊢ ( ( 0 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( 0 ..^ 𝐵 ) = ( ( 0 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) } ) )
12 1 10 11 sylancr ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → ( 0 ..^ 𝐵 ) = ( ( 0 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) } ) )
13 eleq2 ⊢ ( ( 0 ..^ 𝐵 ) = ( ( 0 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) } ) → ( 𝐴 ∈ ( 0 ..^ 𝐵 ) ↔ 𝐴 ∈ ( ( 0 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) } ) ) )
14 elun ⊢ ( 𝐴 ∈ ( ( 0 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) } ) ↔ ( 𝐴 ∈ ( 0 ..^ ( 𝐵 − 1 ) ) ∨ 𝐴 ∈ { ( 𝐵 − 1 ) } ) )
15 elfzo0 ⊢ ( 𝐴 ∈ ( 0 ..^ ( 𝐵 − 1 ) ) ↔ ( 𝐴 ∈ ℕ0 ∧ ( 𝐵 − 1 ) ∈ ℕ ∧ 𝐴 < ( 𝐵 − 1 ) ) )
16 pm2.24 ⊢ ( 𝐴 < ( 𝐵 − 1 ) → ( ¬ 𝐴 < ( 𝐵 − 1 ) → 𝐴 = ( 𝐵 − 1 ) ) )
17 16 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐵 − 1 ) ∈ ℕ ∧ 𝐴 < ( 𝐵 − 1 ) ) → ( ¬ 𝐴 < ( 𝐵 − 1 ) → 𝐴 = ( 𝐵 − 1 ) ) )
18 15 17 sylbi ⊢ ( 𝐴 ∈ ( 0 ..^ ( 𝐵 − 1 ) ) → ( ¬ 𝐴 < ( 𝐵 − 1 ) → 𝐴 = ( 𝐵 − 1 ) ) )
19 elsni ⊢ ( 𝐴 ∈ { ( 𝐵 − 1 ) } → 𝐴 = ( 𝐵 − 1 ) )
20 19 a1d ⊢ ( 𝐴 ∈ { ( 𝐵 − 1 ) } → ( ¬ 𝐴 < ( 𝐵 − 1 ) → 𝐴 = ( 𝐵 − 1 ) ) )
21 18 20 jaoi ⊢ ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 − 1 ) ) ∨ 𝐴 ∈ { ( 𝐵 − 1 ) } ) → ( ¬ 𝐴 < ( 𝐵 − 1 ) → 𝐴 = ( 𝐵 − 1 ) ) )
22 14 21 sylbi ⊢ ( 𝐴 ∈ ( ( 0 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) } ) → ( ¬ 𝐴 < ( 𝐵 − 1 ) → 𝐴 = ( 𝐵 − 1 ) ) )
23 13 22 biimtrdi ⊢ ( ( 0 ..^ 𝐵 ) = ( ( 0 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) } ) → ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → ( ¬ 𝐴 < ( 𝐵 − 1 ) → 𝐴 = ( 𝐵 − 1 ) ) ) )
24 12 23 mpcom ⊢ ( 𝐴 ∈ ( 0 ..^ 𝐵 ) → ( ¬ 𝐴 < ( 𝐵 − 1 ) → 𝐴 = ( 𝐵 − 1 ) ) )
25 24 imp ⊢ ( ( 𝐴 ∈ ( 0 ..^ 𝐵 ) ∧ ¬ 𝐴 < ( 𝐵 − 1 ) ) → 𝐴 = ( 𝐵 − 1 ) )