Proof of Theorem metakunt27
Step | Hyp | Ref
| Expression |
1 | | metakunt27.5 |
. . . . 5
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))) |
3 | | metakunt27.7 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑋 = 𝐼) |
4 | 3 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ¬ 𝑋 = 𝐼) |
5 | | simpr 489 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) |
6 | 5 | eqeq1d 2761 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 = 𝐼 ↔ 𝑋 = 𝐼)) |
7 | 6 | notbid 322 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (¬ 𝑥 = 𝐼 ↔ ¬ 𝑋 = 𝐼)) |
8 | 4, 7 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ¬ 𝑥 = 𝐼) |
9 | 8 | iffalsed 4424 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) |
10 | | metakunt27.8 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 < 𝐼) |
11 | 10 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑋 < 𝐼) |
12 | 5 | breq1d 5035 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 < 𝐼 ↔ 𝑋 < 𝐼)) |
13 | 11, 12 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑥 < 𝐼) |
14 | 13 | iftrued 4421 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) = 𝑥) |
15 | 14, 5 | eqtrd 2794 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) = 𝑋) |
16 | 9, 15 | eqtrd 2794 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = 𝑋) |
17 | | metakunt27.4 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
18 | 2, 16, 17, 17 | fvmptd 6759 |
. . 3
⊢ (𝜑 → (𝐴‘𝑋) = 𝑋) |
19 | 18 | fveq2d 6655 |
. 2
⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝐵‘𝑋)) |
20 | | metakunt27.6 |
. . . 4
⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) |
21 | 20 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))) |
22 | | elfznn 12970 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
23 | 17, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℕ) |
24 | 23 | nnred 11674 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) |
25 | | metakunt27.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ ℕ) |
26 | 25 | nnred 11674 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ ℝ) |
27 | | metakunt27.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
28 | 27 | nnred 11674 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
29 | | metakunt27.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
30 | 24, 26, 28, 10, 29 | ltletrd 10823 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 < 𝑀) |
31 | 24, 30 | ltned 10799 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ≠ 𝑀) |
32 | 31 | neneqd 2954 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑋 = 𝑀) |
33 | 32 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → ¬ 𝑋 = 𝑀) |
34 | | simpr 489 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → 𝑧 = 𝑋) |
35 | 34 | eqeq1d 2761 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → (𝑧 = 𝑀 ↔ 𝑋 = 𝑀)) |
36 | 35 | notbid 322 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → (¬ 𝑧 = 𝑀 ↔ ¬ 𝑋 = 𝑀)) |
37 | 33, 36 | mpbird 260 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → ¬ 𝑧 = 𝑀) |
38 | 37 | iffalsed 4424 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))) = if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))) |
39 | 10 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → 𝑋 < 𝐼) |
40 | 34 | breq1d 5035 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → (𝑧 < 𝐼 ↔ 𝑋 < 𝐼)) |
41 | 39, 40 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → 𝑧 < 𝐼) |
42 | 41 | iftrued 4421 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))) = (𝑧 + (𝑀 − 𝐼))) |
43 | 34 | oveq1d 7158 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → (𝑧 + (𝑀 − 𝐼)) = (𝑋 + (𝑀 − 𝐼))) |
44 | 42, 43 | eqtrd 2794 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))) = (𝑋 + (𝑀 − 𝐼))) |
45 | 38, 44 | eqtrd 2794 |
. . 3
⊢ ((𝜑 ∧ 𝑧 = 𝑋) → if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))) = (𝑋 + (𝑀 − 𝐼))) |
46 | 17 | elfzelzd 12942 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℤ) |
47 | 27 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
48 | 25 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ ℤ) |
49 | 47, 48 | zsubcld 12116 |
. . . 4
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ) |
50 | 46, 49 | zaddcld 12115 |
. . 3
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ) |
51 | 21, 45, 17, 50 | fvmptd 6759 |
. 2
⊢ (𝜑 → (𝐵‘𝑋) = (𝑋 + (𝑀 − 𝐼))) |
52 | 19, 51 | eqtrd 2794 |
1
⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 + (𝑀 − 𝐼))) |