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

Theorem avril1 14464
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 2906 . . . . . . . . . 10
32abeq2i 2019 . . . . . . . . 9
43con2bii 321 . . . . . . . 8
51, 4mpbi 197 . . . . . . 7
6 eleq1 1977 . . . . . . 7
75, 6mtbii 291 . . . . . 6
87vtocleg 2388 . . . . 5
9 elex 2334 . . . . . 6
109con3i 125 . . . . 5
118, 10pm2.61i 154 . . . 4
12 df-br 3384 . . . . 5
13 0cn 7310 . . . . . . . 8
1413mulid1i 7312 . . . . . . 7
1514opeq2i 3212 . . . . . 6
1615eleq1i 1980 . . . . 5
1712, 16bitri 238 . . . 4
1811, 17mtbir 288 . . 3
1918intnan 840 . 2
20 df-i 7221 . . . . . . . 8
2120fveq1i 4736 . . . . . . 7
22 df-fv 4049 . . . . . . 7
2321, 22eqtri 1938 . . . . . 6
2423breq2i 3391 . . . . 5
25 df-r 7222 . . . . . . 7
26 sseq2 2679 . . . . . . . . 9
2726abbidv 2026 . . . . . . . 8
28 df-pw 3072 . . . . . . . 8
29 df-pw 3072 . . . . . . . 8
3027, 28, 293eqtr4g 1974 . . . . . . 7
3125, 30ax-mp 8 . . . . . 6
3231breqi 3389 . . . . 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 2326   wss 2636  c0 2904  cpw 3070  csn 3083  cop 3086  cuni 3233   class class class wbr 3383   cxp 4019  cima 4024  cfv 4033  (class class class)co 5002  cnr 6962  c0r 6963  c1r 6964  cr 7211  cc0 7212  c1 7213  ci 7214   cmul 7217
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 7266  ax-1cn 7267  ax-icn 7268  ax-addcl 7269  ax-mulcl 7271  ax-mulcom 7273  ax-mulass 7275  ax-distr 7276  ax-i2m1 7277  ax-1rid 7279  ax-cnre 7282
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-v 2328  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-nul 2905  df-pw 3072  df-sn 3089  df-pr 3090  df-op 3092  df-uni 3234  df-br 3384  df-opab 3438  df-xp 4035  df-cnv 4037  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fv 4049  df-ov 5004  df-i 7221  df-r 7222
Copyright terms: Public domain