Metamath Proof Explorer

Theorem metakunt15

Description: Construction of another permutation. (Contributed by metakunt, 25-May-2024)

Ref Expression
Hypotheses metakunt15.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt15.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt15.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt15.4 ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
Assertion metakunt15 ( 𝜑 → 𝐹 : ( 1 ... ( 𝐼 − 1 ) ) –1-1-onto→ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 metakunt15.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt15.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt15.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt15.4 ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
5 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → 1 ∈ ℤ )
6 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → 𝐼 ∈ ℤ )
8 7 5 zsubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → ( 𝐼 − 1 ) ∈ ℤ )
9 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → 𝑀 ∈ ℤ )
11 10 7 zsubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → ( 𝑀 − 𝐼 ) ∈ ℤ )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) )
13 elfz3 ⊢ ( ( 𝑀 − 𝐼 ) ∈ ℤ → ( 𝑀 − 𝐼 ) ∈ ( ( 𝑀 − 𝐼 ) ... ( 𝑀 − 𝐼 ) ) )
14 11 13 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → ( 𝑀 − 𝐼 ) ∈ ( ( 𝑀 − 𝐼 ) ... ( 𝑀 − 𝐼 ) ) )
15 11 zcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → ( 𝑀 − 𝐼 ) ∈ ℂ )
16 1cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → 1 ∈ ℂ )
17 15 16 addcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → ( ( 𝑀 − 𝐼 ) + 1 ) = ( 1 + ( 𝑀 − 𝐼 ) ) )
18 1 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
19 2 nncnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
20 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
21 18 19 20 npncand ⊢ ( 𝜑 → ( ( 𝑀 − 𝐼 ) + ( 𝐼 − 1 ) ) = ( 𝑀 − 1 ) )
22 21 eqcomd ⊢ ( 𝜑 → ( 𝑀 − 1 ) = ( ( 𝑀 − 𝐼 ) + ( 𝐼 − 1 ) ) )
23 18 19 subcld ⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) ∈ ℂ )
24 19 20 subcld ⊢ ( 𝜑 → ( 𝐼 − 1 ) ∈ ℂ )
25 23 24 addcomd ⊢ ( 𝜑 → ( ( 𝑀 − 𝐼 ) + ( 𝐼 − 1 ) ) = ( ( 𝐼 − 1 ) + ( 𝑀 − 𝐼 ) ) )
26 22 25 eqtrd ⊢ ( 𝜑 → ( 𝑀 − 1 ) = ( ( 𝐼 − 1 ) + ( 𝑀 − 𝐼 ) ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → ( 𝑀 − 1 ) = ( ( 𝐼 − 1 ) + ( 𝑀 − 𝐼 ) ) )
28 5 8 11 11 12 14 17 27 fzadd2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → ( 𝑥 + ( 𝑀 − 𝐼 ) ) ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) )
29 1zzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → 1 ∈ ℤ )
30 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → 𝐼 ∈ ℤ )
31 30 29 zsubcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( 𝐼 − 1 ) ∈ ℤ )
32 elfzelz ⊢ ( 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) → 𝑦 ∈ ℤ )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → 𝑦 ∈ ℤ )
34 9 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → 𝑀 ∈ ℤ )
35 34 30 zsubcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( 𝑀 − 𝐼 ) ∈ ℤ )
36 33 35 zsubcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( 𝑦 − ( 𝑀 − 𝐼 ) ) ∈ ℤ )
37 elfzle1 ⊢ ( 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) → ( ( 𝑀 − 𝐼 ) + 1 ) ≤ 𝑦 )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( ( 𝑀 − 𝐼 ) + 1 ) ≤ 𝑦 )
39 35 zred ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( 𝑀 − 𝐼 ) ∈ ℝ )
40 1red ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → 1 ∈ ℝ )
41 33 zred ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → 𝑦 ∈ ℝ )
42 39 40 41 leaddsub2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( ( ( 𝑀 − 𝐼 ) + 1 ) ≤ 𝑦 ↔ 1 ≤ ( 𝑦 − ( 𝑀 − 𝐼 ) ) ) )
43 38 42 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → 1 ≤ ( 𝑦 − ( 𝑀 − 𝐼 ) ) )
44 elfzle2 ⊢ ( 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) → 𝑦 ≤ ( 𝑀 − 1 ) )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → 𝑦 ≤ ( 𝑀 − 1 ) )
46 21 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( ( 𝑀 − 𝐼 ) + ( 𝐼 − 1 ) ) = ( 𝑀 − 1 ) )
47 45 46 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → 𝑦 ≤ ( ( 𝑀 − 𝐼 ) + ( 𝐼 − 1 ) ) )
48 31 zred ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( 𝐼 − 1 ) ∈ ℝ )
49 41 39 48 lesubadd2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( ( 𝑦 − ( 𝑀 − 𝐼 ) ) ≤ ( 𝐼 − 1 ) ↔ 𝑦 ≤ ( ( 𝑀 − 𝐼 ) + ( 𝐼 − 1 ) ) ) )
50 47 49 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( 𝑦 − ( 𝑀 − 𝐼 ) ) ≤ ( 𝐼 − 1 ) )
51 29 31 36 43 50 elfzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) → ( 𝑦 − ( 𝑀 − 𝐼 ) ) ∈ ( 1 ... ( 𝐼 − 1 ) ) )
52 eqcom ⊢ ( ( 𝑦 − ( 𝑀 − 𝐼 ) ) = 𝑥 ↔ 𝑥 = ( 𝑦 − ( 𝑀 − 𝐼 ) ) )
53 52 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → ( ( 𝑦 − ( 𝑀 − 𝐼 ) ) = 𝑥 ↔ 𝑥 = ( 𝑦 − ( 𝑀 − 𝐼 ) ) ) )
54 32 zcnd ⊢ ( 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) → 𝑦 ∈ ℂ )
55 54 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → 𝑦 ∈ ℂ )
56 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → 𝑀 ∈ ℂ )
57 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → 𝐼 ∈ ℂ )
58 56 57 subcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → ( 𝑀 − 𝐼 ) ∈ ℂ )
59 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) → 𝑥 ∈ ℕ )
60 59 nncnd ⊢ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) → 𝑥 ∈ ℂ )
61 60 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → 𝑥 ∈ ℂ )
62 55 58 61 subaddd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → ( ( 𝑦 − ( 𝑀 − 𝐼 ) ) = 𝑥 ↔ ( ( 𝑀 − 𝐼 ) + 𝑥 ) = 𝑦 ) )
63 53 62 bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → ( 𝑥 = ( 𝑦 − ( 𝑀 − 𝐼 ) ) ↔ ( ( 𝑀 − 𝐼 ) + 𝑥 ) = 𝑦 ) )
64 58 61 addcomd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → ( ( 𝑀 − 𝐼 ) + 𝑥 ) = ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
65 64 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → ( ( ( 𝑀 − 𝐼 ) + 𝑥 ) = 𝑦 ↔ ( 𝑥 + ( 𝑀 − 𝐼 ) ) = 𝑦 ) )
66 eqcom ⊢ ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) = 𝑦 ↔ 𝑦 = ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
67 66 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) = 𝑦 ↔ 𝑦 = ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) )
68 65 67 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → ( ( ( 𝑀 − 𝐼 ) + 𝑥 ) = 𝑦 ↔ 𝑦 = ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) )
69 63 68 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝑦 ∈ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ) → ( 𝑥 = ( 𝑦 − ( 𝑀 − 𝐼 ) ) ↔ 𝑦 = ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) )
70 4 28 51 69 f1o2d ⊢ ( 𝜑 → 𝐹 : ( 1 ... ( 𝐼 − 1 ) ) –1-1-onto→ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) )