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 e. RR -> ( A e. QQ <-> E. q e. QQ E. r e. QQ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rexnal2	|- ( E. q e. QQ E. r e. QQ -. ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) <-> -. A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) )
2		irrdiff	|- ( A e. RR -> ( -. A e. QQ <-> A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) )
3	2	con1bid	|- ( A e. RR -> ( -. A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) <-> A e. QQ ) )
4	1 3	bitr2id	|- ( A e. RR -> ( A e. QQ <-> E. q e. QQ E. r e. QQ -. ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) )
5		df-an	|- ( ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) <-> -. ( q =/= r -> -. ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) )
6		df-ne	|- ( ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) <-> -. ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) )
7	6	imbi2i	|- ( ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) <-> ( q =/= r -> -. ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) )
8	5 7	xchbinxr	|- ( ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) <-> -. ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) )
9	8	2rexbii	|- ( E. q e. QQ E. r e. QQ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) <-> E. q e. QQ E. r e. QQ -. ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) )
10	4 9	bitr4di	|- ( A e. RR -> ( A e. QQ <-> E. q e. QQ E. r e. QQ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) )