Metamath Proof Explorer

Theorem predfz

Description: Calculate the predecessor of an integer under a finite set of integers. (Contributed by Scott Fenton, 8-Aug-2013) (Proof shortened by Mario Carneiro, 3-May-2015)

Ref Expression
Assertion predfz ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → Pred ( < , ( 𝑀 ... 𝑁 ) , 𝐾 ) = ( 𝑀 ... ( 𝐾 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 elfzelz ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℤ )
2 elfzelz ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℤ )
3 zltlem1 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑥 < 𝐾 ↔ 𝑥 ≤ ( 𝐾 − 1 ) ) )
4 1 2 3 syl2anr ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 < 𝐾 ↔ 𝑥 ≤ ( 𝐾 − 1 ) ) )
5 elfzuz ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
6 peano2zm ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℤ )
7 2 6 syl ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 1 ) ∈ ℤ )
8 elfz5 ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 − 1 ) ∈ ℤ ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ↔ 𝑥 ≤ ( 𝐾 − 1 ) ) )
9 5 7 8 syl2anr ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ↔ 𝑥 ≤ ( 𝐾 − 1 ) ) )
10 4 9 bitr4d ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 < 𝐾 ↔ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) )
11 10 pm5.32da ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 < 𝐾 ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) ) )
12 vex ⊢ 𝑥 ∈ V
13 12 elpred ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑥 ∈ Pred ( < , ( 𝑀 ... 𝑁 ) , 𝐾 ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 < 𝐾 ) ) )
14 elfzuz3 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
15 2 zcnd ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℂ )
16 ax-1cn ⊢ 1 ∈ ℂ
17 npcan ⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
18 15 16 17 sylancl ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
19 18 fveq2d ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ℤ≥ ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( ℤ≥ ‘ 𝐾 ) )
20 14 19 eleqtrrd ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝐾 − 1 ) + 1 ) ) )
21 peano2uzr ⊢ ( ( ( 𝐾 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐾 − 1 ) ) )
22 7 20 21 syl2anc ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐾 − 1 ) ) )
23 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝐾 − 1 ) ) → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) )
24 22 23 syl ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) )
25 24 sseld ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) )
26 25 pm4.71rd ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) ) )
27 11 13 26 3bitr4d ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑥 ∈ Pred ( < , ( 𝑀 ... 𝑁 ) , 𝐾 ) ↔ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) )
28 27 eqrdv ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → Pred ( < , ( 𝑀 ... 𝑁 ) , 𝐾 ) = ( 𝑀 ... ( 𝐾 − 1 ) ) )