Description: Poisson d'Avril's Theorem. This theorem is noted for its Selbstdokumentieren property, which means, literally, "self-documenting" and recalls the principle ofquidquid german dictum sit, altum viditur, often used in set theory. Starting with the seemingly simple yet profound fact that any object x 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) (Proof modification is discouraged.) (New usage is discouraged.)
A reply to skeptics can be found at mmnotes.txt , under the 1-Apr-2006 entry.
| Ref | Expression | ||
|---|---|---|---|
| Assertion | avril1 | |- -. ( A ~P RR ( _i ` 1 ) /\ F (/) ( 0 x. 1 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equid | |- x = x |
|
| 2 | dfnul2 | |- (/) = { x | -. x = x } |
|
| 3 | 2 | abeq2i | |- ( x e. (/) <-> -. x = x ) |
| 4 | 3 | con2bii | |- ( x = x <-> -. x e. (/) ) |
| 5 | 1 4 | mpbi | |- -. x e. (/) |
| 6 | eleq1 | |- ( x = <. F , 0 >. -> ( x e. (/) <-> <. F , 0 >. e. (/) ) ) |
|
| 7 | 5 6 | mtbii | |- ( x = <. F , 0 >. -> -. <. F , 0 >. e. (/) ) |
| 8 | 7 | vtocleg | |- ( <. F , 0 >. e. _V -> -. <. F , 0 >. e. (/) ) |
| 9 | elex | |- ( <. F , 0 >. e. (/) -> <. F , 0 >. e. _V ) |
|
| 10 | 9 | con3i | |- ( -. <. F , 0 >. e. _V -> -. <. F , 0 >. e. (/) ) |
| 11 | 8 10 | pm2.61i | |- -. <. F , 0 >. e. (/) |
| 12 | df-br | |- ( F (/) ( 0 x. 1 ) <-> <. F , ( 0 x. 1 ) >. e. (/) ) |
|
| 13 | 0cn | |- 0 e. CC |
|
| 14 | 13 | mulid1i | |- ( 0 x. 1 ) = 0 |
| 15 | 14 | opeq2i | |- <. F , ( 0 x. 1 ) >. = <. F , 0 >. |
| 16 | 15 | eleq1i | |- ( <. F , ( 0 x. 1 ) >. e. (/) <-> <. F , 0 >. e. (/) ) |
| 17 | 12 16 | bitri | |- ( F (/) ( 0 x. 1 ) <-> <. F , 0 >. e. (/) ) |
| 18 | 11 17 | mtbir | |- -. F (/) ( 0 x. 1 ) |
| 19 | 18 | intnan | |- -. ( A ~P ( R. X. { 0R } ) ( iota y 1 <. 0R , 1R >. y ) /\ F (/) ( 0 x. 1 ) ) |
| 20 | df-i | |- _i = <. 0R , 1R >. |
|
| 21 | 20 | fveq1i | |- ( _i ` 1 ) = ( <. 0R , 1R >. ` 1 ) |
| 22 | df-fv | |- ( <. 0R , 1R >. ` 1 ) = ( iota y 1 <. 0R , 1R >. y ) |
|
| 23 | 21 22 | eqtri | |- ( _i ` 1 ) = ( iota y 1 <. 0R , 1R >. y ) |
| 24 | 23 | breq2i | |- ( A ~P RR ( _i ` 1 ) <-> A ~P RR ( iota y 1 <. 0R , 1R >. y ) ) |
| 25 | df-r | |- RR = ( R. X. { 0R } ) |
|
| 26 | sseq2 | |- ( RR = ( R. X. { 0R } ) -> ( z C_ RR <-> z C_ ( R. X. { 0R } ) ) ) |
|
| 27 | 26 | abbidv | |- ( RR = ( R. X. { 0R } ) -> { z | z C_ RR } = { z | z C_ ( R. X. { 0R } ) } ) |
| 28 | df-pw | |- ~P RR = { z | z C_ RR } |
|
| 29 | df-pw | |- ~P ( R. X. { 0R } ) = { z | z C_ ( R. X. { 0R } ) } |
|
| 30 | 27 28 29 | 3eqtr4g | |- ( RR = ( R. X. { 0R } ) -> ~P RR = ~P ( R. X. { 0R } ) ) |
| 31 | 25 30 | ax-mp | |- ~P RR = ~P ( R. X. { 0R } ) |
| 32 | 31 | breqi | |- ( A ~P RR ( iota y 1 <. 0R , 1R >. y ) <-> A ~P ( R. X. { 0R } ) ( iota y 1 <. 0R , 1R >. y ) ) |
| 33 | 24 32 | bitri | |- ( A ~P RR ( _i ` 1 ) <-> A ~P ( R. X. { 0R } ) ( iota y 1 <. 0R , 1R >. y ) ) |
| 34 | 33 | anbi1i | |- ( ( A ~P RR ( _i ` 1 ) /\ F (/) ( 0 x. 1 ) ) <-> ( A ~P ( R. X. { 0R } ) ( iota y 1 <. 0R , 1R >. y ) /\ F (/) ( 0 x. 1 ) ) ) |
| 35 | 34 | notbii | |- ( -. ( A ~P RR ( _i ` 1 ) /\ F (/) ( 0 x. 1 ) ) <-> -. ( A ~P ( R. X. { 0R } ) ( iota y 1 <. 0R , 1R >. y ) /\ F (/) ( 0 x. 1 ) ) ) |
| 36 | 19 35 | mpbir | |- -. ( A ~P RR ( _i ` 1 ) /\ F (/) ( 0 x. 1 ) ) |