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 ( 𝜑 → ( 𝐵 ‘ ( 𝐴𝑋 ) ) = ( 𝑋𝐼 ) )