Proof of Theorem subsubelfzo0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfzo0 13740 | . . . 4
⊢ (𝐴 ∈ (0..^𝑁) ↔ (𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐴 < 𝑁)) | 
| 2 |  | elfzo0 13740 | . . . . . 6
⊢ (𝐼 ∈ (0..^𝑁) ↔ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) | 
| 3 |  | nnre 12273 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 4 | 3 | 3ad2ant2 1135 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐼 < 𝑁) → 𝑁 ∈ ℝ) | 
| 5 |  | nn0re 12535 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) | 
| 6 | 5 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) → 𝐴 ∈ ℝ) | 
| 7 |  | resubcl 11573 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑁 − 𝐴) ∈ ℝ) | 
| 8 | 4, 6, 7 | syl2anr 597 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) → (𝑁 − 𝐴) ∈ ℝ) | 
| 9 |  | nn0re 12535 | . . . . . . . . . . . . . 14
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℝ) | 
| 10 | 9 | 3ad2ant1 1134 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐼 < 𝑁) → 𝐼 ∈ ℝ) | 
| 11 | 10 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) → 𝐼 ∈ ℝ) | 
| 12 |  | lenlt 11339 | . . . . . . . . . . . . 13
⊢ (((𝑁 − 𝐴) ∈ ℝ ∧ 𝐼 ∈ ℝ) → ((𝑁 − 𝐴) ≤ 𝐼 ↔ ¬ 𝐼 < (𝑁 − 𝐴))) | 
| 13 | 12 | bicomd 223 | . . . . . . . . . . . 12
⊢ (((𝑁 − 𝐴) ∈ ℝ ∧ 𝐼 ∈ ℝ) → (¬ 𝐼 < (𝑁 − 𝐴) ↔ (𝑁 − 𝐴) ≤ 𝐼)) | 
| 14 | 8, 11, 13 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) → (¬ 𝐼 < (𝑁 − 𝐴) ↔ (𝑁 − 𝐴) ≤ 𝐼)) | 
| 15 | 14 | biimpa 476 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → (𝑁 − 𝐴) ≤ 𝐼) | 
| 16 |  | nnz 12634 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 17 | 16 | 3ad2ant2 1135 | . . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐼 < 𝑁) → 𝑁 ∈ ℤ) | 
| 18 |  | nn0z 12638 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℤ) | 
| 19 | 18 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) → 𝐴 ∈ ℤ) | 
| 20 |  | zsubcl 12659 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑁 − 𝐴) ∈ ℤ) | 
| 21 | 17, 19, 20 | syl2anr 597 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) → (𝑁 − 𝐴) ∈ ℤ) | 
| 22 |  | ltle 11349 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 < 𝑁 → 𝐴 ≤ 𝑁)) | 
| 23 | 5, 4, 22 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ0
∧ (𝐼 ∈
ℕ0 ∧ 𝑁
∈ ℕ ∧ 𝐼 <
𝑁)) → (𝐴 < 𝑁 → 𝐴 ≤ 𝑁)) | 
| 24 | 23 | impancom 451 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) → ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁) → 𝐴 ≤ 𝑁)) | 
| 25 | 24 | imp 406 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) → 𝐴 ≤ 𝑁) | 
| 26 |  | subge0 11776 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 ≤
(𝑁 − 𝐴) ↔ 𝐴 ≤ 𝑁)) | 
| 27 | 4, 6, 26 | syl2anr 597 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) → (0 ≤ (𝑁 − 𝐴) ↔ 𝐴 ≤ 𝑁)) | 
| 28 | 25, 27 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) → 0 ≤ (𝑁 − 𝐴)) | 
| 29 |  | elnn0z 12626 | . . . . . . . . . . . . 13
⊢ ((𝑁 − 𝐴) ∈ ℕ0 ↔ ((𝑁 − 𝐴) ∈ ℤ ∧ 0 ≤ (𝑁 − 𝐴))) | 
| 30 | 21, 28, 29 | sylanbrc 583 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) → (𝑁 − 𝐴) ∈
ℕ0) | 
| 31 | 30 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → (𝑁 − 𝐴) ∈
ℕ0) | 
| 32 |  | simplr1 1216 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → 𝐼 ∈
ℕ0) | 
| 33 |  | nn0sub 12576 | . . . . . . . . . . 11
⊢ (((𝑁 − 𝐴) ∈ ℕ0 ∧ 𝐼 ∈ ℕ0)
→ ((𝑁 − 𝐴) ≤ 𝐼 ↔ (𝐼 − (𝑁 − 𝐴)) ∈
ℕ0)) | 
| 34 | 31, 32, 33 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → ((𝑁 − 𝐴) ≤ 𝐼 ↔ (𝐼 − (𝑁 − 𝐴)) ∈
ℕ0)) | 
| 35 | 15, 34 | mpbid 232 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → (𝐼 − (𝑁 − 𝐴)) ∈
ℕ0) | 
| 36 |  | elnn0uz 12923 | . . . . . . . . 9
⊢ ((𝐼 − (𝑁 − 𝐴)) ∈ ℕ0 ↔ (𝐼 − (𝑁 − 𝐴)) ∈
(ℤ≥‘0)) | 
| 37 | 35, 36 | sylib 218 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → (𝐼 − (𝑁 − 𝐴)) ∈
(ℤ≥‘0)) | 
| 38 | 19 | adantr 480 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) → 𝐴 ∈ ℤ) | 
| 39 | 38 | adantr 480 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → 𝐴 ∈ ℤ) | 
| 40 | 9 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝐼 ∈
ℝ) | 
| 41 | 40 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ0
∧ (𝐼 ∈
ℕ0 ∧ 𝑁
∈ ℕ)) → 𝐼
∈ ℝ) | 
| 42 | 3 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℝ) | 
| 43 | 42 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ0
∧ (𝐼 ∈
ℕ0 ∧ 𝑁
∈ ℕ)) → 𝑁
∈ ℝ) | 
| 44 | 42, 5, 7 | syl2anr 597 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ0
∧ (𝐼 ∈
ℕ0 ∧ 𝑁
∈ ℕ)) → (𝑁
− 𝐴) ∈
ℝ) | 
| 45 | 41, 43, 44 | ltsub1d 11872 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ0
∧ (𝐼 ∈
ℕ0 ∧ 𝑁
∈ ℕ)) → (𝐼
< 𝑁 ↔ (𝐼 − (𝑁 − 𝐴)) < (𝑁 − (𝑁 − 𝐴)))) | 
| 46 |  | nncn 12274 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 47 | 46 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℂ) | 
| 48 |  | nn0cn 12536 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℂ) | 
| 49 |  | nncan 11538 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑁 − (𝑁 − 𝐴)) = 𝐴) | 
| 50 | 47, 48, 49 | syl2anr 597 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ0
∧ (𝐼 ∈
ℕ0 ∧ 𝑁
∈ ℕ)) → (𝑁
− (𝑁 − 𝐴)) = 𝐴) | 
| 51 | 50 | breq2d 5155 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ0
∧ (𝐼 ∈
ℕ0 ∧ 𝑁
∈ ℕ)) → ((𝐼
− (𝑁 − 𝐴)) < (𝑁 − (𝑁 − 𝐴)) ↔ (𝐼 − (𝑁 − 𝐴)) < 𝐴)) | 
| 52 | 51 | biimpd 229 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ0
∧ (𝐼 ∈
ℕ0 ∧ 𝑁
∈ ℕ)) → ((𝐼
− (𝑁 − 𝐴)) < (𝑁 − (𝑁 − 𝐴)) → (𝐼 − (𝑁 − 𝐴)) < 𝐴)) | 
| 53 | 45, 52 | sylbid 240 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ0
∧ (𝐼 ∈
ℕ0 ∧ 𝑁
∈ ℕ)) → (𝐼
< 𝑁 → (𝐼 − (𝑁 − 𝐴)) < 𝐴)) | 
| 54 | 53 | ex 412 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ0
→ ((𝐼 ∈
ℕ0 ∧ 𝑁
∈ ℕ) → (𝐼
< 𝑁 → (𝐼 − (𝑁 − 𝐴)) < 𝐴))) | 
| 55 | 54 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) → ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐼 < 𝑁 → (𝐼 − (𝑁 − 𝐴)) < 𝐴))) | 
| 56 | 55 | com3l 89 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐼 < 𝑁 → ((𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁) → (𝐼 − (𝑁 − 𝐴)) < 𝐴))) | 
| 57 | 56 | 3impia 1118 | . . . . . . . . . 10
⊢ ((𝐼 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐼 < 𝑁) → ((𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁) → (𝐼 − (𝑁 − 𝐴)) < 𝐴)) | 
| 58 | 57 | impcom 407 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) → (𝐼 − (𝑁 − 𝐴)) < 𝐴) | 
| 59 | 58 | adantr 480 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → (𝐼 − (𝑁 − 𝐴)) < 𝐴) | 
| 60 | 37, 39, 59 | 3jca 1129 | . . . . . . 7
⊢ ((((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) ∧ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁)) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → ((𝐼 − (𝑁 − 𝐴)) ∈ (ℤ≥‘0)
∧ 𝐴 ∈ ℤ
∧ (𝐼 − (𝑁 − 𝐴)) < 𝐴)) | 
| 61 | 60 | exp31 419 | . . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) → ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁) → (¬ 𝐼 < (𝑁 − 𝐴) → ((𝐼 − (𝑁 − 𝐴)) ∈ (ℤ≥‘0)
∧ 𝐴 ∈ ℤ
∧ (𝐼 − (𝑁 − 𝐴)) < 𝐴)))) | 
| 62 | 2, 61 | biimtrid 242 | . . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐴 < 𝑁) → (𝐼 ∈ (0..^𝑁) → (¬ 𝐼 < (𝑁 − 𝐴) → ((𝐼 − (𝑁 − 𝐴)) ∈ (ℤ≥‘0)
∧ 𝐴 ∈ ℤ
∧ (𝐼 − (𝑁 − 𝐴)) < 𝐴)))) | 
| 63 | 62 | 3adant2 1132 | . . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐴 < 𝑁) → (𝐼 ∈ (0..^𝑁) → (¬ 𝐼 < (𝑁 − 𝐴) → ((𝐼 − (𝑁 − 𝐴)) ∈ (ℤ≥‘0)
∧ 𝐴 ∈ ℤ
∧ (𝐼 − (𝑁 − 𝐴)) < 𝐴)))) | 
| 64 | 1, 63 | sylbi 217 | . . 3
⊢ (𝐴 ∈ (0..^𝑁) → (𝐼 ∈ (0..^𝑁) → (¬ 𝐼 < (𝑁 − 𝐴) → ((𝐼 − (𝑁 − 𝐴)) ∈ (ℤ≥‘0)
∧ 𝐴 ∈ ℤ
∧ (𝐼 − (𝑁 − 𝐴)) < 𝐴)))) | 
| 65 | 64 | 3imp 1111 | . 2
⊢ ((𝐴 ∈ (0..^𝑁) ∧ 𝐼 ∈ (0..^𝑁) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → ((𝐼 − (𝑁 − 𝐴)) ∈ (ℤ≥‘0)
∧ 𝐴 ∈ ℤ
∧ (𝐼 − (𝑁 − 𝐴)) < 𝐴)) | 
| 66 |  | elfzo2 13702 | . 2
⊢ ((𝐼 − (𝑁 − 𝐴)) ∈ (0..^𝐴) ↔ ((𝐼 − (𝑁 − 𝐴)) ∈ (ℤ≥‘0)
∧ 𝐴 ∈ ℤ
∧ (𝐼 − (𝑁 − 𝐴)) < 𝐴)) | 
| 67 | 65, 66 | sylibr 234 | 1
⊢ ((𝐴 ∈ (0..^𝑁) ∧ 𝐼 ∈ (0..^𝑁) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → (𝐼 − (𝑁 − 𝐴)) ∈ (0..^𝐴)) |