Proof of Theorem iinhoiicclem
Step | Hyp | Ref
| Expression |
1 | | iinhoiicclem.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ∩
𝑛 ∈ ℕ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛)))) |
2 | 1 | elexd 3495 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
3 | | 1nn 12220 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℕ) |
5 | | iinhoiicclem.k |
. . . . . . . . 9
⊢
Ⅎ𝑘𝜑 |
6 | | iinhoiicclem.a |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
7 | | iinhoiicclem.b |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) |
8 | | peano2re 11384 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → (𝐵 + 1) ∈
ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵 + 1) ∈ ℝ) |
10 | 9 | rexrd 11261 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵 + 1) ∈
ℝ*) |
11 | | icossre 13402 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 + 1) ∈
ℝ*) → (𝐴[,)(𝐵 + 1)) ⊆ ℝ) |
12 | 6, 10, 11 | syl2anc 585 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴[,)(𝐵 + 1)) ⊆ ℝ) |
13 | 5, 12 | ixpssixp 43767 |
. . . . . . . 8
⊢ (𝜑 → X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 ℝ) |
14 | | oveq2 7414 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (1 / 𝑛) = (1 / 1)) |
15 | | 1div1e1 11901 |
. . . . . . . . . . . . . . 15
⊢ (1 / 1) =
1 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (1 / 1) =
1) |
17 | 14, 16 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (1 / 𝑛) = 1) |
18 | 17 | oveq2d 7422 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → (𝐵 + (1 / 𝑛)) = (𝐵 + 1)) |
19 | 18 | oveq2d 7422 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → (𝐴[,)(𝐵 + (1 / 𝑛))) = (𝐴[,)(𝐵 + 1))) |
20 | 19 | ixpeq2dv 8904 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) = X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) |
21 | 20 | sseq1d 4013 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ ↔ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 ℝ)) |
22 | 21 | rspcev 3613 |
. . . . . . . 8
⊢ ((1
∈ ℕ ∧ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 ℝ) → ∃𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ) |
23 | 4, 13, 22 | syl2anc 585 |
. . . . . . 7
⊢ (𝜑 → ∃𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ) |
24 | | iinss 5059 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ) |
26 | 25, 1 | sseldd 3983 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 ℝ) |
27 | | elixpconstg 43764 |
. . . . . 6
⊢ (𝐹 ∈ ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) → (𝐹 ∈ X𝑘 ∈ 𝑋 ℝ ↔ 𝐹:𝑋⟶ℝ)) |
28 | 1, 27 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ X𝑘 ∈ 𝑋 ℝ ↔ 𝐹:𝑋⟶ℝ)) |
29 | 26, 28 | mpbid 231 |
. . . 4
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
30 | 29 | ffnd 6716 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝑋) |
31 | 29 | ffvelcdmda 7084 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ ℝ) |
32 | 6 | rexrd 11261 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈
ℝ*) |
33 | | ssid 4004 |
. . . . . . . . . . . . 13
⊢ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) |
34 | 33 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) |
35 | 20 | sseq1d 4013 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) ↔ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)))) |
36 | 35 | rspcev 3613 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℕ ∧ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) → ∃𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) |
37 | 4, 34, 36 | syl2anc 585 |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) |
38 | | iinss 5059 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) |
40 | 39, 1 | sseldd 3983 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) |
41 | 40 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) |
42 | | simpr 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
43 | | fvixp2 43884 |
. . . . . . . 8
⊢ ((𝐹 ∈ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + 1)) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + 1))) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + 1))) |
45 | | icogelb 13372 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 + 1) ∈
ℝ* ∧ (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + 1))) → 𝐴 ≤ (𝐹‘𝑘)) |
46 | 32, 10, 44, 45 | syl3anc 1372 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ≤ (𝐹‘𝑘)) |
47 | 31 | adantr 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
48 | 7 | adantr 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ) |
49 | | nnrecre 12251 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
50 | 49 | adantl 483 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ) |
51 | 48, 50 | readdcld 11240 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐵 + (1 / 𝑛)) ∈ ℝ) |
52 | 32 | adantr 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → 𝐴 ∈
ℝ*) |
53 | | ressxr 11255 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℝ* |
54 | 53, 51 | sselid 3980 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐵 + (1 / 𝑛)) ∈
ℝ*) |
55 | | eliin 5002 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ V → (𝐹 ∈ ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ↔ ∀𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))))) |
56 | 2, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 ∈ ∩
𝑛 ∈ ℕ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ↔ ∀𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))))) |
57 | 1, 56 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛)))) |
58 | 57 | r19.21bi 3249 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛)))) |
59 | | elixp2 8892 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛))))) |
60 | 58, 59 | sylib 217 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛))))) |
61 | 60 | simp3d 1145 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛)))) |
62 | 61 | r19.21bi 3249 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛)))) |
63 | 62 | an32s 651 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛)))) |
64 | | icoltub 44208 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 + (1 / 𝑛)) ∈ ℝ*
∧ (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛)))) → (𝐹‘𝑘) < (𝐵 + (1 / 𝑛))) |
65 | 52, 54, 63, 64 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑘) < (𝐵 + (1 / 𝑛))) |
66 | 47, 51, 65 | ltled 11359 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐵 + (1 / 𝑛))) |
67 | 66 | ralrimiva 3147 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ∀𝑛 ∈ ℕ (𝐹‘𝑘) ≤ (𝐵 + (1 / 𝑛))) |
68 | | nfv 1918 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝜑 ∧ 𝑘 ∈ 𝑋) |
69 | 53, 31 | sselid 3980 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈
ℝ*) |
70 | 68, 69, 7 | xrralrecnnle 44080 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐹‘𝑘) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (𝐹‘𝑘) ≤ (𝐵 + (1 / 𝑛)))) |
71 | 67, 70 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ≤ 𝐵) |
72 | 6, 7, 31, 46, 71 | eliccd 44204 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴[,]𝐵)) |
73 | 72 | ex 414 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝑋 → (𝐹‘𝑘) ∈ (𝐴[,]𝐵))) |
74 | 5, 73 | ralrimi 3255 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,]𝐵)) |
75 | 2, 30, 74 | 3jca 1129 |
. 2
⊢ (𝜑 → (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,]𝐵))) |
76 | | elixp2 8892 |
. 2
⊢ (𝐹 ∈ X𝑘 ∈
𝑋 (𝐴[,]𝐵) ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,]𝐵))) |
77 | 75, 76 | sylibr 233 |
1
⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,]𝐵)) |