Proof of Theorem metakunt6
Step | Hyp | Ref
| Expression |
1 | | metakunt6.5 |
. . 3
⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))) |
3 | | metakunt6.4 |
. . . . . . . 8
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
4 | 3 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))) |
5 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
6 | 5 | eqeq1d 2761 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑥 = 𝐼 ↔ 𝑋 = 𝐼)) |
7 | | breq1 5028 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥 < 𝐼 ↔ 𝑋 < 𝐼)) |
8 | | oveq1 7150 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥 − 1) = (𝑋 − 1)) |
9 | 7, 5, 8 | ifbieq12d 4441 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
10 | 6, 9 | ifbieq2d 4439 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) |
11 | 10 | adantl 486 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) |
12 | | metakunt6.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
13 | | elfznn 12970 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ ℕ) |
15 | 14 | nnred 11674 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ ℝ) |
16 | 15 | adantr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ∈ ℝ) |
17 | | simpr 489 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 < 𝐼) |
18 | 16, 17 | ltned 10799 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ≠ 𝐼) |
19 | | df-ne 2950 |
. . . . . . . . . . . 12
⊢ (𝑋 ≠ 𝐼 ↔ ¬ 𝑋 = 𝐼) |
20 | 18, 19 | sylib 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → ¬ 𝑋 = 𝐼) |
21 | | iffalse 4422 |
. . . . . . . . . . 11
⊢ (¬
𝑋 = 𝐼 → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
23 | | iftrue 4419 |
. . . . . . . . . . 11
⊢ (𝑋 < 𝐼 → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = 𝑋) |
24 | 23 | adantl 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = 𝑋) |
25 | 22, 24 | eqtrd 2794 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = 𝑋) |
26 | 25 | adantr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑥 = 𝑋) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = 𝑋) |
27 | 11, 26 | eqtrd 2794 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = 𝑋) |
28 | 12 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ∈ (1...𝑀)) |
29 | 4, 27, 28, 28 | fvmptd 6759 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘𝑋) = 𝑋) |
30 | | eqcom 2766 |
. . . . . . 7
⊢ ((𝐴‘𝑋) = 𝑋 ↔ 𝑋 = (𝐴‘𝑋)) |
31 | 30 | imbi2i 340 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘𝑋) = 𝑋) ↔ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 = (𝐴‘𝑋))) |
32 | 29, 31 | mpbi 233 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 = (𝐴‘𝑋)) |
33 | 32 | eqeq2d 2770 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝑦 = 𝑋 ↔ 𝑦 = (𝐴‘𝑋))) |
34 | | eqeq1 2763 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → (𝑦 = 𝑀 ↔ 𝑋 = 𝑀)) |
35 | | breq1 5028 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → (𝑦 < 𝐼 ↔ 𝑋 < 𝐼)) |
36 | | id 22 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → 𝑦 = 𝑋) |
37 | | oveq1 7150 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → (𝑦 + 1) = (𝑋 + 1)) |
38 | 35, 36, 37 | ifbieq12d 4441 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
39 | 34, 38 | ifbieq2d 4439 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) |
40 | 39 | adantl 486 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) |
41 | | metakunt6.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ ℕ) |
42 | 41 | nnred 11674 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ ℝ) |
43 | 42 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐼 ∈ ℝ) |
44 | | metakunt6.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℕ) |
45 | 44 | nnred 11674 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℝ) |
46 | 45 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑀 ∈ ℝ) |
47 | | metakunt6.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
48 | 47 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐼 ≤ 𝑀) |
49 | 16, 43, 46, 17, 48 | ltletrd 10823 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 < 𝑀) |
50 | 16, 49 | ltned 10799 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ≠ 𝑀) |
51 | 50 | neneqd 2954 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → ¬ 𝑋 = 𝑀) |
52 | | iffalse 4422 |
. . . . . . . . 9
⊢ (¬
𝑋 = 𝑀 → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
53 | 51, 52 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
54 | | iftrue 4419 |
. . . . . . . . 9
⊢ (𝑋 < 𝐼 → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = 𝑋) |
55 | 54 | adantl 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = 𝑋) |
56 | 53, 55 | eqtrd 2794 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = 𝑋) |
57 | 56 | adantr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = 𝑋) |
58 | 40, 57 | eqtrd 2794 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝑋) |
59 | 58 | ex 417 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝑦 = 𝑋 → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝑋)) |
60 | 33, 59 | sylbird 263 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝑦 = (𝐴‘𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝑋)) |
61 | 60 | imp 411 |
. 2
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = (𝐴‘𝑋)) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝑋) |
62 | 44 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑀 ∈ ℕ) |
63 | 41 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐼 ∈ ℕ) |
64 | 62, 63, 48, 3 | metakunt1 39632 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐴:(1...𝑀)⟶(1...𝑀)) |
65 | 64, 28 | ffvelrnd 6836 |
. 2
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘𝑋) ∈ (1...𝑀)) |
66 | 2, 61, 65, 28 | fvmptd 6759 |
1
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋) |