Step | Hyp | Ref
| Expression |
1 | | simpll 519 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 𝑥 < 0) → 𝑥 ∈ ℝ) |
2 | | simpr 109 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 𝑥 < 0) → 𝑥 < 0) |
3 | 1, 2 | lt0ap0d 8503 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 𝑥 < 0) → 𝑥 # 0) |
4 | | rerecclap 8582 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 # 0) → (1 / 𝑥) ∈
ℝ) |
5 | | recn 7844 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
6 | | recidap 8538 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 # 0) → (𝑥 · (1 / 𝑥)) = 1) |
7 | 5, 6 | sylan 281 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 # 0) → (𝑥 · (1 / 𝑥)) = 1) |
8 | | oveq2 5822 |
. . . . . . . . 9
⊢ (𝑧 = (1 / 𝑥) → (𝑥 · 𝑧) = (𝑥 · (1 / 𝑥))) |
9 | 8 | eqeq1d 2163 |
. . . . . . . 8
⊢ (𝑧 = (1 / 𝑥) → ((𝑥 · 𝑧) = 1 ↔ (𝑥 · (1 / 𝑥)) = 1)) |
10 | 9 | rspcev 2813 |
. . . . . . 7
⊢ (((1 /
𝑥) ∈ ℝ ∧
(𝑥 · (1 / 𝑥)) = 1) → ∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1) |
11 | 4, 7, 10 | syl2anc 409 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 # 0) → ∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1) |
12 | 1, 3, 11 | syl2anc 409 |
. . . . 5
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 𝑥 < 0) → ∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1) |
13 | 12 | orcd 723 |
. . . 4
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 𝑥 < 0) → (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0)) |
14 | | simpr 109 |
. . . . 5
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 𝑥 = 0) → 𝑥 = 0) |
15 | 14 | olcd 724 |
. . . 4
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 𝑥 = 0) → (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0)) |
16 | | simpll 519 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 0 < 𝑥) → 𝑥 ∈ ℝ) |
17 | | simpr 109 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 0 < 𝑥) → 0 < 𝑥) |
18 | 16, 17 | gt0ap0d 8483 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 0 < 𝑥) → 𝑥 # 0) |
19 | 16, 18, 11 | syl2anc 409 |
. . . . 5
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 0 < 𝑥) → ∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1) |
20 | 19 | orcd 723 |
. . . 4
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) ∧ 0 < 𝑥) → (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0)) |
21 | | 0re 7857 |
. . . . . 6
⊢ 0 ∈
ℝ |
22 | | breq2 3965 |
. . . . . . . 8
⊢ (𝑦 = 0 → (𝑥 < 𝑦 ↔ 𝑥 < 0)) |
23 | | eqeq2 2164 |
. . . . . . . 8
⊢ (𝑦 = 0 → (𝑥 = 𝑦 ↔ 𝑥 = 0)) |
24 | | breq1 3964 |
. . . . . . . 8
⊢ (𝑦 = 0 → (𝑦 < 𝑥 ↔ 0 < 𝑥)) |
25 | 22, 23, 24 | 3orbi123d 1290 |
. . . . . . 7
⊢ (𝑦 = 0 → ((𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ (𝑥 < 0 ∨ 𝑥 = 0 ∨ 0 < 𝑥))) |
26 | 25 | rspcv 2809 |
. . . . . 6
⊢ (0 ∈
ℝ → (∀𝑦
∈ ℝ (𝑥 <
𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → (𝑥 < 0 ∨ 𝑥 = 0 ∨ 0 < 𝑥))) |
27 | 21, 26 | ax-mp 5 |
. . . . 5
⊢
(∀𝑦 ∈
ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → (𝑥 < 0 ∨ 𝑥 = 0 ∨ 0 < 𝑥)) |
28 | 27 | adantl 275 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) → (𝑥 < 0 ∨ 𝑥 = 0 ∨ 0 < 𝑥)) |
29 | 13, 15, 20, 28 | mpjao3dan 1286 |
. . 3
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) → (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0)) |
30 | 29 | ralimiaa 2516 |
. 2
⊢
(∀𝑥 ∈
ℝ ∀𝑦 ∈
ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → ∀𝑥 ∈ ℝ (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0)) |
31 | | oveq1 5821 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑥 · 𝑧) = (𝑤 · 𝑧)) |
32 | 31 | eqeq1d 2163 |
. . . . . 6
⊢ (𝑥 = 𝑤 → ((𝑥 · 𝑧) = 1 ↔ (𝑤 · 𝑧) = 1)) |
33 | 32 | rexbidv 2455 |
. . . . 5
⊢ (𝑥 = 𝑤 → (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ↔ ∃𝑧 ∈ ℝ (𝑤 · 𝑧) = 1)) |
34 | | eqeq1 2161 |
. . . . 5
⊢ (𝑥 = 𝑤 → (𝑥 = 0 ↔ 𝑤 = 0)) |
35 | 33, 34 | orbi12d 783 |
. . . 4
⊢ (𝑥 = 𝑤 → ((∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0) ↔ (∃𝑧 ∈ ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0))) |
36 | 35 | cbvralv 2677 |
. . 3
⊢
(∀𝑥 ∈
ℝ (∃𝑧 ∈
ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0) ↔ ∀𝑤 ∈ ℝ (∃𝑧 ∈ ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0)) |
37 | | nfcv 2296 |
. . . . . . . . 9
⊢
Ⅎ𝑧ℝ |
38 | | nfre1 2497 |
. . . . . . . . . 10
⊢
Ⅎ𝑧∃𝑧 ∈ ℝ (𝑤 · 𝑧) = 1 |
39 | | nfv 1505 |
. . . . . . . . . 10
⊢
Ⅎ𝑧 𝑤 = 0 |
40 | 38, 39 | nfor 1551 |
. . . . . . . . 9
⊢
Ⅎ𝑧(∃𝑧 ∈ ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) |
41 | 37, 40 | nfralya 2494 |
. . . . . . . 8
⊢
Ⅎ𝑧∀𝑤 ∈ ℝ (∃𝑧 ∈ ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) |
42 | | nfv 1505 |
. . . . . . . 8
⊢
Ⅎ𝑧(𝑥 ∈ ℝ ∧ 𝑦 ∈
ℝ) |
43 | 41, 42 | nfan 1542 |
. . . . . . 7
⊢
Ⅎ𝑧(∀𝑤 ∈ ℝ (∃𝑧 ∈ ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) |
44 | | nfv 1505 |
. . . . . . 7
⊢
Ⅎ𝑧(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) |
45 | | simpr 109 |
. . . . . . . . . . 11
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ (𝑦 − 𝑥) < 0) → (𝑦 − 𝑥) < 0) |
46 | | simprr 522 |
. . . . . . . . . . . . . 14
⊢
((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑦 ∈ ℝ) |
47 | 46 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → 𝑦 ∈ ℝ) |
48 | 47 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ (𝑦 − 𝑥) < 0) → 𝑦 ∈ ℝ) |
49 | | simprl 521 |
. . . . . . . . . . . . . 14
⊢
((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑥 ∈ ℝ) |
50 | 49 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → 𝑥 ∈ ℝ) |
51 | 50 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ (𝑦 − 𝑥) < 0) → 𝑥 ∈ ℝ) |
52 | 48, 51 | sublt0d 8424 |
. . . . . . . . . . 11
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ (𝑦 − 𝑥) < 0) → ((𝑦 − 𝑥) < 0 ↔ 𝑦 < 𝑥)) |
53 | 45, 52 | mpbid 146 |
. . . . . . . . . 10
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ (𝑦 − 𝑥) < 0) → 𝑦 < 𝑥) |
54 | 53 | 3mix3d 1159 |
. . . . . . . . 9
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ (𝑦 − 𝑥) < 0) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) |
55 | | simpr 109 |
. . . . . . . . . . 11
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ 0 < (𝑦 − 𝑥)) → 0 < (𝑦 − 𝑥)) |
56 | 50 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ 0 < (𝑦 − 𝑥)) → 𝑥 ∈ ℝ) |
57 | 47 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ 0 < (𝑦 − 𝑥)) → 𝑦 ∈ ℝ) |
58 | 56, 57 | posdifd 8386 |
. . . . . . . . . . 11
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ 0 < (𝑦 − 𝑥)) → (𝑥 < 𝑦 ↔ 0 < (𝑦 − 𝑥))) |
59 | 55, 58 | mpbird 166 |
. . . . . . . . . 10
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ 0 < (𝑦 − 𝑥)) → 𝑥 < 𝑦) |
60 | 59 | 3mix1d 1157 |
. . . . . . . . 9
⊢
(((((∀𝑤
∈ ℝ (∃𝑧
∈ ℝ (𝑤 ·
𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) ∧ 0 < (𝑦 − 𝑥)) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) |
61 | 47 | recnd 7885 |
. . . . . . . . . . . 12
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → 𝑦 ∈ ℂ) |
62 | 50 | recnd 7885 |
. . . . . . . . . . . 12
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → 𝑥 ∈ ℂ) |
63 | 61, 62 | subcld 8165 |
. . . . . . . . . . 11
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → (𝑦 − 𝑥) ∈ ℂ) |
64 | | simplr 520 |
. . . . . . . . . . . 12
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → 𝑧 ∈ ℝ) |
65 | 64 | recnd 7885 |
. . . . . . . . . . 11
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → 𝑧 ∈ ℂ) |
66 | | simpr 109 |
. . . . . . . . . . . 12
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → ((𝑦 − 𝑥) · 𝑧) = 1) |
67 | | 1ap0 8444 |
. . . . . . . . . . . 12
⊢ 1 #
0 |
68 | 66, 67 | eqbrtrdi 3999 |
. . . . . . . . . . 11
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → ((𝑦 − 𝑥) · 𝑧) # 0) |
69 | 63, 65, 68 | mulap0bad 8512 |
. . . . . . . . . 10
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → (𝑦 − 𝑥) # 0) |
70 | 46, 49 | resubcld 8235 |
. . . . . . . . . . . 12
⊢
((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑦 − 𝑥) ∈ ℝ) |
71 | 70 | ad2antrr 480 |
. . . . . . . . . . 11
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → (𝑦 − 𝑥) ∈ ℝ) |
72 | | reaplt 8442 |
. . . . . . . . . . 11
⊢ (((𝑦 − 𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((𝑦 − 𝑥) # 0 ↔ ((𝑦 − 𝑥) < 0 ∨ 0 < (𝑦 − 𝑥)))) |
73 | 71, 21, 72 | sylancl 410 |
. . . . . . . . . 10
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → ((𝑦 − 𝑥) # 0 ↔ ((𝑦 − 𝑥) < 0 ∨ 0 < (𝑦 − 𝑥)))) |
74 | 69, 73 | mpbid 146 |
. . . . . . . . 9
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → ((𝑦 − 𝑥) < 0 ∨ 0 < (𝑦 − 𝑥))) |
75 | 54, 60, 74 | mpjaodan 788 |
. . . . . . . 8
⊢
((((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝑧 ∈ ℝ) ∧ ((𝑦 − 𝑥) · 𝑧) = 1) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) |
76 | 75 | exp31 362 |
. . . . . . 7
⊢
((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑧 ∈ ℝ → (((𝑦 − 𝑥) · 𝑧) = 1 → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)))) |
77 | 43, 44, 76 | rexlimd 2568 |
. . . . . 6
⊢
((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (∃𝑧 ∈ ℝ ((𝑦 − 𝑥) · 𝑧) = 1 → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))) |
78 | 77 | imp 123 |
. . . . 5
⊢
(((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ ∃𝑧 ∈ ℝ ((𝑦 − 𝑥) · 𝑧) = 1) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) |
79 | 46 | recnd 7885 |
. . . . . . . . 9
⊢
((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑦 ∈ ℂ) |
80 | 79 | adantr 274 |
. . . . . . . 8
⊢
(((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ (𝑦 − 𝑥) = 0) → 𝑦 ∈ ℂ) |
81 | 49 | recnd 7885 |
. . . . . . . . 9
⊢
((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑥 ∈ ℂ) |
82 | 81 | adantr 274 |
. . . . . . . 8
⊢
(((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ (𝑦 − 𝑥) = 0) → 𝑥 ∈ ℂ) |
83 | | simpr 109 |
. . . . . . . 8
⊢
(((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ (𝑦 − 𝑥) = 0) → (𝑦 − 𝑥) = 0) |
84 | 80, 82, 83 | subeq0d 8173 |
. . . . . . 7
⊢
(((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ (𝑦 − 𝑥) = 0) → 𝑦 = 𝑥) |
85 | 84 | equcomd 1684 |
. . . . . 6
⊢
(((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ (𝑦 − 𝑥) = 0) → 𝑥 = 𝑦) |
86 | 85 | 3mix2d 1158 |
. . . . 5
⊢
(((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ (𝑦 − 𝑥) = 0) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) |
87 | | oveq1 5821 |
. . . . . . . . 9
⊢ (𝑤 = (𝑦 − 𝑥) → (𝑤 · 𝑧) = ((𝑦 − 𝑥) · 𝑧)) |
88 | 87 | eqeq1d 2163 |
. . . . . . . 8
⊢ (𝑤 = (𝑦 − 𝑥) → ((𝑤 · 𝑧) = 1 ↔ ((𝑦 − 𝑥) · 𝑧) = 1)) |
89 | 88 | rexbidv 2455 |
. . . . . . 7
⊢ (𝑤 = (𝑦 − 𝑥) → (∃𝑧 ∈ ℝ (𝑤 · 𝑧) = 1 ↔ ∃𝑧 ∈ ℝ ((𝑦 − 𝑥) · 𝑧) = 1)) |
90 | | eqeq1 2161 |
. . . . . . 7
⊢ (𝑤 = (𝑦 − 𝑥) → (𝑤 = 0 ↔ (𝑦 − 𝑥) = 0)) |
91 | 89, 90 | orbi12d 783 |
. . . . . 6
⊢ (𝑤 = (𝑦 − 𝑥) → ((∃𝑧 ∈ ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ↔ (∃𝑧 ∈ ℝ ((𝑦 − 𝑥) · 𝑧) = 1 ∨ (𝑦 − 𝑥) = 0))) |
92 | | simpl 108 |
. . . . . 6
⊢
((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → ∀𝑤 ∈ ℝ (∃𝑧 ∈ ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0)) |
93 | 91, 92, 70 | rspcdva 2818 |
. . . . 5
⊢
((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (∃𝑧 ∈ ℝ ((𝑦 − 𝑥) · 𝑧) = 1 ∨ (𝑦 − 𝑥) = 0)) |
94 | 78, 86, 93 | mpjaodan 788 |
. . . 4
⊢
((∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) |
95 | 94 | ralrimivva 2536 |
. . 3
⊢
(∀𝑤 ∈
ℝ (∃𝑧 ∈
ℝ (𝑤 · 𝑧) = 1 ∨ 𝑤 = 0) → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) |
96 | 36, 95 | sylbi 120 |
. 2
⊢
(∀𝑥 ∈
ℝ (∃𝑧 ∈
ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0) → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) |
97 | 30, 96 | impbii 125 |
1
⊢
(∀𝑥 ∈
ℝ ∀𝑦 ∈
ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑥 ∈ ℝ (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0)) |