Proof of Theorem pfxccatin12lem2a
| 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 |  | elfzoelz 13699 | . . . 4
⊢ (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) → 𝐾 ∈ ℤ) | 
| 10 |  | elfzelz 13564 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (𝐿...𝑋) → 𝑁 ∈ ℤ) | 
| 11 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝐿 ∈
ℤ) | 
| 12 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝑁 ∈
ℤ) | 
| 13 | 11, 12 | anim12i 613 | . . . . . . . . . . . . . . . 16
⊢ (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐿 ∈ ℤ ∧ 𝑁 ∈
ℤ)) | 
| 14 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑀 ∈
ℤ) | 
| 15 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝐾 ∈
ℤ) | 
| 16 | 14, 15 | anim12ci 614 | . . . . . . . . . . . . . . . 16
⊢ (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ ℤ ∧ 𝑀 ∈
ℤ)) | 
| 17 | 13, 16 | jca 511 | . . . . . . . . . . . . . . 15
⊢ (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈
ℤ))) | 
| 18 | 17 | exp32 420 | . . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 ∈ ℤ → (𝐾 ∈ ℤ → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈
ℤ))))) | 
| 19 | 10, 18 | syl5 34 | . . . . . . . . . . . . 13
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 ∈ (𝐿...𝑋) → (𝐾 ∈ ℤ → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ))))) | 
| 20 | 19 | 3adant1 1131 | . . . . . . . . . . . 12
⊢ ((0
∈ ℤ ∧ 𝐿
∈ ℤ ∧ 𝑀
∈ ℤ) → (𝑁
∈ (𝐿...𝑋) → (𝐾 ∈ ℤ → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ))))) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . 11
⊢ (((0
∈ ℤ ∧ 𝐿
∈ ℤ ∧ 𝑀
∈ ℤ) ∧ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝐿)) → (𝑁 ∈ (𝐿...𝑋) → (𝐾 ∈ ℤ → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ))))) | 
| 22 | 1, 21 | sylbi 217 | . . . . . . . . . 10
⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...𝑋) → (𝐾 ∈ ℤ → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ))))) | 
| 23 | 22 | imp 406 | . . . . . . . . 9
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 ∈ ℤ → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)))) | 
| 24 | 23 | impcom 407 | . . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋))) → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ))) | 
| 25 |  | elfzomelpfzo 13810 | . . . . . . . 8
⊢ (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) ↔ (𝐾 + 𝑀) ∈ (𝐿..^𝑁))) | 
| 26 | 24, 25 | syl 17 | . . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋))) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) ↔ (𝐾 + 𝑀) ∈ (𝐿..^𝑁))) | 
| 27 |  | elfz2 13554 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ (𝐿...𝑋) ↔ ((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋))) | 
| 28 |  | simpl3 1194 | . . . . . . . . . . . . . 14
⊢ (((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋)) → 𝑁 ∈ ℤ) | 
| 29 |  | simpl2 1193 | . . . . . . . . . . . . . 14
⊢ (((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋)) → 𝑋 ∈ ℤ) | 
| 30 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋) → 𝑁 ≤ 𝑋) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋)) → 𝑁 ≤ 𝑋) | 
| 32 | 28, 29, 31 | 3jca 1129 | . . . . . . . . . . . . 13
⊢ (((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋)) → (𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋)) | 
| 33 | 27, 32 | sylbi 217 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ (𝐿...𝑋) → (𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋)) | 
| 34 | 33 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋)) | 
| 35 | 34 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐾 ∈ ℤ ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋))) → (𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋)) | 
| 36 |  | eluz2 12884 | . . . . . . . . . 10
⊢ (𝑋 ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋)) | 
| 37 | 35, 36 | sylibr 234 | . . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋))) → 𝑋 ∈ (ℤ≥‘𝑁)) | 
| 38 |  | fzoss2 13727 | . . . . . . . . 9
⊢ (𝑋 ∈
(ℤ≥‘𝑁) → (𝐿..^𝑁) ⊆ (𝐿..^𝑋)) | 
| 39 | 37, 38 | syl 17 | . . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋))) → (𝐿..^𝑁) ⊆ (𝐿..^𝑋)) | 
| 40 | 39 | sseld 3982 | . . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋))) → ((𝐾 + 𝑀) ∈ (𝐿..^𝑁) → (𝐾 + 𝑀) ∈ (𝐿..^𝑋))) | 
| 41 | 26, 40 | sylbid 240 | . . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋))) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) → (𝐾 + 𝑀) ∈ (𝐿..^𝑋))) | 
| 42 | 41 | ex 412 | . . . . 5
⊢ (𝐾 ∈ ℤ → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) → (𝐾 + 𝑀) ∈ (𝐿..^𝑋)))) | 
| 43 | 42 | com23 86 | . . . 4
⊢ (𝐾 ∈ ℤ → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 + 𝑀) ∈ (𝐿..^𝑋)))) | 
| 44 | 9, 43 | mpcom 38 | . . 3
⊢ (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 + 𝑀) ∈ (𝐿..^𝑋))) | 
| 45 | 44 | com12 32 | . 2
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝐾 ∈ ((𝐿 − 𝑀)..^(𝑁 − 𝑀)) → (𝐾 + 𝑀) ∈ (𝐿..^𝑋))) | 
| 46 | 8, 45 | syld 47 | 1
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 + 𝑀) ∈ (𝐿..^𝑋))) |