Metamath Proof Explorer


Theorem metakunt30

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

Ref Expression
Hypotheses metakunt30.1 φ M
metakunt30.2 φ I
metakunt30.3 φ I M
metakunt30.4 φ X 1 M
metakunt30.5 A = x 1 M if x = I M if x < I x x 1
metakunt30.6 B = z 1 M if z = M M if z < I z + M - I z + 1 - I
metakunt30.7 φ ¬ X = I
metakunt30.8 φ ¬ X < I
metakunt30.9 C = y 1 M if y = M I if y < I y y + 1
metakunt30.10 H = if I X I 1 0
Assertion metakunt30 φ C B A X = X - I + H

Proof

Step Hyp Ref Expression
1 metakunt30.1 φ M
2 metakunt30.2 φ I
3 metakunt30.3 φ I M
4 metakunt30.4 φ X 1 M
5 metakunt30.5 A = x 1 M if x = I M if x < I x x 1
6 metakunt30.6 B = z 1 M if z = M M if z < I z + M - I z + 1 - I
7 metakunt30.7 φ ¬ X = I
8 metakunt30.8 φ ¬ X < I
9 metakunt30.9 C = y 1 M if y = M I if y < I y y + 1
10 metakunt30.10 H = if I X I 1 0
11 1 2 3 4 5 6 7 8 metakunt28 φ B A X = X I
12 11 fveq2d φ C B A X = C X I
13 9 a1i φ C = y 1 M if y = M I if y < I y y + 1
14 elfznn X 1 M X
15 4 14 syl φ X
16 nnre X X
17 15 16 syl φ X
18 2 nnred φ I
19 17 18 resubcld φ X I
20 1 nnred φ M
21 20 18 resubcld φ M I
22 elfzle2 X 1 M X M
23 4 22 syl φ X M
24 17 20 18 23 lesub1dd φ X I M I
25 2 nnrpd φ I +
26 20 25 ltsubrpd φ M I < M
27 19 21 20 24 26 lelttrd φ X I < M
28 19 27 ltned φ X I M
29 28 adantr φ y = X I X I M
30 neeq1 y = X I y M X I M
31 30 adantl φ y = X I y M X I M
32 29 31 mpbird φ y = X I y M
33 32 neneqd φ y = X I ¬ y = M
34 33 iffalsed φ y = X I if y = M I if y < I y y + 1 = if y < I y y + 1
35 18 19 lenltd φ I X I ¬ X I < I
36 35 biimpa φ I X I ¬ X I < I
37 36 3adant2 φ y = X I I X I ¬ X I < I
38 breq1 y = X I y < I X I < I
39 38 3ad2ant2 φ y = X I I X I y < I X I < I
40 37 39 mtbird φ y = X I I X I ¬ y < I
41 40 iffalsed φ y = X I I X I if y < I y y + 1 = y + 1
42 simp2 φ y = X I I X I y = X I
43 42 oveq1d φ y = X I I X I y + 1 = X - I + 1
44 simp3 φ y = X I I X I I X I
45 44 iftrued φ y = X I I X I if I X I 1 0 = 1
46 45 eqcomd φ y = X I I X I 1 = if I X I 1 0
47 10 a1i φ y = X I I X I H = if I X I 1 0
48 47 eqcomd φ y = X I I X I if I X I 1 0 = H
49 46 48 eqtrd φ y = X I I X I 1 = H
50 49 oveq2d φ y = X I I X I X - I + 1 = X - I + H
51 43 50 eqtrd φ y = X I I X I y + 1 = X - I + H
52 41 51 eqtrd φ y = X I I X I if y < I y y + 1 = X - I + H
53 52 3expa φ y = X I I X I if y < I y y + 1 = X - I + H
54 simpr φ ¬ I X I ¬ I X I
55 19 adantr φ ¬ I X I X I
56 18 adantr φ ¬ I X I I
57 55 56 ltnled φ ¬ I X I X I < I ¬ I X I
58 54 57 mpbird φ ¬ I X I X I < I
59 58 3adant2 φ y = X I ¬ I X I X I < I
60 38 3ad2ant2 φ y = X I ¬ I X I y < I X I < I
61 59 60 mpbird φ y = X I ¬ I X I y < I
62 61 iftrued φ y = X I ¬ I X I if y < I y y + 1 = y
63 simp2 φ y = X I ¬ I X I y = X I
64 nncn X X
65 15 64 syl φ X
66 65 3ad2ant1 φ y = X I ¬ I X I X
67 2 nncnd φ I
68 67 3ad2ant1 φ y = X I ¬ I X I I
69 66 68 subcld φ y = X I ¬ I X I X I
70 69 addid1d φ y = X I ¬ I X I X - I + 0 = X I
71 70 eqcomd φ y = X I ¬ I X I X I = X - I + 0
72 10 a1i φ y = X I ¬ I X I H = if I X I 1 0
73 simp3 φ y = X I ¬ I X I ¬ I X I
74 73 iffalsed φ y = X I ¬ I X I if I X I 1 0 = 0
75 72 74 eqtrd φ y = X I ¬ I X I H = 0
76 75 eqcomd φ y = X I ¬ I X I 0 = H
77 76 oveq2d φ y = X I ¬ I X I X - I + 0 = X - I + H
78 71 77 eqtrd φ y = X I ¬ I X I X I = X - I + H
79 63 78 eqtrd φ y = X I ¬ I X I y = X - I + H
80 62 79 eqtrd φ y = X I ¬ I X I if y < I y y + 1 = X - I + H
81 80 3expa φ y = X I ¬ I X I if y < I y y + 1 = X - I + H
82 53 81 pm2.61dan φ y = X I if y < I y y + 1 = X - I + H
83 34 82 eqtrd φ y = X I if y = M I if y < I y y + 1 = X - I + H
84 1zzd φ 1
85 1 nnzd φ M
86 15 nnzd φ X
87 2 nnzd φ I
88 86 87 zsubcld φ X I
89 1m1e0 1 1 = 0
90 18 17 8 nltled φ I X
91 7 neqned φ X I
92 90 91 jca φ I X X I
93 18 17 ltlend φ I < X I X X I
94 92 93 mpbird φ I < X
95 18 17 posdifd φ I < X 0 < X I
96 94 95 mpbid φ 0 < X I
97 89 96 eqbrtrid φ 1 1 < X I
98 zlem1lt 1 X I 1 X I 1 1 < X I
99 84 88 98 syl2anc φ 1 X I 1 1 < X I
100 97 99 mpbird φ 1 X I
101 19 20 27 ltled φ X I M
102 84 85 88 100 101 elfzd φ X I 1 M
103 0zd φ 0
104 84 103 ifcld φ if I X I 1 0
105 10 a1i φ H = if I X I 1 0
106 105 eleq1d φ H if I X I 1 0
107 104 106 mpbird φ H
108 88 107 zaddcld φ X - I + H
109 13 83 102 108 fvmptd φ C X I = X - I + H
110 12 109 eqtrd φ C B A X = X - I + H