HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem recext 5684
Description: Existence of reciprocal of nonzero complex number. (Contributed by Eric Schmidt, 22-May-2007.)
Assertion
Ref Expression
recext |- ((A e. CC /\ A =/= 0) -> E.x e. CC (A x. x) = 1)
Distinct variable group:   x,A
Proof of Theorem recext
StepHypRef Expression
1 axcnre 5286 . . 3 |- (A e. CC -> E.a e. RR E.b e. RR A = (a + (i x. b)))
2 recextlem2 5683 . . . . . . . . 9 |- ((a e. RR /\ b e. RR /\ (a + (i x. b)) =/= 0) -> ((a x. a) + (b x. b)) =/= 0)
323expia 835 . . . . . . . 8 |- ((a e. RR /\ b e. RR) -> ((a + (i x. b)) =/= 0 -> ((a x. a) + (b x. b)) =/= 0))
4 axrrecex 5284 . . . . . . . . . . 11 |- ((((a x. a) + (b x. b)) e. RR /\ ((a x. a) + (b x. b)) =/= 0) -> E.y e. RR (((a x. a) + (b x. b)) x. y) = 1)
5 axaddrcl 5272 . . . . . . . . . . . 12 |- (((a x. a) e. RR /\ (b x. b) e. RR) -> ((a x. a) + (b x. b)) e. RR)
6 axmulrcl 5274 . . . . . . . . . . . . 13 |- ((a e. RR /\ a e. RR) -> (a x. a) e. RR)
76anidms 434 . . . . . . . . . . . 12 |- (a e. RR -> (a x. a) e. RR)
8 axmulrcl 5274 . . . . . . . . . . . . 13 |- ((b e. RR /\ b e. RR) -> (b x. b) e. RR)
98anidms 434 . . . . . . . . . . . 12 |- (b e. RR -> (b x. b) e. RR)
105, 7, 9syl2an 454 . . . . . . . . . . 11 |- ((a e. RR /\ b e. RR) -> ((a x. a) + (b x. b)) e. RR)
114, 10sylan 448 . . . . . . . . . 10 |- (((a e. RR /\ b e. RR) /\ ((a x. a) + (b x. b)) =/= 0) -> E.y e. RR (((a x. a) + (b x. b)) x. y) = 1)
12 opreq2 3969 . . . . . . . . . . . . . . . . . 18 |- (x = ((a - (i x. b)) x. y) -> ((a + (i x. b)) x. x) = ((a + (i x. b)) x. ((a - (i x. b)) x. y)))
1312eqeq1d 1483 . . . . . . . . . . . . . . . . 17 |- (x = ((a - (i x. b)) x. y) -> (((a + (i x. b)) x. x) = 1 <-> ((a + (i x. b)) x. ((a - (i x. b)) x. y)) = 1))
1413rcla4ev 1877 . . . . . . . . . . . . . . . 16 |- ((((a - (i x. b)) x. y) e. CC /\ ((a + (i x. b)) x. ((a - (i x. b)) x. y)) = 1) -> E.x e. CC ((a + (i x. b)) x. x) = 1)
15 axmulcl 5273 . . . . . . . . . . . . . . . . . 18 |- (((a - (i x. b)) e. CC /\ y e. CC) -> ((a - (i x. b)) x. y) e. CC)
16 subclt 5367 . . . . . . . . . . . . . . . . . . 19 |- ((a e. CC /\ (i x. b) e. CC) -> (a - (i x. b)) e. CC)
17 axicn 5270 . . . . . . . . . . . . . . . . . . . 20 |- i e. CC
18 axmulcl 5273 . . . . . . . . . . . . . . . . . . . 20 |- ((i e. CC /\ b e. CC) -> (i x. b) e. CC)
1917, 18mpan 695 . . . . . . . . . . . . . . . . . . 19 |- (b e. CC -> (i x. b) e. CC)
2016, 19sylan2 451 . . . . . . . . . . . . . . . . . 18 |- ((a e. CC /\ b e. CC) -> (a - (i x. b)) e. CC)
2115, 20sylan 448 . . . . . . . . . . . . . . . . 17 |- (((a e. CC /\ b e. CC) /\ y e. CC) -> ((a - (i x. b)) x. y) e. CC)
2221adantr 389 . . . . . . . . . . . . . . . 16 |- ((((a e. CC /\ b e. CC) /\ y e. CC) /\ (((a x. a) + (b x. b)) x. y) = 1) -> ((a - (i x. b)) x. y) e. CC)
23 axmulass 5278 . . . . . . . . . . . . . . . . . . 19 |- (((a + (i x. b)) e. CC /\ (a - (i x. b)) e. CC /\ y e. CC) -> (((a + (i x. b)) x. (a - (i x. b))) x. y) = ((a + (i x. b)) x. ((a - (i x. b)) x. y)))
24 axaddcl 5271 . . . . . . . . . . . . . . . . . . . . 21 |- ((a e. CC /\ (i x. b) e. CC) -> (a + (i x. b)) e. CC)
2524, 19sylan2 451 . . . . . . . . . . . . . . . . . . . 20 |- ((a e. CC /\ b e. CC) -> (a + (i x. b)) e. CC)
2625adantr 389 . . . . . . . . . . . . . . . . . . 19 |- (((a e. CC /\ b e. CC) /\ y e. CC) -> (a + (i x. b)) e. CC)
2720adantr 389 . . . . . . . . . . . . . . . . . . 19 |- (((a e. CC /\ b e. CC) /\ y e. CC) -> (a - (i x. b)) e. CC)
28 pm3.27 323 . . . . . . . . . . . . . . . . . . 19 |- (((a e. CC /\ b e. CC) /\ y e. CC) -> y e. CC)
2923, 26, 27, 28syl3anc 858 . . . . . . . . . . . . . . . . . 18 |- (((a e. CC /\ b e. CC) /\ y e. CC) -> (((a + (i x. b)) x. (a - (i x. b))) x. y) = ((a + (i x. b)) x. ((a - (i x. b)) x. y)))
30 recextlem1 5682 . . . . . . . . . . . . . . . . . . . 20 |- ((a e. CC /\ b e. CC) -> ((a + (i x. b)) x. (a - (i x. b))) = ((a x. a) + (b x. b)))
3130adantr 389 . . . . . . . . . . . . . . . . . . 19 |- (((a e. CC /\ b e. CC) /\ y e. CC) -> ((a + (i x. b)) x. (a - (i x. b))) = ((a x. a) + (b x. b)))
3231opreq1d 3975 . . . . . . . . . . . . . . . . . 18 |- (((a e. CC /\ b e. CC) /\ y e. CC) -> (((a + (i x. b)) x. (a - (i x. b))) x. y) = (((a x. a) + (b x. b)) x. y))
3329, 32eqtr3d 1509 . . . . . . . . . . . . . . . . 17 |- (((a e. CC /\ b e. CC) /\ y e. CC) -> ((a + (i x. b)) x. ((a - (i x. b)) x. y)) = (((a x. a) + (b x. b)) x. y))
34 id 59 . . . . . . . . . . . . . . . . 17 |- ((((a x. a) + (b x. b)) x. y) = 1 -> (((a x. a) + (b x. b)) x. y) = 1)
3533, 34sylan9eq 1527 . . . . . . . . . . . . . . . 16 |- ((((a e. CC /\ b e. CC) /\ y e. CC) /\ (((a x. a) + (b x. b)) x. y) = 1) -> ((a + (i x. b)) x. ((a - (i x. b)) x. y)) = 1)
3614, 22, 35sylanc 471 . . . . . . . . . . . . . . 15 |- ((((a e. CC /\ b e. CC) /\ y e. CC) /\ (((a x. a) + (b x. b)) x. y) = 1) -> E.x e. CC ((a + (i x. b)) x. x) = 1)
3736exp31 376 . . . . . . . . . . . . . 14 |- ((a e. CC /\ b e. CC) -> (y e. CC -> ((((a x. a) + (b x. b)) x. y) = 1 -> E.x e. CC ((a + (i x. b)) x. x) = 1)))
38 recnt 5313 . . . . . . . . . . . . . 14 |- (y e. RR -> y e. CC)
3937, 38syl5 21 . . . . . . . . . . . . 13 |- ((a e. CC /\ b e. CC) -> (y e. RR -> ((((a x. a) + (b x. b)) x. y) = 1 -> E.x e. CC ((a + (i x. b)) x. x) = 1)))
4039r19.23adv 1746 . . . . . . . . . . . 12 |- ((a e. CC /\ b e. CC) -> (E.y e. RR (((a x. a) + (b x. b)) x. y) = 1 -> E.x e. CC ((a + (i x. b)) x. x) = 1))
41 recnt 5313 . . . . . . . . . . . 12 |- (a e. RR -> a e. CC)
42 recnt 5313 . . . . . . . . . . . 12 |- (b e. RR -> b e. CC)
4340, 41, 42syl2an 454 . . . . . . . . . . 11 |- ((a e. RR /\ b e. RR) -> (E.y e. RR (((a x. a) + (b x. b)) x. y) = 1 -> E.x e. CC ((a + (i x. b)) x. x) = 1))
4443adantr 389 . . . . . . . . . 10 |- (((a e. RR /\ b e. RR) /\ ((a x. a) + (b x. b)) =/= 0) -> (E.y e. RR (((a x. a) + (b x. b)) x. y) = 1 -> E.x e. CC ((a + (i x. b)) x. x) = 1))
4511, 44mpd 26 . . . . . . . . 9 |- (((a e. RR /\ b e. RR) /\ ((a x. a) + (b x. b)) =/= 0) -> E.x e. CC ((a + (i x. b)) x. x) = 1)
4645ex 373 . . . . . . . 8 |- ((a e. RR /\ b e. RR) -> (((a x. a) + (b x. b)) =/= 0 -> E.x e. CC ((a + (i x. b)) x. x) = 1))
473, 46syld 27 . . . . . . 7 |- ((a e. RR /\ b e. RR) -> ((a + (i x. b)) =/= 0 -> E.x e. CC ((a + (i x. b)) x. x) = 1))
4847adantr 389 . . . . . 6 |- (((a e. RR /\ b e. RR) /\ A = (a + (i x. b))) -> ((a + (i x. b)) =/= 0 -> E.x e. CC ((a + (i x. b)) x. x) = 1))
49 neeq1 1590 . . . . . . 7 |- (A = (a + (i x. b)) -> (A =/= 0 <-> (a + (i x. b)) =/= 0))
5049adantl 388 . . . . . 6 |- (((a e. RR /\ b e. RR) /\ A = (a +