Proof of Theorem elfznelfzo
Step | Hyp | Ref
| Expression |
1 | | elfz2nn0 13338 |
. . 3
⊢ (𝑀 ∈ (0...𝐾) ↔ (𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑀 ≤ 𝐾)) |
2 | | nn0z 12335 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℤ) |
3 | | nn0z 12335 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
4 | 2, 3 | anim12i 613 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ)) |
5 | 4 | 3adant3 1131 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (𝑀 ∈ ℤ ∧ 𝐾 ∈
ℤ)) |
6 | | elfzom1b 13476 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∈ (1..^𝐾) ↔ (𝑀 − 1) ∈ (0..^(𝐾 − 1)))) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (𝑀 ∈ (1..^𝐾) ↔ (𝑀 − 1) ∈ (0..^(𝐾 − 1)))) |
8 | 7 | notbid 318 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬ 𝑀 ∈ (1..^𝐾) ↔ ¬ (𝑀 − 1) ∈ (0..^(𝐾 − 1)))) |
9 | | elfzo0 13418 |
. . . . . . 7
⊢ ((𝑀 − 1) ∈ (0..^(𝐾 − 1)) ↔ ((𝑀 − 1) ∈
ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑀 − 1) < (𝐾 − 1))) |
10 | 9 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → ((𝑀 − 1) ∈ (0..^(𝐾 − 1)) ↔ ((𝑀 − 1) ∈
ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑀 − 1) < (𝐾 − 1)))) |
11 | 10 | notbid 318 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬
(𝑀 − 1) ∈
(0..^(𝐾 − 1)) ↔
¬ ((𝑀 − 1) ∈
ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑀 − 1) < (𝐾 − 1)))) |
12 | | 3ianor 1106 |
. . . . . . 7
⊢ (¬
((𝑀 − 1) ∈
ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑀 − 1) < (𝐾 − 1)) ↔ (¬
(𝑀 − 1) ∈
ℕ0 ∨ ¬ (𝐾 − 1) ∈ ℕ ∨ ¬ (𝑀 − 1) < (𝐾 − 1))) |
13 | | elnnne0 12239 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0
∧ 𝑀 ≠
0)) |
14 | | df-ne 2946 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ≠ 0 ↔ ¬ 𝑀 = 0) |
15 | 14 | anbi2i 623 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≠ 0) ↔
(𝑀 ∈
ℕ0 ∧ ¬ 𝑀 = 0)) |
16 | 13, 15 | bitr2i 275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ0
∧ ¬ 𝑀 = 0) ↔
𝑀 ∈
ℕ) |
17 | | nnm1nn0 12266 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) |
18 | 16, 17 | sylbi 216 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ0
∧ ¬ 𝑀 = 0) →
(𝑀 − 1) ∈
ℕ0) |
19 | 18 | ex 413 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ0
→ (¬ 𝑀 = 0 →
(𝑀 − 1) ∈
ℕ0)) |
20 | 19 | con1d 145 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ (¬ (𝑀 − 1)
∈ ℕ0 → 𝑀 = 0)) |
21 | 20 | imp 407 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ ¬ (𝑀 − 1)
∈ ℕ0) → 𝑀 = 0) |
22 | 21 | orcd 870 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ ¬ (𝑀 − 1)
∈ ℕ0) → (𝑀 = 0 ∨ 𝑀 = 𝐾)) |
23 | 22 | ex 413 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (¬ (𝑀 − 1)
∈ ℕ0 → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
24 | 23 | 3ad2ant1 1132 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬
(𝑀 − 1) ∈
ℕ0 → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
25 | 24 | com12 32 |
. . . . . . . 8
⊢ (¬
(𝑀 − 1) ∈
ℕ0 → ((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑀 ≤ 𝐾) → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
26 | | ioran 981 |
. . . . . . . . . . . 12
⊢ (¬
(𝑀 = 0 ∨ 𝑀 = 𝐾) ↔ (¬ 𝑀 = 0 ∧ ¬ 𝑀 = 𝐾)) |
27 | | nn1m1nn 11986 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ → (𝑀 = 1 ∨ (𝑀 − 1) ∈
ℕ)) |
28 | | df-ne 2946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑀 ≠ 𝐾 ↔ ¬ 𝑀 = 𝐾) |
29 | | necom 2999 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑀 ≠ 𝐾 ↔ 𝐾 ≠ 𝑀) |
30 | | nn0re 12234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
31 | 30 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑀 ≤ 𝐾) → 𝑀 ∈ ℝ) |
32 | | nn0re 12234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → 𝐾 ∈ ℝ) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑀 ≤ 𝐾) → 𝐾 ∈ ℝ) |
35 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑀 ≤ 𝐾) → 𝑀 ≤ 𝐾) |
36 | 31, 34, 35 | leltned 11120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑀 ≤ 𝐾) → (𝑀 < 𝐾 ↔ 𝐾 ≠ 𝑀)) |
37 | 29, 36 | bitr4id 290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑀 ≤ 𝐾) → (𝑀 ≠ 𝐾 ↔ 𝑀 < 𝐾)) |
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑀 ≤ 𝐾) ∧ 𝑀 = 1) → (𝑀 ≠ 𝐾 ↔ 𝑀 < 𝐾)) |
39 | | breq1 5082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑀 = 1 → (𝑀 < 𝐾 ↔ 1 < 𝐾)) |
40 | 39 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑀 = 1 ∧ 𝑀 < 𝐾) → 1 < 𝐾) |
41 | | 1red 10969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → 1 ∈ ℝ) |
42 | 41, 33, 41 | ltsub1d 11576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (1 < 𝐾 ↔ (1 − 1) < (𝐾 − 1))) |
43 | | 1m1e0 12037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (1
− 1) = 0 |
44 | 43 | breq1i 5086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((1
− 1) < (𝐾 −
1) ↔ 0 < (𝐾 −
1)) |
45 | | 1zzd 12343 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐾 ∈ ℕ0
→ 1 ∈ ℤ) |
46 | 3, 45 | zsubcld 12422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐾 ∈ ℕ0
→ (𝐾 − 1) ∈
ℤ) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 − 1) ∈ ℤ) |
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 0 < (𝐾 − 1)) → (𝐾 − 1) ∈ ℤ) |
49 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 0 < (𝐾 − 1)) → 0 < (𝐾 − 1)) |
50 | | elnnz 12321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐾 − 1) ∈ ℕ
↔ ((𝐾 − 1)
∈ ℤ ∧ 0 < (𝐾 − 1))) |
51 | 48, 49, 50 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 0 < (𝐾 − 1)) → (𝐾 − 1) ∈ ℕ) |
52 | 51 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (0 < (𝐾 − 1) → (𝐾 − 1) ∈
ℕ)) |
53 | 44, 52 | syl5bi 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((1 − 1) < (𝐾 − 1) → (𝐾 − 1) ∈
ℕ)) |
54 | 42, 53 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (1 < 𝐾 → (𝐾 − 1) ∈
ℕ)) |
55 | 40, 54 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝑀 = 1 ∧ 𝑀 < 𝐾) → (𝐾 − 1) ∈
ℕ)) |
56 | 55 | expd 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑀 = 1 → (𝑀 < 𝐾 → (𝐾 − 1) ∈
ℕ))) |
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑀 ≤ 𝐾) → (𝑀 = 1 → (𝑀 < 𝐾 → (𝐾 − 1) ∈
ℕ))) |
58 | 57 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑀 ≤ 𝐾) ∧ 𝑀 = 1) → (𝑀 < 𝐾 → (𝐾 − 1) ∈
ℕ)) |
59 | 38, 58 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑀 ≤ 𝐾) ∧ 𝑀 = 1) → (𝑀 ≠ 𝐾 → (𝐾 − 1) ∈
ℕ)) |
60 | 59 | exp31 420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑀 ≤ 𝐾 → (𝑀 = 1 → (𝑀 ≠ 𝐾 → (𝐾 − 1) ∈
ℕ)))) |
61 | 60 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑀 ≠ 𝐾 → (𝑀 ≤ 𝐾 → (𝑀 = 1 → ((𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝐾 − 1) ∈
ℕ)))) |
62 | 28, 61 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝑀 = 𝐾 → (𝑀 ≤ 𝐾 → (𝑀 = 1 → ((𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝐾 − 1) ∈
ℕ)))) |
63 | 62 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
𝑀 = 𝐾 → (𝑀 = 1 → (𝑀 ≤ 𝐾 → ((𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝐾 − 1) ∈
ℕ)))) |
64 | 63 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑀 = 1 → (𝑀 ≤ 𝐾 → (¬ 𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ)))) |
65 | 64 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐾 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → (𝑀 = 1 → (𝑀 ≤ 𝐾 → (¬ 𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
66 | 65 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ≤ 𝐾 → (𝑀 ∈ ℕ0 → (𝑀 = 1 → (𝐾 ∈ ℕ0 → (¬
𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
67 | 66 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 = 1 → (𝑀 ∈ ℕ0 → (𝑀 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
68 | 30 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑀 − 1) ∈ ℕ ∧
𝑀 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝑀 ∈
ℝ) |
69 | 32 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑀 − 1) ∈ ℕ ∧
𝑀 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℝ) |
70 | | 1red 10969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑀 − 1) ∈ ℕ ∧
𝑀 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 1 ∈
ℝ) |
71 | 68, 69, 70 | lesub1d 11574 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑀 − 1) ∈ ℕ ∧
𝑀 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → (𝑀 ≤ 𝐾 ↔ (𝑀 − 1) ≤ (𝐾 − 1))) |
72 | 3 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑀 − 1)
∈ ℕ ∧ 𝑀
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑀 − 1) ≤ (𝐾 − 1)) → 𝐾 ∈
ℤ) |
73 | | 1zzd 12343 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑀 − 1)
∈ ℕ ∧ 𝑀
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑀 − 1) ≤ (𝐾 − 1)) → 1 ∈
ℤ) |
74 | 72, 73 | zsubcld 12422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑀 − 1)
∈ ℕ ∧ 𝑀
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑀 − 1) ≤ (𝐾 − 1)) → (𝐾 − 1) ∈
ℤ) |
75 | | nngt0 11996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑀 − 1) ∈ ℕ
→ 0 < (𝑀 −
1)) |
76 | | 0red 10971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → 0 ∈ ℝ) |
77 | | peano2rem 11280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈
ℝ) |
78 | 30, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑀 ∈ ℕ0
→ (𝑀 − 1) ∈
ℝ) |
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑀 − 1) ∈ ℝ) |
80 | | peano2rem 11280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈
ℝ) |
81 | 32, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝐾 ∈ ℕ0
→ (𝐾 − 1) ∈
ℝ) |
82 | 81 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝐾 − 1) ∈ ℝ) |
83 | | ltletr 11059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((0
∈ ℝ ∧ (𝑀
− 1) ∈ ℝ ∧ (𝐾 − 1) ∈ ℝ) → ((0 <
(𝑀 − 1) ∧ (𝑀 − 1) ≤ (𝐾 − 1)) → 0 <
(𝐾 −
1))) |
84 | 76, 79, 82, 83 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → ((0 < (𝑀 − 1) ∧ (𝑀 − 1) ≤ (𝐾 − 1)) → 0 < (𝐾 − 1))) |
85 | 84 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑀 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → ((0 < (𝑀 − 1) ∧ (𝑀 − 1) ≤ (𝐾 − 1)) → 0 < (𝐾 − 1)))) |
86 | 85 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((0 <
(𝑀 − 1) ∧ (𝑀 − 1) ≤ (𝐾 − 1)) → (𝐾 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → 0 < (𝐾 − 1)))) |
87 | 86 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (0 <
(𝑀 − 1) →
((𝑀 − 1) ≤ (𝐾 − 1) → (𝐾 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → 0 < (𝐾 − 1))))) |
88 | 87 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (0 <
(𝑀 − 1) → (𝑀 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → ((𝑀 − 1) ≤ (𝐾 − 1) → 0 < (𝐾 − 1))))) |
89 | 75, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑀 − 1) ∈ ℕ
→ (𝑀 ∈
ℕ0 → (𝐾 ∈ ℕ0 → ((𝑀 − 1) ≤ (𝐾 − 1) → 0 < (𝐾 − 1))))) |
90 | 89 | imp41 426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑀 − 1)
∈ ℕ ∧ 𝑀
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑀 − 1) ≤ (𝐾 − 1)) → 0 <
(𝐾 −
1)) |
91 | 74, 90, 50 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑀 − 1)
∈ ℕ ∧ 𝑀
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑀 − 1) ≤ (𝐾 − 1)) → (𝐾 − 1) ∈
ℕ) |
92 | 91 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑀 − 1)
∈ ℕ ∧ 𝑀
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑀 − 1) ≤ (𝐾 − 1)) → (¬ 𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ)) |
93 | 92 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑀 − 1) ∈ ℕ ∧
𝑀 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → ((𝑀 − 1) ≤ (𝐾 − 1) → (¬ 𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))) |
94 | 71, 93 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 − 1) ∈ ℕ ∧
𝑀 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → (𝑀 ≤ 𝐾 → (¬ 𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))) |
95 | 94 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 − 1) ∈ ℕ ∧
𝑀 ∈
ℕ0) → (𝐾 ∈ ℕ0 → (𝑀 ≤ 𝐾 → (¬ 𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ)))) |
96 | 95 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 − 1) ∈ ℕ ∧
𝑀 ∈
ℕ0) → (𝑀 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ)))) |
97 | 96 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 − 1) ∈ ℕ
→ (𝑀 ∈
ℕ0 → (𝑀 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
98 | 67, 97 | jaoi 854 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 = 1 ∨ (𝑀 − 1) ∈ ℕ) → (𝑀 ∈ ℕ0
→ (𝑀 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
99 | 27, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ → (𝑀 ∈ ℕ0
→ (𝑀 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
100 | 13, 99 | sylbir 234 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≠ 0) →
(𝑀 ∈
ℕ0 → (𝑀 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
101 | 100 | ex 413 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ0
→ (𝑀 ≠ 0 →
(𝑀 ∈
ℕ0 → (𝑀 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ)))))) |
102 | 101 | pm2.43a 54 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
→ (𝑀 ≠ 0 →
(𝑀 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
103 | 102 | com24 95 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → (𝑀 ≤ 𝐾 → (𝑀 ≠ 0 → (¬ 𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
104 | 103 | 3imp 1110 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (𝑀 ≠ 0 → (¬ 𝑀 = 𝐾 → (𝐾 − 1) ∈
ℕ))) |
105 | 104 | com3l 89 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ≠ 0 → (¬ 𝑀 = 𝐾 → ((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑀 ≤ 𝐾) → (𝐾 − 1) ∈
ℕ))) |
106 | 14, 105 | sylbir 234 |
. . . . . . . . . . . . 13
⊢ (¬
𝑀 = 0 → (¬ 𝑀 = 𝐾 → ((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑀 ≤ 𝐾) → (𝐾 − 1) ∈
ℕ))) |
107 | 106 | imp 407 |
. . . . . . . . . . . 12
⊢ ((¬
𝑀 = 0 ∧ ¬ 𝑀 = 𝐾) → ((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑀 ≤ 𝐾) → (𝐾 − 1) ∈
ℕ)) |
108 | 26, 107 | sylbi 216 |
. . . . . . . . . . 11
⊢ (¬
(𝑀 = 0 ∨ 𝑀 = 𝐾) → ((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑀 ≤ 𝐾) → (𝐾 − 1) ∈
ℕ)) |
109 | 108 | com12 32 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬
(𝑀 = 0 ∨ 𝑀 = 𝐾) → (𝐾 − 1) ∈
ℕ)) |
110 | 109 | con1d 145 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬
(𝐾 − 1) ∈
ℕ → (𝑀 = 0 ∨
𝑀 = 𝐾))) |
111 | 110 | com12 32 |
. . . . . . . 8
⊢ (¬
(𝐾 − 1) ∈
ℕ → ((𝑀 ∈
ℕ0 ∧ 𝐾
∈ ℕ0 ∧ 𝑀 ≤ 𝐾) → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
112 | 30 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → 𝑀 ∈ ℝ) |
113 | 32 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → 𝐾 ∈ ℝ) |
114 | | 1red 10969 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → 1 ∈ ℝ) |
115 | 112, 113,
114 | 3jca 1127 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 1 ∈
ℝ)) |
116 | 115 | 3adant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 1 ∈
ℝ)) |
117 | | ltsub1 11463 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑀 <
𝐾 ↔ (𝑀 − 1) < (𝐾 − 1))) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (𝑀 < 𝐾 ↔ (𝑀 − 1) < (𝐾 − 1))) |
119 | 118 | bicomd 222 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → ((𝑀 − 1) < (𝐾 − 1) ↔ 𝑀 < 𝐾)) |
120 | 119 | notbid 318 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬
(𝑀 − 1) < (𝐾 − 1) ↔ ¬ 𝑀 < 𝐾)) |
121 | | eqlelt 11055 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑀 = 𝐾 ↔ (𝑀 ≤ 𝐾 ∧ ¬ 𝑀 < 𝐾))) |
122 | 30, 32, 121 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑀 = 𝐾 ↔ (𝑀 ≤ 𝐾 ∧ ¬ 𝑀 < 𝐾))) |
123 | 122 | biimpar 478 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) ∧ (𝑀 ≤ 𝐾 ∧ ¬ 𝑀 < 𝐾)) → 𝑀 = 𝐾) |
124 | 123 | olcd 871 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) ∧ (𝑀 ≤ 𝐾 ∧ ¬ 𝑀 < 𝐾)) → (𝑀 = 0 ∨ 𝑀 = 𝐾)) |
125 | 124 | exp43 437 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → (𝑀 ≤ 𝐾 → (¬ 𝑀 < 𝐾 → (𝑀 = 0 ∨ 𝑀 = 𝐾))))) |
126 | 125 | 3imp 1110 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬ 𝑀 < 𝐾 → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
127 | 120, 126 | sylbid 239 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬
(𝑀 − 1) < (𝐾 − 1) → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
128 | 127 | com12 32 |
. . . . . . . 8
⊢ (¬
(𝑀 − 1) < (𝐾 − 1) → ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
129 | 25, 111, 128 | 3jaoi 1426 |
. . . . . . 7
⊢ ((¬
(𝑀 − 1) ∈
ℕ0 ∨ ¬ (𝐾 − 1) ∈ ℕ ∨ ¬ (𝑀 − 1) < (𝐾 − 1)) → ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
130 | 12, 129 | sylbi 216 |
. . . . . 6
⊢ (¬
((𝑀 − 1) ∈
ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑀 − 1) < (𝐾 − 1)) → ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
131 | 130 | com12 32 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬
((𝑀 − 1) ∈
ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑀 − 1) < (𝐾 − 1)) → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
132 | 11, 131 | sylbid 239 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬
(𝑀 − 1) ∈
(0..^(𝐾 − 1)) →
(𝑀 = 0 ∨ 𝑀 = 𝐾))) |
133 | 8, 132 | sylbid 239 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
≤ 𝐾) → (¬ 𝑀 ∈ (1..^𝐾) → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
134 | 1, 133 | sylbi 216 |
. 2
⊢ (𝑀 ∈ (0...𝐾) → (¬ 𝑀 ∈ (1..^𝐾) → (𝑀 = 0 ∨ 𝑀 = 𝐾))) |
135 | 134 | imp 407 |
1
⊢ ((𝑀 ∈ (0...𝐾) ∧ ¬ 𝑀 ∈ (1..^𝐾)) → (𝑀 = 0 ∨ 𝑀 = 𝐾)) |