Proof of Theorem pfxccatin12lem1
Step | Hyp | Ref
| Expression |
1 | | elfz2 13245 |
. . . . 5
⊢ (𝑀 ∈ (0...𝐿) ↔ ((0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (0 ≤
𝑀 ∧ 𝑀 ≤ 𝐿))) |
2 | | zsubcl 12362 |
. . . . . . 7
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐿 − 𝑀) ∈ ℤ) |
3 | 2 | 3adant1 1129 |
. . . . . 6
⊢ ((0
∈ ℤ ∧ 𝐿
∈ ℤ ∧ 𝑀
∈ ℤ) → (𝐿
− 𝑀) ∈
ℤ) |
4 | 3 | adantr 481 |
. . . . 5
⊢ (((0
∈ ℤ ∧ 𝐿
∈ ℤ ∧ 𝑀
∈ ℤ) ∧ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝐿)) → (𝐿 − 𝑀) ∈ ℤ) |
5 | 1, 4 | sylbi 216 |
. . . 4
⊢ (𝑀 ∈ (0...𝐿) → (𝐿 − 𝑀) ∈ ℤ) |
6 | 5 | adantr 481 |
. . 3
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐿 − 𝑀) ∈ ℤ) |
7 | | elfzonelfzo 13487 |
. . 3
⊢ ((𝐿 − 𝑀) ∈ ℤ → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)))) |
8 | 6, 7 | syl 17 |
. 2
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)))) |
9 | | elfz2nn0 13346 |
. . . . . . . 8
⊢ (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿)) |
10 | | nn0cn 12243 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) |
11 | | nn0cn 12243 |
. . . . . . . . . 10
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℂ) |
12 | | elfzelz 13255 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ (𝐿...𝑋) → 𝑁 ∈ ℤ) |
13 | | zcn 12324 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
14 | | subcl 11220 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐿 − 𝑀) ∈ ℂ) |
15 | 14 | ancoms 459 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐿 − 𝑀) ∈ ℂ) |
16 | 15 | addid1d 11175 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → ((𝐿 − 𝑀) + 0) = (𝐿 − 𝑀)) |
17 | 16 | eqcomd 2746 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐿 − 𝑀) = ((𝐿 − 𝑀) + 0)) |
18 | 17 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → (𝐿 − 𝑀) = ((𝐿 − 𝑀) + 0)) |
19 | | simprr 770 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → 𝐿 ∈
ℂ) |
20 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → 𝑀 ∈
ℂ) |
21 | 20 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → 𝑀 ∈
ℂ) |
22 | | simpl 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → 𝑁 ∈
ℂ) |
23 | 19, 21, 22 | npncan3d 11368 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀)) |
24 | 23 | eqcomd 2746 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → (𝑁 − 𝑀) = ((𝐿 − 𝑀) + (𝑁 − 𝐿))) |
25 | 18, 24 | oveq12d 7289 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))) |
26 | 25 | ex 413 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
27 | 12, 13, 26 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (𝐿...𝑋) → ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
28 | 27 | com12 32 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝑁 ∈ (𝐿...𝑋) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
29 | 10, 11, 28 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑁 ∈ (𝐿...𝑋) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
30 | 29 | 3adant3 1131 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → (𝑁 ∈ (𝐿...𝑋) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
31 | 9, 30 | sylbi 216 |
. . . . . . 7
⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...𝑋) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
32 | 31 | imp 407 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))) |
33 | 32 | eleq2d 2826 |
. . . . 5
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) ↔ 𝐾 ∈ (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
34 | 33 | biimpa 477 |
. . . 4
⊢ (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) ∧ 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀))) → 𝐾 ∈ (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))) |
35 | | 0zd 12331 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → 0 ∈ ℤ) |
36 | | elfz2 13245 |
. . . . . . . 8
⊢ (𝑁 ∈ (𝐿...𝑋) ↔ ((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋))) |
37 | | zsubcl 12362 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ) |
38 | 37 | ancoms 459 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ) |
39 | 38 | 3adant2 1130 |
. . . . . . . . 9
⊢ ((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ) |
40 | 39 | adantr 481 |
. . . . . . . 8
⊢ (((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋)) → (𝑁 − 𝐿) ∈ ℤ) |
41 | 36, 40 | sylbi 216 |
. . . . . . 7
⊢ (𝑁 ∈ (𝐿...𝑋) → (𝑁 − 𝐿) ∈ ℤ) |
42 | 41 | adantl 482 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝑁 − 𝐿) ∈ ℤ) |
43 | 6, 35, 42 | 3jca 1127 |
. . . . 5
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐿 − 𝑀) ∈ ℤ ∧ 0 ∈ ℤ
∧ (𝑁 − 𝐿) ∈
ℤ)) |
44 | 43 | adantr 481 |
. . . 4
⊢ (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) ∧ 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀))) → ((𝐿 − 𝑀) ∈ ℤ ∧ 0 ∈ ℤ
∧ (𝑁 − 𝐿) ∈
ℤ)) |
45 | | fzosubel2 13445 |
. . . 4
⊢ ((𝐾 ∈ (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))) ∧ ((𝐿 − 𝑀) ∈ ℤ ∧ 0 ∈ ℤ
∧ (𝑁 − 𝐿) ∈ ℤ)) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿))) |
46 | 34, 44, 45 | syl2anc 584 |
. . 3
⊢ (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) ∧ 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿))) |
47 | 46 | ex 413 |
. 2
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿)))) |
48 | 8, 47 | syld 47 |
1
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿)))) |