Proof of Theorem metakunt10
| Step | Hyp | Ref
| Expression |
| 1 | | metakunt10.4 |
. . 3
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
| 2 | 1 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))) |
| 3 | | eqeq1 2741 |
. . . . 5
⊢ (𝑥 = (𝐶‘𝑋) → (𝑥 = 𝐼 ↔ (𝐶‘𝑋) = 𝐼)) |
| 4 | | breq1 5146 |
. . . . . 6
⊢ (𝑥 = (𝐶‘𝑋) → (𝑥 < 𝐼 ↔ (𝐶‘𝑋) < 𝐼)) |
| 5 | | id 22 |
. . . . . 6
⊢ (𝑥 = (𝐶‘𝑋) → 𝑥 = (𝐶‘𝑋)) |
| 6 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = (𝐶‘𝑋) → (𝑥 − 1) = ((𝐶‘𝑋) − 1)) |
| 7 | 4, 5, 6 | ifbieq12d 4554 |
. . . . 5
⊢ (𝑥 = (𝐶‘𝑋) → if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) = if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) |
| 8 | 3, 7 | ifbieq2d 4552 |
. . . 4
⊢ (𝑥 = (𝐶‘𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)))) |
| 9 | 8 | adantl 481 |
. . 3
⊢ (((𝜑 ∧ 𝑋 = 𝑀) ∧ 𝑥 = (𝐶‘𝑋)) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)))) |
| 10 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑋 = 𝑀 → (𝐶‘𝑋) = (𝐶‘𝑀)) |
| 11 | 10 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → (𝐶‘𝑋) = (𝐶‘𝑀)) |
| 12 | | metakunt10.5 |
. . . . . . . . . 10
⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) |
| 13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))) |
| 14 | | iftrue 4531 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑀 → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝐼) |
| 15 | 14 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝐼) |
| 16 | | 1zzd 12648 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) |
| 17 | | metakunt10.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 18 | 17 | nnzd 12640 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 19 | 17 | nnge1d 12314 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≤ 𝑀) |
| 20 | 17 | nnred 12281 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 21 | 20 | leidd 11829 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
| 22 | 16, 18, 18, 19, 21 | elfzd 13555 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (1...𝑀)) |
| 23 | | metakunt10.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ ℕ) |
| 24 | 13, 15, 22, 23 | fvmptd 7023 |
. . . . . . . 8
⊢ (𝜑 → (𝐶‘𝑀) = 𝐼) |
| 25 | 24 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → (𝐶‘𝑀) = 𝐼) |
| 26 | 11, 25 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → (𝐶‘𝑋) = 𝐼) |
| 27 | | iftrue 4531 |
. . . . . 6
⊢ ((𝐶‘𝑋) = 𝐼 → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = 𝑀) |
| 28 | 26, 27 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = 𝑀) |
| 29 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → 𝑋 = 𝑀) |
| 30 | 29 | eqcomd 2743 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → 𝑀 = 𝑋) |
| 31 | 28, 30 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = 𝑋) |
| 32 | 31 | adantr 480 |
. . 3
⊢ (((𝜑 ∧ 𝑋 = 𝑀) ∧ 𝑥 = (𝐶‘𝑋)) → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = 𝑋) |
| 33 | 9, 32 | eqtrd 2777 |
. 2
⊢ (((𝜑 ∧ 𝑋 = 𝑀) ∧ 𝑥 = (𝐶‘𝑋)) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = 𝑋) |
| 34 | | metakunt10.3 |
. . . . 5
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
| 35 | 17, 23, 34, 12 | metakunt2 42207 |
. . . 4
⊢ (𝜑 → 𝐶:(1...𝑀)⟶(1...𝑀)) |
| 36 | 35 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → 𝐶:(1...𝑀)⟶(1...𝑀)) |
| 37 | | metakunt10.6 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
| 38 | 37 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → 𝑋 ∈ (1...𝑀)) |
| 39 | 36, 38 | ffvelcdmd 7105 |
. 2
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → (𝐶‘𝑋) ∈ (1...𝑀)) |
| 40 | 2, 33, 39, 38 | fvmptd 7023 |
1
⊢ ((𝜑 ∧ 𝑋 = 𝑀) → (𝐴‘(𝐶‘𝑋)) = 𝑋) |