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

Theorem axlowdim 24990
 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 uzuzle23 11207 . . . 4
2 0re 9651 . . . . 5
32, 2axlowdimlem5 24975 . . . 4
41, 3syl 17 . . 3
5 1re 9650 . . . . 5
65, 2axlowdimlem5 24975 . . . 4
71, 6syl 17 . . 3
82, 5axlowdimlem5 24975 . . . 4
91, 8syl 17 . . 3
10 eqid 2422 . . . 4
1110axlowdimlem15 24985 . . 3
12 eqid 2422 . . . . . 6
13 eqid 2422 . . . . . 6
14 eqid 2422 . . . . . 6
1512, 13, 14, 2, 2axlowdimlem17 24987 . . . . 5 Cgr
16 eqid 2422 . . . . . 6
1712, 13, 16, 5, 2axlowdimlem17 24987 . . . . 5 Cgr
18 eqid 2422 . . . . . 6
1912, 13, 18, 2, 5axlowdimlem17 24987 . . . . 5 Cgr
20 1zzd 10976 . . . . . . . . . . . . . 14
21 peano2zm 10988 . . . . . . . . . . . . . . 15
22213ad2ant2 1027 . . . . . . . . . . . . . 14
23 2m1e1 10732 . . . . . . . . . . . . . . 15
24 2re 10687 . . . . . . . . . . . . . . . . . . . 20
25 3re 10691 . . . . . . . . . . . . . . . . . . . 20
26 2lt3 10785 . . . . . . . . . . . . . . . . . . . 20
2724, 25, 26ltleii 9765 . . . . . . . . . . . . . . . . . . 19
28 zre 10949 . . . . . . . . . . . . . . . . . . . 20
29 letr 9735 . . . . . . . . . . . . . . . . . . . . 21
3024, 25, 29mp3an12 1350 . . . . . . . . . . . . . . . . . . . 20
3128, 30syl 17 . . . . . . . . . . . . . . . . . . 19
3227, 31mpani 680 . . . . . . . . . . . . . . . . . 18
3332imp 430 . . . . . . . . . . . . . . . . 17
34333adant1 1023 . . . . . . . . . . . . . . . 16
35283ad2ant2 1027 . . . . . . . . . . . . . . . . 17
36 lesub1 10116 . . . . . . . . . . . . . . . . . 18
3724, 5, 36mp3an13 1351 . . . . . . . . . . . . . . . . 17
3835, 37syl 17 . . . . . . . . . . . . . . . 16
3934, 38mpbid 213 . . . . . . . . . . . . . . 15
4023, 39syl5eqbrr 4458 . . . . . . . . . . . . . 14
4120, 22, 403jca 1185 . . . . . . . . . . . . 13
42 eluz2 11173 . . . . . . . . . . . . 13
43 eluz2 11173 . . . . . . . . . . . . 13
4441, 42, 433imtr4i 269 . . . . . . . . . . . 12
45 eluzfz1 11814 . . . . . . . . . . . 12
4644, 45syl 17 . . . . . . . . . . 11
4746adantr 466 . . . . . . . . . 10
48 eqeq1 2426 . . . . . . . . . . . 12
49 oveq1 6313 . . . . . . . . . . . . . . 15
5049opeq1d 4193 . . . . . . . . . . . . . 14
5150sneqd 4010 . . . . . . . . . . . . 13
5249sneqd 4010 . . . . . . . . . . . . . . 15
5352difeq2d 3583 . . . . . . . . . . . . . 14
5453xpeq1d 4876 . . . . . . . . . . . . 13
5551, 54uneq12d 3621 . . . . . . . . . . . 12
5648, 55ifbieq2d 3936 . . . . . . . . . . 11
57 snex 4662 . . . . . . . . . . . . 13
58 ovex 6334 . . . . . . . . . . . . . . 15
59 difexg 4572 . . . . . . . . . . . . . . 15
6058, 59ax-mp 5 . . . . . . . . . . . . . 14
61 snex 4662 . . . . . . . . . . . . . 14
6260, 61xpex 6610 . . . . . . . . . . . . 13
6357, 62unex 6604 . . . . . . . . . . . 12
64 snex 4662 . . . . . . . . . . . . 13
65 difexg 4572 . . . . . . . . . . . . . . 15
6658, 65ax-mp 5 . . . . . . . . . . . . . 14
6766, 61xpex 6610 . . . . . . . . . . . . 13
6864, 67unex 6604 . . . . . . . . . . . 12
6963, 68ifex 3979 . . . . . . . . . . 11
7056, 10, 69fvmpt 5965 . . . . . . . . . 10
7147, 70syl 17 . . . . . . . . 9
72 eqid 2422 . . . . . . . . . 10
7372iftruei 3918 . . . . . . . . 9
7471, 73syl6eq 2479 . . . . . . . 8
7574opeq1d 4193 . . . . . . 7
76 2eluzge1 11213 . . . . . . . . . . . . 13
77 fzss1 11845 . . . . . . . . . . . . 13
7876, 77ax-mp 5 . . . . . . . . . . . 12
7978sseli 3460 . . . . . . . . . . 11
8079adantl 467 . . . . . . . . . 10
81 eqeq1 2426 . . . . . . . . . . . 12
82 oveq1 6313 . . . . . . . . . . . . . . 15
8382opeq1d 4193 . . . . . . . . . . . . . 14
8483sneqd 4010 . . . . . . . . . . . . 13
8582sneqd 4010 . . . . . . . . . . . . . . 15
8685difeq2d 3583 . . . . . . . . . . . . . 14
8786xpeq1d 4876 . . . . . . . . . . . . 13
8884, 87uneq12d 3621 . . . . . . . . . . . 12
8981, 88ifbieq2d 3936 . . . . . . . . . . 11
90 snex 4662 . . . . . . . . . . . . 13
91 difexg 4572 . . . . . . . . . . . . . . 15
9258, 91ax-mp 5 . . . . . . . . . . . . . 14
9392, 61xpex 6610 . . . . . . . . . . . . 13
9490, 93unex 6604 . . . . . . . . . . . 12
9563, 94ifex 3979 . . . . . . . . . . 11
9689, 10, 95fvmpt 5965 . . . . . . . . . 10
9780, 96syl 17 . . . . . . . . 9
98 1lt2 10784 . . . . . . . . . . . . . . . 16
995, 24ltnlei 9763 . . . . . . . . . . . . . . . 16
10098, 99mpbi 211 . . . . . . . . . . . . . . 15
101100intnanr 923 . . . . . . . . . . . . . 14
102 eluzelz 11176 . . . . . . . . . . . . . . . 16
103102, 21syl 17 . . . . . . . . . . . . . . 15
104 1z 10975 . . . . . . . . . . . . . . . 16
105 2z 10977 . . . . . . . . . . . . . . . 16
106 elfz 11798 . . . . . . . . . . . . . . . 16
107104, 105, 106mp3an12 1350 . . . . . . . . . . . . . . 15
108103, 107syl 17 . . . . . . . . . . . . . 14
109101, 108mtbiri 304 . . . . . . . . . . . . 13
110 eleq1 2495 . . . . . . . . . . . . . 14
111110notbid 295 . . . . . . . . . . . . 13
112109, 111syl5ibrcom 225 . . . . . . . . . . . 12
113112con2d 118 . . . . . . . . . . 11
114113imp 430 . . . . . . . . . 10
115114iffalsed 3922 . . . . . . . . 9
11697, 115eqtrd 2463 . . . . . . . 8
117116opeq1d 4193 . . . . . . 7
11875, 117breq12d 4436 . . . . . 6 Cgr Cgr
11974opeq1d 4193 . . . . . . 7
120116opeq1d 4193 . . . . . . 7
121119, 120breq12d 4436 . . . . . 6 Cgr Cgr
12246, 70syl 17 . . . . . . . . . 10
123122, 73syl6eq 2479 . . . . . . . . 9
124123opeq1d 4193 . . . . . . . 8
125124adantr 466 . . . . . . 7
126116opeq1d 4193 . . . . . . 7
127125, 126breq12d 4436 . . . . . 6 Cgr Cgr
128118, 121, 1273anbi123d 1335 . . . . 5 Cgr Cgr Cgr Cgr Cgr Cgr
12915, 17, 19, 128mpbir3and 1188 . . . 4 Cgr Cgr Cgr
130129ralrimiva 2836 . . 3 Cgr Cgr Cgr
13114, 16, 18axlowdimlem6 24976 . . . 4
1321, 131syl 17 . . 3
133 opeq2 4188 . . . . . . . 8
134 opeq2 4188 . . . . . . . 8
135133, 134breq12d 4436 . . . . . . 7 Cgr Cgr
1361353anbi1d 1339 . . . . . 6 Cgr Cgr Cgr Cgr Cgr Cgr
137136ralbidv 2861 . . . . 5 Cgr Cgr Cgr Cgr Cgr Cgr
138 breq1 4426 . . . . . . 7
139 opeq2 4188 . . . . . . . 8
140139breq2d 4435 . . . . . . 7
141 opeq1 4187 . . . . . . . 8
142141breq2d 4435 . . . . . . 7
143138, 140, 1423orbi123d 1334 . . . . . 6
144143notbid 295 . . . . 5
145137, 1443anbi23d 1338 . . . 4 Cgr Cgr Cgr Cgr Cgr Cgr
146 opeq2 4188 . . . . . . . 8
147 opeq2 4188 . . . . . . . 8