Metamath Proof Explorer

Theorem metakunt7

Description: C is the left inverse for A. (Contributed by metakunt, 24-May-2024)

Ref Expression
Hypotheses metakunt7.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt7.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt7.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt7.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
metakunt7.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
metakunt7.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
Assertion metakunt7 ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( ( 𝐴 ‘ 𝑋 ) = ( 𝑋 − 1 ) ∧ ¬ ( 𝐴 ‘ 𝑋 ) = 𝑀 ∧ ¬ ( 𝐴 ‘ 𝑋 ) < 𝐼 ) )

Proof

Step Hyp Ref Expression
1 metakunt7.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt7.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt7.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt7.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5 metakunt7.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
6 metakunt7.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
7 4 a1i ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) )
8 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝐼 ↔ 𝑋 = 𝐼 ) )
9 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 < 𝐼 ↔ 𝑋 < 𝐼 ) )
10 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
11 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 − 1 ) = ( 𝑋 − 1 ) )
12 9 10 11 ifbieq12d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) )
13 8 12 ifbieq2d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ 𝐼 < 𝑋 ) ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) )
15 2 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝐼 ∈ ℝ )
17 simpr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝐼 < 𝑋 )
18 16 17 ltned ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝐼 ≠ 𝑋 )
19 18 necomd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝑋 ≠ 𝐼 )
20 df-ne ⊢ ( 𝑋 ≠ 𝐼 ↔ ¬ 𝑋 = 𝐼 )
21 19 20 sylib ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ¬ 𝑋 = 𝐼 )
22 iffalse ⊢ ( ¬ 𝑋 = 𝐼 → if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) )
23 21 22 syl ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) )
24 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ∈ ℕ )
25 6 24 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
26 25 nnred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝑋 ∈ ℝ )
28 16 27 17 ltled ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝐼 ≤ 𝑋 )
29 16 27 lenltd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼 ) )
30 28 29 mpbid ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ¬ 𝑋 < 𝐼 )
31 iffalse ⊢ ( ¬ 𝑋 < 𝐼 → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) = ( 𝑋 − 1 ) )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) = ( 𝑋 − 1 ) )
33 23 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) = ( 𝑋 − 1 ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝐼 < 𝑋 ) ∧ 𝑥 = 𝑋 ) → if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) = ( 𝑋 − 1 ) )
35 14 34 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐼 < 𝑋 ) ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = ( 𝑋 − 1 ) )
36 6 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
37 36 elfzelzd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝑋 ∈ ℤ )
38 1zzd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 1 ∈ ℤ )
39 37 38 zsubcld ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝑋 − 1 ) ∈ ℤ )
40 7 35 36 39 fvmptd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 − 1 ) )
41 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
42 26 41 resubcld ⊢ ( 𝜑 → ( 𝑋 − 1 ) ∈ ℝ )
43 elfzle2 ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ≤ 𝑀 )
44 6 43 syl ⊢ ( 𝜑 → 𝑋 ≤ 𝑀 )
45 6 elfzelzd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
46 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
47 zlem1lt ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑋 ≤ 𝑀 ↔ ( 𝑋 − 1 ) < 𝑀 ) )
48 45 46 47 syl2anc ⊢ ( 𝜑 → ( 𝑋 ≤ 𝑀 ↔ ( 𝑋 − 1 ) < 𝑀 ) )
49 44 48 mpbid ⊢ ( 𝜑 → ( 𝑋 − 1 ) < 𝑀 )
50 42 49 ltned ⊢ ( 𝜑 → ( 𝑋 − 1 ) ≠ 𝑀 )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝑋 − 1 ) ≠ 𝑀 )
52 40 51 eqnetrd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝐴 ‘ 𝑋 ) ≠ 𝑀 )
53 52 neneqd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ¬ ( 𝐴 ‘ 𝑋 ) = 𝑀 )
54 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
55 zltlem1 ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝐼 < 𝑋 ↔ 𝐼 ≤ ( 𝑋 − 1 ) ) )
56 55 biimpd ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝐼 < 𝑋 → 𝐼 ≤ ( 𝑋 − 1 ) ) )
57 54 45 56 syl2anc ⊢ ( 𝜑 → ( 𝐼 < 𝑋 → 𝐼 ≤ ( 𝑋 − 1 ) ) )
58 57 imp ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝐼 ≤ ( 𝑋 − 1 ) )
59 58 40 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝐼 ≤ ( 𝐴 ‘ 𝑋 ) )
60 39 zred ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝑋 − 1 ) ∈ ℝ )
61 40 60 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝐴 ‘ 𝑋 ) ∈ ℝ )
62 16 61 lenltd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝐼 ≤ ( 𝐴 ‘ 𝑋 ) ↔ ¬ ( 𝐴 ‘ 𝑋 ) < 𝐼 ) )
63 59 62 mpbid ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ¬ ( 𝐴 ‘ 𝑋 ) < 𝐼 )
64 40 53 63 3jca ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( ( 𝐴 ‘ 𝑋 ) = ( 𝑋 − 1 ) ∧ ¬ ( 𝐴 ‘ 𝑋 ) = 𝑀 ∧ ¬ ( 𝐴 ‘ 𝑋 ) < 𝐼 ) )