Proof of Theorem metakunt12
Step | Hyp | Ref
| Expression |
1 | | ioran 982 |
. 2
⊢ (¬
(𝑋 = 𝑀 ∨ 𝑋 < 𝐼) ↔ (¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼)) |
2 | | metakunt12.4 |
. . . . 5
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
3 | 2 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))) |
4 | | eqeq1 2763 |
. . . . . . 7
⊢ (𝑥 = (𝐶‘𝑋) → (𝑥 = 𝐼 ↔ (𝐶‘𝑋) = 𝐼)) |
5 | | breq1 5028 |
. . . . . . . 8
⊢ (𝑥 = (𝐶‘𝑋) → (𝑥 < 𝐼 ↔ (𝐶‘𝑋) < 𝐼)) |
6 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = (𝐶‘𝑋) → 𝑥 = (𝐶‘𝑋)) |
7 | | oveq1 7150 |
. . . . . . . 8
⊢ (𝑥 = (𝐶‘𝑋) → (𝑥 − 1) = ((𝐶‘𝑋) − 1)) |
8 | 5, 6, 7 | ifbieq12d 4441 |
. . . . . . 7
⊢ (𝑥 = (𝐶‘𝑋) → if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) = if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) |
9 | 4, 8 | ifbieq2d 4439 |
. . . . . 6
⊢ (𝑥 = (𝐶‘𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)))) |
10 | 9 | adantl 486 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝐶‘𝑋)) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)))) |
11 | | metakunt12.5 |
. . . . . . . . . 10
⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) |
12 | 11 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))) |
13 | | eqeq1 2763 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑋 → (𝑦 = 𝑀 ↔ 𝑋 = 𝑀)) |
14 | | breq1 5028 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (𝑦 < 𝐼 ↔ 𝑋 < 𝐼)) |
15 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → 𝑦 = 𝑋) |
16 | | oveq1 7150 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (𝑦 + 1) = (𝑋 + 1)) |
17 | 14, 15, 16 | ifbieq12d 4441 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑋 → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
18 | 13, 17 | ifbieq2d 4439 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑋 → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) |
19 | 18 | adantl 486 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) |
20 | | simp2 1135 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → ¬ 𝑋 = 𝑀) |
21 | | iffalse 4422 |
. . . . . . . . . . . . 13
⊢ (¬
𝑋 = 𝑀 → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
23 | | simp3 1136 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → ¬ 𝑋 < 𝐼) |
24 | | iffalse 4422 |
. . . . . . . . . . . . 13
⊢ (¬
𝑋 < 𝐼 → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = (𝑋 + 1)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = (𝑋 + 1)) |
26 | 22, 25 | eqtrd 2794 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = (𝑋 + 1)) |
27 | 26 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = (𝑋 + 1)) |
28 | 19, 27 | eqtrd 2794 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = (𝑋 + 1)) |
29 | | metakunt12.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
30 | 29 | 3ad2ant1 1131 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝑋 ∈ (1...𝑀)) |
31 | | elfznn 12970 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
32 | 29, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ ℕ) |
33 | 32 | nnzd 12110 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℤ) |
34 | 33 | 3ad2ant1 1131 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝑋 ∈ ℤ) |
35 | 34 | peano2zd 12114 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → (𝑋 + 1) ∈ ℤ) |
36 | 12, 28, 30, 35 | fvmptd 6759 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → (𝐶‘𝑋) = (𝑋 + 1)) |
37 | | eqeq1 2763 |
. . . . . . . . 9
⊢ ((𝐶‘𝑋) = (𝑋 + 1) → ((𝐶‘𝑋) = 𝐼 ↔ (𝑋 + 1) = 𝐼)) |
38 | | breq1 5028 |
. . . . . . . . . 10
⊢ ((𝐶‘𝑋) = (𝑋 + 1) → ((𝐶‘𝑋) < 𝐼 ↔ (𝑋 + 1) < 𝐼)) |
39 | | id 22 |
. . . . . . . . . 10
⊢ ((𝐶‘𝑋) = (𝑋 + 1) → (𝐶‘𝑋) = (𝑋 + 1)) |
40 | | oveq1 7150 |
. . . . . . . . . 10
⊢ ((𝐶‘𝑋) = (𝑋 + 1) → ((𝐶‘𝑋) − 1) = ((𝑋 + 1) − 1)) |
41 | 38, 39, 40 | ifbieq12d 4441 |
. . . . . . . . 9
⊢ ((𝐶‘𝑋) = (𝑋 + 1) → if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1)) = if((𝑋 + 1) < 𝐼, (𝑋 + 1), ((𝑋 + 1) − 1))) |
42 | 37, 41 | ifbieq2d 4439 |
. . . . . . . 8
⊢ ((𝐶‘𝑋) = (𝑋 + 1) → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = if((𝑋 + 1) = 𝐼, 𝑀, if((𝑋 + 1) < 𝐼, (𝑋 + 1), ((𝑋 + 1) − 1)))) |
43 | 36, 42 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = if((𝑋 + 1) = 𝐼, 𝑀, if((𝑋 + 1) < 𝐼, (𝑋 + 1), ((𝑋 + 1) − 1)))) |
44 | | metakunt12.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ ℕ) |
45 | 44 | nnred 11674 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ ℝ) |
46 | 45 | 3ad2ant1 1131 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝐼 ∈ ℝ) |
47 | 34 | zred 12111 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝑋 ∈ ℝ) |
48 | 35 | zred 12111 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → (𝑋 + 1) ∈ ℝ) |
49 | 46, 47 | lenltd 10809 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → (𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼)) |
50 | 23, 49 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝐼 ≤ 𝑋) |
51 | 47 | ltp1d 11593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝑋 < (𝑋 + 1)) |
52 | 46, 47, 48, 50, 51 | lelttrd 10821 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝐼 < (𝑋 + 1)) |
53 | 46, 52 | ltned 10799 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝐼 ≠ (𝑋 + 1)) |
54 | 53 | necomd 3004 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → (𝑋 + 1) ≠ 𝐼) |
55 | 54 | neneqd 2954 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → ¬ (𝑋 + 1) = 𝐼) |
56 | | iffalse 4422 |
. . . . . . . . 9
⊢ (¬
(𝑋 + 1) = 𝐼 → if((𝑋 + 1) = 𝐼, 𝑀, if((𝑋 + 1) < 𝐼, (𝑋 + 1), ((𝑋 + 1) − 1))) = if((𝑋 + 1) < 𝐼, (𝑋 + 1), ((𝑋 + 1) − 1))) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → if((𝑋 + 1) = 𝐼, 𝑀, if((𝑋 + 1) < 𝐼, (𝑋 + 1), ((𝑋 + 1) − 1))) = if((𝑋 + 1) < 𝐼, (𝑋 + 1), ((𝑋 + 1) − 1))) |
58 | 47 | lep1d 11594 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝑋 ≤ (𝑋 + 1)) |
59 | 46, 47, 48, 50, 58 | letrd 10820 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝐼 ≤ (𝑋 + 1)) |
60 | 46, 48 | lenltd 10809 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → (𝐼 ≤ (𝑋 + 1) ↔ ¬ (𝑋 + 1) < 𝐼)) |
61 | 59, 60 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → ¬ (𝑋 + 1) < 𝐼) |
62 | | iffalse 4422 |
. . . . . . . . 9
⊢ (¬
(𝑋 + 1) < 𝐼 → if((𝑋 + 1) < 𝐼, (𝑋 + 1), ((𝑋 + 1) − 1)) = ((𝑋 + 1) − 1)) |
63 | 61, 62 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → if((𝑋 + 1) < 𝐼, (𝑋 + 1), ((𝑋 + 1) − 1)) = ((𝑋 + 1) − 1)) |
64 | 34 | zcnd 12112 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝑋 ∈ ℂ) |
65 | | 1cnd 10659 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 1 ∈ ℂ) |
66 | 64, 65 | pncand 11021 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → ((𝑋 + 1) − 1) = 𝑋) |
67 | 57, 63, 66 | 3eqtrd 2798 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → if((𝑋 + 1) = 𝐼, 𝑀, if((𝑋 + 1) < 𝐼, (𝑋 + 1), ((𝑋 + 1) − 1))) = 𝑋) |
68 | 43, 67 | eqtrd 2794 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = 𝑋) |
69 | 68 | adantr 485 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝐶‘𝑋)) → if((𝐶‘𝑋) = 𝐼, 𝑀, if((𝐶‘𝑋) < 𝐼, (𝐶‘𝑋), ((𝐶‘𝑋) − 1))) = 𝑋) |
70 | 10, 69 | eqtrd 2794 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝐶‘𝑋)) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = 𝑋) |
71 | | metakunt12.1 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) |
72 | | metakunt12.3 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
73 | 71, 44, 72, 11 | metakunt2 39633 |
. . . . . 6
⊢ (𝜑 → 𝐶:(1...𝑀)⟶(1...𝑀)) |
74 | 73 | 3ad2ant1 1131 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → 𝐶:(1...𝑀)⟶(1...𝑀)) |
75 | 74, 30 | ffvelrnd 6836 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → (𝐶‘𝑋) ∈ (1...𝑀)) |
76 | 3, 70, 75, 30 | fvmptd 6759 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼) → (𝐴‘(𝐶‘𝑋)) = 𝑋) |
77 | 76 | 3expb 1118 |
. 2
⊢ ((𝜑 ∧ (¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼)) → (𝐴‘(𝐶‘𝑋)) = 𝑋) |
78 | 1, 77 | sylan2b 597 |
1
⊢ ((𝜑 ∧ ¬ (𝑋 = 𝑀 ∨ 𝑋 < 𝐼)) → (𝐴‘(𝐶‘𝑋)) = 𝑋) |