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

Theorem avril1 13582
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 1544 . . . . . . . 8
2 dfnul2 2900 . . . . . . . . . 10
32abeq2i 2018 . . . . . . . . 9
43con2bii 320 . . . . . . . 8
51, 4mpbi 196 . . . . . . 7
6 eleq1 1976 . . . . . . 7
75, 6mtbii 290 . . . . . 6
87vtocleg 2384 . . . . 5
9 elex 2330 . . . . . 6
109con3i 124 . . . . 5
118, 10pm2.61i 153 . . . 4
12 df-br 3359 . . . . 5
13 0cn 7205 . . . . . . . 8
1413mulid1i 7207 . . . . . . 7
1514opeq2i 3196 . . . . . 6
1615eleq1i 1979 . . . . 5
1712, 16bitri 237 . . . 4
1811, 17mtbir 287 . . 3
1918intnan 839 . 2
20 df-i 7116 . . . . . . . 8
2120fveq1i 4691 . . . . . . 7
22 df-fv 4023 . . . . . . 7
2321, 22eqtri 1937 . . . . . 6
2423breq2i 3366 . . . . 5
25 df-r 7117 . . . . . . 7
26 sseq2 2675 . . . . . . . . 9
2726abbidv 2025 . . . . . . . 8
28 df-pw 3062 . . . . . . . 8
29 df-pw 3062 . . . . . . . 8
3027, 28, 293eqtr4g 1973 . . . . . . 7
3125, 30ax-mp 8 . . . . . 6
3231breqi 3364 . . . . 5
3324, 32bitri 237 . . . 4
3433anbi1i 671 . . 3
3534notbii 284 . 2
3619, 35mpbir 197 1
Colors of variables: wff set class
Syntax hints:   wn 3   wa 356   wceq 1413   wcel 1415  cab 1904  cvv 2322   wss 2632  c0 2898  cpw 3060  csn 3073  cop 3076  cuni 3213   class class class wbr 3358   cxp 3993  cima 3998  cfv 4007  (class class class)co 4944  cnr 6857  c0r 6858  c1r 6859  cr 7106  cc0 7107  c1 7108  ci 7109   cmul 7112
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-resscn 7161  ax-1cn 7162  ax-icn 7163  ax-addcl 7164  ax-mulcl 7166  ax-mulcom 7168  ax-mulass 7170  ax-distr 7171  ax-i2m1 7172  ax-1rid 7174  ax-cnre 7177
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3an 900  df-ex 1335  df-sb 1590  df-clab 1905  df-cleq 1910  df-clel 1913  df-ral 2129  df-rex 2130  df-v 2324  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-nul 2899  df-pw 3062  df-sn 3079  df-pr 3080  df-op 3082  df-uni 3214  df-br 3359  df-opab 3413  df-xp 4009  df-cnv 4011  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fv 4023  df-ov 4946  df-i 7116  df-r 7117
Copyright terms: Public domain