Proof of Theorem metakunt8
Step | Hyp | Ref
| Expression |
1 | | metakunt8.5 |
. . 3
⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))) |
3 | | eqeq1 2741 |
. . . . 5
⊢ (𝑦 = (𝐴‘𝑋) → (𝑦 = 𝑀 ↔ (𝐴‘𝑋) = 𝑀)) |
4 | | breq1 5056 |
. . . . . 6
⊢ (𝑦 = (𝐴‘𝑋) → (𝑦 < 𝐼 ↔ (𝐴‘𝑋) < 𝐼)) |
5 | | id 22 |
. . . . . 6
⊢ (𝑦 = (𝐴‘𝑋) → 𝑦 = (𝐴‘𝑋)) |
6 | | oveq1 7220 |
. . . . . 6
⊢ (𝑦 = (𝐴‘𝑋) → (𝑦 + 1) = ((𝐴‘𝑋) + 1)) |
7 | 4, 5, 6 | ifbieq12d 4467 |
. . . . 5
⊢ (𝑦 = (𝐴‘𝑋) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1))) |
8 | 3, 7 | ifbieq2d 4465 |
. . . 4
⊢ (𝑦 = (𝐴‘𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if((𝐴‘𝑋) = 𝑀, 𝐼, if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1)))) |
9 | 8 | adantl 485 |
. . 3
⊢ (((𝜑 ∧ 𝐼 < 𝑋) ∧ 𝑦 = (𝐴‘𝑋)) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if((𝐴‘𝑋) = 𝑀, 𝐼, if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1)))) |
10 | | metakunt8.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
11 | | metakunt8.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ ℕ) |
12 | | metakunt8.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
13 | | metakunt8.4 |
. . . . . . . . 9
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
14 | | metakunt8.6 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
15 | 10, 11, 12, 13, 1, 14 | metakunt7 39853 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ((𝐴‘𝑋) = (𝑋 − 1) ∧ ¬ (𝐴‘𝑋) = 𝑀 ∧ ¬ (𝐴‘𝑋) < 𝐼)) |
16 | 15 | simp2d 1145 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ¬ (𝐴‘𝑋) = 𝑀) |
17 | | iffalse 4448 |
. . . . . . 7
⊢ (¬
(𝐴‘𝑋) = 𝑀 → if((𝐴‘𝑋) = 𝑀, 𝐼, if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1))) = if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1))) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → if((𝐴‘𝑋) = 𝑀, 𝐼, if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1))) = if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1))) |
19 | 15 | simp3d 1146 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ¬ (𝐴‘𝑋) < 𝐼) |
20 | | iffalse 4448 |
. . . . . . 7
⊢ (¬
(𝐴‘𝑋) < 𝐼 → if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1)) = ((𝐴‘𝑋) + 1)) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1)) = ((𝐴‘𝑋) + 1)) |
22 | 18, 21 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → if((𝐴‘𝑋) = 𝑀, 𝐼, if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1))) = ((𝐴‘𝑋) + 1)) |
23 | 15 | simp1d 1144 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐴‘𝑋) = (𝑋 − 1)) |
24 | 23 | oveq1d 7228 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ((𝐴‘𝑋) + 1) = ((𝑋 − 1) + 1)) |
25 | | elfznn 13141 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
26 | 14, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℕ) |
27 | 26 | nncnd 11846 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
28 | | 1cnd 10828 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) |
29 | 27, 28 | npcand 11193 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 − 1) + 1) = 𝑋) |
30 | 29 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ((𝑋 − 1) + 1) = 𝑋) |
31 | 24, 30 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ((𝐴‘𝑋) + 1) = 𝑋) |
32 | 22, 31 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → if((𝐴‘𝑋) = 𝑀, 𝐼, if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1))) = 𝑋) |
33 | 32 | adantr 484 |
. . 3
⊢ (((𝜑 ∧ 𝐼 < 𝑋) ∧ 𝑦 = (𝐴‘𝑋)) → if((𝐴‘𝑋) = 𝑀, 𝐼, if((𝐴‘𝑋) < 𝐼, (𝐴‘𝑋), ((𝐴‘𝑋) + 1))) = 𝑋) |
34 | 9, 33 | eqtrd 2777 |
. 2
⊢ (((𝜑 ∧ 𝐼 < 𝑋) ∧ 𝑦 = (𝐴‘𝑋)) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝑋) |
35 | 10, 11, 12, 13 | metakunt1 39847 |
. . . 4
⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) |
36 | 35 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐴:(1...𝑀)⟶(1...𝑀)) |
37 | 14 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝑋 ∈ (1...𝑀)) |
38 | 36, 37 | ffvelrnd 6905 |
. 2
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐴‘𝑋) ∈ (1...𝑀)) |
39 | 2, 34, 38, 37 | fvmptd 6825 |
1
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐶‘(𝐴‘𝑋)) = 𝑋) |