Proof of Theorem irrdiff
Step | Hyp | Ref
| Expression |
1 | | simplll 775 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → 𝐴 ∈ ℝ) |
2 | | simpllr 776 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → ¬ 𝐴 ∈ ℚ) |
3 | | simplrl 777 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → 𝑞 ∈ ℚ) |
4 | | simplrr 778 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → 𝑟 ∈ ℚ) |
5 | | simpr 489 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → 𝑞 ≠ 𝑟) |
6 | 1, 2, 3, 4, 5 | irrdifflemf 35004 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟))) |
7 | 6 | ex 417 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) →
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) |
8 | 7 | ralrimivva 3118 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) →
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) |
9 | | simplr 769 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) ∧ 𝐴 ∈ ℚ) → ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) |
10 | | peano2rem 10976 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ∈
ℝ) |
11 | | recn 10650 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
12 | | 1cnd 10659 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 1 ∈
ℂ) |
13 | 11, 12 | negsubd 11026 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 + -1) = (𝐴 − 1)) |
14 | | neg1lt0 11776 |
. . . . . . . . 9
⊢ -1 <
0 |
15 | | 0lt1 11185 |
. . . . . . . . 9
⊢ 0 <
1 |
16 | | neg1rr 11774 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
17 | | 0re 10666 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
18 | | 1re 10664 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
19 | 16, 17, 18 | lttri 10789 |
. . . . . . . . 9
⊢ ((-1 <
0 ∧ 0 < 1) → -1 < 1) |
20 | 14, 15, 19 | mp2an 692 |
. . . . . . . 8
⊢ -1 <
1 |
21 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → -1 ∈
ℝ) |
22 | | 1red 10665 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 1 ∈
ℝ) |
23 | | id 22 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) |
24 | 21, 22, 23 | ltadd2d 10819 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (-1 <
1 ↔ (𝐴 + -1) <
(𝐴 + 1))) |
25 | 20, 24 | mpbii 236 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 + -1) < (𝐴 + 1)) |
26 | 13, 25 | eqbrtrrd 5049 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) < (𝐴 + 1)) |
27 | 10, 26 | ltned 10799 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ≠ (𝐴 + 1)) |
28 | 27 | ad2antrr 726 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) ∧ 𝐴 ∈ ℚ) → (𝐴 − 1) ≠ (𝐴 + 1)) |
29 | | 1z 12036 |
. . . . . . 7
⊢ 1 ∈
ℤ |
30 | | zq 12379 |
. . . . . . 7
⊢ (1 ∈
ℤ → 1 ∈ ℚ) |
31 | 29, 30 | ax-mp 5 |
. . . . . 6
⊢ 1 ∈
ℚ |
32 | | qsubcl 12393 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 1 ∈
ℚ) → (𝐴 −
1) ∈ ℚ) |
33 | 31, 32 | mpan2 691 |
. . . . 5
⊢ (𝐴 ∈ ℚ → (𝐴 − 1) ∈
ℚ) |
34 | | qaddcl 12390 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 1 ∈
ℚ) → (𝐴 + 1)
∈ ℚ) |
35 | 31, 34 | mpan2 691 |
. . . . . 6
⊢ (𝐴 ∈ ℚ → (𝐴 + 1) ∈
ℚ) |
36 | 35 | adantl 486 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) ∧ 𝐴 ∈ ℚ) → (𝐴 + 1) ∈ ℚ) |
37 | | simpl 487 |
. . . . . . . 8
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → 𝑞 = (𝐴 − 1)) |
38 | | simpr 489 |
. . . . . . . 8
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → 𝑟 = (𝐴 + 1)) |
39 | 37, 38 | neeq12d 3010 |
. . . . . . 7
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → (𝑞 ≠ 𝑟 ↔ (𝐴 − 1) ≠ (𝐴 + 1))) |
40 | | oveq2 7151 |
. . . . . . . . . 10
⊢ (𝑞 = (𝐴 − 1) → (𝐴 − 𝑞) = (𝐴 − (𝐴 − 1))) |
41 | 40 | adantr 485 |
. . . . . . . . 9
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → (𝐴 − 𝑞) = (𝐴 − (𝐴 − 1))) |
42 | 41 | fveq2d 6655 |
. . . . . . . 8
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − (𝐴 − 1)))) |
43 | | oveq2 7151 |
. . . . . . . . . 10
⊢ (𝑟 = (𝐴 + 1) → (𝐴 − 𝑟) = (𝐴 − (𝐴 + 1))) |
44 | 43 | adantl 486 |
. . . . . . . . 9
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → (𝐴 − 𝑟) = (𝐴 − (𝐴 + 1))) |
45 | 44 | fveq2d 6655 |
. . . . . . . 8
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝐴 + 1)))) |
46 | 42, 45 | neeq12d 3010 |
. . . . . . 7
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → ((abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐴 − (𝐴 − 1))) ≠ (abs‘(𝐴 − (𝐴 + 1))))) |
47 | 39, 46 | imbi12d 349 |
. . . . . 6
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → ((𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟))) ↔ ((𝐴 − 1) ≠ (𝐴 + 1) → (abs‘(𝐴 − (𝐴 − 1))) ≠ (abs‘(𝐴 − (𝐴 + 1)))))) |
48 | 47 | rspc2gv 3548 |
. . . . 5
⊢ (((𝐴 − 1) ∈ ℚ ∧
(𝐴 + 1) ∈ ℚ)
→ (∀𝑞 ∈
ℚ ∀𝑟 ∈
ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟))) → ((𝐴 − 1) ≠ (𝐴 + 1) → (abs‘(𝐴 − (𝐴 − 1))) ≠ (abs‘(𝐴 − (𝐴 + 1)))))) |
49 | 33, 36, 48 | syl2an2 686 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) ∧ 𝐴 ∈ ℚ) → (∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟))) → ((𝐴 − 1) ≠ (𝐴 + 1) → (abs‘(𝐴 − (𝐴 − 1))) ≠ (abs‘(𝐴 − (𝐴 + 1)))))) |
50 | 9, 28, 49 | mp2d 49 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) ∧ 𝐴 ∈ ℚ) → (abs‘(𝐴 − (𝐴 − 1))) ≠ (abs‘(𝐴 − (𝐴 + 1)))) |
51 | | neirr 2958 |
. . . . 5
⊢ ¬
(abs‘1) ≠ (abs‘1) |
52 | 11, 12 | nncand 11025 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 − (𝐴 − 1)) = 1) |
53 | 52 | fveq2d 6655 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(abs‘(𝐴 −
(𝐴 − 1))) =
(abs‘1)) |
54 | 11, 12 | subnegd 11027 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝐴 − -1) = (𝐴 + 1)) |
55 | 54 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 − (𝐴 − -1)) = (𝐴 − (𝐴 + 1))) |
56 | 21 | recnd 10692 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → -1 ∈
ℂ) |
57 | 11, 56 | nncand 11025 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 − (𝐴 − -1)) = -1) |
58 | 55, 57 | eqtr3d 2796 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (𝐴 + 1)) = -1) |
59 | 58 | fveq2d 6655 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(abs‘(𝐴 −
(𝐴 + 1))) =
(abs‘-1)) |
60 | 12 | absnegd 14842 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(abs‘-1) = (abs‘1)) |
61 | 59, 60 | eqtrd 2794 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(abs‘(𝐴 −
(𝐴 + 1))) =
(abs‘1)) |
62 | 53, 61 | neeq12d 3010 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((abs‘(𝐴 −
(𝐴 − 1))) ≠
(abs‘(𝐴 −
(𝐴 + 1))) ↔
(abs‘1) ≠ (abs‘1))) |
63 | 51, 62 | mtbiri 331 |
. . . 4
⊢ (𝐴 ∈ ℝ → ¬
(abs‘(𝐴 −
(𝐴 − 1))) ≠
(abs‘(𝐴 −
(𝐴 + 1)))) |
64 | 63 | ad2antrr 726 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) ∧ 𝐴 ∈ ℚ) → ¬
(abs‘(𝐴 −
(𝐴 − 1))) ≠
(abs‘(𝐴 −
(𝐴 + 1)))) |
65 | 50, 64 | pm2.65da 817 |
. 2
⊢ ((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) → ¬ 𝐴 ∈ ℚ) |
66 | 8, 65 | impbida 801 |
1
⊢ (𝐴 ∈ ℝ → (¬
𝐴 ∈ ℚ ↔
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟))))) |