Metamath Proof Explorer

Theorem metakunt31

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

Ref Expression
Hypotheses metakunt31.1 ⊢ φ → M ∈ ℕ
metakunt31.2 ⊢ φ → I ∈ ℕ
metakunt31.3 ⊢ φ → I ≤ M
metakunt31.4 ⊢ φ → X ∈ 1 … M
metakunt31.5 ⊢ A = x ∈ 1 … M ⟼ if x = I M if x < I x x − 1
metakunt31.6 ⊢ B = z ∈ 1 … M ⟼ if z = M M if z < I z + M - I z + 1 - I
metakunt31.7 ⊢ C = y ∈ 1 … M ⟼ if y = M I if y < I y y + 1
metakunt31.8 ⊢ G = if I ≤ X + M - I 1 0
metakunt31.9 ⊢ H = if I ≤ X − I 1 0
metakunt31.10 ⊢ R = if X = I X if X < I X + M − I + G X - I + H
Assertion metakunt31 ⊢ φ → C ⁡ B ⁡ A ⁡ X = R

Proof

Step Hyp Ref Expression
1 metakunt31.1 ⊢ φ → M ∈ ℕ
2 metakunt31.2 ⊢ φ → I ∈ ℕ
3 metakunt31.3 ⊢ φ → I ≤ M
4 metakunt31.4 ⊢ φ → X ∈ 1 … M
5 metakunt31.5 ⊢ A = x ∈ 1 … M ⟼ if x = I M if x < I x x − 1
6 metakunt31.6 ⊢ B = z ∈ 1 … M ⟼ if z = M M if z < I z + M - I z + 1 - I
7 metakunt31.7 ⊢ C = y ∈ 1 … M ⟼ if y = M I if y < I y y + 1
8 metakunt31.8 ⊢ G = if I ≤ X + M - I 1 0
9 metakunt31.9 ⊢ H = if I ≤ X − I 1 0
10 metakunt31.10 ⊢ R = if X = I X if X < I X + M − I + G X - I + H
11 1 adantr ⊢ φ ∧ X = I → M ∈ ℕ
12 2 adantr ⊢ φ ∧ X = I → I ∈ ℕ
13 3 adantr ⊢ φ ∧ X = I → I ≤ M
14 simpr ⊢ φ ∧ X = I → X = I
15 11 12 13 5 7 6 14 metakunt26 ⊢ φ ∧ X = I → C ⁡ B ⁡ A ⁡ X = X
16 14 iftrued ⊢ φ ∧ X = I → if X = I X if X < I X + M − I + G X - I + H = X
17 16 eqcomd ⊢ φ ∧ X = I → X = if X = I X if X < I X + M − I + G X - I + H
18 15 17 eqtrd ⊢ φ ∧ X = I → C ⁡ B ⁡ A ⁡ X = if X = I X if X < I X + M − I + G X - I + H
19 10 eqcomi ⊢ if X = I X if X < I X + M − I + G X - I + H = R
20 19 a1i ⊢ φ ∧ X = I → if X = I X if X < I X + M − I + G X - I + H = R
21 18 20 eqtrd ⊢ φ ∧ X = I → C ⁡ B ⁡ A ⁡ X = R
22 1 3ad2ant1 ⊢ φ ∧ ¬ X = I ∧ X < I → M ∈ ℕ
23 2 3ad2ant1 ⊢ φ ∧ ¬ X = I ∧ X < I → I ∈ ℕ
24 3 3ad2ant1 ⊢ φ ∧ ¬ X = I ∧ X < I → I ≤ M
25 4 3ad2ant1 ⊢ φ ∧ ¬ X = I ∧ X < I → X ∈ 1 … M
26 simp2 ⊢ φ ∧ ¬ X = I ∧ X < I → ¬ X = I
27 simp3 ⊢ φ ∧ ¬ X = I ∧ X < I → X < I
28 22 23 24 25 5 6 26 27 7 8 metakunt29 ⊢ φ ∧ ¬ X = I ∧ X < I → C ⁡ B ⁡ A ⁡ X = X + M − I + G
29 26 iffalsed ⊢ φ ∧ ¬ X = I ∧ X < I → if X = I X if X < I X + M − I + G X - I + H = if X < I X + M − I + G X - I + H
30 27 iftrued ⊢ φ ∧ ¬ X = I ∧ X < I → if X < I X + M − I + G X - I + H = X + M − I + G
31 29 30 eqtrd ⊢ φ ∧ ¬ X = I ∧ X < I → if X = I X if X < I X + M − I + G X - I + H = X + M − I + G
32 31 eqcomd ⊢ φ ∧ ¬ X = I ∧ X < I → X + M − I + G = if X = I X if X < I X + M − I + G X - I + H
33 28 32 eqtrd ⊢ φ ∧ ¬ X = I ∧ X < I → C ⁡ B ⁡ A ⁡ X = if X = I X if X < I X + M − I + G X - I + H
34 19 a1i ⊢ φ ∧ ¬ X = I ∧ X < I → if X = I X if X < I X + M − I + G X - I + H = R
35 33 34 eqtrd ⊢ φ ∧ ¬ X = I ∧ X < I → C ⁡ B ⁡ A ⁡ X = R
36 35 3expa ⊢ φ ∧ ¬ X = I ∧ X < I → C ⁡ B ⁡ A ⁡ X = R
37 1 3ad2ant1 ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → M ∈ ℕ
38 2 3ad2ant1 ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → I ∈ ℕ
39 3 3ad2ant1 ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → I ≤ M
40 4 3ad2ant1 ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → X ∈ 1 … M
41 simp2 ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → ¬ X = I
42 simp3 ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → ¬ X < I
43 37 38 39 40 5 6 41 42 7 9 metakunt30 ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → C ⁡ B ⁡ A ⁡ X = X - I + H
44 41 iffalsed ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → if X = I X if X < I X + M − I + G X - I + H = if X < I X + M − I + G X - I + H
45 42 iffalsed ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → if X < I X + M − I + G X - I + H = X - I + H
46 44 45 eqtrd ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → if X = I X if X < I X + M − I + G X - I + H = X - I + H
47 46 eqcomd ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → X - I + H = if X = I X if X < I X + M − I + G X - I + H
48 43 47 eqtrd ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → C ⁡ B ⁡ A ⁡ X = if X = I X if X < I X + M − I + G X - I + H
49 19 a1i ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → if X = I X if X < I X + M − I + G X - I + H = R
50 48 49 eqtrd ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → C ⁡ B ⁡ A ⁡ X = R
51 50 3expa ⊢ φ ∧ ¬ X = I ∧ ¬ X < I → C ⁡ B ⁡ A ⁡ X = R
52 36 51 pm2.61dan ⊢ φ ∧ ¬ X = I → C ⁡ B ⁡ A ⁡ X = R
53 21 52 pm2.61dan ⊢ φ → C ⁡ B ⁡ A ⁡ X = R