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 2739 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑥 = 𝐼 ↔ 𝑋 = 𝐼)) |
| 7 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥 < 𝐼 ↔ 𝑋 < 𝐼)) |
| 8 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥 − 1) = (𝑋 − 1)) |
| 9 | 7, 5, 8 | ifbieq12d 4554 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
| 10 | 6, 9 | ifbieq2d 4552 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) |
| 11 | 10 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) |
| 12 | | metakunt6.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
| 13 | | elfznn 13593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
| 14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ ℕ) |
| 15 | 14 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 16 | 15 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ∈ ℝ) |
| 17 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 < 𝐼) |
| 18 | 16, 17 | ltned 11397 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ≠ 𝐼) |
| 19 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ (𝑋 ≠ 𝐼 ↔ ¬ 𝑋 = 𝐼) |
| 20 | 18, 19 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → ¬ 𝑋 = 𝐼) |
| 21 | | iffalse 4534 |
. . . . . . . . . . 11
⊢ (¬
𝑋 = 𝐼 → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
| 23 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑋 < 𝐼 → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = 𝑋) |
| 24 | 23 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = 𝑋) |
| 25 | 22, 24 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = 𝑋) |
| 26 | 25 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑥 = 𝑋) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = 𝑋) |
| 27 | 11, 26 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = 𝑋) |
| 28 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ∈ (1...𝑀)) |
| 29 | 4, 27, 28, 28 | fvmptd 7023 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘𝑋) = 𝑋) |
| 30 | | eqcom 2744 |
. . . . . . 7
⊢ ((𝐴‘𝑋) = 𝑋 ↔ 𝑋 = (𝐴‘𝑋)) |
| 31 | 30 | imbi2i 336 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘𝑋) = 𝑋) ↔ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 = (𝐴‘𝑋))) |
| 32 | 29, 31 | mpbi 230 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 = (𝐴‘𝑋)) |
| 33 | 32 | eqeq2d 2748 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝑦 = 𝑋 ↔ 𝑦 = (𝐴‘𝑋))) |
| 34 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → (𝑦 = 𝑀 ↔ 𝑋 = 𝑀)) |
| 35 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → (𝑦 < 𝐼 ↔ 𝑋 < 𝐼)) |
| 36 | | id 22 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → 𝑦 = 𝑋) |
| 37 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → (𝑦 + 1) = (𝑋 + 1)) |
| 38 | 35, 36, 37 | ifbieq12d 4554 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
| 39 | 34, 38 | ifbieq2d 4552 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) |
| 40 | 39 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) |
| 41 | | metakunt6.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ ℕ) |
| 42 | 41 | nnred 12281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ ℝ) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐼 ∈ ℝ) |
| 44 | | metakunt6.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 45 | 44 | nnred 12281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑀 ∈ ℝ) |
| 47 | | metakunt6.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐼 ≤ 𝑀) |
| 49 | 16, 43, 46, 17, 48 | ltletrd 11421 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 < 𝑀) |
| 50 | 16, 49 | ltned 11397 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑋 ≠ 𝑀) |
| 51 | 50 | neneqd 2945 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → ¬ 𝑋 = 𝑀) |
| 52 | | iffalse 4534 |
. . . . . . . . 9
⊢ (¬
𝑋 = 𝑀 → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
| 53 | 51, 52 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) |
| 54 | | iftrue 4531 |
. . . . . . . . 9
⊢ (𝑋 < 𝐼 → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = 𝑋) |
| 55 | 54 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = 𝑋) |
| 56 | 53, 55 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = 𝑋) |
| 57 | 56 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))) = 𝑋) |
| 58 | 40, 57 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = 𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝑋) |
| 59 | 58 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝑦 = 𝑋 → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝑋)) |
| 60 | 33, 59 | sylbird 260 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝑦 = (𝐴‘𝑋) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝑋)) |
| 61 | 60 | imp 406 |
. 2
⊢ (((𝜑 ∧ 𝑋 < 𝐼) ∧ 𝑦 = (𝐴‘𝑋)) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = 𝑋) |
| 62 | 44 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝑀 ∈ ℕ) |
| 63 | 41 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐼 ∈ ℕ) |
| 64 | 62, 63, 48, 3 | metakunt1 42206 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → 𝐴:(1...𝑀)⟶(1...𝑀)) |
| 65 | 64, 28 | ffvelcdmd 7105 |
. 2
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘𝑋) ∈ (1...𝑀)) |
| 66 | 2, 61, 65, 28 | fvmptd 7023 |
1
⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋) |