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⟼ifx=IMifx<Ixx−1
metakunt31.6 ⊢B=z∈1…M⟼ifz=MMifz<Iz+M-Iz+1-I
metakunt31.7 ⊢C=y∈1…M⟼ify=MIify<Iyy+1
metakunt31.8 ⊢G=ifI≤X+M-I10
metakunt31.9 ⊢H=ifI≤X−I10
metakunt31.10 ⊢R=ifX=IXifX<IX+M−I+GX-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⟼ifx=IMifx<Ixx−1
6 metakunt31.6 ⊢B=z∈1…M⟼ifz=MMifz<Iz+M-Iz+1-I
7 metakunt31.7 ⊢C=y∈1…M⟼ify=MIify<Iyy+1
8 metakunt31.8 ⊢G=ifI≤X+M-I10
9 metakunt31.9 ⊢H=ifI≤X−I10
10 metakunt31.10 ⊢R=ifX=IXifX<IX+M−I+GX-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→ifX=IXifX<IX+M−I+GX-I+H=X
17 16 eqcomd ⊢φ∧X=I→X=ifX=IXifX<IX+M−I+GX-I+H
18 15 17 eqtrd ⊢φ∧X=I→C⁡B⁡A⁡X=ifX=IXifX<IX+M−I+GX-I+H
19 10 eqcomi ⊢ifX=IXifX<IX+M−I+GX-I+H=R
20 19 a1i ⊢φ∧X=I→ifX=IXifX<IX+M−I+GX-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→ifX=IXifX<IX+M−I+GX-I+H=ifX<IX+M−I+GX-I+H
30 27 iftrued ⊢φ∧¬X=I∧X<I→ifX<IX+M−I+GX-I+H=X+M−I+G
31 29 30 eqtrd ⊢φ∧¬X=I∧X<I→ifX=IXifX<IX+M−I+GX-I+H=X+M−I+G
32 31 eqcomd ⊢φ∧¬X=I∧X<I→X+M−I+G=ifX=IXifX<IX+M−I+GX-I+H
33 28 32 eqtrd ⊢φ∧¬X=I∧X<I→C⁡B⁡A⁡X=ifX=IXifX<IX+M−I+GX-I+H
34 19 a1i ⊢φ∧¬X=I∧X<I→ifX=IXifX<IX+M−I+GX-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→ifX=IXifX<IX+M−I+GX-I+H=ifX<IX+M−I+GX-I+H
45 42 iffalsed ⊢φ∧¬X=I∧¬X<I→ifX<IX+M−I+GX-I+H=X-I+H
46 44 45 eqtrd ⊢φ∧¬X=I∧¬X<I→ifX=IXifX<IX+M−I+GX-I+H=X-I+H
47 46 eqcomd ⊢φ∧¬X=I∧¬X<I→X-I+H=ifX=IXifX<IX+M−I+GX-I+H
48 43 47 eqtrd ⊢φ∧¬X=I∧¬X<I→C⁡B⁡A⁡X=ifX=IXifX<IX+M−I+GX-I+H
49 19 a1i ⊢φ∧¬X=I∧¬X<I→ifX=IXifX<IX+M−I+GX-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