Proof of Theorem irrdiff
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simplll 774 | . . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → 𝐴 ∈ ℝ) | 
| 2 |  | simpllr 775 | . . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → ¬ 𝐴 ∈ ℚ) | 
| 3 |  | simplrl 776 | . . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → 𝑞 ∈ ℚ) | 
| 4 |  | simplrr 777 | . . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → 𝑟 ∈ ℚ) | 
| 5 |  | simpr 484 | . . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → 𝑞 ≠ 𝑟) | 
| 6 | 1, 2, 3, 4, 5 | irrdifflemf 37327 | . . . 4
⊢ ((((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) ∧
𝑞 ≠ 𝑟) → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟))) | 
| 7 | 6 | ex 412 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝑞 ∈ ℚ ∧
𝑟 ∈ ℚ)) →
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) | 
| 8 | 7 | ralrimivva 3201 | . 2
⊢ ((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) →
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) | 
| 9 |  | simplr 768 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) ∧ 𝐴 ∈ ℚ) → ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) | 
| 10 |  | peano2rem 11577 | . . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ∈
ℝ) | 
| 11 |  | recn 11246 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) | 
| 12 |  | 1cnd 11257 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → 1 ∈
ℂ) | 
| 13 | 11, 12 | negsubd 11627 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 + -1) = (𝐴 − 1)) | 
| 14 |  | neg1lt0 12384 | . . . . . . . . 9
⊢ -1 <
0 | 
| 15 |  | 0lt1 11786 | . . . . . . . . 9
⊢ 0 <
1 | 
| 16 |  | neg1rr 12382 | . . . . . . . . . 10
⊢ -1 ∈
ℝ | 
| 17 |  | 0re 11264 | . . . . . . . . . 10
⊢ 0 ∈
ℝ | 
| 18 |  | 1re 11262 | . . . . . . . . . 10
⊢ 1 ∈
ℝ | 
| 19 | 16, 17, 18 | lttri 11388 | . . . . . . . . 9
⊢ ((-1 <
0 ∧ 0 < 1) → -1 < 1) | 
| 20 | 14, 15, 19 | mp2an 692 | . . . . . . . 8
⊢ -1 <
1 | 
| 21 | 16 | a1i 11 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → -1 ∈
ℝ) | 
| 22 |  | 1red 11263 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 1 ∈
ℝ) | 
| 23 |  | id 22 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) | 
| 24 | 21, 22, 23 | ltadd2d 11418 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (-1 <
1 ↔ (𝐴 + -1) <
(𝐴 + 1))) | 
| 25 | 20, 24 | mpbii 233 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 + -1) < (𝐴 + 1)) | 
| 26 | 13, 25 | eqbrtrrd 5166 | . . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) < (𝐴 + 1)) | 
| 27 | 10, 26 | ltned 11398 | . . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ≠ (𝐴 + 1)) | 
| 28 | 27 | ad2antrr 726 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) ∧ 𝐴 ∈ ℚ) → (𝐴 − 1) ≠ (𝐴 + 1)) | 
| 29 |  | 1z 12649 | . . . . . . 7
⊢ 1 ∈
ℤ | 
| 30 |  | zq 12997 | . . . . . . 7
⊢ (1 ∈
ℤ → 1 ∈ ℚ) | 
| 31 | 29, 30 | ax-mp 5 | . . . . . 6
⊢ 1 ∈
ℚ | 
| 32 |  | qsubcl 13011 | . . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 1 ∈
ℚ) → (𝐴 −
1) ∈ ℚ) | 
| 33 | 31, 32 | mpan2 691 | . . . . 5
⊢ (𝐴 ∈ ℚ → (𝐴 − 1) ∈
ℚ) | 
| 34 |  | qaddcl 13008 | . . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 1 ∈
ℚ) → (𝐴 + 1)
∈ ℚ) | 
| 35 | 31, 34 | mpan2 691 | . . . . . 6
⊢ (𝐴 ∈ ℚ → (𝐴 + 1) ∈
ℚ) | 
| 36 | 35 | adantl 481 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) ∧ 𝐴 ∈ ℚ) → (𝐴 + 1) ∈ ℚ) | 
| 37 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → 𝑞 = (𝐴 − 1)) | 
| 38 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → 𝑟 = (𝐴 + 1)) | 
| 39 | 37, 38 | neeq12d 3001 | . . . . . . 7
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → (𝑞 ≠ 𝑟 ↔ (𝐴 − 1) ≠ (𝐴 + 1))) | 
| 40 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑞 = (𝐴 − 1) → (𝐴 − 𝑞) = (𝐴 − (𝐴 − 1))) | 
| 41 | 40 | adantr 480 | . . . . . . . . 9
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → (𝐴 − 𝑞) = (𝐴 − (𝐴 − 1))) | 
| 42 | 41 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − (𝐴 − 1)))) | 
| 43 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑟 = (𝐴 + 1) → (𝐴 − 𝑟) = (𝐴 − (𝐴 + 1))) | 
| 44 | 43 | adantl 481 | . . . . . . . . 9
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → (𝐴 − 𝑟) = (𝐴 − (𝐴 + 1))) | 
| 45 | 44 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝐴 + 1)))) | 
| 46 | 42, 45 | neeq12d 3001 | . . . . . . 7
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → ((abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐴 − (𝐴 − 1))) ≠ (abs‘(𝐴 − (𝐴 + 1))))) | 
| 47 | 39, 46 | imbi12d 344 | . . . . . 6
⊢ ((𝑞 = (𝐴 − 1) ∧ 𝑟 = (𝐴 + 1)) → ((𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟))) ↔ ((𝐴 − 1) ≠ (𝐴 + 1) → (abs‘(𝐴 − (𝐴 − 1))) ≠ (abs‘(𝐴 − (𝐴 + 1)))))) | 
| 48 | 47 | rspc2gv 3631 | . . . . 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 2948 | . . . . 5
⊢  ¬
(abs‘1) ≠ (abs‘1) | 
| 52 | 11, 12 | nncand 11626 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 − (𝐴 − 1)) = 1) | 
| 53 | 52 | fveq2d 6909 | . . . . . 6
⊢ (𝐴 ∈ ℝ →
(abs‘(𝐴 −
(𝐴 − 1))) =
(abs‘1)) | 
| 54 | 11, 12 | subnegd 11628 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝐴 − -1) = (𝐴 + 1)) | 
| 55 | 54 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 − (𝐴 − -1)) = (𝐴 − (𝐴 + 1))) | 
| 56 | 21 | recnd 11290 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → -1 ∈
ℂ) | 
| 57 | 11, 56 | nncand 11626 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 − (𝐴 − -1)) = -1) | 
| 58 | 55, 57 | eqtr3d 2778 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (𝐴 + 1)) = -1) | 
| 59 | 58 | fveq2d 6909 | . . . . . . 7
⊢ (𝐴 ∈ ℝ →
(abs‘(𝐴 −
(𝐴 + 1))) =
(abs‘-1)) | 
| 60 | 12 | absnegd 15489 | . . . . . . 7
⊢ (𝐴 ∈ ℝ →
(abs‘-1) = (abs‘1)) | 
| 61 | 59, 60 | eqtrd 2776 | . . . . . 6
⊢ (𝐴 ∈ ℝ →
(abs‘(𝐴 −
(𝐴 + 1))) =
(abs‘1)) | 
| 62 | 53, 61 | neeq12d 3001 | . . . . 5
⊢ (𝐴 ∈ ℝ →
((abs‘(𝐴 −
(𝐴 − 1))) ≠
(abs‘(𝐴 −
(𝐴 + 1))) ↔
(abs‘1) ≠ (abs‘1))) | 
| 63 | 51, 62 | mtbiri 327 | . . . 4
⊢ (𝐴 ∈ ℝ → ¬
(abs‘(𝐴 −
(𝐴 − 1))) ≠
(abs‘(𝐴 −
(𝐴 + 1)))) | 
| 64 | 63 | ad2antrr 726 | . . 3
⊢ (((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) ∧ 𝐴 ∈ ℚ) → ¬
(abs‘(𝐴 −
(𝐴 − 1))) ≠
(abs‘(𝐴 −
(𝐴 + 1)))) | 
| 65 | 50, 64 | pm2.65da 816 | . 2
⊢ ((𝐴 ∈ ℝ ∧
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))) → ¬ 𝐴 ∈ ℚ) | 
| 66 | 8, 65 | impbida 800 | 1
⊢ (𝐴 ∈ ℝ → (¬
𝐴 ∈ ℚ ↔
∀𝑞 ∈ ℚ
∀𝑟 ∈ ℚ
(𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟))))) |