HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem avril1 14765
Description: Poisson d'Avril's Theorem. This theorem is noted for its Selbstdokumentieren property, which means, literally, "self-documenting" and recalls the principle of quidquid germanus dictum sit, altum viditur, often used in set theory. Starting with the seemingly simple yet profound fact that any object equals itself (proved by Tarski in 1965; see Lemma 6 of [Tarski] p. 68), we demonstrate that the power set of the real numbers, as a relation on the value of the imaginary unit, does not conjoin with an empty relation on the product of the additive and multiplicative identity elements, leading to this startling conclusion that has left even seasoned professional mathematicians scratching their heads. (Contributed by Prof. Loof Lirpa, 1-Apr-2005.)

A reply to skeptics can be found at http://us.metamath.org/mpegif/mmnotes.txt, under the 1-Apr-2006 entry.

Assertion
Ref Expression
avril1

Proof of Theorem avril1
StepHypRef Expression
1 equid 1545 . . . . . . . 8
2 dfnul2 2909 . . . . . . . . . 10
32abeq2i 2019 . . . . . . . . 9
43con2bii 321 . . . . . . . 8
51, 4mpbi 197 . . . . . . 7
6 eleq1 1977 . . . . . . 7
75, 6mtbii 291 . . . . . 6
87vtocleg 2389 . . . . 5
9 elex 2335 . . . . . 6
109con3i 125 . . . . 5
118, 10pm2.61i 154 . . . 4
12 df-br 3397 . . . . 5
13 0cn 7356 . . . . . . . 8
1413mulid1i 7358 . . . . . . 7
1514opeq2i 3224 . . . . . 6
1615eleq1i 1980 . . . . 5
1712, 16bitri 238 . . . 4
1811, 17mtbir 288 . . 3
1918intnan 840 . 2
20 df-i 7266 . . . . . . . 8
2120fveq1i 4762 . . . . . . 7
22 df-fv 4062 . . . . . . 7
2321, 22eqtri 1938 . . . . . 6
2423breq2i 3404 . . . . 5
25 df-r 7267 . . . . . . 7
26 sseq2 2680 . . . . . . . . 9
2726abbidv 2026 . . . . . . . 8
28 df-pw 3075 . . . . . . . 8
29 df-pw 3075 . . . . . . . 8
3027, 28, 293eqtr4g 1974 . . . . . . 7
3125, 30ax-mp 8 . . . . . 6
3231breqi 3402 . . . . 5
3324, 32bitri 238 . . . 4
3433anbi1i 672 . . 3
3534notbii 285 . 2
3619, 35mpbir 198 1
Colors of variables: wff set class
Syntax hints:   wn 3   wa 357   wceq 1414   wcel 1416  cab 1905  cvv 2327   wss 2637  c0 2907  cpw 3073  csn 3086  cop 3089  cuni 3246   class class class wbr 3396   cxp 4032  cima 4037  cfv 4046  (class class class)co 5032  cnr 7007  c0r 7008  c1r 7009  cr 7256  cc0 7257  c1 7258  ci 7259   cmul 7262
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-resscn 7311  ax-1cn 7312  ax-icn 7313  ax-addcl 7314  ax-mulcl 7316  ax-mulcom 7318  ax-mulass 7320  ax-distr 7321  ax-i2m1 7322  ax-1rid 7324  ax-cnre 7327
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1336  df-sb 1591  df-clab 1906  df-cleq 1911  df-clel 1914  df-ral 2131  df-rex 2132  df-rab 2134  df-v 2329  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-nul 2908  df-if 3015  df-pw 3075  df-sn 3092  df-pr 3093  df-op 3095  df-uni 3247  df-br 3397  df-opab 3450  df-xp 4048  df-cnv 4050  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fv 4062  df-ov 5034  df-i 7266  df-r 7267
Copyright terms: Public domain