apdiff - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > apdiff		Unicode version

Theorem apdiff 13560

Description: The irrationals (reals apart from any rational) are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 17-May-2024.)

**Assertion**
Ref	Expression
apdiff	# #

Distinct variable group:

Proof of Theorem apdiff Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 3965	. . 3 # #
2	1	cbvralv 2677	. 2 # #
3		simplll 523	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$
4	3	adantr 274	. . . . . . 7 $/\$ # $/\$ $/\$ $/\$ $/\$
5		simplrl 525	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$
6	5	adantr 274	. . . . . . 7 $/\$ # $/\$ $/\$ $/\$ $/\$
7		simplrr 526	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$
8	7	adantr 274	. . . . . . 7 $/\$ # $/\$ $/\$ $/\$ $/\$
9		simpr 109	. . . . . . 7 $/\$ # $/\$ $/\$ $/\$ $/\$
10		breq2 3965	. . . . . . . . . 10 # #
11		simpllr 524	. . . . . . . . . 10 $/\$ # $/\$ $/\$ $/\$ #
12		qaddcl 9522	. . . . . . . . . . . 12 $/\$
13	5, 7, 12	syl2anc 409	. . . . . . . . . . 11 $/\$ # $/\$ $/\$ $/\$
14		2z 9174	. . . . . . . . . . . 12
15		zq 9513	. . . . . . . . . . . 12
16	14, 15	mp1i 10	. . . . . . . . . . 11 $/\$ # $/\$ $/\$ $/\$
17		2ne0 8904	. . . . . . . . . . . 12
18	17	a1i 9	. . . . . . . . . . 11 $/\$ # $/\$ $/\$ $/\$
19		qdivcl 9530	. . . . . . . . . . 11 $/\$ $/\$
20	13, 16, 18, 19	syl3anc 1217	. . . . . . . . . 10 $/\$ # $/\$ $/\$ $/\$
21	10, 11, 20	rspcdva 2818	. . . . . . . . 9 $/\$ # $/\$ $/\$ $/\$ #
22	3	recnd 7885	. . . . . . . . . 10 $/\$ # $/\$ $/\$ $/\$
23		qcn 9521	. . . . . . . . . . 11
24	20, 23	syl 14	. . . . . . . . . 10 $/\$ # $/\$ $/\$ $/\$
25		apsym 8460	. . . . . . . . . 10 $/\$ # #
26	22, 24, 25	syl2anc 409	. . . . . . . . 9 $/\$ # $/\$ $/\$ $/\$ # #
27	21, 26	mpbid 146	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$ #
28	27	adantr 274	. . . . . . 7 $/\$ # $/\$ $/\$ $/\$ $/\$ #
29	4, 6, 8, 9, 28	apdifflemf 13558	. . . . . 6 $/\$ # $/\$ $/\$ $/\$ $/\$ #
30	3	adantr 274	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$ $/\$
31	7	adantr 274	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$ $/\$
32	5	adantr 274	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$ $/\$
33		simpr 109	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$ $/\$
34		qcn 9521	. . . . . . . . . . . . 13
35	5, 34	syl 14	. . . . . . . . . . . 12 $/\$ # $/\$ $/\$ $/\$
36		qcn 9521	. . . . . . . . . . . . 13
37	7, 36	syl 14	. . . . . . . . . . . 12 $/\$ # $/\$ $/\$ $/\$
38	35, 37	addcomd 8005	. . . . . . . . . . 11 $/\$ # $/\$ $/\$ $/\$
39	38	oveq1d 5829	. . . . . . . . . 10 $/\$ # $/\$ $/\$ $/\$
40	39, 27	eqbrtrrd 3984	. . . . . . . . 9 $/\$ # $/\$ $/\$ $/\$ #
41	40	adantr 274	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$ $/\$ #
42	30, 31, 32, 33, 41	apdifflemf 13558	. . . . . . 7 $/\$ # $/\$ $/\$ $/\$ $/\$ #
43	22	adantr 274	. . . . . . . . . . 11 $/\$ # $/\$ $/\$ $/\$ $/\$
44	31, 36	syl 14	. . . . . . . . . . 11 $/\$ # $/\$ $/\$ $/\$ $/\$
45	43, 44	subcld 8165	. . . . . . . . . 10 $/\$ # $/\$ $/\$ $/\$ $/\$
46	45	abscld 11058	. . . . . . . . 9 $/\$ # $/\$ $/\$ $/\$ $/\$
47	46	recnd 7885	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$ $/\$
48	32, 34	syl 14	. . . . . . . . . . 11 $/\$ # $/\$ $/\$ $/\$ $/\$
49	43, 48	subcld 8165	. . . . . . . . . 10 $/\$ # $/\$ $/\$ $/\$ $/\$
50	49	abscld 11058	. . . . . . . . 9 $/\$ # $/\$ $/\$ $/\$ $/\$
51	50	recnd 7885	. . . . . . . 8 $/\$ # $/\$ $/\$ $/\$ $/\$
52		apsym 8460	. . . . . . . 8 $/\$ # #
53	47, 51, 52	syl2anc 409	. . . . . . 7 $/\$ # $/\$ $/\$ $/\$ $/\$ # #
54	42, 53	mpbid 146	. . . . . 6 $/\$ # $/\$ $/\$ $/\$ $/\$ #
55		simpr 109	. . . . . . 7 $/\$ # $/\$ $/\$ $/\$
56		qlttri2 9528	. . . . . . . 8 $/\$ $\/$
57	5, 7, 56	syl2anc 409	. . . . . . 7 $/\$ # $/\$ $/\$ $/\$ $\/$
58	55, 57	mpbid 146	. . . . . 6 $/\$ # $/\$ $/\$ $/\$ $\/$
59	29, 54, 58	mpjaodan 788	. . . . 5 $/\$ # $/\$ $/\$ $/\$ #
60	59	ex 114	. . . 4 $/\$ # $/\$ $/\$ #
61	60	ralrimivva 2536	. . 3 $/\$ # #
62		simpll 519	. . . . 5 $/\$ # $/\$
63		simpr 109	. . . . 5 $/\$ # $/\$
64		simplr 520	. . . . . 6 $/\$ # $/\$ #
65		neg1rr 8918	. . . . . . . 8
66		neg1lt0 8920	. . . . . . . . 9
67		0lt1 7981	. . . . . . . . 9
68		0re 7857	. . . . . . . . . 10
69		1re 7856	. . . . . . . . . 10
70	65, 68, 69	lttri 7960	. . . . . . . . 9 $/\$
71	66, 67, 70	mp2an 423	. . . . . . . 8
72	65, 71	ltneii 7952	. . . . . . 7
73	72	a1i 9	. . . . . 6 $/\$ # $/\$
74		neg1z 9178	. . . . . . . 8
75		zq 9513	. . . . . . . 8
76	74, 75	mp1i 10	. . . . . . 7 $/\$ # $/\$
77		1z 9172	. . . . . . . 8
78		zq 9513	. . . . . . . 8
79	77, 78	mp1i 10	. . . . . . 7 $/\$ # $/\$
80		simpl 108	. . . . . . . . . 10 $/\$
81		simpr 109	. . . . . . . . . 10 $/\$
82	80, 81	neeq12d 2344	. . . . . . . . 9 $/\$
83	80	oveq2d 5830	. . . . . . . . . . 11 $/\$
84	83	fveq2d 5465	. . . . . . . . . 10 $/\$
85	81	oveq2d 5830	. . . . . . . . . . 11 $/\$
86	85	fveq2d 5465	. . . . . . . . . 10 $/\$
87	84, 86	breq12d 3974	. . . . . . . . 9 $/\$ # #
88	82, 87	imbi12d 233	. . . . . . . 8 $/\$ # #
89	88	rspc2gv 2825	. . . . . . 7 $/\$ # #
90	76, 79, 89	syl2anc 409	. . . . . 6 $/\$ # $/\$ # #
91	64, 73, 90	mp2d 47	. . . . 5 $/\$ # $/\$ #
92		simpllr 524	. . . . . 6 $/\$ # $/\$ $/\$ #
93		2cnd 8885	. . . . . . . . 9 $/\$ # $/\$ $/\$
94		simplr 520	. . . . . . . . . 10 $/\$ # $/\$ $/\$
95		qcn 9521	. . . . . . . . . 10
96	94, 95	syl 14	. . . . . . . . 9 $/\$ # $/\$ $/\$
97		2ap0 8905	. . . . . . . . . 10 #
98	97	a1i 9	. . . . . . . . 9 $/\$ # $/\$ $/\$ #
99		simpr 109	. . . . . . . . . 10 $/\$ # $/\$ $/\$
100		0z 9157	. . . . . . . . . . . 12
101		zq 9513	. . . . . . . . . . . 12
102	100, 101	mp1i 10	. . . . . . . . . . 11 $/\$ # $/\$ $/\$
103		qapne 9526	. . . . . . . . . . 11 $/\$ #
104	94, 102, 103	syl2anc 409	. . . . . . . . . 10 $/\$ # $/\$ $/\$ #
105	99, 104	mpbird 166	. . . . . . . . 9 $/\$ # $/\$ $/\$ #
106	93, 96, 98, 105	mulap0d 8511	. . . . . . . 8 $/\$ # $/\$ $/\$ #
107	14, 15	mp1i 10	. . . . . . . . . . 11 $/\$ # $/\$ $/\$
108		qmulcl 9524	. . . . . . . . . . 11 $/\$
109	107, 94, 108	syl2anc 409	. . . . . . . . . 10 $/\$ # $/\$ $/\$
110		qcn 9521	. . . . . . . . . 10
111	109, 110	syl 14	. . . . . . . . 9 $/\$ # $/\$ $/\$
112		0cnd 7850	. . . . . . . . 9 $/\$ # $/\$ $/\$
113		apsym 8460	. . . . . . . . 9 $/\$ # #
114	111, 112, 113	syl2anc 409	. . . . . . . 8 $/\$ # $/\$ $/\$ # #
115	106, 114	mpbid 146	. . . . . . 7 $/\$ # $/\$ $/\$ #
116		qapne 9526	. . . . . . . 8 $/\$ #
117	102, 109, 116	syl2anc 409	. . . . . . 7 $/\$ # $/\$ $/\$ #
118	115, 117	mpbid 146	. . . . . 6 $/\$ # $/\$ $/\$
119		simpl 108	. . . . . . . . . 10 $/\$
120		simpr 109	. . . . . . . . . 10 $/\$
121	119, 120	neeq12d 2344	. . . . . . . . 9 $/\$
122	119	oveq2d 5830	. . . . . . . . . . 11 $/\$
123	122	fveq2d 5465	. . . . . . . . . 10 $/\$
124	120	oveq2d 5830	. . . . . . . . . . 11 $/\$
125	124	fveq2d 5465	. . . . . . . . . 10 $/\$
126	123, 125	breq12d 3974	. . . . . . . . 9 $/\$ # #
127	121, 126	imbi12d 233	. . . . . . . 8 $/\$ # #
128	127	rspc2gv 2825	. . . . . . 7 $/\$ # #
129	102, 109, 128	syl2anc 409	. . . . . 6 $/\$ # $/\$ $/\$ # #
130	92, 118, 129	mp2d 47	. . . . 5 $/\$ # $/\$ $/\$ #
131	62, 63, 91, 130	apdifflemr 13559	. . . 4 $/\$ # $/\$ #
132	131	ralrimiva 2527	. . 3 $/\$ # #
133	61, 132	impbida 586	. 2 # #
134	2, 133	syl5bb 191	1 # #

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698

wceq 1332

wcel 2125

wne 2324

wral 2432 class class class wbr 3961

cfv 5163 (class class class)co 5814

cc 7709

cr 7710

cc0 7711

c1 7712

caddc 7714

cmul 7716

clt 7891

cmin 8025

cneg 8026 # cap 8435

cdiv 8524

c2 8863

cz 9146

cq 9506

cabs 10874

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-coll 4075 ax-sep 4078 ax-nul 4086 ax-pow 4130 ax-pr 4164 ax-un 4388 ax-setind 4490 ax-iinf 4541 ax-cnex 7802 ax-resscn 7803 ax-1cn 7804 ax-1re 7805 ax-icn 7806 ax-addcl 7807 ax-addrcl 7808 ax-mulcl 7809 ax-mulrcl 7810 ax-addcom 7811 ax-mulcom 7812 ax-addass 7813 ax-mulass 7814 ax-distr 7815 ax-i2m1 7816 ax-0lt1 7817 ax-1rid 7818 ax-0id 7819 ax-rnegex 7820 ax-precex 7821 ax-cnre 7822 ax-pre-ltirr 7823 ax-pre-ltwlin 7824 ax-pre-lttrn 7825 ax-pre-apti 7826 ax-pre-ltadd 7827 ax-pre-mulgt0 7828 ax-pre-mulext 7829 ax-arch 7830 ax-caucvg 7831

This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-nel 2420 df-ral 2437 df-rex 2438 df-reu 2439 df-rmo 2440 df-rab 2441 df-v 2711 df-sbc 2934 df-csb 3028 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-nul 3391 df-if 3502 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-int 3804 df-iun 3847 df-br 3962 df-opab 4022 df-mpt 4023 df-tr 4059 df-id 4248 df-po 4251 df-iso 4252 df-iord 4321 df-on 4323 df-ilim 4324 df-suc 4326 df-iom 4544 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-rn 4590 df-res 4591 df-ima 4592 df-iota 5128 df-fun 5165 df-fn 5166 df-f 5167 df-f1 5168 df-fo 5169 df-f1o 5170 df-fv 5171 df-riota 5770 df-ov 5817 df-oprab 5818 df-mpo 5819 df-1st 6078 df-2nd 6079 df-recs 6242 df-frec 6328 df-pnf 7893 df-mnf 7894 df-xr 7895 df-ltxr 7896 df-le 7897 df-sub 8027 df-neg 8028 df-reap 8429 df-ap 8436 df-div 8525 df-inn 8813 df-2 8871 df-3 8872 df-4 8873 df-n0 9070 df-z 9147 df-uz 9419 df-q 9507 df-rp 9539 df-seqfrec 10323 df-exp 10397 df-cj 10719 df-re 10720 df-im 10721 df-rsqrt 10875 df-abs 10876

This theorem is referenced by: (None)

W3C validator