Proof of Theorem pfxccatin12lem1
| Step | Hyp | Ref
| Expression |
| 1 | | elfz2 13554 |
. . . . 5
⊢ (𝑀 ∈ (0...𝐿) ↔ ((0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (0 ≤
𝑀 ∧ 𝑀 ≤ 𝐿))) |
| 2 | | zsubcl 12659 |
. . . . . . 7
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐿 − 𝑀) ∈ ℤ) |
| 3 | 2 | 3adant1 1131 |
. . . . . 6
⊢ ((0
∈ ℤ ∧ 𝐿
∈ ℤ ∧ 𝑀
∈ ℤ) → (𝐿
− 𝑀) ∈
ℤ) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ (((0
∈ ℤ ∧ 𝐿
∈ ℤ ∧ 𝑀
∈ ℤ) ∧ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝐿)) → (𝐿 − 𝑀) ∈ ℤ) |
| 5 | 1, 4 | sylbi 217 |
. . . 4
⊢ (𝑀 ∈ (0...𝐿) → (𝐿 − 𝑀) ∈ ℤ) |
| 6 | 5 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐿 − 𝑀) ∈ ℤ) |
| 7 | | elfzonelfzo 13808 |
. . 3
⊢ ((𝐿 − 𝑀) ∈ ℤ → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)))) |
| 8 | 6, 7 | syl 17 |
. 2
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)))) |
| 9 | | elfz2nn0 13658 |
. . . . . . . 8
⊢ (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿)) |
| 10 | | nn0cn 12536 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) |
| 11 | | nn0cn 12536 |
. . . . . . . . . 10
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℂ) |
| 12 | | elfzelz 13564 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ (𝐿...𝑋) → 𝑁 ∈ ℤ) |
| 13 | | zcn 12618 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
| 14 | | subcl 11507 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐿 − 𝑀) ∈ ℂ) |
| 15 | 14 | ancoms 458 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐿 − 𝑀) ∈ ℂ) |
| 16 | 15 | addridd 11461 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → ((𝐿 − 𝑀) + 0) = (𝐿 − 𝑀)) |
| 17 | 16 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐿 − 𝑀) = ((𝐿 − 𝑀) + 0)) |
| 18 | 17 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → (𝐿 − 𝑀) = ((𝐿 − 𝑀) + 0)) |
| 19 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → 𝐿 ∈
ℂ) |
| 20 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → 𝑀 ∈
ℂ) |
| 21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → 𝑀 ∈
ℂ) |
| 22 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → 𝑁 ∈
ℂ) |
| 23 | 19, 21, 22 | npncan3d 11656 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀)) |
| 24 | 23 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → (𝑁 − 𝑀) = ((𝐿 − 𝑀) + (𝑁 − 𝐿))) |
| 25 | 18, 24 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))) |
| 26 | 25 | ex 412 |
. . . . . . . . . . . 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 1133 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → (𝑁 ∈ (𝐿...𝑋) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
| 31 | 9, 30 | sylbi 217 |
. . . . . . 7
⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...𝑋) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
| 32 | 31 | imp 406 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) = (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))) |
| 33 | 32 | eleq2d 2827 |
. . . . 5
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) ↔ 𝐾 ∈ (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
| 34 | 33 | biimpa 476 |
. . . 4
⊢ (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) ∧ 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀))) → 𝐾 ∈ (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))) |
| 35 | | 0zd 12625 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → 0 ∈ ℤ) |
| 36 | | elfz2 13554 |
. . . . . . . 8
⊢ (𝑁 ∈ (𝐿...𝑋) ↔ ((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋))) |
| 37 | | zsubcl 12659 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ) |
| 38 | 37 | ancoms 458 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ) |
| 39 | 38 | 3adant2 1132 |
. . . . . . . . 9
⊢ ((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ) |
| 40 | 39 | adantr 480 |
. . . . . . . 8
⊢ (((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋)) → (𝑁 − 𝐿) ∈ ℤ) |
| 41 | 36, 40 | sylbi 217 |
. . . . . . 7
⊢ (𝑁 ∈ (𝐿...𝑋) → (𝑁 − 𝐿) ∈ ℤ) |
| 42 | 41 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝑁 − 𝐿) ∈ ℤ) |
| 43 | 6, 35, 42 | 3jca 1129 |
. . . . 5
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐿 − 𝑀) ∈ ℤ ∧ 0 ∈ ℤ
∧ (𝑁 − 𝐿) ∈
ℤ)) |
| 44 | 43 | adantr 480 |
. . . 4
⊢ (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) ∧ 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀))) → ((𝐿 − 𝑀) ∈ ℤ ∧ 0 ∈ ℤ
∧ (𝑁 − 𝐿) ∈
ℤ)) |
| 45 | | fzosubel2 13764 |
. . . 4
⊢ ((𝐾 ∈ (((𝐿 − 𝑀) + 0)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))) ∧ ((𝐿 − 𝑀) ∈ ℤ ∧ 0 ∈ ℤ
∧ (𝑁 − 𝐿) ∈ ℤ)) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿))) |
| 46 | 34, 44, 45 | syl2anc 584 |
. . 3
⊢ (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) ∧ 𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿))) |
| 47 | 46 | ex 412 |
. 2
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿)))) |
| 48 | 8, 47 | syld 47 |
1
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿)))) |