Metamath Proof Explorer

Theorem metakunt28

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024)

Ref Expression
Hypotheses metakunt28.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt28.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt28.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt28.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
metakunt28.5 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
metakunt28.6 ⊢ 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) )
metakunt28.7 ⊢ ( 𝜑 → ¬ 𝑋 = 𝐼 )
metakunt28.8 ⊢ ( 𝜑 → ¬ 𝑋 < 𝐼 )
Assertion metakunt28 ( 𝜑 → ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑋 − 𝐼 ) )

Proof

Step Hyp Ref Expression
1 metakunt28.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt28.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt28.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt28.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
5 metakunt28.5 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
6 metakunt28.6 ⊢ 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) )
7 metakunt28.7 ⊢ ( 𝜑 → ¬ 𝑋 = 𝐼 )
8 metakunt28.8 ⊢ ( 𝜑 → ¬ 𝑋 < 𝐼 )
9 5 a1i ⊢ ( 𝜑 → 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) )
10 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ¬ 𝑋 = 𝐼 )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
12 11 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 = 𝐼 ↔ 𝑋 = 𝐼 ) )
13 12 notbid ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ¬ 𝑥 = 𝐼 ↔ ¬ 𝑋 = 𝐼 ) )
14 10 13 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ¬ 𝑥 = 𝐼 )
15 14 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ¬ 𝑋 < 𝐼 )
17 11 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 < 𝐼 ↔ 𝑋 < 𝐼 ) )
18 17 notbid ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ¬ 𝑥 < 𝐼 ↔ ¬ 𝑋 < 𝐼 ) )
19 16 18 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ¬ 𝑥 < 𝐼 )
20 19 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = ( 𝑥 − 1 ) )
21 11 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 − 1 ) = ( 𝑋 − 1 ) )
22 20 21 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = ( 𝑋 − 1 ) )
23 15 22 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = ( 𝑋 − 1 ) )
24 4 elfzelzd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
25 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
26 24 25 zsubcld ⊢ ( 𝜑 → ( 𝑋 − 1 ) ∈ ℤ )
27 9 23 4 26 fvmptd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 − 1 ) )
28 27 fveq2d ⊢ ( 𝜑 → ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 ‘ ( 𝑋 − 1 ) ) )
29 6 a1i ⊢ ( 𝜑 → 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) ) )
30 26 zred ⊢ ( 𝜑 → ( 𝑋 − 1 ) ∈ ℝ )
31 24 zred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
32 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
33 1rp ⊢ 1 ∈ ℝ+
34 33 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
35 31 34 ltsubrpd ⊢ ( 𝜑 → ( 𝑋 − 1 ) < 𝑋 )
36 elfzle2 ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ≤ 𝑀 )
37 4 36 syl ⊢ ( 𝜑 → 𝑋 ≤ 𝑀 )
38 30 31 32 35 37 ltletrd ⊢ ( 𝜑 → ( 𝑋 − 1 ) < 𝑀 )
39 30 38 ltned ⊢ ( 𝜑 → ( 𝑋 − 1 ) ≠ 𝑀 )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( 𝑋 − 1 ) ≠ 𝑀 )
41 40 neneqd ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ¬ ( 𝑋 − 1 ) = 𝑀 )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → 𝑧 = ( 𝑋 − 1 ) )
43 42 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( 𝑧 = 𝑀 ↔ ( 𝑋 − 1 ) = 𝑀 ) )
44 43 notbid ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( ¬ 𝑧 = 𝑀 ↔ ¬ ( 𝑋 − 1 ) = 𝑀 ) )
45 41 44 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ¬ 𝑧 = 𝑀 )
46 45 iffalsed ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) = if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) )
47 7 neqned ⊢ ( 𝜑 → 𝑋 ≠ 𝐼 )
48 2 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
49 48 31 8 nltled ⊢ ( 𝜑 → 𝐼 ≤ 𝑋 )
50 48 31 49 leltned ⊢ ( 𝜑 → ( 𝐼 < 𝑋 ↔ 𝑋 ≠ 𝐼 ) )
51 47 50 mpbird ⊢ ( 𝜑 → 𝐼 < 𝑋 )
52 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
53 52 24 zltlem1d ⊢ ( 𝜑 → ( 𝐼 < 𝑋 ↔ 𝐼 ≤ ( 𝑋 − 1 ) ) )
54 51 53 mpbid ⊢ ( 𝜑 → 𝐼 ≤ ( 𝑋 − 1 ) )
55 48 30 lenltd ⊢ ( 𝜑 → ( 𝐼 ≤ ( 𝑋 − 1 ) ↔ ¬ ( 𝑋 − 1 ) < 𝐼 ) )
56 54 55 mpbid ⊢ ( 𝜑 → ¬ ( 𝑋 − 1 ) < 𝐼 )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ¬ ( 𝑋 − 1 ) < 𝐼 )
58 42 breq1d ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( 𝑧 < 𝐼 ↔ ( 𝑋 − 1 ) < 𝐼 ) )
59 58 notbid ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( ¬ 𝑧 < 𝐼 ↔ ¬ ( 𝑋 − 1 ) < 𝐼 ) )
60 57 59 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ¬ 𝑧 < 𝐼 )
61 60 iffalsed ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) = ( 𝑧 + ( 1 − 𝐼 ) ) )
62 42 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( 𝑧 + ( 1 − 𝐼 ) ) = ( ( 𝑋 − 1 ) + ( 1 − 𝐼 ) ) )
63 24 zcnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
64 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
65 2 nncnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
66 63 64 65 npncand ⊢ ( 𝜑 → ( ( 𝑋 − 1 ) + ( 1 − 𝐼 ) ) = ( 𝑋 − 𝐼 ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( ( 𝑋 − 1 ) + ( 1 − 𝐼 ) ) = ( 𝑋 − 𝐼 ) )
68 62 67 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( 𝑧 + ( 1 − 𝐼 ) ) = ( 𝑋 − 𝐼 ) )
69 61 68 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) = ( 𝑋 − 𝐼 ) )
70 46 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) = ( 𝑋 − 𝐼 ) )
71 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
72 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
73 2 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐼 )
74 72 48 31 73 51 lelttrd ⊢ ( 𝜑 → 1 < 𝑋 )
75 25 24 zltlem1d ⊢ ( 𝜑 → ( 1 < 𝑋 ↔ 1 ≤ ( 𝑋 − 1 ) ) )
76 74 75 mpbid ⊢ ( 𝜑 → 1 ≤ ( 𝑋 − 1 ) )
77 31 72 resubcld ⊢ ( 𝜑 → ( 𝑋 − 1 ) ∈ ℝ )
78 0le1 ⊢ 0 ≤ 1
79 78 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
80 31 72 subge02d ⊢ ( 𝜑 → ( 0 ≤ 1 ↔ ( 𝑋 − 1 ) ≤ 𝑋 ) )
81 79 80 mpbid ⊢ ( 𝜑 → ( 𝑋 − 1 ) ≤ 𝑋 )
82 77 31 32 81 37 letrd ⊢ ( 𝜑 → ( 𝑋 − 1 ) ≤ 𝑀 )
83 25 71 26 76 82 elfzd ⊢ ( 𝜑 → ( 𝑋 − 1 ) ∈ ( 1 ... 𝑀 ) )
84 24 52 zsubcld ⊢ ( 𝜑 → ( 𝑋 − 𝐼 ) ∈ ℤ )
85 29 70 83 84 fvmptd ⊢ ( 𝜑 → ( 𝐵 ‘ ( 𝑋 − 1 ) ) = ( 𝑋 − 𝐼 ) )
86 28 85 eqtrd ⊢ ( 𝜑 → ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑋 − 𝐼 ) )