![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > inelr | GIF version |
Description: The imaginary unit i is not a real number. (Contributed by NM, 6-May-1999.) |
Ref | Expression |
---|---|
inelr | ⊢ ¬ i ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ine0 8376 | . . 3 ⊢ i ≠ 0 | |
2 | 1 | neii 2362 | . 2 ⊢ ¬ i = 0 |
3 | 0lt1 8109 | . . . . . 6 ⊢ 0 < 1 | |
4 | 0re 7982 | . . . . . . 7 ⊢ 0 ∈ ℝ | |
5 | 1re 7981 | . . . . . . 7 ⊢ 1 ∈ ℝ | |
6 | 4, 5 | ltnsymi 8082 | . . . . . 6 ⊢ (0 < 1 → ¬ 1 < 0) |
7 | 3, 6 | ax-mp 5 | . . . . 5 ⊢ ¬ 1 < 0 |
8 | ixi 8565 | . . . . . . . 8 ⊢ (i · i) = -1 | |
9 | 5 | renegcli 8244 | . . . . . . . 8 ⊢ -1 ∈ ℝ |
10 | 8, 9 | eqeltri 2262 | . . . . . . 7 ⊢ (i · i) ∈ ℝ |
11 | 4, 10, 5 | ltadd1i 8484 | . . . . . 6 ⊢ (0 < (i · i) ↔ (0 + 1) < ((i · i) + 1)) |
12 | ax-1cn 7929 | . . . . . . . 8 ⊢ 1 ∈ ℂ | |
13 | 12 | addid2i 8125 | . . . . . . 7 ⊢ (0 + 1) = 1 |
14 | ax-i2m1 7941 | . . . . . . 7 ⊢ ((i · i) + 1) = 0 | |
15 | 13, 14 | breq12i 4027 | . . . . . 6 ⊢ ((0 + 1) < ((i · i) + 1) ↔ 1 < 0) |
16 | 11, 15 | bitri 184 | . . . . 5 ⊢ (0 < (i · i) ↔ 1 < 0) |
17 | 7, 16 | mtbir 672 | . . . 4 ⊢ ¬ 0 < (i · i) |
18 | mullt0 8462 | . . . . . 6 ⊢ (((i ∈ ℝ ∧ i < 0) ∧ (i ∈ ℝ ∧ i < 0)) → 0 < (i · i)) | |
19 | 18 | anidms 397 | . . . . 5 ⊢ ((i ∈ ℝ ∧ i < 0) → 0 < (i · i)) |
20 | 19 | ex 115 | . . . 4 ⊢ (i ∈ ℝ → (i < 0 → 0 < (i · i))) |
21 | 17, 20 | mtoi 665 | . . 3 ⊢ (i ∈ ℝ → ¬ i < 0) |
22 | mulgt0 8057 | . . . . . 6 ⊢ (((i ∈ ℝ ∧ 0 < i) ∧ (i ∈ ℝ ∧ 0 < i)) → 0 < (i · i)) | |
23 | 22 | anidms 397 | . . . . 5 ⊢ ((i ∈ ℝ ∧ 0 < i) → 0 < (i · i)) |
24 | 23 | ex 115 | . . . 4 ⊢ (i ∈ ℝ → (0 < i → 0 < (i · i))) |
25 | 17, 24 | mtoi 665 | . . 3 ⊢ (i ∈ ℝ → ¬ 0 < i) |
26 | lttri3 8062 | . . . 4 ⊢ ((i ∈ ℝ ∧ 0 ∈ ℝ) → (i = 0 ↔ (¬ i < 0 ∧ ¬ 0 < i))) | |
27 | 4, 26 | mpan2 425 | . . 3 ⊢ (i ∈ ℝ → (i = 0 ↔ (¬ i < 0 ∧ ¬ 0 < i))) |
28 | 21, 25, 27 | mpbir2and 946 | . 2 ⊢ (i ∈ ℝ → i = 0) |
29 | 2, 28 | mto 663 | 1 ⊢ ¬ i ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 104 ↔ wb 105 = wceq 1364 ∈ wcel 2160 class class class wbr 4018 (class class class)co 5892 ℝcr 7835 0cc0 7836 1c1 7837 ici 7838 + caddc 7839 · cmul 7841 < clt 8017 -cneg 8154 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4189 ax-pr 4224 ax-un 4448 ax-setind 4551 ax-cnex 7927 ax-resscn 7928 ax-1cn 7929 ax-1re 7930 ax-icn 7931 ax-addcl 7932 ax-addrcl 7933 ax-mulcl 7934 ax-mulrcl 7935 ax-addcom 7936 ax-mulcom 7937 ax-addass 7938 ax-distr 7940 ax-i2m1 7941 ax-0lt1 7942 ax-0id 7944 ax-rnegex 7945 ax-cnre 7947 ax-pre-ltirr 7948 ax-pre-lttrn 7950 ax-pre-apti 7951 ax-pre-ltadd 7952 ax-pre-mulgt0 7953 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rab 2477 df-v 2754 df-sbc 2978 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-br 4019 df-opab 4080 df-id 4308 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-iota 5193 df-fun 5234 df-fv 5240 df-riota 5848 df-ov 5895 df-oprab 5896 df-mpo 5897 df-pnf 8019 df-mnf 8020 df-ltxr 8022 df-sub 8155 df-neg 8156 |
This theorem is referenced by: rimul 8567 |
Copyright terms: Public domain | W3C validator |