Step | Hyp | Ref
| Expression |
1 | | elnnuz 8655 |
. . . . . 6
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
2 | 1 | biimpi 118 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘1)) |
3 | 2 | adantl 271 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
(ℤ≥‘1)) |
4 | | reex 7107 |
. . . . . 6
⊢ ℝ
∈ V |
5 | | rpssre 8744 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
6 | 4, 5 | ssexi 3916 |
. . . . 5
⊢
ℝ+ ∈ V |
7 | 6 | a1i 9 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ℝ+
∈ V) |
8 | | elnnuz 8655 |
. . . . . 6
⊢ (𝑎 ∈ ℕ ↔ 𝑎 ∈
(ℤ≥‘1)) |
9 | | resqrexlemex.seq |
. . . . . . 7
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}),
ℝ+) |
10 | | resqrexlemex.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
11 | | resqrexlemex.agt0 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝐴) |
12 | 9, 10, 11 | resqrexlem1arp 9891 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → ((ℕ × {(1
+ 𝐴)})‘𝑎) ∈
ℝ+) |
13 | 8, 12 | sylan2br 282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (ℤ≥‘1))
→ ((ℕ × {(1 + 𝐴)})‘𝑎) ∈
ℝ+) |
14 | 13 | adantlr 460 |
. . . 4
⊢ (((𝜑 ∧ 𝑁 ∈ ℕ) ∧ 𝑎 ∈ (ℤ≥‘1))
→ ((ℕ × {(1 + 𝐴)})‘𝑎) ∈
ℝ+) |
15 | 9, 10, 11 | resqrexlemp1rp 9892 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ (𝑎(𝑦 ∈ ℝ+,
𝑧 ∈
ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2))𝑏) ∈
ℝ+) |
16 | 15 | adantlr 460 |
. . . 4
⊢ (((𝜑 ∧ 𝑁 ∈ ℕ) ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ (𝑎(𝑦 ∈ ℝ+,
𝑧 ∈
ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2))𝑏) ∈
ℝ+) |
17 | 3, 7, 14, 16 | iseqp1 9445 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (seq1((𝑦 ∈ ℝ+,
𝑧 ∈
ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}),
ℝ+)‘(𝑁 + 1)) = ((seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}),
ℝ+)‘𝑁)(𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2))((ℕ × {(1 + 𝐴)})‘(𝑁 + 1)))) |
18 | 9 | fveq1i 5199 |
. . 3
⊢ (𝐹‘(𝑁 + 1)) = (seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}),
ℝ+)‘(𝑁 + 1)) |
19 | 9 | fveq1i 5199 |
. . . 4
⊢ (𝐹‘𝑁) = (seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}),
ℝ+)‘𝑁) |
20 | 19 | oveq1i 5542 |
. . 3
⊢ ((𝐹‘𝑁)(𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2))((ℕ × {(1 + 𝐴)})‘(𝑁 + 1))) = ((seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}),
ℝ+)‘𝑁)(𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2))((ℕ × {(1 + 𝐴)})‘(𝑁 + 1))) |
21 | 17, 18, 20 | 3eqtr4g 2138 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐹‘(𝑁 + 1)) = ((𝐹‘𝑁)(𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2))((ℕ × {(1 + 𝐴)})‘(𝑁 + 1)))) |
22 | | id 19 |
. . . . . . 7
⊢ (𝑦 = 𝑐 → 𝑦 = 𝑐) |
23 | | oveq2 5540 |
. . . . . . 7
⊢ (𝑦 = 𝑐 → (𝐴 / 𝑦) = (𝐴 / 𝑐)) |
24 | 22, 23 | oveq12d 5550 |
. . . . . 6
⊢ (𝑦 = 𝑐 → (𝑦 + (𝐴 / 𝑦)) = (𝑐 + (𝐴 / 𝑐))) |
25 | 24 | oveq1d 5547 |
. . . . 5
⊢ (𝑦 = 𝑐 → ((𝑦 + (𝐴 / 𝑦)) / 2) = ((𝑐 + (𝐴 / 𝑐)) / 2)) |
26 | | eqidd 2082 |
. . . . 5
⊢ (𝑧 = 𝑑 → ((𝑐 + (𝐴 / 𝑐)) / 2) = ((𝑐 + (𝐴 / 𝑐)) / 2)) |
27 | 25, 26 | cbvmpt2v 5604 |
. . . 4
⊢ (𝑦 ∈ ℝ+,
𝑧 ∈
ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)) = (𝑐 ∈ ℝ+, 𝑑 ∈ ℝ+
↦ ((𝑐 + (𝐴 / 𝑐)) / 2)) |
28 | 27 | a1i 9 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)) = (𝑐 ∈ ℝ+, 𝑑 ∈ ℝ+
↦ ((𝑐 + (𝐴 / 𝑐)) / 2))) |
29 | | id 19 |
. . . . . 6
⊢ (𝑐 = (𝐹‘𝑁) → 𝑐 = (𝐹‘𝑁)) |
30 | | oveq2 5540 |
. . . . . 6
⊢ (𝑐 = (𝐹‘𝑁) → (𝐴 / 𝑐) = (𝐴 / (𝐹‘𝑁))) |
31 | 29, 30 | oveq12d 5550 |
. . . . 5
⊢ (𝑐 = (𝐹‘𝑁) → (𝑐 + (𝐴 / 𝑐)) = ((𝐹‘𝑁) + (𝐴 / (𝐹‘𝑁)))) |
32 | 31 | oveq1d 5547 |
. . . 4
⊢ (𝑐 = (𝐹‘𝑁) → ((𝑐 + (𝐴 / 𝑐)) / 2) = (((𝐹‘𝑁) + (𝐴 / (𝐹‘𝑁))) / 2)) |
33 | 32 | ad2antrl 473 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ ℕ) ∧ (𝑐 = (𝐹‘𝑁) ∧ 𝑑 = ((ℕ × {(1 + 𝐴)})‘(𝑁 + 1)))) → ((𝑐 + (𝐴 / 𝑐)) / 2) = (((𝐹‘𝑁) + (𝐴 / (𝐹‘𝑁))) / 2)) |
34 | 9, 10, 11 | resqrexlemf 9893 |
. . . 4
⊢ (𝜑 → 𝐹:ℕ⟶ℝ+) |
35 | 34 | ffvelrnda 5323 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐹‘𝑁) ∈
ℝ+) |
36 | | peano2nn 8051 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
37 | 9, 10, 11 | resqrexlem1arp 9891 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ ℕ) → ((ℕ
× {(1 + 𝐴)})‘(𝑁 + 1)) ∈
ℝ+) |
38 | 36, 37 | sylan2 280 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ((ℕ ×
{(1 + 𝐴)})‘(𝑁 + 1)) ∈
ℝ+) |
39 | 35 | rpred 8773 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐹‘𝑁) ∈ ℝ) |
40 | 10 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ ℝ) |
41 | 40, 35 | rerpdivcld 8805 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐴 / (𝐹‘𝑁)) ∈ ℝ) |
42 | 39, 41 | readdcld 7148 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ((𝐹‘𝑁) + (𝐴 / (𝐹‘𝑁))) ∈ ℝ) |
43 | 42 | rehalfcld 8277 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (((𝐹‘𝑁) + (𝐴 / (𝐹‘𝑁))) / 2) ∈ ℝ) |
44 | 28, 33, 35, 38, 43 | ovmpt2d 5648 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ((𝐹‘𝑁)(𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2))((ℕ × {(1 + 𝐴)})‘(𝑁 + 1))) = (((𝐹‘𝑁) + (𝐴 / (𝐹‘𝑁))) / 2)) |
45 | 21, 44 | eqtrd 2113 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐹‘(𝑁 + 1)) = (((𝐹‘𝑁) + (𝐴 / (𝐹‘𝑁))) / 2)) |