Proof of Theorem caucvgrelemcau
Step | Hyp | Ref
| Expression |
1 | | simplr 520 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝑛 ∈ ℕ) |
2 | 1 | nnred 8846 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝑛 ∈ ℝ) |
3 | | simpr 109 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
4 | 3 | nnred 8846 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ) |
5 | | ltle 7964 |
. . . . . 6
⊢ ((𝑛 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑛 < 𝑘 → 𝑛 ≤ 𝑘)) |
6 | 2, 4, 5 | syl2anc 409 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝑛 < 𝑘 → 𝑛 ≤ 𝑘)) |
7 | | eluznn 9511 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
8 | 7 | ex 114 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑘 ∈
(ℤ≥‘𝑛) → 𝑘 ∈ ℕ)) |
9 | | nnz 9186 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
10 | | eluz1 9443 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → (𝑘 ∈
(ℤ≥‘𝑛) ↔ (𝑘 ∈ ℤ ∧ 𝑛 ≤ 𝑘))) |
11 | 9, 10 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑘 ∈
(ℤ≥‘𝑛) ↔ (𝑘 ∈ ℤ ∧ 𝑛 ≤ 𝑘))) |
12 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ≤ 𝑘) → 𝑛 ≤ 𝑘) |
13 | 11, 12 | syl6bi 162 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑘 ∈
(ℤ≥‘𝑛) → 𝑛 ≤ 𝑘)) |
14 | 8, 13 | jcad 305 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝑘 ∈
(ℤ≥‘𝑛) → (𝑘 ∈ ℕ ∧ 𝑛 ≤ 𝑘))) |
15 | | nnz 9186 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
16 | 15 | anim1i 338 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ≤ 𝑘) → (𝑘 ∈ ℤ ∧ 𝑛 ≤ 𝑘)) |
17 | 16, 11 | syl5ibr 155 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ∧ 𝑛 ≤ 𝑘) → 𝑘 ∈ (ℤ≥‘𝑛))) |
18 | 14, 17 | impbid 128 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝑘 ∈
(ℤ≥‘𝑛) ↔ (𝑘 ∈ ℕ ∧ 𝑛 ≤ 𝑘))) |
19 | 18 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (ℤ≥‘𝑛) ↔ (𝑘 ∈ ℕ ∧ 𝑛 ≤ 𝑘))) |
20 | 19 | biimpar 295 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ 𝑛 ≤ 𝑘)) → 𝑘 ∈ (ℤ≥‘𝑛)) |
21 | | caucvgre.cau |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛)))) |
22 | 21 | r19.21bi 2545 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛)))) |
23 | 22 | r19.21bi 2545 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛)))) |
24 | 20, 23 | syldan 280 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑘 ∈ ℕ ∧ 𝑛 ≤ 𝑘)) → ((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛)))) |
25 | 24 | expr 373 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝑛 ≤ 𝑘 → ((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛))))) |
26 | 6, 25 | syld 45 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝑛 < 𝑘 → ((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛))))) |
27 | | ltxrlt 7943 |
. . . . 5
⊢ ((𝑛 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑛 < 𝑘 ↔ 𝑛 <ℝ 𝑘)) |
28 | 2, 4, 27 | syl2anc 409 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝑛 < 𝑘 ↔ 𝑛 <ℝ 𝑘)) |
29 | | caucvgre.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
30 | 29 | ad2antrr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶ℝ) |
31 | 30, 1 | ffvelrnd 5603 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑛) ∈ ℝ) |
32 | 30, 3 | ffvelrnd 5603 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
33 | 1 | nnrecred 8880 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (1 / 𝑛) ∈
ℝ) |
34 | 32, 33 | readdcld 7907 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) + (1 / 𝑛)) ∈ ℝ) |
35 | | ltxrlt 7943 |
. . . . . . 7
⊢ (((𝐹‘𝑛) ∈ ℝ ∧ ((𝐹‘𝑘) + (1 / 𝑛)) ∈ ℝ) → ((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ↔ (𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (1 / 𝑛)))) |
36 | 31, 34, 35 | syl2anc 409 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ↔ (𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (1 / 𝑛)))) |
37 | | nnap0 8862 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 # 0) |
38 | 1, 37 | syl 14 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝑛 # 0) |
39 | | caucvgrelemrec 10879 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℝ ∧ 𝑛 # 0) →
(℩𝑟 ∈
ℝ (𝑛 · 𝑟) = 1) = (1 / 𝑛)) |
40 | 2, 38, 39 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1) = (1 / 𝑛)) |
41 | 40 | oveq2d 5840 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) = ((𝐹‘𝑘) + (1 / 𝑛))) |
42 | 41 | breq2d 3977 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ↔ (𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (1 / 𝑛)))) |
43 | 36, 42 | bitr4d 190 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ↔ (𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))) |
44 | 31, 33 | readdcld 7907 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑛) + (1 / 𝑛)) ∈ ℝ) |
45 | | ltxrlt 7943 |
. . . . . . 7
⊢ (((𝐹‘𝑘) ∈ ℝ ∧ ((𝐹‘𝑛) + (1 / 𝑛)) ∈ ℝ) → ((𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛)) ↔ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (1 / 𝑛)))) |
46 | 32, 44, 45 | syl2anc 409 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛)) ↔ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (1 / 𝑛)))) |
47 | 40 | oveq2d 5840 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) = ((𝐹‘𝑛) + (1 / 𝑛))) |
48 | 47 | breq2d 3977 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ↔ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (1 / 𝑛)))) |
49 | 46, 48 | bitr4d 190 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛)) ↔ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))) |
50 | 43, 49 | anbi12d 465 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛))) ↔ ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) |
51 | 26, 28, 50 | 3imtr3d 201 |
. . 3
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) |
52 | 51 | ralrimiva 2530 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ℕ (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) |
53 | 52 | ralrimiva 2530 |
1
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ ℕ (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) |