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

Theorem axlowdim 24589
 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 9815 . . . . . . . 8
2 3re 9817 . . . . . . . 8
3 2lt3 9887 . . . . . . . 8
41, 2, 3ltleii 8941 . . . . . . 7
5 2z 10054 . . . . . . . 8
6 3nn 9878 . . . . . . . . 9
76nnzi 10047 . . . . . . . 8
8 eluz 10241 . . . . . . . 8
95, 7, 8mp2an 653 . . . . . . 7
104, 9mpbir 200 . . . . . 6
11 uzss 10248 . . . . . 6
1210, 11ax-mp 8 . . . . 5
1312sseli 3176 . . . 4
14 0re 8838 . . . . 5
1514, 14axlowdimlem5 24574 . . . 4
1613, 15syl 15 . . 3
17 1re 8837 . . . . 5
1817, 14axlowdimlem5 24574 . . . 4
1913, 18syl 15 . . 3
2014, 17axlowdimlem5 24574 . . . 4
2113, 20syl 15 . . 3
22 eqid 2283 . . . 4
2322axlowdimlem15 24584 . . 3
24 eqid 2283 . . . . . 6
25 eqid 2283 . . . . . 6
26 eqid 2283 . . . . . 6
2724, 25, 26, 14, 14axlowdimlem17 24586 . . . . 5 Cgr
28 eqid 2283 . . . . . 6
2924, 25, 28, 17, 14axlowdimlem17 24586 . . . . 5 Cgr
30 eqid 2283 . . . . . 6
3124, 25, 30, 14, 17axlowdimlem17 24586 . . . . 5 Cgr
32 1z 10053 . . . . . . . . . . . . . . 15
3332a1i 10 . . . . . . . . . . . . . 14
34 peano2zm 10062 . . . . . . . . . . . . . . 15
35343ad2ant2 977 . . . . . . . . . . . . . 14
36 2cn 9816 . . . . . . . . . . . . . . . 16
37 ax-1cn 8795 . . . . . . . . . . . . . . . 16
38 1p1e2 9840 . . . . . . . . . . . . . . . 16
3936, 37, 37, 38subaddrii 9135 . . . . . . . . . . . . . . 15
40 zre 10028 . . . . . . . . . . . . . . . . . . . 20
41 letr 8914 . . . . . . . . . . . . . . . . . . . . 21
421, 2, 41mp3an12 1267 . . . . . . . . . . . . . . . . . . . 20
4340, 42syl 15 . . . . . . . . . . . . . . . . . . 19
444, 43mpani 657 . . . . . . . . . . . . . . . . . 18
4544imp 418 . . . . . . . . . . . . . . . . 17
46453adant1 973 . . . . . . . . . . . . . . . 16
47403ad2ant2 977 . . . . . . . . . . . . . . . . 17
48 lesub1 9268 . . . . . . . . . . . . . . . . . 18
491, 17, 48mp3an13 1268 . . . . . . . . . . . . . . . . 17
5047, 49syl 15 . . . . . . . . . . . . . . . 16
5146, 50mpbid 201 . . . . . . . . . . . . . . 15
5239, 51syl5eqbrr 4057 . . . . . . . . . . . . . 14
5333, 35, 523jca 1132 . . . . . . . . . . . . 13
54 eluz2 10236 . . . . . . . . . . . . 13
55 eluz2 10236 . . . . . . . . . . . . 13
5653, 54, 553imtr4i 257 . . . . . . . . . . . 12
57 eluzfz1 10803 . . . . . . . . . . . 12
5856, 57syl 15 . . . . . . . . . . 11
5958adantr 451 . . . . . . . . . 10
60 eqeq1 2289 . . . . . . . . . . . 12
61 oveq1 5865 . . . . . . . . . . . . . . 15
6261opeq1d 3802 . . . . . . . . . . . . . 14
6362sneqd 3653 . . . . . . . . . . . . 13
6461sneqd 3653 . . . . . . . . . . . . . . 15
6564difeq2d 3294 . . . . . . . . . . . . . 14
6665xpeq1d 4712 . . . . . . . . . . . . 13
6763, 66uneq12d 3330 . . . . . . . . . . . 12
6860, 67ifbieq2d 3585 . . . . . . . . . . 11
69 snex 4216 . . . . . . . . . . . . 13
70 ovex 5883 . . . . . . . . . . . . . . 15
71 difexg 4162 . . . . . . . . . . . . . . 15
7270, 71ax-mp 8 . . . . . . . . . . . . . 14
73 snex 4216 . . . . . . . . . . . . . 14
7472, 73xpex 4801 . . . . . . . . . . . . 13
7569, 74unex 4518 . . . . . . . . . . . 12
76 snex 4216 . . . . . . . . . . . . 13
77 difexg 4162 . . . . . . . . . . . . . . 15
7870, 77ax-mp 8 . . . . . . . . . . . . . 14
7978, 73xpex 4801 . . . . . . . . . . . . 13
8076, 79unex 4518 . . . . . . . . . . . 12
8175, 80ifex 3623 . . . . . . . . . . 11
8268, 22, 81fvmpt 5602 . . . . . . . . . 10
8359, 82syl 15 . . . . . . . . 9
84 eqid 2283 . . . . . . . . . 10
85 iftrue 3571 . . . . . . . . . 10
8684, 85ax-mp 8 . . . . . . . . 9
8783, 86syl6eq 2331 . . . . . . . 8
8887opeq1d 3802 . . . . . . 7
89 2nn 9877 . . . . . . . . . . . . . 14
90 nnuz 10263 . . . . . . . . . . . . . 14
9189, 90eleqtri 2355 . . . . . . . . . . . . 13
92 fzss1 10830 . . . . . . . . . . . . 13
9391, 92ax-mp 8 . . . . . . . . . . . 12
9493sseli 3176 . . . . . . . . . . 11
9594adantl 452 . . . . . . . . . 10
96 eqeq1 2289 . . . . . . . . . . . 12
97 oveq1 5865 . . . . . . . . . . . . . . 15
9897opeq1d 3802 . . . . . . . . . . . . . 14
9998sneqd 3653 . . . . . . . . . . . . 13
10097sneqd 3653 . . . . . . . . . . . . . . 15
101100difeq2d 3294 . . . . . . . . . . . . . 14
102101xpeq1d 4712 . . . . . . . . . . . . 13
10399, 102uneq12d 3330 . . . . . . . . . . . 12
10496, 103ifbieq2d 3585 . . . . . . . . . . 11
105 snex 4216 . . . . . . . . . . . . 13
106 difexg 4162 . . . . . . . . . . . . . . 15
10770, 106ax-mp 8 . . . . . . . . . . . . . 14
108107, 73xpex 4801 . . . . . . . . . . . . 13
109105, 108unex 4518 . . . . . . . . . . . 12
11075, 109ifex 3623 . . . . . . . . . . 11
111104, 22, 110fvmpt 5602 . . . . . . . . . 10
11295, 111syl 15 . . . . . . . . 9
113 1lt2 9886 . . . . . . . . . . . . . . . 16
11417, 1ltnlei 8939 . . . . . . . . . . . . . . . 16
115113, 114mpbi 199 . . . . . . . . . . . . . . 15
116115intnanr 881 . . . . . . . . . . . . . 14
117 eluzelz 10238 . . . . . . . . . . . . . . . 16
118117, 34syl 15 . . . . . . . . . . . . . . 15
119 elfz 10788 . . . . . . . . . . . . . . . 16
12032, 5, 119mp3an12 1267 . . . . . . . . . . . . . . 15
121118, 120syl 15 . . . . . . . . . . . . . 14
122116, 121mtbiri 294 . . . . . . . . . . . . 13
123 eleq1 2343 . . . . . . . . . . . . . 14
124123notbid 285 . . . . . . . . . . . . 13
125122, 124syl5ibrcom 213 . . . . . . . . . . . 12
126125con2d 107 . . . . . . . . . . 11
127126imp 418 . . . . . . . . . 10
128 iffalse 3572 . . . . . . . . . 10
129127, 128syl 15 . . . . . . . . 9
130112, 129eqtrd 2315 . . . . . . . 8
131130opeq1d 3802 . . . . . . 7
13288, 131breq12d 4036 . . . . . 6 Cgr Cgr
13387opeq1d 3802 . . . . . . 7
134130opeq1d 3802 . . . . . . 7
135133, 134breq12d 4036 . . . . . 6 Cgr Cgr
13658, 82syl 15 . . . . . . . . . 10
137136, 86syl6eq 2331 . . . . . . . . 9
138137opeq1d 3802 . . . . . . . 8
139138adantr 451 . . . . . . 7
140130opeq1d 3802 . . . . . . 7
141139, 140breq12d 4036 . . . . . 6 Cgr Cgr
142132, 135, 1413anbi123d 1252 . . . . 5 Cgr Cgr Cgr Cgr Cgr Cgr
14327, 29, 31, 142mpbir3and 1135 . . . 4 Cgr Cgr Cgr
144143ralrimiva 2626 . . 3 Cgr Cgr Cgr
14526, 28, 30axlowdimlem6 24575 . . . 4
14613, 145syl 15 . . 3
147 opeq2 3797 . . . . . . . 8
148 opeq2 3797 . . . . . . . 8
149147, 148breq12d 4036 . . . . . . 7 Cgr Cgr
1501493anbi1d 1256 . . . . . 6 Cgr Cgr Cgr Cgr Cgr Cgr
151150ralbidv 2563 . . . . 5 Cgr Cgr Cgr Cgr Cgr Cgr
152 breq1 4026 . . . . . . 7
153 opeq2 3797 . . . . . . . 8
154153breq2d 4035 . . . . . . 7
155 opeq1 3796 . . . . . . . 8
156155breq2d 4035 . . . . . . 7
157152, 154, 1563orbi123d 1251 . . . . . 6
158157notbid 285 . . . . 5
159151, 1583anbi23d 1255 . . . 4 Cgr Cgr Cgr Cgr Cgr