Proof of Theorem metakunt31
| Step | Hyp | Ref
| Expression |
| 1 | | metakunt31.1 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = 𝐼) → 𝑀 ∈ ℕ) |
| 3 | | metakunt31.2 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℕ) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = 𝐼) → 𝐼 ∈ ℕ) |
| 5 | | metakunt31.3 |
. . . . . 6
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
| 6 | 5 | adantr 480 |
. . . . 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 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = 𝐼) → 𝑋 = 𝐼) |
| 11 | 2, 4, 6, 7, 8, 9, 10 | metakunt26 42231 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = 𝐼) → (𝐶‘(𝐵‘(𝐴‘𝑋))) = 𝑋) |
| 12 | 10 | iftrued 4533 |
. . . . 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 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼) → 𝑀 ∈ ℕ) |
| 20 | 3 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼) → 𝐼 ∈ ℕ) |
| 21 | 5 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼) → 𝐼 ≤ 𝑀) |
| 22 | | metakunt31.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
| 23 | 22 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼) → 𝑋 ∈ (1...𝑀)) |
| 24 | | simp2 1138 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼) → ¬ 𝑋 = 𝐼) |
| 25 | | simp3 1139 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼) → 𝑋 < 𝐼) |
| 26 | | metakunt31.8 |
. . . . . . 7
⊢ 𝐺 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) |
| 27 | 19, 20, 21, 23, 7, 9, 24, 25, 8, 26 | metakunt29 42234 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼) → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐺)) |
| 28 | 24 | iffalsed 4536 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) = if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) |
| 29 | 25 | iftrued 4533 |
. . . . . . . 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 1119 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝑋 = 𝐼) ∧ 𝑋 < 𝐼) → (𝐶‘(𝐵‘(𝐴‘𝑋))) = 𝑅) |
| 36 | 1 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼) → 𝑀 ∈ ℕ) |
| 37 | 3 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼) → 𝐼 ∈ ℕ) |
| 38 | 5 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼) → 𝐼 ≤ 𝑀) |
| 39 | 22 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼) → 𝑋 ∈ (1...𝑀)) |
| 40 | | simp2 1138 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼) → ¬ 𝑋 = 𝐼) |
| 41 | | simp3 1139 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼) → ¬ 𝑋 < 𝐼) |
| 42 | | metakunt31.9 |
. . . . . . 7
⊢ 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) |
| 43 | 36, 37, 38, 39, 7, 9, 40, 41, 8, 42 | metakunt30 42235 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼) → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 − 𝐼) + 𝐻)) |
| 44 | 40 | iffalsed 4536 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼 ∧ ¬ 𝑋 < 𝐼) → if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) = if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) |
| 45 | 41 | iffalsed 4536 |
. . . . . . . 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 1119 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝑋 = 𝐼) ∧ ¬ 𝑋 < 𝐼) → (𝐶‘(𝐵‘(𝐴‘𝑋))) = 𝑅) |
| 52 | 35, 51 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝐼) → (𝐶‘(𝐵‘(𝐴‘𝑋))) = 𝑅) |
| 53 | 18, 52 | pm2.61dan 813 |
1
⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = 𝑅) |