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 38439

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 38438 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 38438, see qdiffALT 38440. (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 3021	. . . . 5 ⊢ (𝑞 = (𝐴 − 1) → (𝑞 ≠ 𝑟 ↔ (𝐴 − 1) ≠ 𝑟))
2		oveq2 7448	. . . . . 6 ⊢ (𝑞 = (𝐴 − 1) → (𝐴 − 𝑞) = (𝐴 − (𝐴 − 1)))
3	2	fveqeq2d 6913	. . . . 5 ⊢ (𝑞 = (𝐴 − 1) → ((abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟))))
4	1, 3	anbi12d 644	. . . 4 ⊢ (𝑞 = (𝐴 − 1) → ((𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) ↔ ((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟)))))
5	4	rexbidv 3190	. . 3 ⊢ (𝑞 = (𝐴 − 1) → (∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) ↔ ∃𝑟 ∈ ℚ ((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟)))))
6		1z 12750	. . . . 5 ⊢ 1 ∈ ℤ
7		zq 13105	. . . . 5 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
8	6, 7	ax-mp 5	. . . 4 ⊢ 1 ∈ ℚ
9		qsubcl 13120	. . . 4 ⊢ ((𝐴 ∈ ℚ ∧ 1 ∈ ℚ) → (𝐴 − 1) ∈ ℚ)
10	8, 9	mpan2 704	. . 3 ⊢ (𝐴 ∈ ℚ → (𝐴 − 1) ∈ ℚ)
11		qaddcl 13117	. . . . 5 ⊢ ((𝐴 ∈ ℚ ∧ 1 ∈ ℚ) → (𝐴 + 1) ∈ ℚ)
12	8, 11	mpan2 704	. . . 4 ⊢ (𝐴 ∈ ℚ → (𝐴 + 1) ∈ ℚ)
13		qre 13104	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)
14		1rp 13148	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ⁺
15	14, 14	pm3.2i 476	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ⁺ ∧ 1 ∈ ℝ⁺)
16		rpaddcl 13168	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ⁺ ∧ 1 ∈ ℝ⁺) → (1 + 1) ∈ ℝ⁺)
17	15, 16	mp1i 14	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℚ → (1 + 1) ∈ ℝ⁺)
18	13, 17	ltaddrpd 13221	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℚ → 𝐴 < (𝐴 + (1 + 1)))
19	13, 18	ltned 11470	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → 𝐴 ≠ (𝐴 + (1 + 1)))
20	19	neneqd 2964	. . . . . . . 8 ⊢ (𝐴 ∈ ℚ → ¬ 𝐴 = (𝐴 + (1 + 1)))
21	20	neqcomd 2773	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → ¬ (𝐴 + (1 + 1)) = 𝐴)
22		qcn 13114	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
23		1cnd 11326	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → 1 ∈ ℂ)
24	22, 23, 23	addassd 11355	. . . . . . . 8 ⊢ (𝐴 ∈ ℚ → ((𝐴 + 1) + 1) = (𝐴 + (1 + 1)))
25	24	eqeq1d 2765	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → (((𝐴 + 1) + 1) = 𝐴 ↔ (𝐴 + (1 + 1)) = 𝐴))
26	21, 25	mtbird 328	. . . . . 6 ⊢ (𝐴 ∈ ℚ → ¬ ((𝐴 + 1) + 1) = 𝐴)
27	22, 23	addcld 11352	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → (𝐴 + 1) ∈ ℂ)
28	22, 23, 27	subadd2d 11712	. . . . . 6 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 1) = (𝐴 + 1) ↔ ((𝐴 + 1) + 1) = 𝐴))
29	26, 28	mtbird 328	. . . . 5 ⊢ (𝐴 ∈ ℚ → ¬ (𝐴 − 1) = (𝐴 + 1))
30	29	neqned 2966	. . . 4 ⊢ (𝐴 ∈ ℚ → (𝐴 − 1) ≠ (𝐴 + 1))
31	23	absnegd 15645	. . . . 5 ⊢ (𝐴 ∈ ℚ → (abs‘ -1) = (abs‘1))
32	22, 22, 23	subsub4d 11724	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 𝐴) − 1) = (𝐴 − (𝐴 + 1)))
33	22	subidd 11681	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → (𝐴 − 𝐴) = 0)
34	33	oveq1d 7455	. . . . . . . 8 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 𝐴) − 1) = (0 − 1))
35		df-neg 11568	. . . . . . . 8 ⊢ -1 = (0 − 1)
36	34, 35	eqtr4di 2816	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 𝐴) − 1) = -1)
37	32, 36	eqtr3d 2800	. . . . . 6 ⊢ (𝐴 ∈ ℚ → (𝐴 − (𝐴 + 1)) = -1)
38	37	fveq2d 6909	. . . . 5 ⊢ (𝐴 ∈ ℚ → (abs‘(𝐴 − (𝐴 + 1))) = (abs‘ -1))
39	22, 23	nncand 11698	. . . . . 6 ⊢ (𝐴 ∈ ℚ → (𝐴 − (𝐴 − 1)) = 1)
40	39	fveq2d 6909	. . . . 5 ⊢ (𝐴 ∈ ℚ → (abs‘(𝐴 − (𝐴 − 1))) = (abs‘1))
41	31, 38, 40	3eqtr4rd 2809	. . . 4 ⊢ (𝐴 ∈ ℚ → (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − (𝐴 + 1))))
42		neeq2 3022	. . . . . 6 ⊢ (𝑟 = (𝐴 + 1) → ((𝐴 − 1) ≠ 𝑟 ↔ (𝐴 − 1) ≠ (𝐴 + 1)))
43		oveq2 7448	. . . . . . . 8 ⊢ (𝑟 = (𝐴 + 1) → (𝐴 − 𝑟) = (𝐴 − (𝐴 + 1)))
44	43	fveq2d 6909	. . . . . . 7 ⊢ (𝑟 = (𝐴 + 1) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝐴 + 1))))
45	44	eqeq2d 2774	. . . . . 6 ⊢ (𝑟 = (𝐴 + 1) → ((abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − (𝐴 + 1)))))
46	42, 45	anbi12d 644	. . . . 5 ⊢ (𝑟 = (𝐴 + 1) → (((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟))) ↔ ((𝐴 − 1) ≠ (𝐴 + 1) ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − (𝐴 + 1))))))
47	46	rspcev 3580	. . . 4 ⊢ (((𝐴 + 1) ∈ ℚ ∧ ((𝐴 − 1) ≠ (𝐴 + 1) ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − (𝐴 + 1))))) → ∃𝑟 ∈ ℚ ((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟))))
48	12, 30, 41, 47	syl12anc 850	. . 3 ⊢ (𝐴 ∈ ℚ → ∃𝑟 ∈ ℚ ((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟))))
49	5, 10, 48	rspcedvdw 3583	. 2 ⊢ (𝐴 ∈ ℚ → ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))))
50		2cnd 12445	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 2 ∈ ℂ)
51		simpll 779	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝐴 ∈ ℝ)
52	51	recnd 11361	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝐴 ∈ ℂ)
53		simplrl 789	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ∈ ℚ)
54	53	qred 13106	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ∈ ℝ)
55	54	recnd 11361	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ∈ ℂ)
56	52, 55	mulcld 11353	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 · 𝑞) ∈ ℂ)
57		simplrr 790	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑟 ∈ ℚ)
58	57	qred 13106	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑟 ∈ ℝ)
59	58	recnd 11361	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑟 ∈ ℂ)
60	52, 59	mulcld 11353	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 · 𝑟) ∈ ℂ)
61	50, 56, 60	subdid 11796	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · ((𝐴 · 𝑞) − (𝐴 · 𝑟))) = ((2 · (𝐴 · 𝑞)) − (2 · (𝐴 · 𝑟))))
62	52	sqcld 14311	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴↑2) ∈ ℂ)
63	50, 60	mulcld 11353	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · (𝐴 · 𝑟)) ∈ ℂ)
64	50, 56	mulcld 11353	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · (𝐴 · 𝑞)) ∈ ℂ)
65	62, 63, 64	nnncan1d 11727	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝐴↑2) − (2 · (𝐴 · 𝑟))) − ((𝐴↑2) − (2 · (𝐴 · 𝑞)))) = ((2 · (𝐴 · 𝑞)) − (2 · (𝐴 · 𝑟))))
66		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))
67	51, 54	resubcld 11768	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 − 𝑞) ∈ ℝ)
68	51, 58	resubcld 11768	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 − 𝑟) ∈ ℝ)
69		sqabs 15500	. . . . . . . . . . . . 13 ⊢ (((𝐴 − 𝑞) ∈ ℝ ∧ (𝐴 − 𝑟) ∈ ℝ) → (((𝐴 − 𝑞)↑2) = ((𝐴 − 𝑟)↑2) ↔ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))))
70	67, 68, 69	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝐴 − 𝑞)↑2) = ((𝐴 − 𝑟)↑2) ↔ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))))
71	66, 70	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 − 𝑞)↑2) = ((𝐴 − 𝑟)↑2))
72		binom2sub 14388	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑞 ∈ ℂ) → ((𝐴 − 𝑞)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑞))) + (𝑞↑2)))
73	52, 55, 72	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 − 𝑞)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑞))) + (𝑞↑2)))
74		binom2sub 14388	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑟 ∈ ℂ) → ((𝐴 − 𝑟)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑟))) + (𝑟↑2)))
75	52, 59, 74	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 − 𝑟)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑟))) + (𝑟↑2)))
76	71, 73, 75	3eqtr3d 2806	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝐴↑2) − (2 · (𝐴 · 𝑞))) + (𝑞↑2)) = (((𝐴↑2) − (2 · (𝐴 · 𝑟))) + (𝑟↑2)))
77	62, 64	subcld 11693	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴↑2) − (2 · (𝐴 · 𝑞))) ∈ ℂ)
78	55	sqcld 14311	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞↑2) ∈ ℂ)
79	62, 63	subcld 11693	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴↑2) − (2 · (𝐴 · 𝑟))) ∈ ℂ)
80	59	sqcld 14311	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑟↑2) ∈ ℂ)
81	77, 78, 79, 80	addsubeq4d 11744	. . . . . . . . . 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 2804	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · ((𝐴 · 𝑞) − (𝐴 · 𝑟))) = ((𝑞↑2) − (𝑟↑2)))
84	78, 80	subcld 11693	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝑞↑2) − (𝑟↑2)) ∈ ℂ)
85	56, 60	subcld 11693	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 · 𝑞) − (𝐴 · 𝑟)) ∈ ℂ)
86		2ne0 12473	. . . . . . . . . 10 ⊢ 2 ≠ 0
87	86	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 2 ≠ 0)
88	84, 50, 85, 87	divmuld 12139	. . . . . . . 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 11796	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 · (𝑞 − 𝑟)) = ((𝐴 · 𝑞) − (𝐴 · 𝑟)))
91	89, 90	eqtr4d 2801	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝑞↑2) − (𝑟↑2)) / 2) = (𝐴 · (𝑞 − 𝑟)))
92	84	halfcld 12615	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℂ)
93	55, 59	subcld 11693	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞 − 𝑟) ∈ ℂ)
94		simprl 783	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ≠ 𝑟)
95	55, 59, 94	subne0d 11703	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞 − 𝑟) ≠ 0)
96	92, 52, 93, 95	divmul3d 12151	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) = 𝐴 ↔ (((𝑞↑2) − (𝑟↑2)) / 2) = (𝐴 · (𝑞 − 𝑟))))
97	91, 96	mpbird 260	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) = 𝐴)
98		qsqcl 14297	. . . . . . . . 9 ⊢ (𝑞 ∈ ℚ → (𝑞↑2) ∈ ℚ)
99	53, 98	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞↑2) ∈ ℚ)
100		qsqcl 14297	. . . . . . . . 9 ⊢ (𝑟 ∈ ℚ → (𝑟↑2) ∈ ℚ)
101	57, 100	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑟↑2) ∈ ℚ)
102		qsubcl 13120	. . . . . . . 8 ⊢ (((𝑞↑2) ∈ ℚ ∧ (𝑟↑2) ∈ ℚ) → ((𝑞↑2) − (𝑟↑2)) ∈ ℚ)
103	99, 101, 102	syl2anc 596	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝑞↑2) − (𝑟↑2)) ∈ ℚ)
104		2z 12752	. . . . . . . 8 ⊢ 2 ∈ ℤ
105		zq 13105	. . . . . . . 8 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
106	104, 105	mp1i 14	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 2 ∈ ℚ)
107		qdivcl 13122	. . . . . . 7 ⊢ ((((𝑞↑2) − (𝑟↑2)) ∈ ℚ ∧ 2 ∈ ℚ ∧ 2 ≠ 0) → (((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℚ)
108	103, 106, 87, 107	syl3anc 1399	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℚ)
109		qsubcl 13120	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ) → (𝑞 − 𝑟) ∈ ℚ)
110	53, 57, 109	syl2anc 596	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞 − 𝑟) ∈ ℚ)
111		qdivcl 13122	. . . . . 6 ⊢ (((((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℚ ∧ (𝑞 − 𝑟) ∈ ℚ ∧ (𝑞 − 𝑟) ≠ 0) → ((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) ∈ ℚ)
112	108, 110, 95, 111	syl3anc 1399	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) ∈ ℚ)
113	97, 112	eqeltrrd 2865	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝐴 ∈ ℚ)
114	113	ex 418	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) → ((𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) → 𝐴 ∈ ℚ))
115	114	rexlimdvva 3223	. 2 ⊢ (𝐴 ∈ ℝ → (∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) → 𝐴 ∈ ℚ))
116	49, 115	impbid2 229	1 ⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∃wrex 3090 ‘cfv 6555 (class class class)co 7440 ℂcc 11222 ℝcr 11223 0cc0 11224 1c1 11225 + caddc 11227 · cmul 11229 − cmin 11565 -cneg 11566 / cdiv 11997 2c2 12421 ℤcz 12717 ℚcq 13099 ℝ⁺crp 13144 ↑cexp 14228 abscabs 15427

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-om 7899 df-1st 8022 df-2nd 8023 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-er 8742 df-en 8999 df-dom 9000 df-sdom 9001 df-sup 9458 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-n0 12631 df-z 12718 df-uz 12990 df-q 13100 df-rp 13145 df-seq 14169 df-exp 14229 df-cj 15292 df-re 15293 df-im 15294 df-sqrt 15428 df-abs 15429

This theorem is used by: (None)

W3C validator