Proof of Theorem cnreeu
Step | Hyp | Ref
| Expression |
1 | | oveq1 7150 |
. . . 4
⊢ ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) → ((𝑟 + (i · 𝑠)) + (i · (0 −ℝ
𝑠))) = ((𝑡 + (i · 𝑢)) + (i · (0 −ℝ
𝑠)))) |
2 | 1 | oveq2d 7159 |
. . 3
⊢ ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) → ((0 −ℝ 𝑡) + ((𝑟 + (i · 𝑠)) + (i · (0 −ℝ
𝑠)))) = ((0
−ℝ 𝑡) + ((𝑡 + (i · 𝑢)) + (i · (0 −ℝ
𝑠))))) |
3 | | cnreeu.r |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑟 ∈ ℝ) |
4 | 3 | recnd 10692 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑟 ∈ ℂ) |
5 | | ax-icn 10619 |
. . . . . . . . . . . 12
⊢ i ∈
ℂ |
6 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → i ∈
ℂ) |
7 | | cnreeu.s |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑠 ∈ ℝ) |
8 | 7 | recnd 10692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑠 ∈ ℂ) |
9 | 6, 8 | mulcld 10684 |
. . . . . . . . . 10
⊢ (𝜑 → (i · 𝑠) ∈
ℂ) |
10 | | rernegcl 39836 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ → (0
−ℝ 𝑠) ∈ ℝ) |
11 | 7, 10 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0
−ℝ 𝑠) ∈ ℝ) |
12 | 11 | recnd 10692 |
. . . . . . . . . . 11
⊢ (𝜑 → (0
−ℝ 𝑠) ∈ ℂ) |
13 | 6, 12 | mulcld 10684 |
. . . . . . . . . 10
⊢ (𝜑 → (i · (0
−ℝ 𝑠)) ∈ ℂ) |
14 | 4, 9, 13 | addassd 10686 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑟 + (i · 𝑠)) + (i · (0 −ℝ
𝑠))) = (𝑟 + ((i · 𝑠) + (i · (0 −ℝ
𝑠))))) |
15 | | renegid 39838 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ → (𝑠 + (0 −ℝ
𝑠)) = 0) |
16 | 7, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑠 + (0 −ℝ 𝑠)) = 0) |
17 | 16 | oveq2d 7159 |
. . . . . . . . . . 11
⊢ (𝜑 → (i · (𝑠 + (0 −ℝ
𝑠))) = (i ·
0)) |
18 | 6, 8, 12 | adddid 10688 |
. . . . . . . . . . 11
⊢ (𝜑 → (i · (𝑠 + (0 −ℝ
𝑠))) = ((i · 𝑠) + (i · (0
−ℝ 𝑠)))) |
19 | | sn-it0e0 39879 |
. . . . . . . . . . . 12
⊢ (i
· 0) = 0 |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (i · 0) =
0) |
21 | 17, 18, 20 | 3eqtr3d 2802 |
. . . . . . . . . 10
⊢ (𝜑 → ((i · 𝑠) + (i · (0
−ℝ 𝑠))) = 0) |
22 | 21 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝜑 → (𝑟 + ((i · 𝑠) + (i · (0 −ℝ
𝑠)))) = (𝑟 + 0)) |
23 | | readdid1 39874 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ → (𝑟 + 0) = 𝑟) |
24 | 3, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑟 + 0) = 𝑟) |
25 | 14, 22, 24 | 3eqtrd 2798 |
. . . . . . . 8
⊢ (𝜑 → ((𝑟 + (i · 𝑠)) + (i · (0 −ℝ
𝑠))) = 𝑟) |
26 | 25 | oveq2d 7159 |
. . . . . . 7
⊢ (𝜑 → ((0
−ℝ 𝑡) + ((𝑟 + (i · 𝑠)) + (i · (0 −ℝ
𝑠)))) = ((0
−ℝ 𝑡) + 𝑟)) |
27 | | cnreeu.t |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑡 ∈ ℝ) |
28 | | rernegcl 39836 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ → (0
−ℝ 𝑡) ∈ ℝ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0
−ℝ 𝑡) ∈ ℝ) |
30 | 29 | recnd 10692 |
. . . . . . . . . 10
⊢ (𝜑 → (0
−ℝ 𝑡) ∈ ℂ) |
31 | 27 | recnd 10692 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑡 ∈ ℂ) |
32 | | cnreeu.u |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑢 ∈ ℝ) |
33 | 32 | recnd 10692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑢 ∈ ℂ) |
34 | 6, 33 | mulcld 10684 |
. . . . . . . . . 10
⊢ (𝜑 → (i · 𝑢) ∈
ℂ) |
35 | 30, 31, 34 | addassd 10686 |
. . . . . . . . 9
⊢ (𝜑 → (((0
−ℝ 𝑡) + 𝑡) + (i · 𝑢)) = ((0 −ℝ 𝑡) + (𝑡 + (i · 𝑢)))) |
36 | 35 | oveq1d 7158 |
. . . . . . . 8
⊢ (𝜑 → ((((0
−ℝ 𝑡) + 𝑡) + (i · 𝑢)) + (i · (0 −ℝ
𝑠))) = (((0
−ℝ 𝑡) + (𝑡 + (i · 𝑢))) + (i · (0
−ℝ 𝑠)))) |
37 | | sn-addid2 39869 |
. . . . . . . . . . 11
⊢ ((i
· 𝑢) ∈ ℂ
→ (0 + (i · 𝑢))
= (i · 𝑢)) |
38 | 34, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0 + (i · 𝑢)) = (i · 𝑢)) |
39 | 38 | oveq1d 7158 |
. . . . . . . . 9
⊢ (𝜑 → ((0 + (i · 𝑢)) + (i · (0
−ℝ 𝑠))) = ((i · 𝑢) + (i · (0 −ℝ
𝑠)))) |
40 | | renegid2 39878 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ → ((0
−ℝ 𝑡) + 𝑡) = 0) |
41 | 27, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0
−ℝ 𝑡) + 𝑡) = 0) |
42 | 41 | oveq1d 7158 |
. . . . . . . . . 10
⊢ (𝜑 → (((0
−ℝ 𝑡) + 𝑡) + (i · 𝑢)) = (0 + (i · 𝑢))) |
43 | 42 | oveq1d 7158 |
. . . . . . . . 9
⊢ (𝜑 → ((((0
−ℝ 𝑡) + 𝑡) + (i · 𝑢)) + (i · (0 −ℝ
𝑠))) = ((0 + (i ·
𝑢)) + (i · (0
−ℝ 𝑠)))) |
44 | 6, 33, 12 | adddid 10688 |
. . . . . . . . 9
⊢ (𝜑 → (i · (𝑢 + (0 −ℝ
𝑠))) = ((i · 𝑢) + (i · (0
−ℝ 𝑠)))) |
45 | 39, 43, 44 | 3eqtr4d 2804 |
. . . . . . . 8
⊢ (𝜑 → ((((0
−ℝ 𝑡) + 𝑡) + (i · 𝑢)) + (i · (0 −ℝ
𝑠))) = (i · (𝑢 + (0 −ℝ
𝑠)))) |
46 | 31, 34 | addcld 10683 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 + (i · 𝑢)) ∈ ℂ) |
47 | 30, 46, 13 | addassd 10686 |
. . . . . . . 8
⊢ (𝜑 → (((0
−ℝ 𝑡) + (𝑡 + (i · 𝑢))) + (i · (0
−ℝ 𝑠))) = ((0 −ℝ 𝑡) + ((𝑡 + (i · 𝑢)) + (i · (0 −ℝ
𝑠))))) |
48 | 36, 45, 47 | 3eqtr3rd 2803 |
. . . . . . 7
⊢ (𝜑 → ((0
−ℝ 𝑡) + ((𝑡 + (i · 𝑢)) + (i · (0 −ℝ
𝑠)))) = (i · (𝑢 + (0 −ℝ
𝑠)))) |
49 | 26, 48 | eqeq12d 2775 |
. . . . . 6
⊢ (𝜑 → (((0
−ℝ 𝑡) + ((𝑟 + (i · 𝑠)) + (i · (0 −ℝ
𝑠)))) = ((0
−ℝ 𝑡) + ((𝑡 + (i · 𝑢)) + (i · (0 −ℝ
𝑠)))) ↔ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠))))) |
50 | 49 | biimpa 481 |
. . . . 5
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + ((𝑟 + (i · 𝑠)) + (i · (0 −ℝ
𝑠)))) = ((0
−ℝ 𝑡) + ((𝑡 + (i · 𝑢)) + (i · (0 −ℝ
𝑠))))) → ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) |
51 | | simpr 489 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) |
52 | 32 | adantr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → 𝑢 ∈ ℝ) |
53 | 11 | adantr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → (0
−ℝ 𝑠) ∈ ℝ) |
54 | 52, 53 | readdcld 10693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → (𝑢 + (0 −ℝ 𝑠)) ∈
ℝ) |
55 | 29 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → (0
−ℝ 𝑡) ∈ ℝ) |
56 | 3 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → 𝑟 ∈ ℝ) |
57 | 55, 56 | readdcld 10693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → ((0
−ℝ 𝑡) + 𝑟) ∈ ℝ) |
58 | 51, 57 | eqeltrrd 2852 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → (i · (𝑢 + (0 −ℝ
𝑠))) ∈
ℝ) |
59 | | itrere 39918 |
. . . . . . . . . . 11
⊢ ((𝑢 + (0 −ℝ
𝑠)) ∈ ℝ →
((i · (𝑢 + (0
−ℝ 𝑠))) ∈ ℝ ↔ (𝑢 + (0 −ℝ 𝑠)) = 0)) |
60 | 59 | biimpa 481 |
. . . . . . . . . 10
⊢ (((𝑢 + (0 −ℝ
𝑠)) ∈ ℝ ∧ (i
· (𝑢 + (0
−ℝ 𝑠))) ∈ ℝ) → (𝑢 + (0 −ℝ
𝑠)) = 0) |
61 | 54, 58, 60 | syl2anc 588 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → (𝑢 + (0 −ℝ 𝑠)) = 0) |
62 | 61 | oveq2d 7159 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → (i · (𝑢 + (0 −ℝ
𝑠))) = (i ·
0)) |
63 | 19 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → (i · 0) =
0) |
64 | 51, 62, 63 | 3eqtrd 2798 |
. . . . . . 7
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → ((0
−ℝ 𝑡) + 𝑟) = 0) |
65 | | oveq2 7151 |
. . . . . . . . 9
⊢ (((0
−ℝ 𝑡) + 𝑟) = 0 → (𝑡 + ((0 −ℝ 𝑡) + 𝑟)) = (𝑡 + 0)) |
66 | 65 | adantl 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → (𝑡 + ((0 −ℝ 𝑡) + 𝑟)) = (𝑡 + 0)) |
67 | | renegid 39838 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ → (𝑡 + (0 −ℝ
𝑡)) = 0) |
68 | 27, 67 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 + (0 −ℝ 𝑡)) = 0) |
69 | 68 | adantr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → (𝑡 + (0 −ℝ 𝑡)) = 0) |
70 | 69 | oveq1d 7158 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → ((𝑡 + (0 −ℝ 𝑡)) + 𝑟) = (0 + 𝑟)) |
71 | 31 | adantr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → 𝑡 ∈ ℂ) |
72 | 30 | adantr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → (0 −ℝ
𝑡) ∈
ℂ) |
73 | 4 | adantr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → 𝑟 ∈ ℂ) |
74 | 71, 72, 73 | addassd 10686 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → ((𝑡 + (0 −ℝ 𝑡)) + 𝑟) = (𝑡 + ((0 −ℝ 𝑡) + 𝑟))) |
75 | | readdid2 39868 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ → (0 +
𝑟) = 𝑟) |
76 | 3, 75 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0 + 𝑟) = 𝑟) |
77 | 76 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → (0 + 𝑟) = 𝑟) |
78 | 70, 74, 77 | 3eqtr3d 2802 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → (𝑡 + ((0 −ℝ 𝑡) + 𝑟)) = 𝑟) |
79 | 27 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → 𝑡 ∈ ℝ) |
80 | | readdid1 39874 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ → (𝑡 + 0) = 𝑡) |
81 | 79, 80 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → (𝑡 + 0) = 𝑡) |
82 | 66, 78, 81 | 3eqtr3d 2802 |
. . . . . . 7
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = 0) → 𝑟 = 𝑡) |
83 | 64, 82 | syldan 595 |
. . . . . 6
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → 𝑟 = 𝑡) |
84 | 33, 12, 8 | addassd 10686 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑢 + (0 −ℝ 𝑠)) + 𝑠) = (𝑢 + ((0 −ℝ 𝑠) + 𝑠))) |
85 | | renegid2 39878 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℝ → ((0
−ℝ 𝑠) + 𝑠) = 0) |
86 | 7, 85 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0
−ℝ 𝑠) + 𝑠) = 0) |
87 | 86 | oveq2d 7159 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑢 + ((0 −ℝ 𝑠) + 𝑠)) = (𝑢 + 0)) |
88 | | readdid1 39874 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ℝ → (𝑢 + 0) = 𝑢) |
89 | 32, 88 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑢 + 0) = 𝑢) |
90 | 84, 87, 89 | 3eqtrd 2798 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑢 + (0 −ℝ 𝑠)) + 𝑠) = 𝑢) |
91 | | oveq1 7150 |
. . . . . . . . 9
⊢ ((𝑢 + (0 −ℝ
𝑠)) = 0 → ((𝑢 + (0 −ℝ
𝑠)) + 𝑠) = (0 + 𝑠)) |
92 | 90, 91 | sylan9req 2815 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 + (0 −ℝ 𝑠)) = 0) → 𝑢 = (0 + 𝑠)) |
93 | | readdid2 39868 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ℝ → (0 +
𝑠) = 𝑠) |
94 | 7, 93 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0 + 𝑠) = 𝑠) |
95 | 94 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 + (0 −ℝ 𝑠)) = 0) → (0 + 𝑠) = 𝑠) |
96 | 92, 95 | eqtr2d 2795 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 + (0 −ℝ 𝑠)) = 0) → 𝑠 = 𝑢) |
97 | 61, 96 | syldan 595 |
. . . . . 6
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → 𝑠 = 𝑢) |
98 | 83, 97 | jca 516 |
. . . . 5
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + 𝑟) = (i · (𝑢 + (0 −ℝ 𝑠)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)) |
99 | 50, 98 | syldan 595 |
. . . 4
⊢ ((𝜑 ∧ ((0
−ℝ 𝑡) + ((𝑟 + (i · 𝑠)) + (i · (0 −ℝ
𝑠)))) = ((0
−ℝ 𝑡) + ((𝑡 + (i · 𝑢)) + (i · (0 −ℝ
𝑠))))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)) |
100 | 99 | ex 417 |
. . 3
⊢ (𝜑 → (((0
−ℝ 𝑡) + ((𝑟 + (i · 𝑠)) + (i · (0 −ℝ
𝑠)))) = ((0
−ℝ 𝑡) + ((𝑡 + (i · 𝑢)) + (i · (0 −ℝ
𝑠)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))) |
101 | 2, 100 | syl5 34 |
. 2
⊢ (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))) |
102 | | id 22 |
. . 3
⊢ (𝑟 = 𝑡 → 𝑟 = 𝑡) |
103 | | oveq2 7151 |
. . 3
⊢ (𝑠 = 𝑢 → (i · 𝑠) = (i · 𝑢)) |
104 | 102, 103 | oveqan12d 7162 |
. 2
⊢ ((𝑟 = 𝑡 ∧ 𝑠 = 𝑢) → (𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢))) |
105 | 101, 104 | impbid1 228 |
1
⊢ (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) ↔ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))) |