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 38064

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 38063 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 38063, see qdiffALT 38065. (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 3019	. . . . 5 ⊢ (𝑞 = (𝐴 − 1) → (𝑞 ≠ 𝑟 ↔ (𝐴 − 1) ≠ 𝑟))
2		oveq2 7424	. . . . . 6 ⊢ (𝑞 = (𝐴 − 1) → (𝐴 − 𝑞) = (𝐴 − (𝐴 − 1)))
3	2	fveqeq2d 6890	. . . . 5 ⊢ (𝑞 = (𝐴 − 1) → ((abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟))))
4	1, 3	anbi12d 644	. . . 4 ⊢ (𝑞 = (𝐴 − 1) → ((𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) ↔ ((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟)))))
5	4	rexbidv 3188	. . 3 ⊢ (𝑞 = (𝐴 − 1) → (∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) ↔ ∃𝑟 ∈ ℚ ((𝐴 − 1) ≠ 𝑟 ∧ (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − 𝑟)))))
6		1z 12649	. . . . 5 ⊢ 1 ∈ ℤ
7		zq 13004	. . . . 5 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
8	6, 7	ax-mp 5	. . . 4 ⊢ 1 ∈ ℚ
9		qsubcl 13018	. . . 4 ⊢ ((𝐴 ∈ ℚ ∧ 1 ∈ ℚ) → (𝐴 − 1) ∈ ℚ)
10	8, 9	mpan2 704	. . 3 ⊢ (𝐴 ∈ ℚ → (𝐴 − 1) ∈ ℚ)
11		qaddcl 13015	. . . . 5 ⊢ ((𝐴 ∈ ℚ ∧ 1 ∈ ℚ) → (𝐴 + 1) ∈ ℚ)
12	8, 11	mpan2 704	. . . 4 ⊢ (𝐴 ∈ ℚ → (𝐴 + 1) ∈ ℚ)
13		qre 13003	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)
14		1rp 13046	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ⁺
15	14, 14	pm3.2i 476	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ⁺ ∧ 1 ∈ ℝ⁺)
16		rpaddcl 13066	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ⁺ ∧ 1 ∈ ℝ⁺) → (1 + 1) ∈ ℝ⁺)
17	15, 16	mp1i 14	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℚ → (1 + 1) ∈ ℝ⁺)
18	13, 17	ltaddrpd 13119	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℚ → 𝐴 < (𝐴 + (1 + 1)))
19	13, 18	ltned 11371	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → 𝐴 ≠ (𝐴 + (1 + 1)))
20	19	neneqd 2962	. . . . . . . 8 ⊢ (𝐴 ∈ ℚ → ¬ 𝐴 = (𝐴 + (1 + 1)))
21	20	neqcomd 2772	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → ¬ (𝐴 + (1 + 1)) = 𝐴)
22		qcn 13013	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
23		1cnd 11227	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → 1 ∈ ℂ)
24	22, 23, 23	addassd 11256	. . . . . . . 8 ⊢ (𝐴 ∈ ℚ → ((𝐴 + 1) + 1) = (𝐴 + (1 + 1)))
25	24	eqeq1d 2764	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → (((𝐴 + 1) + 1) = 𝐴 ↔ (𝐴 + (1 + 1)) = 𝐴))
26	21, 25	mtbird 328	. . . . . 6 ⊢ (𝐴 ∈ ℚ → ¬ ((𝐴 + 1) + 1) = 𝐴)
27	22, 23	addcld 11253	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → (𝐴 + 1) ∈ ℂ)
28	22, 23, 27	subadd2d 11613	. . . . . 6 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 1) = (𝐴 + 1) ↔ ((𝐴 + 1) + 1) = 𝐴))
29	26, 28	mtbird 328	. . . . 5 ⊢ (𝐴 ∈ ℚ → ¬ (𝐴 − 1) = (𝐴 + 1))
30	29	neqned 2964	. . . 4 ⊢ (𝐴 ∈ ℚ → (𝐴 − 1) ≠ (𝐴 + 1))
31	23	absnegd 15539	. . . . 5 ⊢ (𝐴 ∈ ℚ → (abs‘-1) = (abs‘1))
32	22, 22, 23	subsub4d 11625	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 𝐴) − 1) = (𝐴 − (𝐴 + 1)))
33	22	subidd 11582	. . . . . . . . 9 ⊢ (𝐴 ∈ ℚ → (𝐴 − 𝐴) = 0)
34	33	oveq1d 7431	. . . . . . . 8 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 𝐴) − 1) = (0 − 1))
35		df-neg 11469	. . . . . . . 8 ⊢ -1 = (0 − 1)
36	34, 35	eqtr4di 2815	. . . . . . 7 ⊢ (𝐴 ∈ ℚ → ((𝐴 − 𝐴) − 1) = -1)
37	32, 36	eqtr3d 2799	. . . . . 6 ⊢ (𝐴 ∈ ℚ → (𝐴 − (𝐴 + 1)) = -1)
38	37	fveq2d 6886	. . . . 5 ⊢ (𝐴 ∈ ℚ → (abs‘(𝐴 − (𝐴 + 1))) = (abs‘-1))
39	22, 23	nncand 11599	. . . . . 6 ⊢ (𝐴 ∈ ℚ → (𝐴 − (𝐴 − 1)) = 1)
40	39	fveq2d 6886	. . . . 5 ⊢ (𝐴 ∈ ℚ → (abs‘(𝐴 − (𝐴 − 1))) = (abs‘1))
41	31, 38, 40	3eqtr4rd 2808	. . . 4 ⊢ (𝐴 ∈ ℚ → (abs‘(𝐴 − (𝐴 − 1))) = (abs‘(𝐴 − (𝐴 + 1))))
42		neeq2 3020	. . . . . 6 ⊢ (𝑟 = (𝐴 + 1) → ((𝐴 − 1) ≠ 𝑟 ↔ (𝐴 − 1) ≠ (𝐴 + 1)))
43		oveq2 7424	. . . . . . . 8 ⊢ (𝑟 = (𝐴 + 1) → (𝐴 − 𝑟) = (𝐴 − (𝐴 + 1)))
44	43	fveq2d 6886	. . . . . . 7 ⊢ (𝑟 = (𝐴 + 1) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝐴 + 1))))
45	44	eqeq2d 2773	. . . . . 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 3579	. . . 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 3582	. 2 ⊢ (𝐴 ∈ ℚ → ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))))
50		2cnd 12344	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 2 ∈ ℂ)
51		simpll 779	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝐴 ∈ ℝ)
52	51	recnd 11262	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝐴 ∈ ℂ)
53		simplrl 789	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ∈ ℚ)
54	53	qred 13005	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ∈ ℝ)
55	54	recnd 11262	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ∈ ℂ)
56	52, 55	mulcld 11254	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 · 𝑞) ∈ ℂ)
57		simplrr 790	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑟 ∈ ℚ)
58	57	qred 13005	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑟 ∈ ℝ)
59	58	recnd 11262	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑟 ∈ ℂ)
60	52, 59	mulcld 11254	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 · 𝑟) ∈ ℂ)
61	50, 56, 60	subdid 11695	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · ((𝐴 · 𝑞) − (𝐴 · 𝑟))) = ((2 · (𝐴 · 𝑞)) − (2 · (𝐴 · 𝑟))))
62	52	sqcld 14208	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴↑2) ∈ ℂ)
63	50, 60	mulcld 11254	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · (𝐴 · 𝑟)) ∈ ℂ)
64	50, 56	mulcld 11254	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · (𝐴 · 𝑞)) ∈ ℂ)
65	62, 63, 64	nnncan1d 11628	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝐴↑2) − (2 · (𝐴 · 𝑟))) − ((𝐴↑2) − (2 · (𝐴 · 𝑞)))) = ((2 · (𝐴 · 𝑞)) − (2 · (𝐴 · 𝑟))))
66		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))
67	51, 54	resubcld 11667	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 − 𝑞) ∈ ℝ)
68	51, 58	resubcld 11667	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 − 𝑟) ∈ ℝ)
69		sqabs 15394	. . . . . . . . . . . . 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 14284	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑞 ∈ ℂ) → ((𝐴 − 𝑞)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑞))) + (𝑞↑2)))
73	52, 55, 72	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 − 𝑞)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑞))) + (𝑞↑2)))
74		binom2sub 14284	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑟 ∈ ℂ) → ((𝐴 − 𝑟)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑟))) + (𝑟↑2)))
75	52, 59, 74	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 − 𝑟)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝑟))) + (𝑟↑2)))
76	71, 73, 75	3eqtr3d 2805	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝐴↑2) − (2 · (𝐴 · 𝑞))) + (𝑞↑2)) = (((𝐴↑2) − (2 · (𝐴 · 𝑟))) + (𝑟↑2)))
77	62, 64	subcld 11594	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴↑2) − (2 · (𝐴 · 𝑞))) ∈ ℂ)
78	55	sqcld 14208	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞↑2) ∈ ℂ)
79	62, 63	subcld 11594	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴↑2) − (2 · (𝐴 · 𝑟))) ∈ ℂ)
80	59	sqcld 14208	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑟↑2) ∈ ℂ)
81	77, 78, 79, 80	addsubeq4d 11645	. . . . . . . . . 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 2803	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (2 · ((𝐴 · 𝑞) − (𝐴 · 𝑟))) = ((𝑞↑2) − (𝑟↑2)))
84	78, 80	subcld 11594	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝑞↑2) − (𝑟↑2)) ∈ ℂ)
85	56, 60	subcld 11594	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝐴 · 𝑞) − (𝐴 · 𝑟)) ∈ ℂ)
86		2ne0 12372	. . . . . . . . . 10 ⊢ 2 ≠ 0
87	86	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 2 ≠ 0)
88	84, 50, 85, 87	divmuld 12038	. . . . . . . 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 11695	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝐴 · (𝑞 − 𝑟)) = ((𝐴 · 𝑞) − (𝐴 · 𝑟)))
91	89, 90	eqtr4d 2800	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝑞↑2) − (𝑟↑2)) / 2) = (𝐴 · (𝑞 − 𝑟)))
92	84	halfcld 12514	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℂ)
93	55, 59	subcld 11594	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞 − 𝑟) ∈ ℂ)
94		simprl 783	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝑞 ≠ 𝑟)
95	55, 59, 94	subne0d 11603	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞 − 𝑟) ≠ 0)
96	92, 52, 93, 95	divmul3d 12050	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) = 𝐴 ↔ (((𝑞↑2) − (𝑟↑2)) / 2) = (𝐴 · (𝑞 − 𝑟))))
97	91, 96	mpbird 260	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) = 𝐴)
98		qsqcl 14194	. . . . . . . . 9 ⊢ (𝑞 ∈ ℚ → (𝑞↑2) ∈ ℚ)
99	53, 98	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞↑2) ∈ ℚ)
100		qsqcl 14194	. . . . . . . . 9 ⊢ (𝑟 ∈ ℚ → (𝑟↑2) ∈ ℚ)
101	57, 100	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑟↑2) ∈ ℚ)
102		qsubcl 13018	. . . . . . . 8 ⊢ (((𝑞↑2) ∈ ℚ ∧ (𝑟↑2) ∈ ℚ) → ((𝑞↑2) − (𝑟↑2)) ∈ ℚ)
103	99, 101, 102	syl2anc 596	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((𝑞↑2) − (𝑟↑2)) ∈ ℚ)
104		2z 12651	. . . . . . . 8 ⊢ 2 ∈ ℤ
105		zq 13004	. . . . . . . 8 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
106	104, 105	mp1i 14	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 2 ∈ ℚ)
107		qdivcl 13020	. . . . . . 7 ⊢ ((((𝑞↑2) − (𝑟↑2)) ∈ ℚ ∧ 2 ∈ ℚ ∧ 2 ≠ 0) → (((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℚ)
108	103, 106, 87, 107	syl3anc 1398	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℚ)
109		qsubcl 13018	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ) → (𝑞 − 𝑟) ∈ ℚ)
110	53, 57, 109	syl2anc 596	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → (𝑞 − 𝑟) ∈ ℚ)
111		qdivcl 13020	. . . . . 6 ⊢ (((((𝑞↑2) − (𝑟↑2)) / 2) ∈ ℚ ∧ (𝑞 − 𝑟) ∈ ℚ ∧ (𝑞 − 𝑟) ≠ 0) → ((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) ∈ ℚ)
112	108, 110, 95, 111	syl3anc 1398	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → ((((𝑞↑2) − (𝑟↑2)) / 2) / (𝑞 − 𝑟)) ∈ ℚ)
113	97, 112	eqeltrrd 2863	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) ∧ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) → 𝐴 ∈ ℚ)
114	113	ex 418	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ (𝑞 ∈ ℚ ∧ 𝑟 ∈ ℚ)) → ((𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟))) → 𝐴 ∈ ℚ))
115	114	rexlimdvva 3221	. 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 2145 ≠ wne 2957 ∃wrex 3088 ‘cfv 6537 (class class class)co 7416 ℂcc 11123 ℝcr 11124 0cc0 11125 1c1 11126 + caddc 11128 · cmul 11130 − cmin 11466 -cneg 11467 / cdiv 11896 2c2 12320 ℤcz 12616 ℚcq 12998 ℝ⁺crp 13042 ↑cexp 14125 abscabs 15321

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202 ax-pre-sup 11203

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 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 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 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-sup 9415 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-div 11897 df-nn 12259 df-2 12328 df-3 12329 df-n0 12530 df-z 12617 df-uz 12889 df-q 12999 df-rp 13043 df-seq 14066 df-exp 14126 df-cj 15186 df-re 15187 df-im 15188 df-sqrt 15322 df-abs 15323

This theorem is used by: (None)

W3C validator