| Step | Hyp | Ref
| Expression |
| 1 | | iooiinioc.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝐴 ∈
ℝ*) |
| 3 | | iooiinioc.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝐵 ∈ ℝ) |
| 5 | 4 | rexrd 11311 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝐵 ∈
ℝ*) |
| 6 | | 1nn 12277 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
| 7 | | ioossre 13448 |
. . . . . . . . . 10
⊢ (𝐴(,)(𝐵 + (1 / 1))) ⊆
ℝ |
| 8 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (1 / 𝑛) = (1 / 1)) |
| 9 | 8 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (𝐵 + (1 / 𝑛)) = (𝐵 + (1 / 1))) |
| 10 | 9 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → (𝐴(,)(𝐵 + (1 / 𝑛))) = (𝐴(,)(𝐵 + (1 / 1)))) |
| 11 | 10 | sseq1d 4015 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → ((𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ ℝ ↔ (𝐴(,)(𝐵 + (1 / 1))) ⊆
ℝ)) |
| 12 | 11 | rspcev 3622 |
. . . . . . . . . 10
⊢ ((1
∈ ℕ ∧ (𝐴(,)(𝐵 + (1 / 1))) ⊆ ℝ) →
∃𝑛 ∈ ℕ
(𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ ℝ) |
| 13 | 6, 7, 12 | mp2an 692 |
. . . . . . . . 9
⊢
∃𝑛 ∈
ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ ℝ |
| 14 | | iinss 5056 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ ℝ → ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ ℝ) |
| 15 | 13, 14 | ax-mp 5 |
. . . . . . . 8
⊢ ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ ℝ |
| 16 | 15 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ ℝ) |
| 17 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 18 | 16, 17 | sseldd 3984 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝑥 ∈ ℝ) |
| 19 | 18 | rexrd 11311 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝑥 ∈ ℝ*) |
| 20 | | 1red 11262 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
| 21 | | ax-1ne0 11224 |
. . . . . . . . . . 11
⊢ 1 ≠
0 |
| 22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≠ 0) |
| 23 | 20, 20, 22 | redivcld 12095 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 1) ∈
ℝ) |
| 24 | 3, 23 | readdcld 11290 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 + (1 / 1)) ∈ ℝ) |
| 25 | 24 | rexrd 11311 |
. . . . . . 7
⊢ (𝜑 → (𝐵 + (1 / 1)) ∈
ℝ*) |
| 26 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → (𝐵 + (1 / 1)) ∈
ℝ*) |
| 27 | | id 22 |
. . . . . . . 8
⊢ (𝑥 ∈ ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) → 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 28 | 6 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) → 1 ∈ ℕ) |
| 29 | 10 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑛 = 1 → (𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛))) ↔ 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 1))))) |
| 30 | 27, 28, 29 | eliind 45076 |
. . . . . . 7
⊢ (𝑥 ∈ ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) → 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 1)))) |
| 31 | 30 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 1)))) |
| 32 | | ioogtlb 45508 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 + (1 / 1)) ∈
ℝ* ∧ 𝑥
∈ (𝐴(,)(𝐵 + (1 / 1)))) → 𝐴 < 𝑥) |
| 33 | 2, 26, 31, 32 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝐴 < 𝑥) |
| 34 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑛𝜑 |
| 35 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝑥 |
| 36 | | nfii1 5029 |
. . . . . . . . 9
⊢
Ⅎ𝑛∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) |
| 37 | 35, 36 | nfel 2920 |
. . . . . . . 8
⊢
Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) |
| 38 | 34, 37 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 39 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → 𝜑) |
| 40 | | iinss2 5057 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 41 | 40 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ∧ 𝑛 ∈ ℕ) → ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 42 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 43 | 41, 42 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 44 | 43 | adantll 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 45 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
| 46 | | elioore 13417 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛))) → 𝑥 ∈ ℝ) |
| 47 | 46 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛))) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ) |
| 48 | 47 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ) |
| 49 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ) |
| 50 | | nnrecre 12308 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
| 51 | 50 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ) |
| 52 | 49, 51 | readdcld 11290 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 + (1 / 𝑛)) ∈ ℝ) |
| 53 | 52 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → (𝐵 + (1 / 𝑛)) ∈ ℝ) |
| 54 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈
ℝ*) |
| 55 | 54 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → 𝐴 ∈
ℝ*) |
| 56 | 52 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 + (1 / 𝑛)) ∈
ℝ*) |
| 57 | 56 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → (𝐵 + (1 / 𝑛)) ∈
ℝ*) |
| 58 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 59 | | iooltub 45523 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 + (1 / 𝑛)) ∈ ℝ*
∧ 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝑥 < (𝐵 + (1 / 𝑛))) |
| 60 | 55, 57, 58, 59 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → 𝑥 < (𝐵 + (1 / 𝑛))) |
| 61 | 48, 53, 60 | ltled 11409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → 𝑥 ≤ (𝐵 + (1 / 𝑛))) |
| 62 | 39, 44, 45, 61 | syl21anc 838 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) ∧ 𝑛 ∈ ℕ) → 𝑥 ≤ (𝐵 + (1 / 𝑛))) |
| 63 | 62 | ex 412 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → (𝑛 ∈ ℕ → 𝑥 ≤ (𝐵 + (1 / 𝑛)))) |
| 64 | 38, 63 | ralrimi 3257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → ∀𝑛 ∈ ℕ 𝑥 ≤ (𝐵 + (1 / 𝑛))) |
| 65 | 38, 19, 4 | xrralrecnnle 45394 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → (𝑥 ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ 𝑥 ≤ (𝐵 + (1 / 𝑛)))) |
| 66 | 64, 65 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝑥 ≤ 𝐵) |
| 67 | 2, 5, 19, 33, 66 | eliocd 45520 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) → 𝑥 ∈ (𝐴(,]𝐵)) |
| 68 | 67 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))𝑥 ∈ (𝐴(,]𝐵)) |
| 69 | | dfss3 3972 |
. . 3
⊢ (∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ (𝐴(,]𝐵) ↔ ∀𝑥 ∈ ∩
𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))𝑥 ∈ (𝐴(,]𝐵)) |
| 70 | 68, 69 | sylibr 234 |
. 2
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ⊆ (𝐴(,]𝐵)) |
| 71 | 1 | xrleidd 13194 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝐴) |
| 72 | 71 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ≤ 𝐴) |
| 73 | | 1rp 13038 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
| 74 | 73 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 1 ∈
ℝ+) |
| 75 | | nnrp 13046 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
| 76 | 74, 75 | rpdivcld 13094 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ+) |
| 77 | 76 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ+) |
| 78 | 49, 77 | ltaddrpd 13110 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 < (𝐵 + (1 / 𝑛))) |
| 79 | | iocssioo 13479 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 + (1 / 𝑛)) ∈ ℝ*)
∧ (𝐴 ≤ 𝐴 ∧ 𝐵 < (𝐵 + (1 / 𝑛)))) → (𝐴(,]𝐵) ⊆ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 80 | 54, 56, 72, 78, 79 | syl22anc 839 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴(,]𝐵) ⊆ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 81 | 80 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐴(,]𝐵) ⊆ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 82 | | ssiin 5055 |
. . 3
⊢ ((𝐴(,]𝐵) ⊆ ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) ↔ ∀𝑛 ∈ ℕ (𝐴(,]𝐵) ⊆ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 83 | 81, 82 | sylibr 234 |
. 2
⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛)))) |
| 84 | 70, 83 | eqssd 4001 |
1
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) = (𝐴(,]𝐵)) |