Proof of Theorem swrdccatin12lem2b
Step | Hyp | Ref
| Expression |
1 | | elfz2 12204 |
. . . . 5
⊢ (𝑀 ∈ (0...𝐿) ↔ ((0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (0 ≤
𝑀 ∧ 𝑀 ≤ 𝐿))) |
2 | | zsubcl 11296 |
. . . . . . 7
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐿 − 𝑀) ∈ ℤ) |
3 | 2 | 3adant1 1072 |
. . . . . 6
⊢ ((0
∈ ℤ ∧ 𝐿
∈ ℤ ∧ 𝑀
∈ ℤ) → (𝐿
− 𝑀) ∈
ℤ) |
4 | 3 | adantr 480 |
. . . . 5
⊢ (((0
∈ ℤ ∧ 𝐿
∈ ℤ ∧ 𝑀
∈ ℤ) ∧ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝐿)) → (𝐿 − 𝑀) ∈ ℤ) |
5 | 1, 4 | sylbi 206 |
. . . 4
⊢ (𝑀 ∈ (0...𝐿) → (𝐿 − 𝑀) ∈ ℤ) |
6 | 5 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐿 − 𝑀) ∈ ℤ) |
7 | | elfzonelfzo 12436 |
. . 3
⊢ ((𝐿 − 𝑀) ∈ ℤ → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)))) |
8 | 6, 7 | syl 17 |
. 2
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)))) |
9 | | elfz2nn0 12300 |
. . . . . . . 8
⊢ (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿)) |
10 | | nn0cn 11179 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) |
11 | | nn0cn 11179 |
. . . . . . . . . 10
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℂ) |
12 | | elfzelz 12213 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ (𝐿...𝑋) → 𝑁 ∈ ℤ) |
13 | | zcn 11259 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
14 | | subcl 10159 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐿 − 𝑀) ∈ ℂ) |
15 | 14 | ancoms 468 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐿 − 𝑀) ∈ ℂ) |
16 | 15 | addid1d 10115 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → ((𝐿 − 𝑀) + 0) = (𝐿 − 𝑀)) |
17 | 16 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐿 − 𝑀) = ((𝐿 − 𝑀) + 0)) |
18 | 17 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → (𝐿 − 𝑀) = ((𝐿 − 𝑀) + 0)) |
19 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → 𝐿 ∈
ℂ) |
20 | | simpl 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → 𝑀 ∈
ℂ) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → 𝑀 ∈
ℂ) |
22 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → 𝑁 ∈
ℂ) |
23 | 19, 21, 22 | npncan3d 10307 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀)) |
24 | | subcl 10159 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝑁 − 𝐿) ∈ ℂ) |
25 | | subid1 10180 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 𝐿) ∈ ℂ → ((𝑁 − 𝐿) − 0) = (𝑁 − 𝐿)) |
26 | 25 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 − 𝐿) ∈ ℂ → (𝑁 − 𝐿) = ((𝑁 − 𝐿) − 0)) |
27 | 24, 26 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝑁 − 𝐿) = ((𝑁 − 𝐿) − 0)) |
28 | 27 | adantrl 748 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → (𝑁 − 𝐿) = ((𝑁 − 𝐿) − 0)) |
29 | 28 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = ((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0))) |
30 | 23, 29 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → (𝑁 − 𝑀) = ((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0))) |
31 | 18, 30 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0)))) |
32 | 31 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0))))) |
33 | 12, 13, 32 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (𝐿...𝑋) → ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0))))) |
34 | 33 | com12 32 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝑁 ∈ (𝐿...𝑋) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0))))) |
35 | 10, 11, 34 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑁 ∈ (𝐿...𝑋) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0))))) |
36 | 35 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → (𝑁 ∈ (𝐿...𝑋) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0))))) |
37 | 9, 36 | sylbi 206 |
. . . . . . 7
⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...𝑋) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0))))) |
38 | 37 | imp 444 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0)))) |
39 | 38 | eleq2d 2673 |
. . . . 5
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) ↔ 𝐾 ∈ (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0))))) |
40 | 39 | biimpa 500 |
. . . 4
⊢ (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) ∧ 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀))) → 𝐾 ∈ (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0)))) |
41 | | 0zd 11266 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → 0 ∈ ℤ) |
42 | | elfz2 12204 |
. . . . . . . 8
⊢ (𝑁 ∈ (𝐿...𝑋) ↔ ((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋))) |
43 | | zsubcl 11296 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ) |
44 | 43 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ) |
45 | | 0zd 11266 |
. . . . . . . . . . 11
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈
ℤ) |
46 | 44, 45 | zsubcld 11363 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 − 𝐿) − 0) ∈
ℤ) |
47 | 46 | 3adant2 1073 |
. . . . . . . . 9
⊢ ((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 − 𝐿) − 0) ∈
ℤ) |
48 | 47 | adantr 480 |
. . . . . . . 8
⊢ (((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋)) → ((𝑁 − 𝐿) − 0) ∈
ℤ) |
49 | 42, 48 | sylbi 206 |
. . . . . . 7
⊢ (𝑁 ∈ (𝐿...𝑋) → ((𝑁 − 𝐿) − 0) ∈
ℤ) |
50 | 49 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝑁 − 𝐿) − 0) ∈
ℤ) |
51 | 6, 41, 50 | 3jca 1235 |
. . . . 5
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐿 − 𝑀) ∈ ℤ ∧ 0 ∈ ℤ
∧ ((𝑁 − 𝐿) − 0) ∈
ℤ)) |
52 | 51 | adantr 480 |
. . . 4
⊢ (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) ∧ 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀))) → ((𝐿 − 𝑀) ∈ ℤ ∧ 0 ∈ ℤ
∧ ((𝑁 − 𝐿) − 0) ∈
ℤ)) |
53 | | fzosubel2 12395 |
. . . 4
⊢ ((𝐾 ∈ (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + ((𝑁 − 𝐿) − 0))) ∧ ((𝐿 − 𝑀) ∈ ℤ ∧ 0 ∈ ℤ
∧ ((𝑁 − 𝐿) − 0) ∈ ℤ))
→ (𝐾 − (𝐿 − 𝑀)) ∈ (0..^((𝑁 − 𝐿) − 0))) |
54 | 40, 52, 53 | syl2anc 691 |
. . 3
⊢ (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) ∧ 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^((𝑁 − 𝐿) − 0))) |
55 | 54 | ex 449 |
. 2
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^((𝑁 − 𝐿) − 0)))) |
56 | 8, 55 | syld 46 |
1
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^((𝑁 − 𝐿) − 0)))) |