Metamath Proof Explorer

Theorem metakunt16

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

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

Proof

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