Step | Hyp | Ref
| Expression |
1 | | breq2 3965 |
. . 3
⊢ (𝑞 = 𝑠 → (𝐴 # 𝑞 ↔ 𝐴 # 𝑠)) |
2 | 1 | cbvralv 2677 |
. 2
⊢
(∀𝑞 ∈
ℚ 𝐴 # 𝑞 ↔ ∀𝑠 ∈ ℚ 𝐴 # 𝑠) |
3 | | simplll 523 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → 𝐴 ∈ ℝ) |
4 | 3 | adantr 274 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑞 < 𝑟) → 𝐴 ∈ ℝ) |
5 | | simplrl 525 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → 𝑞 ∈ ℚ) |
6 | 5 | adantr 274 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑞 < 𝑟) → 𝑞 ∈ ℚ) |
7 | | simplrr 526 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → 𝑟 ∈ ℚ) |
8 | 7 | adantr 274 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑞 < 𝑟) → 𝑟 ∈ ℚ) |
9 | | simpr 109 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑞 < 𝑟) → 𝑞 < 𝑟) |
10 | | breq2 3965 |
. . . . . . . . . 10
⊢ (𝑠 = ((𝑞 + 𝑟) / 2) → (𝐴 # 𝑠 ↔ 𝐴 # ((𝑞 + 𝑟) / 2))) |
11 | | simpllr 524 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → ∀𝑠 ∈ ℚ 𝐴 # 𝑠) |
12 | | qaddcl 9522 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ) → (𝑞 + 𝑟) ∈ ℚ) |
13 | 5, 7, 12 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → (𝑞 + 𝑟) ∈ ℚ) |
14 | | 2z 9174 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
15 | | zq 9513 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℤ → 2 ∈ ℚ) |
16 | 14, 15 | mp1i 10 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → 2 ∈ ℚ) |
17 | | 2ne0 8904 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
18 | 17 | a1i 9 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → 2 ≠ 0) |
19 | | qdivcl 9530 |
. . . . . . . . . . 11
⊢ (((𝑞 + 𝑟) ∈ ℚ ∧ 2 ∈ ℚ ∧
2 ≠ 0) → ((𝑞 +
𝑟) / 2) ∈
ℚ) |
20 | 13, 16, 18, 19 | syl3anc 1217 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → ((𝑞 + 𝑟) / 2) ∈ ℚ) |
21 | 10, 11, 20 | rspcdva 2818 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → 𝐴 # ((𝑞 + 𝑟) / 2)) |
22 | 3 | recnd 7885 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → 𝐴 ∈ ℂ) |
23 | | qcn 9521 |
. . . . . . . . . . 11
⊢ (((𝑞 + 𝑟) / 2) ∈ ℚ → ((𝑞 + 𝑟) / 2) ∈ ℂ) |
24 | 20, 23 | syl 14 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → ((𝑞 + 𝑟) / 2) ∈ ℂ) |
25 | | apsym 8460 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ ((𝑞 + 𝑟) / 2) ∈ ℂ) → (𝐴 # ((𝑞 + 𝑟) / 2) ↔ ((𝑞 + 𝑟) / 2) # 𝐴)) |
26 | 22, 24, 25 | syl2anc 409 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → (𝐴 # ((𝑞 + 𝑟) / 2) ↔ ((𝑞 + 𝑟) / 2) # 𝐴)) |
27 | 21, 26 | mpbid 146 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → ((𝑞 + 𝑟) / 2) # 𝐴) |
28 | 27 | adantr 274 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑞 < 𝑟) → ((𝑞 + 𝑟) / 2) # 𝐴) |
29 | 4, 6, 8, 9, 28 | apdifflemf 13558 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑞 < 𝑟) → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))) |
30 | 3 | adantr 274 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → 𝐴 ∈ ℝ) |
31 | 7 | adantr 274 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → 𝑟 ∈ ℚ) |
32 | 5 | adantr 274 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → 𝑞 ∈ ℚ) |
33 | | simpr 109 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → 𝑟 < 𝑞) |
34 | | qcn 9521 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℚ → 𝑞 ∈
ℂ) |
35 | 5, 34 | syl 14 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → 𝑞 ∈ ℂ) |
36 | | qcn 9521 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℚ → 𝑟 ∈
ℂ) |
37 | 7, 36 | syl 14 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → 𝑟 ∈ ℂ) |
38 | 35, 37 | addcomd 8005 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → (𝑞 + 𝑟) = (𝑟 + 𝑞)) |
39 | 38 | oveq1d 5829 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → ((𝑞 + 𝑟) / 2) = ((𝑟 + 𝑞) / 2)) |
40 | 39, 27 | eqbrtrrd 3984 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → ((𝑟 + 𝑞) / 2) # 𝐴) |
41 | 40 | adantr 274 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → ((𝑟 + 𝑞) / 2) # 𝐴) |
42 | 30, 31, 32, 33, 41 | apdifflemf 13558 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → (abs‘(𝐴 − 𝑟)) # (abs‘(𝐴 − 𝑞))) |
43 | 22 | adantr 274 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → 𝐴 ∈ ℂ) |
44 | 31, 36 | syl 14 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → 𝑟 ∈ ℂ) |
45 | 43, 44 | subcld 8165 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → (𝐴 − 𝑟) ∈ ℂ) |
46 | 45 | abscld 11058 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → (abs‘(𝐴 − 𝑟)) ∈ ℝ) |
47 | 46 | recnd 7885 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → (abs‘(𝐴 − 𝑟)) ∈ ℂ) |
48 | 32, 34 | syl 14 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → 𝑞 ∈ ℂ) |
49 | 43, 48 | subcld 8165 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → (𝐴 − 𝑞) ∈ ℂ) |
50 | 49 | abscld 11058 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → (abs‘(𝐴 − 𝑞)) ∈ ℝ) |
51 | 50 | recnd 7885 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → (abs‘(𝐴 − 𝑞)) ∈ ℂ) |
52 | | apsym 8460 |
. . . . . . . 8
⊢
(((abs‘(𝐴
− 𝑟)) ∈ ℂ
∧ (abs‘(𝐴 −
𝑞)) ∈ ℂ) →
((abs‘(𝐴 −
𝑟)) # (abs‘(𝐴 − 𝑞)) ↔ (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) |
53 | 47, 51, 52 | syl2anc 409 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → ((abs‘(𝐴 − 𝑟)) # (abs‘(𝐴 − 𝑞)) ↔ (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) |
54 | 42, 53 | mpbid 146 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ ∀𝑠
∈ ℚ 𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) ∧ 𝑟 < 𝑞) → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))) |
55 | | simpr 109 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → 𝑞 ≠ 𝑟) |
56 | | qlttri2 9528 |
. . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ) → (𝑞 ≠ 𝑟 ↔ (𝑞 < 𝑟 ∨ 𝑟 < 𝑞))) |
57 | 5, 7, 56 | syl2anc 409 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → (𝑞 ≠ 𝑟 ↔ (𝑞 < 𝑟 ∨ 𝑟 < 𝑞))) |
58 | 55, 57 | mpbid 146 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → (𝑞 < 𝑟 ∨ 𝑟 < 𝑞)) |
59 | 29, 54, 58 | mpjaodan 788 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ 𝑞 ≠ 𝑟) → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))) |
60 | 59 | ex 114 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) → (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) |
61 | 60 | ralrimivva 2536 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
∀𝑠 ∈ ℚ
𝐴 # 𝑠) → ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) |
62 | | simpll 519 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) → 𝐴 ∈ ℝ) |
63 | | simpr 109 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) → 𝑠 ∈ ℚ) |
64 | | simplr 520 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) → ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) |
65 | | neg1rr 8918 |
. . . . . . . 8
⊢ -1 ∈
ℝ |
66 | | neg1lt0 8920 |
. . . . . . . . 9
⊢ -1 <
0 |
67 | | 0lt1 7981 |
. . . . . . . . 9
⊢ 0 <
1 |
68 | | 0re 7857 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
69 | | 1re 7856 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
70 | 65, 68, 69 | lttri 7960 |
. . . . . . . . 9
⊢ ((-1 <
0 ∧ 0 < 1) → -1 < 1) |
71 | 66, 67, 70 | mp2an 423 |
. . . . . . . 8
⊢ -1 <
1 |
72 | 65, 71 | ltneii 7952 |
. . . . . . 7
⊢ -1 ≠
1 |
73 | 72 | a1i 9 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) → -1 ≠
1) |
74 | | neg1z 9178 |
. . . . . . . 8
⊢ -1 ∈
ℤ |
75 | | zq 9513 |
. . . . . . . 8
⊢ (-1
∈ ℤ → -1 ∈ ℚ) |
76 | 74, 75 | mp1i 10 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) → -1 ∈
ℚ) |
77 | | 1z 9172 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
78 | | zq 9513 |
. . . . . . . 8
⊢ (1 ∈
ℤ → 1 ∈ ℚ) |
79 | 77, 78 | mp1i 10 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) → 1 ∈
ℚ) |
80 | | simpl 108 |
. . . . . . . . . 10
⊢ ((𝑞 = -1 ∧ 𝑟 = 1) → 𝑞 = -1) |
81 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝑞 = -1 ∧ 𝑟 = 1) → 𝑟 = 1) |
82 | 80, 81 | neeq12d 2344 |
. . . . . . . . 9
⊢ ((𝑞 = -1 ∧ 𝑟 = 1) → (𝑞 ≠ 𝑟 ↔ -1 ≠ 1)) |
83 | 80 | oveq2d 5830 |
. . . . . . . . . . 11
⊢ ((𝑞 = -1 ∧ 𝑟 = 1) → (𝐴 − 𝑞) = (𝐴 − -1)) |
84 | 83 | fveq2d 5465 |
. . . . . . . . . 10
⊢ ((𝑞 = -1 ∧ 𝑟 = 1) → (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − -1))) |
85 | 81 | oveq2d 5830 |
. . . . . . . . . . 11
⊢ ((𝑞 = -1 ∧ 𝑟 = 1) → (𝐴 − 𝑟) = (𝐴 − 1)) |
86 | 85 | fveq2d 5465 |
. . . . . . . . . 10
⊢ ((𝑞 = -1 ∧ 𝑟 = 1) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 1))) |
87 | 84, 86 | breq12d 3974 |
. . . . . . . . 9
⊢ ((𝑞 = -1 ∧ 𝑟 = 1) → ((abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐴 − -1)) # (abs‘(𝐴 − 1)))) |
88 | 82, 87 | imbi12d 233 |
. . . . . . . 8
⊢ ((𝑞 = -1 ∧ 𝑟 = 1) → ((𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))) ↔ (-1 ≠ 1 →
(abs‘(𝐴 − -1))
# (abs‘(𝐴 −
1))))) |
89 | 88 | rspc2gv 2825 |
. . . . . . 7
⊢ ((-1
∈ ℚ ∧ 1 ∈ ℚ) → (∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))) → (-1 ≠ 1 →
(abs‘(𝐴 − -1))
# (abs‘(𝐴 −
1))))) |
90 | 76, 79, 89 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) → (∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))) → (-1 ≠ 1 →
(abs‘(𝐴 − -1))
# (abs‘(𝐴 −
1))))) |
91 | 64, 73, 90 | mp2d 47 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) → (abs‘(𝐴 − -1)) #
(abs‘(𝐴 −
1))) |
92 | | simpllr 524 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) |
93 | | 2cnd 8885 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 2 ∈
ℂ) |
94 | | simplr 520 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℚ) |
95 | | qcn 9521 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ℚ → 𝑠 ∈
ℂ) |
96 | 94, 95 | syl 14 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ) |
97 | | 2ap0 8905 |
. . . . . . . . . 10
⊢ 2 #
0 |
98 | 97 | a1i 9 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 2 # 0) |
99 | | simpr 109 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 𝑠 ≠ 0) |
100 | | 0z 9157 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℤ |
101 | | zq 9513 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
102 | 100, 101 | mp1i 10 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 0 ∈
ℚ) |
103 | | qapne 9526 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ ℚ ∧ 0 ∈
ℚ) → (𝑠 # 0
↔ 𝑠 ≠
0)) |
104 | 94, 102, 103 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → (𝑠 # 0 ↔ 𝑠 ≠ 0)) |
105 | 99, 104 | mpbird 166 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 𝑠 # 0) |
106 | 93, 96, 98, 105 | mulap0d 8511 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → (2 · 𝑠) # 0) |
107 | 14, 15 | mp1i 10 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 2 ∈
ℚ) |
108 | | qmulcl 9524 |
. . . . . . . . . . 11
⊢ ((2
∈ ℚ ∧ 𝑠
∈ ℚ) → (2 · 𝑠) ∈ ℚ) |
109 | 107, 94, 108 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → (2 · 𝑠) ∈
ℚ) |
110 | | qcn 9521 |
. . . . . . . . . 10
⊢ ((2
· 𝑠) ∈ ℚ
→ (2 · 𝑠)
∈ ℂ) |
111 | 109, 110 | syl 14 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → (2 · 𝑠) ∈
ℂ) |
112 | | 0cnd 7850 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 0 ∈
ℂ) |
113 | | apsym 8460 |
. . . . . . . . 9
⊢ (((2
· 𝑠) ∈ ℂ
∧ 0 ∈ ℂ) → ((2 · 𝑠) # 0 ↔ 0 # (2 · 𝑠))) |
114 | 111, 112,
113 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → ((2 · 𝑠) # 0 ↔ 0 # (2 ·
𝑠))) |
115 | 106, 114 | mpbid 146 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 0 # (2 · 𝑠)) |
116 | | qapne 9526 |
. . . . . . . 8
⊢ ((0
∈ ℚ ∧ (2 · 𝑠) ∈ ℚ) → (0 # (2 ·
𝑠) ↔ 0 ≠ (2
· 𝑠))) |
117 | 102, 109,
116 | syl2anc 409 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → (0 # (2 · 𝑠) ↔ 0 ≠ (2 ·
𝑠))) |
118 | 115, 117 | mpbid 146 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → 0 ≠ (2 · 𝑠)) |
119 | | simpl 108 |
. . . . . . . . . 10
⊢ ((𝑞 = 0 ∧ 𝑟 = (2 · 𝑠)) → 𝑞 = 0) |
120 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝑞 = 0 ∧ 𝑟 = (2 · 𝑠)) → 𝑟 = (2 · 𝑠)) |
121 | 119, 120 | neeq12d 2344 |
. . . . . . . . 9
⊢ ((𝑞 = 0 ∧ 𝑟 = (2 · 𝑠)) → (𝑞 ≠ 𝑟 ↔ 0 ≠ (2 · 𝑠))) |
122 | 119 | oveq2d 5830 |
. . . . . . . . . . 11
⊢ ((𝑞 = 0 ∧ 𝑟 = (2 · 𝑠)) → (𝐴 − 𝑞) = (𝐴 − 0)) |
123 | 122 | fveq2d 5465 |
. . . . . . . . . 10
⊢ ((𝑞 = 0 ∧ 𝑟 = (2 · 𝑠)) → (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 0))) |
124 | 120 | oveq2d 5830 |
. . . . . . . . . . 11
⊢ ((𝑞 = 0 ∧ 𝑟 = (2 · 𝑠)) → (𝐴 − 𝑟) = (𝐴 − (2 · 𝑠))) |
125 | 124 | fveq2d 5465 |
. . . . . . . . . 10
⊢ ((𝑞 = 0 ∧ 𝑟 = (2 · 𝑠)) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (2 · 𝑠)))) |
126 | 123, 125 | breq12d 3974 |
. . . . . . . . 9
⊢ ((𝑞 = 0 ∧ 𝑟 = (2 · 𝑠)) → ((abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑠))))) |
127 | 121, 126 | imbi12d 233 |
. . . . . . . 8
⊢ ((𝑞 = 0 ∧ 𝑟 = (2 · 𝑠)) → ((𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))) ↔ (0 ≠ (2 · 𝑠) → (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑠)))))) |
128 | 127 | rspc2gv 2825 |
. . . . . . 7
⊢ ((0
∈ ℚ ∧ (2 · 𝑠) ∈ ℚ) → (∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))) → (0 ≠ (2 · 𝑠) → (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑠)))))) |
129 | 102, 109,
128 | syl2anc 409 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → (∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))) → (0 ≠ (2 · 𝑠) → (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑠)))))) |
130 | 92, 118, 129 | mp2d 47 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) ∧ 𝑠 ≠ 0) → (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑠)))) |
131 | 62, 63, 91, 130 | apdifflemr 13559 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) ∧ 𝑠 ∈ ℚ) → 𝐴 # 𝑠) |
132 | 131 | ralrimiva 2527 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))) → ∀𝑠 ∈ ℚ 𝐴 # 𝑠) |
133 | 61, 132 | impbida 586 |
. 2
⊢ (𝐴 ∈ ℝ →
(∀𝑠 ∈ ℚ
𝐴 # 𝑠 ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))))) |
134 | 2, 133 | syl5bb 191 |
1
⊢ (𝐴 ∈ ℝ →
(∀𝑞 ∈ ℚ
𝐴 # 𝑞 ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))))) |