Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axlowdim Structured version   Unicode version

Theorem axlowdim 25892
 Description: The general lower dimensional 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", by Alfred Tarski and Steven Givant, Bull. 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 10061 . . . . . . . 8
2 3re 10063 . . . . . . . 8
3 2lt3 10135 . . . . . . . 8
41, 2, 3ltleii 9188 . . . . . . 7
5 2z 10304 . . . . . . . 8
6 3nn 10126 . . . . . . . . 9
76nnzi 10297 . . . . . . . 8
8 eluz 10491 . . . . . . . 8
95, 7, 8mp2an 654 . . . . . . 7
104, 9mpbir 201 . . . . . 6
11 uzss 10498 . . . . . 6
1210, 11ax-mp 8 . . . . 5
1312sseli 3336 . . . 4
14 0re 9083 . . . . 5
1514, 14axlowdimlem5 25877 . . . 4
1613, 15syl 16 . . 3
17 1re 9082 . . . . 5
1817, 14axlowdimlem5 25877 . . . 4
1913, 18syl 16 . . 3
2014, 17axlowdimlem5 25877 . . . 4
2113, 20syl 16 . . 3
22 eqid 2435 . . . 4
2322axlowdimlem15 25887 . . 3
24 eqid 2435 . . . . . 6
25 eqid 2435 . . . . . 6
26 eqid 2435 . . . . . 6
2724, 25, 26, 14, 14axlowdimlem17 25889 . . . . 5 Cgr
28 eqid 2435 . . . . . 6
2924, 25, 28, 17, 14axlowdimlem17 25889 . . . . 5 Cgr
30 eqid 2435 . . . . . 6
3124, 25, 30, 14, 17axlowdimlem17 25889 . . . . 5 Cgr
32 1z 10303 . . . . . . . . . . . . . . 15
3332a1i 11 . . . . . . . . . . . . . 14
34 peano2zm 10312 . . . . . . . . . . . . . . 15
35343ad2ant2 979 . . . . . . . . . . . . . 14
36 2m1e1 10087 . . . . . . . . . . . . . . 15
37 zre 10278 . . . . . . . . . . . . . . . . . . . 20
38 letr 9159 . . . . . . . . . . . . . . . . . . . . 21
391, 2, 38mp3an12 1269 . . . . . . . . . . . . . . . . . . . 20
4037, 39syl 16 . . . . . . . . . . . . . . . . . . 19
414, 40mpani 658 . . . . . . . . . . . . . . . . . 18
4241imp 419 . . . . . . . . . . . . . . . . 17
43423adant1 975 . . . . . . . . . . . . . . . 16
44373ad2ant2 979 . . . . . . . . . . . . . . . . 17
45 lesub1 9514 . . . . . . . . . . . . . . . . . 18
461, 17, 45mp3an13 1270 . . . . . . . . . . . . . . . . 17
4744, 46syl 16 . . . . . . . . . . . . . . . 16
4843, 47mpbid 202 . . . . . . . . . . . . . . 15
4936, 48syl5eqbrr 4238 . . . . . . . . . . . . . 14
5033, 35, 493jca 1134 . . . . . . . . . . . . 13
51 eluz2 10486 . . . . . . . . . . . . 13
52 eluz2 10486 . . . . . . . . . . . . 13
5350, 51, 523imtr4i 258 . . . . . . . . . . . 12
54 eluzfz1 11056 . . . . . . . . . . . 12
5553, 54syl 16 . . . . . . . . . . 11
5655adantr 452 . . . . . . . . . 10
57 eqeq1 2441 . . . . . . . . . . . 12
58 oveq1 6080 . . . . . . . . . . . . . . 15
5958opeq1d 3982 . . . . . . . . . . . . . 14
6059sneqd 3819 . . . . . . . . . . . . 13
6158sneqd 3819 . . . . . . . . . . . . . . 15
6261difeq2d 3457 . . . . . . . . . . . . . 14
6362xpeq1d 4893 . . . . . . . . . . . . 13
6460, 63uneq12d 3494 . . . . . . . . . . . 12
6557, 64ifbieq2d 3751 . . . . . . . . . . 11
66 snex 4397 . . . . . . . . . . . . 13
67 ovex 6098 . . . . . . . . . . . . . . 15
68 difexg 4343 . . . . . . . . . . . . . . 15
6967, 68ax-mp 8 . . . . . . . . . . . . . 14
70 snex 4397 . . . . . . . . . . . . . 14
7169, 70xpex 4982 . . . . . . . . . . . . 13
7266, 71unex 4699 . . . . . . . . . . . 12
73 snex 4397 . . . . . . . . . . . . 13
74 difexg 4343 . . . . . . . . . . . . . . 15
7567, 74ax-mp 8 . . . . . . . . . . . . . 14
7675, 70xpex 4982 . . . . . . . . . . . . 13
7773, 76unex 4699 . . . . . . . . . . . 12
7872, 77ifex 3789 . . . . . . . . . . 11
7965, 22, 78fvmpt 5798 . . . . . . . . . 10
8056, 79syl 16 . . . . . . . . 9
81 eqid 2435 . . . . . . . . . 10
82 iftrue 3737 . . . . . . . . . 10
8381, 82ax-mp 8 . . . . . . . . 9
8480, 83syl6eq 2483 . . . . . . . 8
8584opeq1d 3982 . . . . . . 7
86 2nn 10125 . . . . . . . . . . . . . 14
87 nnuz 10513 . . . . . . . . . . . . . 14
8886, 87eleqtri 2507 . . . . . . . . . . . . 13
89 fzss1 11083 . . . . . . . . . . . . 13
9088, 89ax-mp 8 . . . . . . . . . . . 12
9190sseli 3336 . . . . . . . . . . 11
9291adantl 453 . . . . . . . . . 10
93 eqeq1 2441 . . . . . . . . . . . 12
94 oveq1 6080 . . . . . . . . . . . . . . 15
9594opeq1d 3982 . . . . . . . . . . . . . 14
9695sneqd 3819 . . . . . . . . . . . . 13
9794sneqd 3819 . . . . . . . . . . . . . . 15
9897difeq2d 3457 . . . . . . . . . . . . . 14
9998xpeq1d 4893 . . . . . . . . . . . . 13
10096, 99uneq12d 3494 . . . . . . . . . . . 12
10193, 100ifbieq2d 3751 . . . . . . . . . . 11
102 snex 4397 . . . . . . . . . . . . 13
103 difexg 4343 . . . . . . . . . . . . . . 15
10467, 103ax-mp 8 . . . . . . . . . . . . . 14
105104, 70xpex 4982 . . . . . . . . . . . . 13
106102, 105unex 4699 . . . . . . . . . . . 12
10772, 106ifex 3789 . . . . . . . . . . 11
108101, 22, 107fvmpt 5798 . . . . . . . . . 10
10992, 108syl 16 . . . . . . . . 9
110 1lt2 10134 . . . . . . . . . . . . . . . 16
11117, 1ltnlei 9186 . . . . . . . . . . . . . . . 16
112110, 111mpbi 200 . . . . . . . . . . . . . . 15
113112intnanr 882 . . . . . . . . . . . . . 14
114 eluzelz 10488 . . . . . . . . . . . . . . . 16
115114, 34syl 16 . . . . . . . . . . . . . . 15
116 elfz 11041 . . . . . . . . . . . . . . . 16
11732, 5, 116mp3an12 1269 . . . . . . . . . . . . . . 15
118115, 117syl 16 . . . . . . . . . . . . . 14
119113, 118mtbiri 295 . . . . . . . . . . . . 13
120 eleq1 2495 . . . . . . . . . . . . . 14
121120notbid 286 . . . . . . . . . . . . 13
122119, 121syl5ibrcom 214 . . . . . . . . . . . 12
123122con2d 109 . . . . . . . . . . 11
124123imp 419 . . . . . . . . . 10
125 iffalse 3738 . . . . . . . . . 10
126124, 125syl 16 . . . . . . . . 9
127109, 126eqtrd 2467 . . . . . . . 8
128127opeq1d 3982 . . . . . . 7
12985, 128breq12d 4217 . . . . . 6 Cgr Cgr
13084opeq1d 3982 . . . . . . 7
131127opeq1d 3982 . . . . . . 7
132130, 131breq12d 4217 . . . . . 6 Cgr Cgr
13355, 79syl 16 . . . . . . . . . 10
134133, 83syl6eq 2483 . . . . . . . . 9
135134opeq1d 3982 . . . . . . . 8
136135adantr 452 . . . . . . 7
137127opeq1d 3982 . . . . . . 7
138136, 137breq12d 4217 . . . . . 6 Cgr Cgr
139129, 132, 1383anbi123d 1254 . . . . 5 Cgr Cgr Cgr Cgr Cgr Cgr
14027, 29, 31, 139mpbir3and 1137 . . . 4 Cgr Cgr Cgr
141140ralrimiva 2781 . . 3 Cgr Cgr Cgr
14226, 28, 30axlowdimlem6 25878 . . . 4
14313, 142syl 16 . . 3
144 opeq2 3977 . . . . . . . 8
145 opeq2 3977 . . . . . . . 8
146144, 145breq12d 4217 . . . . . . 7 Cgr Cgr
1471463anbi1d 1258 . . . . . 6 Cgr Cgr Cgr Cgr Cgr Cgr
148147ralbidv 2717 . . . . 5 Cgr Cgr Cgr Cgr Cgr Cgr
149 breq1 4207 . . . . . . 7
150 opeq2 3977 . . . . . . . 8
151150breq2d 4216 . . . . . . 7
152 opeq1 3976 . . . . . . . 8
153152breq2d 4216 . . . . . . 7
154149, 151, 1533orbi123d 1253 . . . . . 6
155154notbid 286 . . . . 5
156148, 1553anbi23d 1257 . . . 4 Cgr Cgr Cgr Cgr Cgr Cgr