Proof of Theorem resqrexlemgt0
Step | Hyp | Ref
| Expression |
1 | | oveq2 5850 |
. . . . . . . . 9
⊢ (𝑒 = -𝐿 → (𝐿 + 𝑒) = (𝐿 + -𝐿)) |
2 | 1 | breq2d 3994 |
. . . . . . . 8
⊢ (𝑒 = -𝐿 → ((𝐹‘𝑖) < (𝐿 + 𝑒) ↔ (𝐹‘𝑖) < (𝐿 + -𝐿))) |
3 | | oveq2 5850 |
. . . . . . . . 9
⊢ (𝑒 = -𝐿 → ((𝐹‘𝑖) + 𝑒) = ((𝐹‘𝑖) + -𝐿)) |
4 | 3 | breq2d 3994 |
. . . . . . . 8
⊢ (𝑒 = -𝐿 → (𝐿 < ((𝐹‘𝑖) + 𝑒) ↔ 𝐿 < ((𝐹‘𝑖) + -𝐿))) |
5 | 2, 4 | anbi12d 465 |
. . . . . . 7
⊢ (𝑒 = -𝐿 → (((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) ↔ ((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)))) |
6 | 5 | rexralbidv 2492 |
. . . . . 6
⊢ (𝑒 = -𝐿 → (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) ↔ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)))) |
7 | | resqrexlemgt0.lim |
. . . . . . 7
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒))) |
8 | 7 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 < 0) → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒))) |
9 | | resqrexlemgt0.rr |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ ℝ) |
10 | 9 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 < 0) → 𝐿 ∈ ℝ) |
11 | 10 | renegcld 8278 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 < 0) → -𝐿 ∈ ℝ) |
12 | 9 | lt0neg1d 8413 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 < 0 ↔ 0 < -𝐿)) |
13 | 12 | biimpa 294 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 < 0) → 0 < -𝐿) |
14 | 11, 13 | elrpd 9629 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 < 0) → -𝐿 ∈
ℝ+) |
15 | 6, 8, 14 | rspcdva 2835 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 < 0) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿))) |
16 | | simpl 108 |
. . . . . . . 8
⊢ (((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)) → (𝐹‘𝑖) < (𝐿 + -𝐿)) |
17 | 10 | recnd 7927 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐿 < 0) → 𝐿 ∈ ℂ) |
18 | 17 | negidd 8199 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐿 < 0) → (𝐿 + -𝐿) = 0) |
19 | 18 | breq2d 3994 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 < 0) → ((𝐹‘𝑖) < (𝐿 + -𝐿) ↔ (𝐹‘𝑖) < 0)) |
20 | 16, 19 | syl5ib 153 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 < 0) → (((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)) → (𝐹‘𝑖) < 0)) |
21 | 20 | ralimdv 2534 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 < 0) → (∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)) → ∀𝑖 ∈ (ℤ≥‘𝑗)(𝐹‘𝑖) < 0)) |
22 | 21 | reximdv 2567 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 < 0) → (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + -𝐿) ∧ 𝐿 < ((𝐹‘𝑖) + -𝐿)) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)(𝐹‘𝑖) < 0)) |
23 | 15, 22 | mpd 13 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 < 0) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)(𝐹‘𝑖) < 0) |
24 | | 0red 7900 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → 0 ∈
ℝ) |
25 | | eluznn 9538 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ℕ ∧ 𝑖 ∈
(ℤ≥‘𝑗)) → 𝑖 ∈ ℕ) |
26 | | resqrexlemex.seq |
. . . . . . . . . . . . . . 15
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)})) |
27 | | resqrexlemex.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
28 | | resqrexlemex.agt0 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ 𝐴) |
29 | 26, 27, 28 | resqrexlemf 10949 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℕ⟶ℝ+) |
30 | 29 | ffvelrnda 5620 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈
ℝ+) |
31 | 25, 30 | sylan2 284 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑖) ∈
ℝ+) |
32 | 31 | rpred 9632 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑖) ∈ ℝ) |
33 | 31 | rpgt0d 9635 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → 0 < (𝐹‘𝑖)) |
34 | 24, 32, 33 | ltnsymd 8018 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → ¬ (𝐹‘𝑖) < 0) |
35 | 34 | pm2.21d 609 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑖) < 0 → ⊥)) |
36 | 35 | anassrs 398 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑖) < 0 → ⊥)) |
37 | 36 | ralimdva 2533 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∀𝑖 ∈
(ℤ≥‘𝑗)(𝐹‘𝑖) < 0 → ∀𝑖 ∈ (ℤ≥‘𝑗)⊥)) |
38 | | nnz 9210 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
39 | | uzid 9480 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
40 | | elex2 2742 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → ∃𝑧 𝑧 ∈ (ℤ≥‘𝑗)) |
41 | | r19.3rmv 3499 |
. . . . . . . . . 10
⊢
(∃𝑧 𝑧 ∈
(ℤ≥‘𝑗) → (⊥ ↔ ∀𝑖 ∈
(ℤ≥‘𝑗)⊥)) |
42 | 39, 40, 41 | 3syl 17 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℤ → (⊥
↔ ∀𝑖 ∈
(ℤ≥‘𝑗)⊥)) |
43 | 38, 42 | syl 14 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → (⊥
↔ ∀𝑖 ∈
(ℤ≥‘𝑗)⊥)) |
44 | 43 | adantl 275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (⊥ ↔
∀𝑖 ∈
(ℤ≥‘𝑗)⊥)) |
45 | 37, 44 | sylibrd 168 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∀𝑖 ∈
(ℤ≥‘𝑗)(𝐹‘𝑖) < 0 → ⊥)) |
46 | 45 | rexlimdva 2583 |
. . . . 5
⊢ (𝜑 → (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)(𝐹‘𝑖) < 0 → ⊥)) |
47 | 46 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 < 0) → (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)(𝐹‘𝑖) < 0 → ⊥)) |
48 | 23, 47 | mpd 13 |
. . 3
⊢ ((𝜑 ∧ 𝐿 < 0) → ⊥) |
49 | 48 | inegd 1362 |
. 2
⊢ (𝜑 → ¬ 𝐿 < 0) |
50 | | 0re 7899 |
. . 3
⊢ 0 ∈
ℝ |
51 | | lenlt 7974 |
. . 3
⊢ ((0
∈ ℝ ∧ 𝐿
∈ ℝ) → (0 ≤ 𝐿 ↔ ¬ 𝐿 < 0)) |
52 | 50, 9, 51 | sylancr 411 |
. 2
⊢ (𝜑 → (0 ≤ 𝐿 ↔ ¬ 𝐿 < 0)) |
53 | 49, 52 | mpbird 166 |
1
⊢ (𝜑 → 0 ≤ 𝐿) |