![]() |
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 7565 | . . 3 ⊢ i ≠ 0 | |
2 | 1 | neii 2248 | . 2 ⊢ ¬ i = 0 |
3 | 0lt1 7303 | . . . . . 6 ⊢ 0 < 1 | |
4 | 0re 7181 | . . . . . . 7 ⊢ 0 ∈ ℝ | |
5 | 1re 7180 | . . . . . . 7 ⊢ 1 ∈ ℝ | |
6 | 4, 5 | ltnsymi 7277 | . . . . . 6 ⊢ (0 < 1 → ¬ 1 < 0) |
7 | 3, 6 | ax-mp 7 | . . . . 5 ⊢ ¬ 1 < 0 |
8 | ixi 7750 | . . . . . . . 8 ⊢ (i · i) = -1 | |
9 | 5 | renegcli 7437 | . . . . . . . 8 ⊢ -1 ∈ ℝ |
10 | 8, 9 | eqeltri 2152 | . . . . . . 7 ⊢ (i · i) ∈ ℝ |
11 | 4, 10, 5 | ltadd1i 7670 | . . . . . 6 ⊢ (0 < (i · i) ↔ (0 + 1) < ((i · i) + 1)) |
12 | ax-1cn 7131 | . . . . . . . 8 ⊢ 1 ∈ ℂ | |
13 | 12 | addid2i 7318 | . . . . . . 7 ⊢ (0 + 1) = 1 |
14 | ax-i2m1 7143 | . . . . . . 7 ⊢ ((i · i) + 1) = 0 | |
15 | 13, 14 | breq12i 3802 | . . . . . 6 ⊢ ((0 + 1) < ((i · i) + 1) ↔ 1 < 0) |
16 | 11, 15 | bitri 182 | . . . . 5 ⊢ (0 < (i · i) ↔ 1 < 0) |
17 | 7, 16 | mtbir 629 | . . . 4 ⊢ ¬ 0 < (i · i) |
18 | mullt0 7651 | . . . . . 6 ⊢ (((i ∈ ℝ ∧ i < 0) ∧ (i ∈ ℝ ∧ i < 0)) → 0 < (i · i)) | |
19 | 18 | anidms 389 | . . . . 5 ⊢ ((i ∈ ℝ ∧ i < 0) → 0 < (i · i)) |
20 | 19 | ex 113 | . . . 4 ⊢ (i ∈ ℝ → (i < 0 → 0 < (i · i))) |
21 | 17, 20 | mtoi 623 | . . 3 ⊢ (i ∈ ℝ → ¬ i < 0) |
22 | mulgt0 7253 | . . . . . 6 ⊢ (((i ∈ ℝ ∧ 0 < i) ∧ (i ∈ ℝ ∧ 0 < i)) → 0 < (i · i)) | |
23 | 22 | anidms 389 | . . . . 5 ⊢ ((i ∈ ℝ ∧ 0 < i) → 0 < (i · i)) |
24 | 23 | ex 113 | . . . 4 ⊢ (i ∈ ℝ → (0 < i → 0 < (i · i))) |
25 | 17, 24 | mtoi 623 | . . 3 ⊢ (i ∈ ℝ → ¬ 0 < i) |
26 | lttri3 7258 | . . . 4 ⊢ ((i ∈ ℝ ∧ 0 ∈ ℝ) → (i = 0 ↔ (¬ i < 0 ∧ ¬ 0 < i))) | |
27 | 4, 26 | mpan2 416 | . . 3 ⊢ (i ∈ ℝ → (i = 0 ↔ (¬ i < 0 ∧ ¬ 0 < i))) |
28 | 21, 25, 27 | mpbir2and 886 | . 2 ⊢ (i ∈ ℝ → i = 0) |
29 | 2, 28 | mto 621 | 1 ⊢ ¬ i ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 102 ↔ wb 103 = wceq 1285 ∈ wcel 1434 class class class wbr 3793 (class class class)co 5543 ℝcr 7042 0cc0 7043 1c1 7044 ici 7045 + caddc 7046 · cmul 7048 < clt 7215 -cneg 7347 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-sep 3904 ax-pow 3956 ax-pr 3972 ax-un 4196 ax-setind 4288 ax-cnex 7129 ax-resscn 7130 ax-1cn 7131 ax-1re 7132 ax-icn 7133 ax-addcl 7134 ax-addrcl 7135 ax-mulcl 7136 ax-mulrcl 7137 ax-addcom 7138 ax-mulcom 7139 ax-addass 7140 ax-distr 7142 ax-i2m1 7143 ax-0lt1 7144 ax-0id 7146 ax-rnegex 7147 ax-cnre 7149 ax-pre-ltirr 7150 ax-pre-lttrn 7152 ax-pre-apti 7153 ax-pre-ltadd 7154 ax-pre-mulgt0 7155 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-nel 2341 df-ral 2354 df-rex 2355 df-reu 2356 df-rab 2358 df-v 2604 df-sbc 2817 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-pw 3392 df-sn 3412 df-pr 3413 df-op 3415 df-uni 3610 df-br 3794 df-opab 3848 df-id 4056 df-xp 4377 df-rel 4378 df-cnv 4379 df-co 4380 df-dm 4381 df-iota 4897 df-fun 4934 df-fv 4940 df-riota 5499 df-ov 5546 df-oprab 5547 df-mpt2 5548 df-pnf 7217 df-mnf 7218 df-ltxr 7220 df-sub 7348 df-neg 7349 |
This theorem is referenced by: rimul 7752 |
Copyright terms: Public domain | W3C validator |