Metamath Proof Explorer


Theorem metakunt27

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

Ref Expression
Hypotheses metakunt27.1 φ M
metakunt27.2 φ I
metakunt27.3 φ I M
metakunt27.4 φ X 1 M
metakunt27.5 A = x 1 M if x = I M if x < I x x 1
metakunt27.6 B = z 1 M if z = M M if z < I z + M - I z + 1 - I
metakunt27.7 φ ¬ X = I
metakunt27.8 φ X < I
Assertion metakunt27 φ B A X = X + M - I

Proof

Step Hyp Ref Expression
1 metakunt27.1 φ M
2 metakunt27.2 φ I
3 metakunt27.3 φ I M
4 metakunt27.4 φ X 1 M
5 metakunt27.5 A = x 1 M if x = I M if x < I x x 1
6 metakunt27.6 B = z 1 M if z = M M if z < I z + M - I z + 1 - I
7 metakunt27.7 φ ¬ X = I
8 metakunt27.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 16 17 mpbird φ x = X x < I
19 18 iftrued φ x = X if x < I x x 1 = x
20 19 11 eqtrd φ x = X if x < I x x 1 = X
21 15 20 eqtrd φ x = X if x = I M if x < I x x 1 = X
22 9 21 4 4 fvmptd φ A X = X
23 22 fveq2d φ B A X = B X
24 6 a1i φ B = z 1 M if z = M M if z < I z + M - I z + 1 - I
25 elfznn X 1 M X
26 4 25 syl φ X
27 26 nnred φ X
28 2 nnred φ I
29 1 nnred φ M
30 27 28 29 8 3 ltletrd φ X < M
31 27 30 ltned φ X M
32 31 neneqd φ ¬ X = M
33 32 adantr φ z = X ¬ X = M
34 simpr φ z = X z = X
35 34 eqeq1d φ z = X z = M X = M
36 35 notbid φ z = X ¬ z = M ¬ X = M
37 33 36 mpbird φ z = X ¬ z = M
38 37 iffalsed φ z = X if z = M M if z < I z + M - I z + 1 - I = if z < I z + M - I z + 1 - I
39 8 adantr φ z = X X < I
40 34 breq1d φ z = X z < I X < I
41 39 40 mpbird φ z = X z < I
42 41 iftrued φ z = X if z < I z + M - I z + 1 - I = z + M - I
43 34 oveq1d φ z = X z + M - I = X + M - I
44 42 43 eqtrd φ z = X if z < I z + M - I z + 1 - I = X + M - I
45 38 44 eqtrd φ z = X if z = M M if z < I z + M - I z + 1 - I = X + M - I
46 4 elfzelzd φ X
47 1 nnzd φ M
48 2 nnzd φ I
49 47 48 zsubcld φ M I
50 46 49 zaddcld φ X + M - I
51 24 45 4 50 fvmptd φ B X = X + M - I
52 23 51 eqtrd φ B A X = X + M - I