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