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