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	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℚ ↔ ∃ 𝑞 ∈ ℚ ∃ 𝑟 ∈ ℚ ( 𝑞 ≠ 𝑟 ∧ ( abs ‘ ( 𝐴 − 𝑞 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rexnal2	⊢ ( ∃ 𝑞 ∈ ℚ ∃ 𝑟 ∈ ℚ ¬ ( 𝑞 ≠ 𝑟 → ( abs ‘ ( 𝐴 − 𝑞 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ¬ ∀ 𝑞 ∈ ℚ ∀ 𝑟 ∈ ℚ ( 𝑞 ≠ 𝑟 → ( abs ‘ ( 𝐴 − 𝑞 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
2		irrdiff	⊢ ( 𝐴 ∈ ℝ → ( ¬ 𝐴 ∈ ℚ ↔ ∀ 𝑞 ∈ ℚ ∀ 𝑟 ∈ ℚ ( 𝑞 ≠ 𝑟 → ( abs ‘ ( 𝐴 − 𝑞 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
3	2	con1bid	⊢ ( 𝐴 ∈ ℝ → ( ¬ ∀ 𝑞 ∈ ℚ ∀ 𝑟 ∈ ℚ ( 𝑞 ≠ 𝑟 → ( abs ‘ ( 𝐴 − 𝑞 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ 𝐴 ∈ ℚ ) )
4	1 3	bitr2id	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℚ ↔ ∃ 𝑞 ∈ ℚ ∃ 𝑟 ∈ ℚ ¬ ( 𝑞 ≠ 𝑟 → ( abs ‘ ( 𝐴 − 𝑞 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )
5		df-an	⊢ ( ( 𝑞 ≠ 𝑟 ∧ ( abs ‘ ( 𝐴 − 𝑞 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ¬ ( 𝑞 ≠ 𝑟 → ¬ ( abs ‘ ( 𝐴 − 𝑞 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
6		df-ne	⊢ ( ( abs ‘ ( 𝐴 − 𝑞 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ ¬ ( abs ‘ ( 𝐴 − 𝑞 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) )
7	6	imbi2i	⊢ ( ( 𝑞 ≠ 𝑟 → ( abs ‘ ( 𝐴 − 𝑞 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ( 𝑞 ≠ 𝑟 → ¬ ( abs ‘ ( 𝐴 − 𝑞 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
8	5 7	xchbinxr	⊢ ( ( 𝑞 ≠ 𝑟 ∧ ( abs ‘ ( 𝐴 − 𝑞 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ¬ ( 𝑞 ≠ 𝑟 → ( abs ‘ ( 𝐴 − 𝑞 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
9	8	2rexbii	⊢ ( ∃ 𝑞 ∈ ℚ ∃ 𝑟 ∈ ℚ ( 𝑞 ≠ 𝑟 ∧ ( abs ‘ ( 𝐴 − 𝑞 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ∃ 𝑞 ∈ ℚ ∃ 𝑟 ∈ ℚ ¬ ( 𝑞 ≠ 𝑟 → ( abs ‘ ( 𝐴 − 𝑞 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) )
10	4 9	bitr4di	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℚ ↔ ∃ 𝑞 ∈ ℚ ∃ 𝑟 ∈ ℚ ( 𝑞 ≠ 𝑟 ∧ ( abs ‘ ( 𝐴 − 𝑞 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )