Proof of Theorem metakunt7
Step | Hyp | Ref
| Expression |
1 | | metakunt7.4 |
. . . 4
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))) |
3 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 = 𝐼 ↔ 𝑋 = 𝐼)) |
4 | | breq1 5056 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 < 𝐼 ↔ 𝑋 < 𝐼)) |
5 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
6 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 − 1) = (𝑋 − 1)) |
7 | 4, 5, 6 | ifbieq12d 4467 |
. . . . . 6
⊢ (𝑥 = 𝑋 → if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
8 | 3, 7 | ifbieq2d 4465 |
. . . . 5
⊢ (𝑥 = 𝑋 → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) |
9 | 8 | adantl 485 |
. . . 4
⊢ (((𝜑 ∧ 𝐼 < 𝑋) ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) |
10 | | metakunt7.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ ℕ) |
11 | 10 | nnred 11845 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ ℝ) |
12 | 11 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 ∈ ℝ) |
13 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 < 𝑋) |
14 | 12, 13 | ltned 10968 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 ≠ 𝑋) |
15 | 14 | necomd 2996 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝑋 ≠ 𝐼) |
16 | | df-ne 2941 |
. . . . . . . 8
⊢ (𝑋 ≠ 𝐼 ↔ ¬ 𝑋 = 𝐼) |
17 | 15, 16 | sylib 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ¬ 𝑋 = 𝐼) |
18 | | iffalse 4448 |
. . . . . . 7
⊢ (¬
𝑋 = 𝐼 → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
20 | | metakunt7.6 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
21 | | elfznn 13141 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℕ) |
23 | 22 | nnred 11845 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) |
24 | 23 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝑋 ∈ ℝ) |
25 | 12, 24, 13 | ltled 10980 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 ≤ 𝑋) |
26 | 12, 24 | lenltd 10978 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼)) |
27 | 25, 26 | mpbid 235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ¬ 𝑋 < 𝐼) |
28 | | iffalse 4448 |
. . . . . . 7
⊢ (¬
𝑋 < 𝐼 → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = (𝑋 − 1)) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = (𝑋 − 1)) |
30 | 19, 29 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = (𝑋 − 1)) |
31 | 30 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ 𝐼 < 𝑋) ∧ 𝑥 = 𝑋) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = (𝑋 − 1)) |
32 | 9, 31 | eqtrd 2777 |
. . 3
⊢ (((𝜑 ∧ 𝐼 < 𝑋) ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = (𝑋 − 1)) |
33 | 20 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝑋 ∈ (1...𝑀)) |
34 | 33 | elfzelzd 13113 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝑋 ∈ ℤ) |
35 | | 1zzd 12208 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 1 ∈ ℤ) |
36 | 34, 35 | zsubcld 12287 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝑋 − 1) ∈ ℤ) |
37 | 2, 32, 33, 36 | fvmptd 6825 |
. 2
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐴‘𝑋) = (𝑋 − 1)) |
38 | | 1red 10834 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
39 | 23, 38 | resubcld 11260 |
. . . . . 6
⊢ (𝜑 → (𝑋 − 1) ∈ ℝ) |
40 | | elfzle2 13116 |
. . . . . . . 8
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ≤ 𝑀) |
41 | 20, 40 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≤ 𝑀) |
42 | 20 | elfzelzd 13113 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℤ) |
43 | | metakunt7.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
44 | 43 | nnzd 12281 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
45 | | zlem1lt 12229 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑋 ≤ 𝑀 ↔ (𝑋 − 1) < 𝑀)) |
46 | 42, 44, 45 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ≤ 𝑀 ↔ (𝑋 − 1) < 𝑀)) |
47 | 41, 46 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → (𝑋 − 1) < 𝑀) |
48 | 39, 47 | ltned 10968 |
. . . . 5
⊢ (𝜑 → (𝑋 − 1) ≠ 𝑀) |
49 | 48 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝑋 − 1) ≠ 𝑀) |
50 | 37, 49 | eqnetrd 3008 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐴‘𝑋) ≠ 𝑀) |
51 | 50 | neneqd 2945 |
. 2
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ¬ (𝐴‘𝑋) = 𝑀) |
52 | 10 | nnzd 12281 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℤ) |
53 | | zltlem1 12230 |
. . . . . . 7
⊢ ((𝐼 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝐼 < 𝑋 ↔ 𝐼 ≤ (𝑋 − 1))) |
54 | 53 | biimpd 232 |
. . . . . 6
⊢ ((𝐼 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝐼 < 𝑋 → 𝐼 ≤ (𝑋 − 1))) |
55 | 52, 42, 54 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐼 < 𝑋 → 𝐼 ≤ (𝑋 − 1))) |
56 | 55 | imp 410 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 ≤ (𝑋 − 1)) |
57 | 56, 37 | breqtrrd 5081 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 ≤ (𝐴‘𝑋)) |
58 | 36 | zred 12282 |
. . . . 5
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝑋 − 1) ∈ ℝ) |
59 | 37, 58 | eqeltrd 2838 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐴‘𝑋) ∈ ℝ) |
60 | 12, 59 | lenltd 10978 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐼 ≤ (𝐴‘𝑋) ↔ ¬ (𝐴‘𝑋) < 𝐼)) |
61 | 57, 60 | mpbid 235 |
. 2
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ¬ (𝐴‘𝑋) < 𝐼) |
62 | 37, 51, 61 | 3jca 1130 |
1
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ((𝐴‘𝑋) = (𝑋 − 1) ∧ ¬ (𝐴‘𝑋) = 𝑀 ∧ ¬ (𝐴‘𝑋) < 𝐼)) |