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 φ M
metakunt28.2 φ I
metakunt28.3 φ I M
metakunt28.4 φ X 1 M
metakunt28.5 A = x 1 M if x = I M if x < I x x 1
metakunt28.6 B = z 1 M if z = M M if z < I z + M - I z + 1 - I
metakunt28.7 φ ¬ X = I
metakunt28.8 φ ¬ X < I
Assertion metakunt28 φ B A X = X I

Proof

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