Metamath Proof Explorer

Theorem metakunt2

Description: A is an endomapping. (Contributed by metakunt, 23-May-2024)

Ref Expression
Hypotheses metakunt2.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt2.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt2.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt2.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝐼 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ) )
Assertion metakunt2 ( 𝜑 → 𝐴 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )

Proof

Step Hyp Ref Expression
1 metakunt2.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt2.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt2.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt2.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝐼 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ) )
5 eleq1 ⊢ ( 𝐼 = if ( 𝑥 = 𝑀 , 𝐼 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ) → ( 𝐼 ∈ ( 1 ... 𝑀 ) ↔ if ( 𝑥 = 𝑀 , 𝐼 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ) ∈ ( 1 ... 𝑀 ) ) )
6 eleq1 ⊢ ( if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) = if ( 𝑥 = 𝑀 , 𝐼 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ) → ( if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ∈ ( 1 ... 𝑀 ) ↔ if ( 𝑥 = 𝑀 , 𝐼 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ) ∈ ( 1 ... 𝑀 ) ) )
7 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑀 ) → 1 ∈ ℤ )
8 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
9 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑀 ) → 𝑀 ∈ ℤ )
10 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
11 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑀 ) → 𝐼 ∈ ℤ )
12 2 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐼 )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑀 ) → 1 ≤ 𝐼 )
14 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑀 ) → 𝐼 ≤ 𝑀 )
15 7 9 11 13 14 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑀 ) → 𝐼 ∈ ( 1 ... 𝑀 ) )
16 eleq1 ⊢ ( 𝑥 = if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) → ( 𝑥 ∈ ( 1 ... 𝑀 ) ↔ if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ∈ ( 1 ... 𝑀 ) ) )
17 eleq1 ⊢ ( ( 𝑥 + 1 ) = if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) → ( ( 𝑥 + 1 ) ∈ ( 1 ... 𝑀 ) ↔ if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ∈ ( 1 ... 𝑀 ) ) )
18 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ 𝑥 < 𝐼 ) → 𝑥 ∈ ( 1 ... 𝑀 ) )
19 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼 ) ) → 1 ∈ ℤ )
20 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼 ) ) → 𝑀 ∈ ℤ )
21 elfznn ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 𝑥 ∈ ℕ )
22 21 nnzd ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 𝑥 ∈ ℤ )
23 22 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼 ) ) → 𝑥 ∈ ℤ )
24 23 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼 ) ) → ( 𝑥 + 1 ) ∈ ℤ )
25 0p1e1 ⊢ ( 0 + 1 ) = 1
26 0red ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 0 ∈ ℝ )
27 21 nnred ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 𝑥 ∈ ℝ )
28 1red ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 1 ∈ ℝ )
29 21 nnnn0d ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 𝑥 ∈ ℕ0 )
30 29 nn0ge0d ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 0 ≤ 𝑥 )
31 26 27 28 30 leadd1dd ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → ( 0 + 1 ) ≤ ( 𝑥 + 1 ) )
32 25 31 eqbrtrrid ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 1 ≤ ( 𝑥 + 1 ) )
33 32 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼 ) ) → 1 ≤ ( 𝑥 + 1 ) )
34 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) → 𝑥 ∈ ( 1 ... 𝑀 ) )
35 neqne ⊢ ( ¬ 𝑥 = 𝑀 → 𝑥 ≠ 𝑀 )
36 35 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) → 𝑥 ≠ 𝑀 )
37 34 36 fzne2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) → 𝑥 < 𝑀 )
38 37 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼 ) ) → 𝑥 < 𝑀 )
39 22 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 𝑥 ∈ ℤ )
40 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 𝑀 ∈ ℤ )
41 39 40 zltp1led ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( 𝑥 < 𝑀 ↔ ( 𝑥 + 1 ) ≤ 𝑀 ) )
42 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼 ) ) → ( 𝑥 < 𝑀 ↔ ( 𝑥 + 1 ) ≤ 𝑀 ) )
43 38 42 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼 ) ) → ( 𝑥 + 1 ) ≤ 𝑀 )
44 19 20 24 33 43 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼 ) ) → ( 𝑥 + 1 ) ∈ ( 1 ... 𝑀 ) )
45 44 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) ∧ ¬ 𝑥 < 𝐼 ) → ( 𝑥 + 1 ) ∈ ( 1 ... 𝑀 ) )
46 16 17 18 45 ifbothda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝑀 ) → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ∈ ( 1 ... 𝑀 ) )
47 5 6 15 46 ifbothda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑥 = 𝑀 , 𝐼 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ) ∈ ( 1 ... 𝑀 ) )
48 47 4 fmptd ⊢ ( 𝜑 → 𝐴 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )