Metamath Proof Explorer

Theorem qdiffALT

Description: Alternate proof of qdiff . This is a proof from irrdiff using excluded middle in a variety of places. (Contributed by Jim Kingdon, 27-Apr-2026) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion qdiffALT ⊢ A ∈ ℝ → A ∈ ℚ ↔ ∃ q ∈ ℚ ∃ r ∈ ℚ q ≠ r ∧ A − q = A − r

Proof

Step Hyp Ref Expression
1 rexnal2 ⊢ ∃ q ∈ ℚ ∃ r ∈ ℚ ¬ q ≠ r → A − q ≠ A − r ↔ ¬ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r
2 irrdiff ⊢ A ∈ ℝ → ¬ A ∈ ℚ ↔ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r
3 2 con1bid ⊢ A ∈ ℝ → ¬ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r ↔ A ∈ ℚ
4 1 3 bitr2id ⊢ A ∈ ℝ → A ∈ ℚ ↔ ∃ q ∈ ℚ ∃ r ∈ ℚ ¬ q ≠ r → A − q ≠ A − r
5 df-an ⊢ q ≠ r ∧ A − q = A − r ↔ ¬ q ≠ r → ¬ A − q = A − r
6 df-ne ⊢ A − q ≠ A − r ↔ ¬ A − q = A − r
7 6 imbi2i ⊢ q ≠ r → A − q ≠ A − r ↔ q ≠ r → ¬ A − q = A − r
8 5 7 xchbinxr ⊢ q ≠ r ∧ A − q = A − r ↔ ¬ q ≠ r → A − q ≠ A − r
9 8 2rexbii ⊢ ∃ q ∈ ℚ ∃ r ∈ ℚ q ≠ r ∧ A − q = A − r ↔ ∃ q ∈ ℚ ∃ r ∈ ℚ ¬ q ≠ r → A − q ≠ A − r
10 4 9 bitr4di ⊢ A ∈ ℝ → A ∈ ℚ ↔ ∃ q ∈ ℚ ∃ r ∈ ℚ q ≠ r ∧ A − q = A − r