Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axlowdim Structured version   Unicode version

Theorem axlowdim 23940
 Description: The general lower dimension axiom. Take a dimension greater than or equal to three. Then, there are three non-colinear points in dimensional space that are equidistant from distinct points. Derived from remarks in Tarski's System of Geometry, Alfred Tarski and Steven Givant, Bulletin of Symbolic Logic, Volume 5, Number 2 (1999), 175-214. (Contributed by Scott Fenton, 22-Apr-2013.)
Assertion
Ref Expression
axlowdim Cgr Cgr Cgr
Distinct variable group:   ,,,,,

Proof of Theorem axlowdim
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 2re 10601 . . . . . . . 8
2 3re 10605 . . . . . . . 8
3 2lt3 10699 . . . . . . . 8
41, 2, 3ltleii 9703 . . . . . . 7
5 2z 10892 . . . . . . . 8
6 3z 10893 . . . . . . . 8
7 eluz 11091 . . . . . . . 8
85, 6, 7mp2an 672 . . . . . . 7
94, 8mpbir 209 . . . . . 6
10 uzss 11098 . . . . . 6
119, 10ax-mp 5 . . . . 5
1211sseli 3500 . . . 4
13 0re 9592 . . . . 5
1413, 13axlowdimlem5 23925 . . . 4
1512, 14syl 16 . . 3
16 1re 9591 . . . . 5
1716, 13axlowdimlem5 23925 . . . 4
1812, 17syl 16 . . 3
1913, 16axlowdimlem5 23925 . . . 4
2012, 19syl 16 . . 3
21 eqid 2467 . . . 4
2221axlowdimlem15 23935 . . 3
23 eqid 2467 . . . . . 6
24 eqid 2467 . . . . . 6
25 eqid 2467 . . . . . 6
2623, 24, 25, 13, 13axlowdimlem17 23937 . . . . 5 Cgr
27 eqid 2467 . . . . . 6
2823, 24, 27, 16, 13axlowdimlem17 23937 . . . . 5 Cgr
29 eqid 2467 . . . . . 6
3023, 24, 29, 13, 16axlowdimlem17 23937 . . . . 5 Cgr
31 1z 10890 . . . . . . . . . . . . . . 15
3231a1i 11 . . . . . . . . . . . . . 14
33 peano2zm 10902 . . . . . . . . . . . . . . 15
34333ad2ant2 1018 . . . . . . . . . . . . . 14
35 2m1e1 10646 . . . . . . . . . . . . . . 15
36 zre 10864 . . . . . . . . . . . . . . . . . . . 20
37 letr 9674 . . . . . . . . . . . . . . . . . . . . 21
381, 2, 37mp3an12 1314 . . . . . . . . . . . . . . . . . . . 20
3936, 38syl 16 . . . . . . . . . . . . . . . . . . 19
404, 39mpani 676 . . . . . . . . . . . . . . . . . 18
4140imp 429 . . . . . . . . . . . . . . . . 17
42413adant1 1014 . . . . . . . . . . . . . . . 16
43363ad2ant2 1018 . . . . . . . . . . . . . . . . 17
44 lesub1 10042 . . . . . . . . . . . . . . . . . 18
451, 16, 44mp3an13 1315 . . . . . . . . . . . . . . . . 17
4643, 45syl 16 . . . . . . . . . . . . . . . 16
4742, 46mpbid 210 . . . . . . . . . . . . . . 15
4835, 47syl5eqbrr 4481 . . . . . . . . . . . . . 14
4932, 34, 483jca 1176 . . . . . . . . . . . . 13
50 eluz2 11084 . . . . . . . . . . . . 13
51 eluz2 11084 . . . . . . . . . . . . 13
5249, 50, 513imtr4i 266 . . . . . . . . . . . 12
53 eluzfz1 11689 . . . . . . . . . . . 12
5452, 53syl 16 . . . . . . . . . . 11
5554adantr 465 . . . . . . . . . 10
56 eqeq1 2471 . . . . . . . . . . . 12
57 oveq1 6289 . . . . . . . . . . . . . . 15
5857opeq1d 4219 . . . . . . . . . . . . . 14
5958sneqd 4039 . . . . . . . . . . . . 13
6057sneqd 4039 . . . . . . . . . . . . . . 15
6160difeq2d 3622 . . . . . . . . . . . . . 14
6261xpeq1d 5022 . . . . . . . . . . . . 13
6359, 62uneq12d 3659 . . . . . . . . . . . 12
6456, 63ifbieq2d 3964 . . . . . . . . . . 11
65 snex 4688 . . . . . . . . . . . . 13
66 ovex 6307 . . . . . . . . . . . . . . 15
67 difexg 4595 . . . . . . . . . . . . . . 15
6866, 67ax-mp 5 . . . . . . . . . . . . . 14
69 snex 4688 . . . . . . . . . . . . . 14
7068, 69xpex 6711 . . . . . . . . . . . . 13
7165, 70unex 6580 . . . . . . . . . . . 12
72 snex 4688 . . . . . . . . . . . . 13
73 difexg 4595 . . . . . . . . . . . . . . 15
7466, 73ax-mp 5 . . . . . . . . . . . . . 14
7574, 69xpex 6711 . . . . . . . . . . . . 13
7672, 75unex 6580 . . . . . . . . . . . 12
7771, 76ifex 4008 . . . . . . . . . . 11
7864, 21, 77fvmpt 5948 . . . . . . . . . 10
7955, 78syl 16 . . . . . . . . 9
80 eqid 2467 . . . . . . . . . 10
8180iftruei 3946 . . . . . . . . 9
8279, 81syl6eq 2524 . . . . . . . 8
8382opeq1d 4219 . . . . . . 7
84 2nn 10689 . . . . . . . . . . . . . 14
85 nnuz 11113 . . . . . . . . . . . . . 14
8684, 85eleqtri 2553 . . . . . . . . . . . . 13
87 fzss1 11718 . . . . . . . . . . . . 13
8886, 87ax-mp 5 . . . . . . . . . . . 12
8988sseli 3500 . . . . . . . . . . 11
9089adantl 466 . . . . . . . . . 10
91 eqeq1 2471 . . . . . . . . . . . 12
92 oveq1 6289 . . . . . . . . . . . . . . 15
9392opeq1d 4219 . . . . . . . . . . . . . 14
9493sneqd 4039 . . . . . . . . . . . . 13
9592sneqd 4039 . . . . . . . . . . . . . . 15
9695difeq2d 3622 . . . . . . . . . . . . . 14
9796xpeq1d 5022 . . . . . . . . . . . . 13
9894, 97uneq12d 3659 . . . . . . . . . . . 12
9991, 98ifbieq2d 3964 . . . . . . . . . . 11
100 snex 4688 . . . . . . . . . . . . 13
101 difexg 4595 . . . . . . . . . . . . . . 15
10266, 101ax-mp 5 . . . . . . . . . . . . . 14
103102, 69xpex 6711 . . . . . . . . . . . . 13
104100, 103unex 6580 . . . . . . . . . . . 12
10571, 104ifex 4008 . . . . . . . . . . 11
10699, 21, 105fvmpt 5948 . . . . . . . . . 10
10790, 106syl 16 . . . . . . . . 9
108 1lt2 10698 . . . . . . . . . . . . . . . 16
10916, 1ltnlei 9701 . . . . . . . . . . . . . . . 16
110108, 109mpbi 208 . . . . . . . . . . . . . . 15
111110intnanr 913 . . . . . . . . . . . . . 14
112 eluzelz 11087 . . . . . . . . . . . . . . . 16
113112, 33syl 16 . . . . . . . . . . . . . . 15
114 elfz 11674 . . . . . . . . . . . . . . . 16
11531, 5, 114mp3an12 1314 . . . . . . . . . . . . . . 15
116113, 115syl 16 . . . . . . . . . . . . . 14
117111, 116mtbiri 303 . . . . . . . . . . . . 13
118 eleq1 2539 . . . . . . . . . . . . . 14
119118notbid 294 . . . . . . . . . . . . 13
120117, 119syl5ibrcom 222 . . . . . . . . . . . 12
121120con2d 115 . . . . . . . . . . 11
122121imp 429 . . . . . . . . . 10
123 iffalse 3948 . . . . . . . . . 10
124122, 123syl 16 . . . . . . . . 9
125107, 124eqtrd 2508 . . . . . . . 8
126125opeq1d 4219 . . . . . . 7
12783, 126breq12d 4460 . . . . . 6 Cgr Cgr
12882opeq1d 4219 . . . . . . 7
129125opeq1d 4219 . . . . . . 7
130128, 129breq12d 4460 . . . . . 6 Cgr Cgr
13154, 78syl 16 . . . . . . . . . 10
132131, 81syl6eq 2524 . . . . . . . . 9
133132opeq1d 4219 . . . . . . . 8
134133adantr 465 . . . . . . 7
135125opeq1d 4219 . . . . . . 7
136134, 135breq12d 4460 . . . . . 6 Cgr Cgr
137127, 130, 1363anbi123d 1299 . . . . 5 Cgr Cgr Cgr Cgr Cgr Cgr
13826, 28, 30, 137mpbir3and 1179 . . . 4 Cgr Cgr Cgr
139138ralrimiva 2878 . . 3 Cgr Cgr Cgr
14025, 27, 29axlowdimlem6 23926 . . . 4
14112, 140syl 16 . . 3
142 opeq2 4214 . . . . . . . 8
143 opeq2 4214 . . . . . . . 8
144142, 143breq12d 4460 . . . . . . 7 Cgr Cgr
1451443anbi1d 1303 . . . . . 6 Cgr Cgr Cgr Cgr Cgr Cgr
146145ralbidv 2903 . . . . 5 Cgr Cgr Cgr Cgr Cgr Cgr
147 breq1 4450 . . . . . . 7
148 opeq2 4214 . . . . . . . 8
149148breq2d 4459 . . . . . . 7
150 opeq1 4213 . . . . . . . 8
151150breq2d 4459 . . . . . . 7
152147, 149, 1513orbi123d 1298 . . . . . 6
153152notbid 294 . . . . 5
154146, 1533anbi23d 1302 . . . 4 Cgr Cgr Cgr Cgr Cgr Cgr
155 opeq2 4214 . . . . . . . 8