Proof of Theorem elfznelfzo
Step | Hyp | Ref
| Expression |
1 | | elfz2nn0 12300 |
. . 3
⊢ (𝑦 ∈ (0...𝐾) ↔ (𝑦 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑦 ≤ 𝐾)) |
2 | | nn0z 11277 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) |
3 | | nn0z 11277 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
4 | 2, 3 | anim12i 588 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑦 ∈ ℤ ∧ 𝐾 ∈ ℤ)) |
5 | 4 | 3adant3 1074 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (𝑦 ∈ ℤ ∧ 𝐾 ∈
ℤ)) |
6 | | elfzom1b 12433 |
. . . . . 6
⊢ ((𝑦 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑦 ∈ (1..^𝐾) ↔ (𝑦 − 1) ∈ (0..^(𝐾 − 1)))) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (𝑦 ∈ (1..^𝐾) ↔ (𝑦 − 1) ∈ (0..^(𝐾 − 1)))) |
8 | 7 | notbid 307 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (¬ 𝑦 ∈ (1..^𝐾) ↔ ¬ (𝑦 − 1) ∈ (0..^(𝐾 − 1)))) |
9 | | elfzo0 12376 |
. . . . . . 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 307 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (¬
(𝑦 − 1) ∈
(0..^(𝐾 − 1)) ↔
¬ ((𝑦 − 1) ∈
ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑦 − 1) < (𝐾 − 1)))) |
12 | | 3ianor 1048 |
. . . . . . 7
⊢ (¬
((𝑦 − 1) ∈
ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑦 − 1) < (𝐾 − 1)) ↔ (¬
(𝑦 − 1) ∈
ℕ0 ∨ ¬ (𝐾 − 1) ∈ ℕ ∨ ¬ (𝑦 − 1) < (𝐾 − 1))) |
13 | | elnnne0 11183 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ ↔ (𝑦 ∈ ℕ0
∧ 𝑦 ≠
0)) |
14 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ≠ 0 ↔ ¬ 𝑦 = 0) |
15 | 14 | anbi2i 726 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ0
∧ 𝑦 ≠ 0) ↔
(𝑦 ∈
ℕ0 ∧ ¬ 𝑦 = 0)) |
16 | 13, 15 | bitr2i 264 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ0
∧ ¬ 𝑦 = 0) ↔
𝑦 ∈
ℕ) |
17 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 − 1) ∈
ℕ0) |
18 | 16, 17 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ0
∧ ¬ 𝑦 = 0) →
(𝑦 − 1) ∈
ℕ0) |
19 | 18 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ (¬ 𝑦 = 0 →
(𝑦 − 1) ∈
ℕ0)) |
20 | 19 | con1d 138 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ0
→ (¬ (𝑦 − 1)
∈ ℕ0 → 𝑦 = 0)) |
21 | 20 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ¬ (𝑦 − 1)
∈ ℕ0) → 𝑦 = 0) |
22 | 21 | orcd 406 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ¬ (𝑦 − 1)
∈ ℕ0) → (𝑦 = 0 ∨ 𝑦 = 𝐾)) |
23 | 22 | ex 449 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ (¬ (𝑦 − 1)
∈ ℕ0 → (𝑦 = 0 ∨ 𝑦 = 𝐾))) |
24 | 23 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (¬
(𝑦 − 1) ∈
ℕ0 → (𝑦 = 0 ∨ 𝑦 = 𝐾))) |
25 | 24 | com12 32 |
. . . . . . . 8
⊢ (¬
(𝑦 − 1) ∈
ℕ0 → ((𝑦 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑦 ≤ 𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾))) |
26 | | ioran 510 |
. . . . . . . . . . . 12
⊢ (¬
(𝑦 = 0 ∨ 𝑦 = 𝐾) ↔ (¬ 𝑦 = 0 ∧ ¬ 𝑦 = 𝐾)) |
27 | | nn1m1nn 10917 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℕ → (𝑦 = 1 ∨ (𝑦 − 1) ∈ ℕ)) |
28 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ≠ 𝐾 ↔ ¬ 𝑦 = 𝐾) |
29 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℝ) |
30 | 29 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 𝑦 ≤ 𝐾) → 𝑦 ∈ ℝ) |
31 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → 𝐾 ∈ ℝ) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 𝑦 ≤ 𝐾) → 𝐾 ∈ ℝ) |
34 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 𝑦 ≤ 𝐾) → 𝑦 ≤ 𝐾) |
35 | 30, 33, 34 | leltned 10069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 𝑦 ≤ 𝐾) → (𝑦 < 𝐾 ↔ 𝐾 ≠ 𝑦)) |
36 | | necom 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ≠ 𝐾 ↔ 𝐾 ≠ 𝑦) |
37 | 35, 36 | syl6rbbr 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 𝑦 ≤ 𝐾) → (𝑦 ≠ 𝐾 ↔ 𝑦 < 𝐾)) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 𝑦 ≤ 𝐾) ∧ 𝑦 = 1) → (𝑦 ≠ 𝐾 ↔ 𝑦 < 𝐾)) |
39 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 = 1 → (𝑦 < 𝐾 ↔ 1 < 𝐾)) |
40 | 39 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑦 = 1 ∧ 𝑦 < 𝐾) → 1 < 𝐾) |
41 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → 1 ∈ ℝ) |
42 | 41, 32, 41 | ltsub1d 10515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (1 < 𝐾 ↔ (1 − 1) < (𝐾 − 1))) |
43 | | 1m1e0 10966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (1
− 1) = 0 |
44 | 43 | breq1i 4590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((1
− 1) < (𝐾 −
1) ↔ 0 < (𝐾 −
1)) |
45 | | 1zzd 11285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐾 ∈ ℕ0
→ 1 ∈ ℤ) |
46 | 3, 45 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐾 ∈ ℕ0
→ (𝐾 − 1) ∈
ℤ) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝐾 − 1) ∈ ℤ) |
48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 0 < (𝐾 − 1)) → (𝐾 − 1) ∈ ℤ) |
49 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 0 < (𝐾 − 1)) → 0 < (𝐾 − 1)) |
50 | | elnnz 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐾 − 1) ∈ ℕ
↔ ((𝐾 − 1)
∈ ℤ ∧ 0 < (𝐾 − 1))) |
51 | 48, 49, 50 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 0 < (𝐾 − 1)) → (𝐾 − 1) ∈ ℕ) |
52 | 51 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (0 < (𝐾 − 1) → (𝐾 − 1) ∈
ℕ)) |
53 | 44, 52 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → ((1 − 1) < (𝐾 − 1) → (𝐾 − 1) ∈
ℕ)) |
54 | 42, 53 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (1 < 𝐾 → (𝐾 − 1) ∈
ℕ)) |
55 | 40, 54 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → ((𝑦 = 1 ∧ 𝑦 < 𝐾) → (𝐾 − 1) ∈
ℕ)) |
56 | 55 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑦 = 1 → (𝑦 < 𝐾 → (𝐾 − 1) ∈
ℕ))) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 𝑦 ≤ 𝐾) → (𝑦 = 1 → (𝑦 < 𝐾 → (𝐾 − 1) ∈
ℕ))) |
58 | 57 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 𝑦 ≤ 𝐾) ∧ 𝑦 = 1) → (𝑦 < 𝐾 → (𝐾 − 1) ∈
ℕ)) |
59 | 38, 58 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) ∧ 𝑦 ≤ 𝐾) ∧ 𝑦 = 1) → (𝑦 ≠ 𝐾 → (𝐾 − 1) ∈
ℕ)) |
60 | 59 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑦 ≤ 𝐾 → (𝑦 = 1 → (𝑦 ≠ 𝐾 → (𝐾 − 1) ∈
ℕ)))) |
61 | 60 | com14 94 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ≠ 𝐾 → (𝑦 ≤ 𝐾 → (𝑦 = 1 → ((𝐾 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝐾 − 1) ∈
ℕ)))) |
62 | 28, 61 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝑦 = 𝐾 → (𝑦 ≤ 𝐾 → (𝑦 = 1 → ((𝐾 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝐾 − 1) ∈
ℕ)))) |
63 | 62 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
𝑦 = 𝐾 → (𝑦 = 1 → (𝑦 ≤ 𝐾 → ((𝐾 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)
→ (𝐾 − 1) ∈
ℕ)))) |
64 | 63 | com14 94 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐾 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑦 = 1 → (𝑦 ≤ 𝐾 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ)))) |
65 | 64 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐾 ∈ ℕ0
→ (𝑦 ∈
ℕ0 → (𝑦 = 1 → (𝑦 ≤ 𝐾 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
66 | 65 | com14 94 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ≤ 𝐾 → (𝑦 ∈ ℕ0 → (𝑦 = 1 → (𝐾 ∈ ℕ0 → (¬
𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
67 | 66 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 1 → (𝑦 ∈ ℕ0 → (𝑦 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
68 | 29 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑦 − 1) ∈ ℕ ∧
𝑦 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝑦 ∈
ℝ) |
69 | 31 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑦 − 1) ∈ ℕ ∧
𝑦 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℝ) |
70 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑦 − 1) ∈ ℕ ∧
𝑦 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 1 ∈
ℝ) |
71 | 68, 69, 70 | lesub1d 10513 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑦 − 1) ∈ ℕ ∧
𝑦 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → (𝑦 ≤ 𝐾 ↔ (𝑦 − 1) ≤ (𝐾 − 1))) |
72 | 3 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑦 − 1)
∈ ℕ ∧ 𝑦
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 𝐾 ∈
ℤ) |
73 | | 1zzd 11285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑦 − 1)
∈ ℕ ∧ 𝑦
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 1 ∈
ℤ) |
74 | 72, 73 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑦 − 1)
∈ ℕ ∧ 𝑦
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → (𝐾 − 1) ∈
ℤ) |
75 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑦 − 1) ∈ ℕ
→ 0 < (𝑦 −
1)) |
76 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → 0 ∈ ℝ) |
77 | | peano2rem 10227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑦 ∈ ℝ → (𝑦 − 1) ∈
ℝ) |
78 | 29, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 ∈ ℕ0
→ (𝑦 − 1) ∈
ℝ) |
79 | 78 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑦 − 1) ∈ ℝ) |
80 | | peano2rem 10227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈
ℝ) |
81 | 31, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝐾 ∈ ℕ0
→ (𝐾 − 1) ∈
ℝ) |
82 | 81 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝐾 − 1) ∈ ℝ) |
83 | | ltletr 10008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((0
∈ ℝ ∧ (𝑦
− 1) ∈ ℝ ∧ (𝐾 − 1) ∈ ℝ) → ((0 <
(𝑦 − 1) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 0 <
(𝐾 −
1))) |
84 | 76, 79, 82, 83 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → ((0 < (𝑦 − 1) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 0 < (𝐾 − 1))) |
85 | 84 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → ((0 < (𝑦 − 1) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 0 < (𝐾 − 1)))) |
86 | 85 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((0 <
(𝑦 − 1) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → (𝐾 ∈ ℕ0
→ (𝑦 ∈
ℕ0 → 0 < (𝐾 − 1)))) |
87 | 86 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (0 <
(𝑦 − 1) →
((𝑦 − 1) ≤ (𝐾 − 1) → (𝐾 ∈ ℕ0
→ (𝑦 ∈
ℕ0 → 0 < (𝐾 − 1))))) |
88 | 87 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑦 − 1)
∈ ℕ ∧ 𝑦
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 0 <
(𝐾 −
1)) |
91 | 74, 90, 50 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑦 − 1)
∈ ℕ ∧ 𝑦
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → (𝐾 − 1) ∈
ℕ) |
92 | 91 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑦 − 1)
∈ ℕ ∧ 𝑦
∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ)) |
93 | 92 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑦 − 1) ∈ ℕ ∧
𝑦 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → ((𝑦 − 1) ≤ (𝐾 − 1) → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))) |
94 | 71, 93 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑦 − 1) ∈ ℕ ∧
𝑦 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → (𝑦 ≤ 𝐾 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))) |
95 | 94 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 − 1) ∈ ℕ ∧
𝑦 ∈
ℕ0) → (𝐾 ∈ ℕ0 → (𝑦 ≤ 𝐾 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ)))) |
96 | 95 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 − 1) ∈ ℕ ∧
𝑦 ∈
ℕ0) → (𝑦 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ)))) |
97 | 96 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 − 1) ∈ ℕ
→ (𝑦 ∈
ℕ0 → (𝑦 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
98 | 67, 97 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 = 1 ∨ (𝑦 − 1) ∈ ℕ) → (𝑦 ∈ ℕ0
→ (𝑦 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
99 | 27, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℕ0
→ (𝑦 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
100 | 13, 99 | sylbir 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ0
∧ 𝑦 ≠ 0) →
(𝑦 ∈
ℕ0 → (𝑦 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
101 | 100 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ0
→ (𝑦 ≠ 0 →
(𝑦 ∈
ℕ0 → (𝑦 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ)))))) |
102 | 101 | pm2.43a 52 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ0
→ (𝑦 ≠ 0 →
(𝑦 ≤ 𝐾 → (𝐾 ∈ ℕ0 → (¬
𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
103 | 102 | com24 93 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → (𝑦 ≤ 𝐾 → (𝑦 ≠ 0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))))) |
104 | 103 | 3imp 1249 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (𝑦 ≠ 0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈
ℕ))) |
105 | 104 | com3l 87 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ≠ 0 → (¬ 𝑦 = 𝐾 → ((𝑦 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑦 ≤ 𝐾) → (𝐾 − 1) ∈
ℕ))) |
106 | 14, 105 | sylbir 224 |
. . . . . . . . . . . . 13
⊢ (¬
𝑦 = 0 → (¬ 𝑦 = 𝐾 → ((𝑦 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑦 ≤ 𝐾) → (𝐾 − 1) ∈
ℕ))) |
107 | 106 | imp 444 |
. . . . . . . . . . . 12
⊢ ((¬
𝑦 = 0 ∧ ¬ 𝑦 = 𝐾) → ((𝑦 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑦 ≤ 𝐾) → (𝐾 − 1) ∈
ℕ)) |
108 | 26, 107 | sylbi 206 |
. . . . . . . . . . 11
⊢ (¬
(𝑦 = 0 ∨ 𝑦 = 𝐾) → ((𝑦 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝑦 ≤ 𝐾) → (𝐾 − 1) ∈
ℕ)) |
109 | 108 | com12 32 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (¬
(𝑦 = 0 ∨ 𝑦 = 𝐾) → (𝐾 − 1) ∈
ℕ)) |
110 | 109 | con1d 138 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (¬
(𝐾 − 1) ∈
ℕ → (𝑦 = 0 ∨
𝑦 = 𝐾))) |
111 | 110 | com12 32 |
. . . . . . . 8
⊢ (¬
(𝐾 − 1) ∈
ℕ → ((𝑦 ∈
ℕ0 ∧ 𝐾
∈ ℕ0 ∧ 𝑦 ≤ 𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾))) |
112 | 29 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → 𝑦 ∈ ℝ) |
113 | 31 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → 𝐾 ∈ ℝ) |
114 | | 1red 9934 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → 1 ∈ ℝ) |
115 | 112, 113,
114 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 1 ∈
ℝ)) |
116 | 115 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 1 ∈
ℝ)) |
117 | | ltsub1 10403 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑦 <
𝐾 ↔ (𝑦 − 1) < (𝐾 − 1))) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (𝑦 < 𝐾 ↔ (𝑦 − 1) < (𝐾 − 1))) |
119 | 118 | bicomd 212 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → ((𝑦 − 1) < (𝐾 − 1) ↔ 𝑦 < 𝐾)) |
120 | 119 | notbid 307 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (¬
(𝑦 − 1) < (𝐾 − 1) ↔ ¬ 𝑦 < 𝐾)) |
121 | | eqlelt 10004 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑦 = 𝐾 ↔ (𝑦 ≤ 𝐾 ∧ ¬ 𝑦 < 𝐾))) |
122 | 29, 31, 121 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑦 = 𝐾 ↔ (𝑦 ≤ 𝐾 ∧ ¬ 𝑦 < 𝐾))) |
123 | 122 | biimpar 501 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) ∧ (𝑦 ≤ 𝐾 ∧ ¬ 𝑦 < 𝐾)) → 𝑦 = 𝐾) |
124 | 123 | olcd 407 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) ∧ (𝑦 ≤ 𝐾 ∧ ¬ 𝑦 < 𝐾)) → (𝑦 = 0 ∨ 𝑦 = 𝐾)) |
125 | 124 | exp43 638 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → (𝑦 ≤ 𝐾 → (¬ 𝑦 < 𝐾 → (𝑦 = 0 ∨ 𝑦 = 𝐾))))) |
126 | 125 | 3imp 1249 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (¬ 𝑦 < 𝐾 → (𝑦 = 0 ∨ 𝑦 = 𝐾))) |
127 | 120, 126 | sylbid 229 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (¬
(𝑦 − 1) < (𝐾 − 1) → (𝑦 = 0 ∨ 𝑦 = 𝐾))) |
128 | 127 | com12 32 |
. . . . . . . 8
⊢ (¬
(𝑦 − 1) < (𝐾 − 1) → ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾))) |
129 | 25, 111, 128 | 3jaoi 1383 |
. . . . . . 7
⊢ ((¬
(𝑦 − 1) ∈
ℕ0 ∨ ¬ (𝐾 − 1) ∈ ℕ ∨ ¬ (𝑦 − 1) < (𝐾 − 1)) → ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾))) |
130 | 12, 129 | sylbi 206 |
. . . . . 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 229 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (¬
(𝑦 − 1) ∈
(0..^(𝐾 − 1)) →
(𝑦 = 0 ∨ 𝑦 = 𝐾))) |
133 | 8, 132 | sylbid 229 |
. . 3
⊢ ((𝑦 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑦
≤ 𝐾) → (¬ 𝑦 ∈ (1..^𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾))) |
134 | 1, 133 | sylbi 206 |
. 2
⊢ (𝑦 ∈ (0...𝐾) → (¬ 𝑦 ∈ (1..^𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾))) |
135 | 134 | imp 444 |
1
⊢ ((𝑦 ∈ (0...𝐾) ∧ ¬ 𝑦 ∈ (1..^𝐾)) → (𝑦 = 0 ∨ 𝑦 = 𝐾)) |