Metamath Proof Explorer


Theorem metakunt32

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

Ref Expression
Hypotheses metakunt32.1 φ M
metakunt32.2 φ I
metakunt32.3 φ I M
metakunt32.4 φ X 1 M
metakunt32.5 D = x 1 M if x = I x if x < I x + M I + if I x + M - I 1 0 x - I + if I x I 1 0
metakunt32.6 G = if I X + M - I 1 0
metakunt32.7 H = if I X I 1 0
metakunt32.8 R = if X = I X if X < I X + M I + G X - I + H
Assertion metakunt32 φ D X = R

Proof

Step Hyp Ref Expression
1 metakunt32.1 φ M
2 metakunt32.2 φ I
3 metakunt32.3 φ I M
4 metakunt32.4 φ X 1 M
5 metakunt32.5 D = x 1 M if x = I x if x < I x + M I + if I x + M - I 1 0 x - I + if I x I 1 0
6 metakunt32.6 G = if I X + M - I 1 0
7 metakunt32.7 H = if I X I 1 0
8 metakunt32.8 R = if X = I X if X < I X + M I + G X - I + H
9 5 a1i φ D = x 1 M if x = I x if x < I x + M I + if I x + M - I 1 0 x - I + if I x I 1 0
10 simpr φ x = X x = X
11 10 eqeq1d φ x = X x = I X = I
12 10 breq1d φ x = X x < I X < I
13 oveq1 x = X x + M - I = X + M - I
14 13 adantl φ x = X x + M - I = X + M - I
15 14 breq2d φ x = X I x + M - I I X + M - I
16 15 ifbid φ x = X if I x + M - I 1 0 = if I X + M - I 1 0
17 14 16 oveq12d φ x = X x + M I + if I x + M - I 1 0 = X + M I + if I X + M - I 1 0
18 6 a1i φ x = X G = if I X + M - I 1 0
19 18 eqcomd φ x = X if I X + M - I 1 0 = G
20 19 oveq2d φ x = X X + M I + if I X + M - I 1 0 = X + M I + G
21 17 20 eqtrd φ x = X x + M I + if I x + M - I 1 0 = X + M I + G
22 10 oveq1d φ x = X x I = X I
23 22 breq2d φ x = X I x I I X I
24 23 ifbid φ x = X if I x I 1 0 = if I X I 1 0
25 22 24 oveq12d φ x = X x - I + if I x I 1 0 = X - I + if I X I 1 0
26 7 a1i φ x = X H = if I X I 1 0
27 26 eqcomd φ x = X if I X I 1 0 = H
28 27 oveq2d φ x = X X - I + if I X I 1 0 = X - I + H
29 25 28 eqtrd φ x = X x - I + if I x I 1 0 = X - I + H
30 12 21 29 ifbieq12d φ x = X if x < I x + M I + if I x + M - I 1 0 x - I + if I x I 1 0 = if X < I X + M I + G X - I + H
31 11 10 30 ifbieq12d φ x = X if x = I x if x < I x + M I + if I x + M - I 1 0 x - I + if I x I 1 0 = if X = I X if X < I X + M I + G X - I + H
32 8 a1i φ x = X R = if X = I X if X < I X + M I + G X - I + H
33 32 eqcomd φ x = X if X = I X if X < I X + M I + G X - I + H = R
34 31 33 eqtrd φ x = X if x = I x if x < I x + M I + if I x + M - I 1 0 x - I + if I x I 1 0 = R
35 4 elfzelzd φ X
36 1 nnzd φ M
37 2 nnzd φ I
38 36 37 zsubcld φ M I
39 35 38 zaddcld φ X + M - I
40 1zzd φ 1
41 0zd φ 0
42 40 41 ifcld φ if I X + M - I 1 0
43 6 a1i φ G = if I X + M - I 1 0
44 43 eleq1d φ G if I X + M - I 1 0
45 42 44 mpbird φ G
46 39 45 zaddcld φ X + M I + G
47 35 37 zsubcld φ X I
48 40 41 ifcld φ if I X I 1 0
49 7 a1i φ H = if I X I 1 0
50 49 eleq1d φ H if I X I 1 0
51 48 50 mpbird φ H
52 47 51 zaddcld φ X - I + H
53 46 52 ifcld φ if X < I X + M I + G X - I + H
54 35 53 ifcld φ if X = I X if X < I X + M I + G X - I + H
55 8 a1i φ R = if X = I X if X < I X + M I + G X - I + H
56 55 eleq1d φ R if X = I X if X < I X + M I + G X - I + H
57 54 56 mpbird φ R
58 9 34 4 57 fvmptd φ D X = R