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

Theorem avril1 15865
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 1657 . . . . . . . 8
2 dfnul2 3027 . . . . . . . . . 10
32abeq2i 2131 . . . . . . . . 9
43con2bii 321 . . . . . . . 8
51, 4mpbi 197 . . . . . . 7
6 eleq1 2089 . . . . . . 7
75, 6mtbii 291 . . . . . 6
87vtocleg 2502 . . . . 5
9 elex 2448 . . . . . 6
109con3i 125 . . . . 5
118, 10pm2.61i 154 . . . 4
12 df-br 3532 . . . . 5
13 0cn 8007 . . . . . . . 8
1413mulid1i 8009 . . . . . . 7
1514opeq2i 3352 . . . . . 6
1615eleq1i 2092 . . . . 5
1712, 16bitri 238 . . . 4
1811, 17mtbir 288 . . 3
1918intnan 840 . 2
20 df-i 7917 . . . . . . . 8
2120fveq1i 4911 . . . . . . 7
22 df-fv 4200 . . . . . . 7
2321, 22eqtri 2050 . . . . . 6
2423breq2i 3539 . . . . 5
25 df-r 7918 . . . . . . 7
26 sseq2 2793 . . . . . . . . 9
2726abbidv 2138 . . . . . . . 8
28 df-pw 3196 . . . . . . . 8
29 df-pw 3196 . . . . . . . 8
3027, 28, 293eqtr4g 2086 . . . . . . 7
3125, 30ax-mp 8 . . . . . 6
3231breqi 3537 . . . . 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 1526   wcel 1528  cab 2017  cvv 2440   wss 2750  c0 3025  cpw 3194  csn 3208  cop 3211  cuni 3374   class class class wbr 3531   cxp 4170  cima 4175  cfv 4184  (class class class)co 5206  cnr 7658  c0r 7659  c1r 7660  cr 7907  cc0 7908  c1 7909  ci 7910   cmul 7913
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-resscn 7962  ax-1cn 7963  ax-icn 7964  ax-addcl 7965  ax-mulcl 7967  ax-mulcom 7969  ax-mulass 7971  ax-distr 7972  ax-i2m1 7973  ax-1rid 7975  ax-cnre 7978
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1448  df-sb 1703  df-clab 2018  df-cleq 2023  df-clel 2026  df-ral 2243  df-rex 2244  df-rab 2246  df-v 2442  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-nul 3026  df-if 3135  df-pw 3196  df-sn 3214  df-pr 3215  df-op 3217  df-uni 3375  df-br 3532  df-opab 3585  df-xp 4186  df-cnv 4188  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fv 4200  df-ov 5208  df-i 7917  df-r 7918
Copyright terms: Public domain