Proof of Theorem resqrexlemgt0
Step | Hyp | Ref
| Expression |
1 | | resqrexlemgt0.rr |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ ℝ) |
2 | 1 | adantr 270 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 < 0) → 𝐿 ∈ ℝ) |
3 | 2 | renegcld 7484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 < 0) → -𝐿 ∈ ℝ) |
4 | 1 | lt0neg1d 7616 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 < 0 ↔ 0 < -𝐿)) |
5 | 4 | biimpa 290 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 < 0) → 0 < -𝐿) |
6 | 3, 5 | elrpd 8771 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 < 0) → -𝐿 ∈
ℝ+) |
7 | | resqrexlemgt0.lim |
. . . . . . 7
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒))) |
8 | 7 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 < 0) → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒))) |
9 | | oveq2 5540 |
. . . . . . . . . 10
⊢ (𝑒 = -𝐿 → (𝐿 + 𝑒) = (𝐿 + -𝐿)) |
10 | 9 | breq2d 3797 |
. . . . . . . . 9
⊢ (𝑒 = -𝐿 → ((𝐹‘𝑖) < (𝐿 + 𝑒) ↔ (𝐹‘𝑖) < (𝐿 + -𝐿))) |
11 | | oveq2 5540 |
. . . . . . . . . 10
⊢ (𝑒 = -𝐿 → ((𝐹‘𝑖) + 𝑒) = ((𝐹‘𝑖) + -𝐿)) |
12 | 11 | breq2d 3797 |
. . . . . . . . 9
⊢ (𝑒 = -𝐿 → (𝐿 < ((𝐹‘𝑖) + 𝑒) ↔ 𝐿 < ((𝐹‘𝑖) + -𝐿))) |
13 | 10, 12 | anbi12d 456 |
. . . . . . . 8
⊢ (𝑒 = -𝐿 → (((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) ↔ ((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)))) |
14 | 13 | rexralbidv 2392 |
. . . . . . 7
⊢ (𝑒 = -𝐿 → (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) ↔ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)))) |
15 | 14 | rspcv 2697 |
. . . . . 6
⊢ (-𝐿 ∈ ℝ+
→ (∀𝑒 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)))) |
16 | 6, 8, 15 | sylc 61 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 < 0) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿))) |
17 | | simpl 107 |
. . . . . . . 8
⊢ (((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)) → (𝐹‘𝑖) < (𝐿 + -𝐿)) |
18 | 2 | recnd 7147 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐿 < 0) → 𝐿 ∈ ℂ) |
19 | 18 | negidd 7409 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐿 < 0) → (𝐿 + -𝐿) = 0) |
20 | 19 | breq2d 3797 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 < 0) → ((𝐹‘𝑖) < (𝐿 + -𝐿) ↔ (𝐹‘𝑖) < 0)) |
21 | 17, 20 | syl5ib 152 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 < 0) → (((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)) → (𝐹‘𝑖) < 0)) |
22 | 21 | ralimdv 2430 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 < 0) → (∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)) → ∀𝑖 ∈ (ℤ≥‘𝑗)(𝐹‘𝑖) < 0)) |
23 | 22 | reximdv 2462 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 < 0) → (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)(𝐹‘𝑖) < 0)) |
24 | 16, 23 | mpd 13 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 < 0) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)(𝐹‘𝑖) < 0) |
25 | | 0red 7120 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → 0 ∈
ℝ) |
26 | | eluznn 8687 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ℕ ∧ 𝑖 ∈
(ℤ≥‘𝑗)) → 𝑖 ∈ ℕ) |
27 | | resqrexlemex.seq |
. . . . . . . . . . . . . . 15
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}),
ℝ+) |
28 | | resqrexlemex.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
29 | | resqrexlemex.agt0 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ 𝐴) |
30 | 27, 28, 29 | resqrexlemf 9893 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℕ⟶ℝ+) |
31 | 30 | ffvelrnda 5323 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈
ℝ+) |
32 | 26, 31 | sylan2 280 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑖) ∈
ℝ+) |
33 | 32 | rpred 8773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑖) ∈ ℝ) |
34 | 32 | rpgt0d 8776 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → 0 < (𝐹‘𝑖)) |
35 | 25, 33, 34 | ltnsymd 7229 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → ¬ (𝐹‘𝑖) < 0) |
36 | 35 | pm2.21d 581 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑖) < 0 → ⊥)) |
37 | 36 | anassrs 392 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑖) < 0 → ⊥)) |
38 | 37 | ralimdva 2429 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∀𝑖 ∈
(ℤ≥‘𝑗)(𝐹‘𝑖) < 0 → ∀𝑖 ∈ (ℤ≥‘𝑗)⊥)) |
39 | | nnz 8370 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
40 | | uzid 8633 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
41 | | elex2 2615 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → ∃𝑧 𝑧 ∈ (ℤ≥‘𝑗)) |
42 | | r19.3rmv 3332 |
. . . . . . . . . 10
⊢
(∃𝑧 𝑧 ∈
(ℤ≥‘𝑗) → (⊥ ↔ ∀𝑖 ∈
(ℤ≥‘𝑗)⊥)) |
43 | 40, 41, 42 | 3syl 17 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℤ → (⊥
↔ ∀𝑖 ∈
(ℤ≥‘𝑗)⊥)) |
44 | 39, 43 | syl 14 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → (⊥
↔ ∀𝑖 ∈
(ℤ≥‘𝑗)⊥)) |
45 | 44 | adantl 271 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (⊥ ↔
∀𝑖 ∈
(ℤ≥‘𝑗)⊥)) |
46 | 38, 45 | sylibrd 167 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∀𝑖 ∈
(ℤ≥‘𝑗)(𝐹‘𝑖) < 0 → ⊥)) |
47 | 46 | rexlimdva 2477 |
. . . . 5
⊢ (𝜑 → (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)(𝐹‘𝑖) < 0 → ⊥)) |
48 | 47 | adantr 270 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 < 0) → (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)(𝐹‘𝑖) < 0 → ⊥)) |
49 | 24, 48 | mpd 13 |
. . 3
⊢ ((𝜑 ∧ 𝐿 < 0) → ⊥) |
50 | 49 | inegd 1303 |
. 2
⊢ (𝜑 → ¬ 𝐿 < 0) |
51 | | 0re 7119 |
. . 3
⊢ 0 ∈
ℝ |
52 | | lenlt 7187 |
. . 3
⊢ ((0
∈ ℝ ∧ 𝐿
∈ ℝ) → (0 ≤ 𝐿 ↔ ¬ 𝐿 < 0)) |
53 | 51, 1, 52 | sylancr 405 |
. 2
⊢ (𝜑 → (0 ≤ 𝐿 ↔ ¬ 𝐿 < 0)) |
54 | 50, 53 | mpbird 165 |
1
⊢ (𝜑 → 0 ≤ 𝐿) |