Metamath Proof Explorer

Theorem preduz

Description: The value of the predecessor class over an upper integer set. (Contributed by Scott Fenton, 16-May-2014)

Ref Expression
Assertion preduz ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 1 elpred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ∈ Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑁 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 < 𝑁 ) ) )
3 eluzelz ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑥 ∈ ℤ )
4 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
5 zltlem1 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑥 < 𝑁 ↔ 𝑥 ≤ ( 𝑁 − 1 ) ) )
6 3 4 5 syl2anr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑥 < 𝑁 ↔ 𝑥 ≤ ( 𝑁 − 1 ) ) )
7 6 pm5.32da ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 < 𝑁 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) )
8 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
9 eluz1 ⊢ ( 𝑀 ∈ ℤ → ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) )
10 8 9 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) )
11 10 anbi1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ↔ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) )
12 7 11 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 < 𝑁 ) ↔ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) )
13 2 12 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ∈ Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑁 ) ↔ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) )
14 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
15 4 14 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 1 ) ∈ ℤ )
16 8 15 jca ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) )
17 16 biantrurd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) ) )
18 13 17 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ∈ Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) ) )
19 elfz2 ⊢ ( 𝑥 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑥 ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) )
20 df-3an ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) )
21 20 anbi1i ⊢ ( ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑥 ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) ↔ ( ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑥 ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) )
22 anass ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑥 ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ ( 𝑀 ≤ 𝑥 ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) ) )
23 anass ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ↔ ( 𝑥 ∈ ℤ ∧ ( 𝑀 ≤ 𝑥 ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) )
24 23 anbi2i ⊢ ( ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ ( 𝑀 ≤ 𝑥 ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) ) )
25 22 24 bitr4i ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑥 ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) )
26 19 21 25 3bitri ⊢ ( 𝑥 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ∧ 𝑥 ≤ ( 𝑁 − 1 ) ) ) )
27 18 26 bitr4di ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ∈ Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑁 ) ↔ 𝑥 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) )
28 27 eqrdv ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )