Proof of Theorem 2elfz2melfz
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfzelz 13565 | . . . . 5
⊢ (𝐴 ∈ (0...𝑁) → 𝐴 ∈ ℤ) | 
| 2 |  | elfzel2 13563 | . . . . . 6
⊢ (𝐵 ∈ (0...𝑁) → 𝑁 ∈ ℤ) | 
| 3 |  | elfzelz 13565 | . . . . . 6
⊢ (𝐵 ∈ (0...𝑁) → 𝐵 ∈ ℤ) | 
| 4 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → 𝐵 ∈
ℤ) | 
| 5 |  | zsubcl 12661 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑁 − 𝐴) ∈ ℤ) | 
| 6 | 5 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝑁 − 𝐴) ∈ ℤ) | 
| 7 | 4, 6 | zsubcld 12729 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝐵 − (𝑁 − 𝐴)) ∈ ℤ) | 
| 8 | 7 | adantr 480 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) ∧ 𝑁 < (𝐴 + 𝐵)) → (𝐵 − (𝑁 − 𝐴)) ∈ ℤ) | 
| 9 |  | zre 12619 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 10 | 9 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → 𝑁 ∈
ℝ) | 
| 11 |  | zaddcl 12659 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℤ) | 
| 12 | 11 | zred 12724 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℝ) | 
| 13 | 12 | expcom 413 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℤ → (𝐴 ∈ ℤ → (𝐴 + 𝐵) ∈ ℝ)) | 
| 14 | 13 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∈ ℤ → (𝐴 + 𝐵) ∈ ℝ)) | 
| 15 | 14 | imp 406 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℝ) | 
| 16 | 10, 15, 10 | ltsub1d 11873 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝑁 < (𝐴 + 𝐵) ↔ (𝑁 − 𝑁) < ((𝐴 + 𝐵) − 𝑁))) | 
| 17 |  | zre 12619 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℝ) | 
| 18 | 9, 17 | anim12i 613 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑁 ∈ ℝ ∧ 𝐵 ∈
ℝ)) | 
| 19 |  | zre 12619 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) | 
| 20 | 18, 19 | anim12i 613 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → ((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈
ℝ)) | 
| 21 |  | id 22 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℝ) | 
| 22 | 21, 21 | resubcld 11692 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℝ → (𝑁 − 𝑁) ∈ ℝ) | 
| 23 | 22 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝑁 − 𝑁) ∈ ℝ) | 
| 24 |  | readdcl 11239 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | 
| 25 | 24 | expcom 413 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℝ → (𝐴 ∈ ℝ → (𝐴 + 𝐵) ∈ ℝ)) | 
| 26 | 25 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ∈ ℝ → (𝐴 + 𝐵) ∈ ℝ)) | 
| 27 | 26 | imp 406 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | 
| 28 |  | simpll 766 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → 𝑁 ∈
ℝ) | 
| 29 | 27, 28 | resubcld 11692 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → ((𝐴 + 𝐵) − 𝑁) ∈ ℝ) | 
| 30 | 23, 29 | jca 511 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → ((𝑁 − 𝑁) ∈ ℝ ∧ ((𝐴 + 𝐵) − 𝑁) ∈ ℝ)) | 
| 31 |  | ltle 11350 | . . . . . . . . . . . 12
⊢ (((𝑁 − 𝑁) ∈ ℝ ∧ ((𝐴 + 𝐵) − 𝑁) ∈ ℝ) → ((𝑁 − 𝑁) < ((𝐴 + 𝐵) − 𝑁) → (𝑁 − 𝑁) ≤ ((𝐴 + 𝐵) − 𝑁))) | 
| 32 | 20, 30, 31 | 3syl 18 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → ((𝑁 − 𝑁) < ((𝐴 + 𝐵) − 𝑁) → (𝑁 − 𝑁) ≤ ((𝐴 + 𝐵) − 𝑁))) | 
| 33 |  | zcn 12620 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) | 
| 34 | 33 | subidd 11609 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (𝑁 − 𝑁) = 0) | 
| 35 | 34 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝑁 − 𝑁) = 0) | 
| 36 |  | zcn 12620 | . . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) | 
| 37 | 36 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈
ℂ) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → 𝐵 ∈
ℂ) | 
| 39 | 33 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → 𝑁 ∈
ℂ) | 
| 40 |  | zcn 12620 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) | 
| 41 | 40 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → 𝐴 ∈
ℂ) | 
| 42 |  | simp3 1138 | . . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝐴 ∈
ℂ) | 
| 43 |  | simp1 1136 | . . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝐵 ∈
ℂ) | 
| 44 | 42, 43 | addcomd 11464 | . . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | 
| 45 | 44 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝐴 + 𝐵) − 𝑁) = ((𝐵 + 𝐴) − 𝑁)) | 
| 46 |  | subsub3 11542 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − (𝑁 − 𝐴)) = ((𝐵 + 𝐴) − 𝑁)) | 
| 47 | 45, 46 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝐴 + 𝐵) − 𝑁) = (𝐵 − (𝑁 − 𝐴))) | 
| 48 | 38, 39, 41, 47 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → ((𝐴 + 𝐵) − 𝑁) = (𝐵 − (𝑁 − 𝐴))) | 
| 49 | 35, 48 | breq12d 5155 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → ((𝑁 − 𝑁) ≤ ((𝐴 + 𝐵) − 𝑁) ↔ 0 ≤ (𝐵 − (𝑁 − 𝐴)))) | 
| 50 | 32, 49 | sylibd 239 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → ((𝑁 − 𝑁) < ((𝐴 + 𝐵) − 𝑁) → 0 ≤ (𝐵 − (𝑁 − 𝐴)))) | 
| 51 | 16, 50 | sylbid 240 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝑁 < (𝐴 + 𝐵) → 0 ≤ (𝐵 − (𝑁 − 𝐴)))) | 
| 52 | 51 | imp 406 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) ∧ 𝑁 < (𝐴 + 𝐵)) → 0 ≤ (𝐵 − (𝑁 − 𝐴))) | 
| 53 |  | elnn0z 12628 | . . . . . . . 8
⊢ ((𝐵 − (𝑁 − 𝐴)) ∈ ℕ0 ↔ ((𝐵 − (𝑁 − 𝐴)) ∈ ℤ ∧ 0 ≤ (𝐵 − (𝑁 − 𝐴)))) | 
| 54 | 8, 52, 53 | sylanbrc 583 | . . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) ∧ 𝑁 < (𝐴 + 𝐵)) → (𝐵 − (𝑁 − 𝐴)) ∈
ℕ0) | 
| 55 | 54 | exp31 419 | . . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∈ ℤ → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁 − 𝐴)) ∈
ℕ0))) | 
| 56 | 2, 3, 55 | syl2anc 584 | . . . . 5
⊢ (𝐵 ∈ (0...𝑁) → (𝐴 ∈ ℤ → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁 − 𝐴)) ∈
ℕ0))) | 
| 57 | 1, 56 | mpan9 506 | . . . 4
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁 − 𝐴)) ∈
ℕ0)) | 
| 58 | 57 | imp 406 | . . 3
⊢ (((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) ∧ 𝑁 < (𝐴 + 𝐵)) → (𝐵 − (𝑁 − 𝐴)) ∈
ℕ0) | 
| 59 |  | elfznn0 13661 | . . . 4
⊢ (𝐴 ∈ (0...𝑁) → 𝐴 ∈
ℕ0) | 
| 60 | 59 | ad2antrr 726 | . . 3
⊢ (((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) ∧ 𝑁 < (𝐴 + 𝐵)) → 𝐴 ∈
ℕ0) | 
| 61 |  | elfzle2 13569 | . . . . . . 7
⊢ (𝐵 ∈ (0...𝑁) → 𝐵 ≤ 𝑁) | 
| 62 | 61 | adantl 481 | . . . . . 6
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → 𝐵 ≤ 𝑁) | 
| 63 |  | elfzel2 13563 | . . . . . . . . . 10
⊢ (𝐴 ∈ (0...𝑁) → 𝑁 ∈ ℤ) | 
| 64 | 63 | zcnd 12725 | . . . . . . . . 9
⊢ (𝐴 ∈ (0...𝑁) → 𝑁 ∈ ℂ) | 
| 65 | 1 | zcnd 12725 | . . . . . . . . 9
⊢ (𝐴 ∈ (0...𝑁) → 𝐴 ∈ ℂ) | 
| 66 | 64, 65 | jca 511 | . . . . . . . 8
⊢ (𝐴 ∈ (0...𝑁) → (𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ)) | 
| 67 | 66 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ)) | 
| 68 |  | npcan 11518 | . . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑁 − 𝐴) + 𝐴) = 𝑁) | 
| 69 | 67, 68 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → ((𝑁 − 𝐴) + 𝐴) = 𝑁) | 
| 70 | 62, 69 | breqtrrd 5170 | . . . . 5
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → 𝐵 ≤ ((𝑁 − 𝐴) + 𝐴)) | 
| 71 | 3 | zred 12724 | . . . . . . 7
⊢ (𝐵 ∈ (0...𝑁) → 𝐵 ∈ ℝ) | 
| 72 | 71 | adantl 481 | . . . . . 6
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → 𝐵 ∈ ℝ) | 
| 73 | 63 | zred 12724 | . . . . . . . 8
⊢ (𝐴 ∈ (0...𝑁) → 𝑁 ∈ ℝ) | 
| 74 | 1 | zred 12724 | . . . . . . . 8
⊢ (𝐴 ∈ (0...𝑁) → 𝐴 ∈ ℝ) | 
| 75 | 73, 74 | resubcld 11692 | . . . . . . 7
⊢ (𝐴 ∈ (0...𝑁) → (𝑁 − 𝐴) ∈ ℝ) | 
| 76 | 75 | adantr 480 | . . . . . 6
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 − 𝐴) ∈ ℝ) | 
| 77 | 74 | adantr 480 | . . . . . 6
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → 𝐴 ∈ ℝ) | 
| 78 | 72, 76, 77 | lesubadd2d 11863 | . . . . 5
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → ((𝐵 − (𝑁 − 𝐴)) ≤ 𝐴 ↔ 𝐵 ≤ ((𝑁 − 𝐴) + 𝐴))) | 
| 79 | 70, 78 | mpbird 257 | . . . 4
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝐵 − (𝑁 − 𝐴)) ≤ 𝐴) | 
| 80 | 79 | adantr 480 | . . 3
⊢ (((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) ∧ 𝑁 < (𝐴 + 𝐵)) → (𝐵 − (𝑁 − 𝐴)) ≤ 𝐴) | 
| 81 |  | elfz2nn0 13659 | . . 3
⊢ ((𝐵 − (𝑁 − 𝐴)) ∈ (0...𝐴) ↔ ((𝐵 − (𝑁 − 𝐴)) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0
∧ (𝐵 − (𝑁 − 𝐴)) ≤ 𝐴)) | 
| 82 | 58, 60, 80, 81 | syl3anbrc 1343 | . 2
⊢ (((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) ∧ 𝑁 < (𝐴 + 𝐵)) → (𝐵 − (𝑁 − 𝐴)) ∈ (0...𝐴)) | 
| 83 | 82 | ex 412 | 1
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁 − 𝐴)) ∈ (0...𝐴))) |