Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 6cn | Unicode version |
Description: The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
6cn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 6re 8929 | . 2 | |
2 | 1 | recni 7902 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2135 cc 7742 c6 8903 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-resscn 7836 ax-1re 7838 ax-addrcl 7841 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 df-2 8907 df-3 8908 df-4 8909 df-5 8910 df-6 8911 |
This theorem is referenced by: 7m1e6 8972 6p2e8 8997 6p3e9 8998 halfpm6th 9068 6p4e10 9384 6t2e12 9416 6t3e18 9417 6t5e30 9419 5recm6rec 9456 efi4p 11644 ef01bndlem 11683 cos01bnd 11685 3lcm2e6woprm 11997 6lcm4e12 11998 sincos6thpi 13310 sincos3rdpi 13311 ex-exp 13451 ex-bc 13453 ex-gcd 13455 |
Copyright terms: Public domain | W3C validator |