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 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt31.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt31.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt31.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
metakunt31.5 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
metakunt31.6 ⊢ 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) )
metakunt31.7 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
metakunt31.8 ⊢ 𝐺 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 )
metakunt31.9 ⊢ 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 )
metakunt31.10 ⊢ 𝑅 = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) )
Assertion metakunt31 ( 𝜑 → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = 𝑅 )

Proof

Step Hyp Ref Expression
1 metakunt31.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt31.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt31.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt31.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
5 metakunt31.5 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
6 metakunt31.6 ⊢ 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) )
7 metakunt31.7 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
8 metakunt31.8 ⊢ 𝐺 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 )
9 metakunt31.9 ⊢ 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 )
10 metakunt31.10 ⊢ 𝑅 = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → 𝑀 ∈ ℕ )
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → 𝐼 ∈ ℕ )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → 𝐼 ≤ 𝑀 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → 𝑋 = 𝐼 )
15 11 12 13 5 7 6 14 metakunt26 ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = 𝑋 )
16 14 iftrued ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) = 𝑋 )
17 16 eqcomd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → 𝑋 = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) )
18 15 17 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) )
19 10 eqcomi ⊢ if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) = 𝑅
20 19 a1i ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) = 𝑅 )
21 18 20 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = 𝑅 )
22 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → 𝑀 ∈ ℕ )
23 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → 𝐼 ∈ ℕ )
24 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → 𝐼 ≤ 𝑀 )
25 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
26 simp2 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → ¬ 𝑋 = 𝐼 )
27 simp3 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → 𝑋 < 𝐼 )
28 22 23 24 25 5 6 26 27 7 8 metakunt29 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) )
29 26 iffalsed ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) = if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) )
30 27 iftrued ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) )
31 29 30 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) )
32 31 eqcomd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) )
33 28 32 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) )
34 19 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) = 𝑅 )
35 33 34 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = 𝑅 )
36 35 3expa ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ) ∧ 𝑋 < 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = 𝑅 )
37 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → 𝑀 ∈ ℕ )
38 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → 𝐼 ∈ ℕ )
39 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → 𝐼 ≤ 𝑀 )
40 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
41 simp2 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → ¬ 𝑋 = 𝐼 )
42 simp3 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → ¬ 𝑋 < 𝐼 )
43 37 38 39 40 5 6 41 42 7 9 metakunt30 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
44 41 iffalsed ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) = if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) )
45 42 iffalsed ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
46 44 45 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
47 46 eqcomd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → ( ( 𝑋 − 𝐼 ) + 𝐻 ) = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) )
48 43 47 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) )
49 19 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) = 𝑅 )
50 48 49 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = 𝑅 )
51 50 3expa ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ) ∧ ¬ 𝑋 < 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = 𝑅 )
52 36 51 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝐼 ) → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = 𝑅 )
53 21 52 pm2.61dan ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = 𝑅 )