qdiff - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > qdiff		Structured version Visualization version GIF version

Theorem qdiff 37894

Description: The rationals are exactly those reals for which there exist two distinct rationals that are the same distance from the original number. Similar to irrdiff 37893 but here proved with a proof which would also work in constructive mathematics. From an online post by Ingo Blechschmidt. For a proof using irrdiff 37893, see qdiffALT 37895. (Contributed by Jim Kingdon, 24-Apr-2026.)

**Assertion**
Ref	Expression
qdiff	⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))))

Distinct variable group: 𝐴,𝑞,𝑟

**Proof of Theorem qdiff**
Step	Hyp	Ref	Expression
1		neeq1 3026	. . . . 5 ⊢ (𝑞 = (𝐴 − 1) → (𝑞 ≠ 𝑟 ↔ (𝐴 − 1) ≠ 𝑟))
2		oveq2 7419	. . . . . 6 ⊢ (𝑞 = (𝐴 − 1) → (𝐴 − 𝑞) = (𝐴 − (𝐴 − 1)))
3	2	fveqeq2d 6890	. . . . 5 ⊢ (𝑞 = (𝐴 − 1) → ((abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟))))
4	1, 3	anbi12d 643	. . . 4 ⊢ (𝑞 = (𝐴 − 1) → ((𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) ↔ ((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟)))))
5	4	rexbidv 3195	. . 3 ⊢ (𝑞 = (𝐴 − 1) → (∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) ↔ ∃𝑟 ∈ ℚ ((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟)))))
6		1z 12624	. . . . 5 ⊢ 1 ∈ ℤ
7		zq 12978	. . . . 5 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
8	6, 7	ax-mp 5	. . . 4 ⊢ 1 ∈ ℚ
9		qsubcl 12992	. . . 4 ⊢ ((𝐴 ∈ ℚ ∧ 1 ∈ ℚ) → (𝐴 − 1) ∈ ℚ)
10	8, 9	mpan2 703	. . 3 ⊢ (𝐴 ∈ ℚ → (𝐴 − 1) ∈ ℚ)
11		qaddcl 12989	. . . . 5 ⊢ ((𝐴 ∈ ℚ ∧ 1 ∈ ℚ) → (𝐴 + 1) ∈ ℚ)
12	8, 11	mpan2 703	. . . 4 ⊢ (𝐴 ∈ ℚ → (𝐴 + 1) ∈ ℚ)
13		qre 12977	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)
14		1rp 13020	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ⁺
15	14, 14	pm3.2i 475	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ⁺ ∧ 1 ∈ ℝ⁺)
16		rpaddcl 13040	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ⁺ ∧ 1 ∈ ℝ⁺) → (1 + 1) ∈ ℝ⁺)
17	15, 16	mp1i 14	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℚ → (1 + 1) ∈ ℝ⁺)
18	13, 17	ltaddrpd 13093	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℚ → 𝐴 < (𝐴 + (1 + 1)))
19	13, 18	ltned 11346	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → 𝐴 ≠ (𝐴 + (1 + 1)))
20	19	neneqd 2969	. . . . . . . 8 ⊢ (𝐴 ∈ ℚ → ¬ 𝐴 = (𝐴 + (1 + 1)))
21	20	neqcomd 2779	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → ¬ (𝐴 + (1 + 1)) = 𝐴)
22		qcn 12987	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
23		1cnd 11202	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → 1 ∈ ℂ)
24	22, 23, 23	addassd 11231	. . . . . . . 8 ⊢ (𝐴 ∈ ℚ → ((𝐴 + 1) + 1) = (𝐴 + (1 + 1)))
25	24	eqeq1d 2771	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → (((𝐴 + 1) + 1) = 𝐴 ↔ (𝐴 + (1 + 1)) = 𝐴))
26	21, 25	mtbird 328	. . . . . 6 ⊢ (𝐴 ∈ ℚ → ¬ ((𝐴 + 1) + 1) = 𝐴)
27	22, 23	addcld 11228	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → (𝐴 + 1) ∈ ℂ)
28	22, 23, 27	subadd2d 11588	. . . . . 6 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 1) = (𝐴 + 1) ↔ ((𝐴 + 1) + 1) = 𝐴))
29	26, 28	mtbird 328	. . . . 5 ⊢ (𝐴 ∈ ℚ → ¬ (𝐴 − 1) = (𝐴 + 1))
30	29	neqned 2971	. . . 4 ⊢ (𝐴 ∈ ℚ → (𝐴 − 1) ≠ (𝐴 + 1))
31	23	absnegd 15503	. . . . 5 ⊢ (𝐴 ∈ ℚ → (abs‘-1) = (abs‘1))
32	22, 22, 23	subsub4d 11600	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 𝐴) − 1) = (𝐴 − (𝐴 + 1)))
33	22	subidd 11557	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → (𝐴 − 𝐴) = 0)
34	33	oveq1d 7426	. . . . . . . 8 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 𝐴) − 1) = (0 − 1))
35		df-neg 11444	. . . . . . . 8 ⊢ -1 = (0 − 1)
36	34, 35	eqtr4di 2822	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 𝐴) − 1) = -1)
37	32, 36	eqtr3d 2806	. . . . . 6 ⊢ (𝐴 ∈ ℚ → (𝐴 − (𝐴 + 1)) = -1)
38	37	fveq2d 6886	. . . . 5 ⊢ (𝐴 ∈ ℚ → (abs‘(𝐴 − (𝐴 + 1))) = (abs‘-1))
39	22, 23	nncand 11574	. . . . . 6 ⊢ (𝐴 ∈ ℚ → (𝐴 − (𝐴 − 1)) = 1)
40	39	fveq2d 6886	. . . . 5 ⊢ (𝐴 ∈ ℚ → (abs‘(𝐴 − (𝐴 − 1))) = (abs‘1))
41	31, 38, 40	3eqtr4rd 2815	. . . 4 ⊢ (𝐴 ∈ ℚ → (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − (𝐴 + 1))))
42		neeq2 3027	. . . . . 6 ⊢ (𝑟 = (𝐴 + 1) → ((𝐴 − 1) ≠ 𝑟 ↔ (𝐴 − 1) ≠ (𝐴 + 1)))
43		oveq2 7419	. . . . . . . 8 ⊢ (𝑟 = (𝐴 + 1) → (𝐴 − 𝑟) = (𝐴 − (𝐴 + 1)))
44	43	fveq2d 6886	. . . . . . 7 ⊢ (𝑟 = (𝐴 + 1) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝐴 + 1))))
45	44	eqeq2d 2780	. . . . . 6 ⊢ (𝑟 = (𝐴 + 1) → ((abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − (𝐴 + 1)))))
46	42, 45	anbi12d 643	. . . . 5 ⊢ (𝑟 = (𝐴 + 1) → (((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟))) ↔ ((𝐴 − 1) ≠ (𝐴 + 1) ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − (𝐴 + 1))))))
47	46	rspcev 3588	. . . 4 ⊢ (((𝐴 + 1) ∈ ℚ ∧ ((𝐴 − 1) ≠ (𝐴 + 1) ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − (𝐴 + 1))))) → ∃𝑟 ∈ ℚ ((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟))))
48	12, 30, 41, 47	syl12anc 849	. . 3 ⊢ (𝐴 ∈ ℚ → ∃𝑟 ∈ ℚ ((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟))))
49	5, 10, 48	rspcedvdw 3591	. 2 ⊢ (𝐴 ∈ ℚ → ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))))
50		2cnd 12319	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 2 ∈ ℂ)
51		simpll 778	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝐴 ∈ ℝ)
52	51	recnd 11237	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝐴 ∈ ℂ)
53		simplrl 788	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ∈ ℚ)
54	53	qred 12979	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ∈ ℝ)
55	54	recnd 11237	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ∈ ℂ)
56	52, 55	mulcld 11229	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 · 𝑞) ∈ ℂ)
57		simplrr 789	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑟 ∈ ℚ)
58	57	qred 12979	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑟 ∈ ℝ)
59	58	recnd 11237	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑟 ∈ ℂ)
60	52, 59	mulcld 11229	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 · 𝑟) ∈ ℂ)
61	50, 56, 60	subdid 11670	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · ((𝐴 · 𝑞) − (𝐴 · 𝑟))) = ((2 · (𝐴 · 𝑞)) − (2 · (𝐴 · 𝑟))))
62	52	sqcld 14180	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴↑2) ∈ ℂ)
63	50, 60	mulcld 11229	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · (𝐴 · 𝑟)) ∈ ℂ)
64	50, 56	mulcld 11229	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · (𝐴 · 𝑞)) ∈ ℂ)
65	62, 63, 64	nnncan1d 11603	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝐴↑2) − (2 · (𝐴 · 𝑟))) − ((𝐴↑2) − (2 · (𝐴 · 𝑞)))) = ((2 · (𝐴 · 𝑞)) − (2 · (𝐴 · 𝑟))))
66		simprr 784	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))
67	51, 54	resubcld 11642	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 − 𝑞) ∈ ℝ)
68	51, 58	resubcld 11642	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 − 𝑟) ∈ ℝ)
69		sqabs 15358	. . . . . . . . . . . . 13 ⊢ (((𝐴 − 𝑞) ∈ ℝ ∧ (𝐴 − 𝑟) ∈ ℝ) → (((𝐴 − 𝑞)↑2) = ((𝐴 − 𝑟)↑2) ↔ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))))
70	67, 68, 69	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝐴 − 𝑞)↑2) = ((𝐴 − 𝑟)↑2) ↔ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))))
71	66, 70	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 − 𝑞)↑2) = ((𝐴 − 𝑟)↑2))
72		binom2sub 14256	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑞 ∈ ℂ) → ((𝐴 − 𝑞)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑞))) + (𝑞↑2)))
73	52, 55, 72	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 − 𝑞)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑞))) + (𝑞↑2)))
74		binom2sub 14256	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑟 ∈ ℂ) → ((𝐴 − 𝑟)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑟))) + (𝑟↑2)))
75	52, 59, 74	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 − 𝑟)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑟))) + (𝑟↑2)))
76	71, 73, 75	3eqtr3d 2812	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝐴↑2) − (2 · (𝐴 · 𝑞))) + (𝑞↑2)) = (((𝐴↑2) − (2 · (𝐴 · 𝑟))) + (𝑟↑2)))
77	62, 64	subcld 11569	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴↑2) − (2 · (𝐴 · 𝑞))) ∈ ℂ)
78	55	sqcld 14180	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞↑2) ∈ ℂ)
79	62, 63	subcld 11569	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴↑2) − (2 · (𝐴 · 𝑟))) ∈ ℂ)
80	59	sqcld 14180	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑟↑2) ∈ ℂ)
81	77, 78, 79, 80	addsubeq4d 11620	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((((𝐴↑2) − (2 · (𝐴 · 𝑞))) + (𝑞↑2)) = (((𝐴↑2) − (2 · (𝐴 · 𝑟))) + (𝑟↑2)) ↔ (((𝐴↑2) − (2 · (𝐴 · 𝑟))) − ((𝐴↑2) − (2 · (𝐴 · 𝑞)))) = ((𝑞↑2) − (𝑟↑2))))
82	76, 81	mpbid 235	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝐴↑2) − (2 · (𝐴 · 𝑟))) − ((𝐴↑2) − (2 · (𝐴 · 𝑞)))) = ((𝑞↑2) − (𝑟↑2)))
83	61, 65, 82	3eqtr2d 2810	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · ((𝐴 · 𝑞) − (𝐴 · 𝑟))) = ((𝑞↑2) − (𝑟↑2)))
84	78, 80	subcld 11569	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝑞↑2) − (𝑟↑2)) ∈ ℂ)
85	56, 60	subcld 11569	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 · 𝑞) − (𝐴 · 𝑟)) ∈ ℂ)
86		2ne0 12347	. . . . . . . . . 10 ⊢ 2 ≠ 0
87	86	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 2 ≠ 0)
88	84, 50, 85, 87	divmuld 12013	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((((𝑞↑2) − (𝑟↑2)) / 2) = ((𝐴 · 𝑞) − (𝐴 · 𝑟)) ↔ (2 · ((𝐴 · 𝑞) − (𝐴 · 𝑟))) = ((𝑞↑2) − (𝑟↑2))))
89	83, 88	mpbird 260	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝑞↑2) − (𝑟↑2)) / 2) = ((𝐴 · 𝑞) − (𝐴 · 𝑟)))
90	52, 55, 59	subdid 11670	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 · (𝑞 − 𝑟)) = ((𝐴 · 𝑞) − (𝐴 · 𝑟)))
91	89, 90	eqtr4d 2807	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝑞↑2) − (𝑟↑2)) / 2) = (𝐴 · (𝑞 − 𝑟)))
92	84	halfcld 12489	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℂ)
93	55, 59	subcld 11569	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞 − 𝑟) ∈ ℂ)
94		simprl 782	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ≠ 𝑟)
95	55, 59, 94	subne0d 11578	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞 − 𝑟) ≠ 0)
96	92, 52, 93, 95	divmul3d 12025	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) = 𝐴 ↔ (((𝑞↑2) − (𝑟↑2)) / 2) = (𝐴 · (𝑞 − 𝑟))))
97	91, 96	mpbird 260	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) = 𝐴)
98		qsqcl 14166	. . . . . . . . 9 ⊢ (𝑞 ∈ ℚ → (𝑞↑2) ∈ ℚ)
99	53, 98	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞↑2) ∈ ℚ)
100		qsqcl 14166	. . . . . . . . 9 ⊢ (𝑟 ∈ ℚ → (𝑟↑2) ∈ ℚ)
101	57, 100	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑟↑2) ∈ ℚ)
102		qsubcl 12992	. . . . . . . 8 ⊢ (((𝑞↑2) ∈ ℚ ∧ (𝑟↑2) ∈ ℚ) → ((𝑞↑2) − (𝑟↑2)) ∈ ℚ)
103	99, 101, 102	syl2anc 595	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝑞↑2) − (𝑟↑2)) ∈ ℚ)
104		2z 12626	. . . . . . . 8 ⊢ 2 ∈ ℤ
105		zq 12978	. . . . . . . 8 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
106	104, 105	mp1i 14	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 2 ∈ ℚ)
107		qdivcl 12994	. . . . . . 7 ⊢ ((((𝑞↑2) − (𝑟↑2)) ∈ ℚ ∧ 2 ∈ ℚ ∧ 2 ≠ 0) → (((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℚ)
108	103, 106, 87, 107	syl3anc 1396	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℚ)
109		qsubcl 12992	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ) → (𝑞 − 𝑟) ∈ ℚ)
110	53, 57, 109	syl2anc 595	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞 − 𝑟) ∈ ℚ)
111		qdivcl 12994	. . . . . 6 ⊢ (((((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℚ ∧ (𝑞 − 𝑟) ∈ ℚ ∧ (𝑞 − 𝑟) ≠ 0) → ((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) ∈ ℚ)
112	108, 110, 95, 111	syl3anc 1396	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) ∈ ℚ)
113	97, 112	eqeltrrd 2870	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝐴 ∈ ℚ)
114	113	ex 417	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) → ((𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) → 𝐴 ∈ ℚ))
115	114	rexlimdvva 3228	. 2 ⊢ (𝐴 ∈ ℝ → (∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) → 𝐴 ∈ ℚ))
116	49, 115	impbid2 229	1 ⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∃wrex 3095 ‘cfv 6537 (class class class)co 7411 ℂcc 11098 ℝcr 11099 0cc0 11100 1c1 11101 + caddc 11103 · cmul 11105 − cmin 11441 -cneg 11442 / cdiv 11871 2c2 12295 ℤcz 12591 ℚcq 12972 ℝ⁺crp 13016 ↑cexp 14097 abscabs 15285

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-er 8694 df-en 8944 df-dom 8945 df-sdom 8946 df-sup 9402 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-n0 12505 df-z 12592 df-uz 12863 df-q 12973 df-rp 13017 df-seq 14038 df-exp 14098 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287

This theorem is referenced by: (None)

W3C validator