This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-0tie0

Description: Lemma for sn-mul02 . Commuted version of sn-it0e0 . (Contributed by SN, 30-Jun-2024)

Ref Expression
Assertion sn-0tie0 
|- ( 0 x. _i ) = 0

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 ax-icn 
 |-  _i e. CC
3 1 2 mulcli 
 |-  ( 0 x. _i ) e. CC
4 cnre 
 |-  ( ( 0 x. _i ) e. CC -> E. a e. RR E. b e. RR ( 0 x. _i ) = ( a + ( _i x. b ) ) )
5 simplr 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. _i ) = ( a + ( _i x. b ) ) )
6 neqne 
 |-  ( -. ( 0 x. _i ) = 0 -> ( 0 x. _i ) =/= 0 )
7 6 adantl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. _i ) =/= 0 )
8 simplll 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> a e. RR )
9 rernegcl 
 |-  ( a e. RR -> ( 0 -R a ) e. RR )
10 8 9 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 -R a ) e. RR )
11 1red 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> 1 e. RR )
12 10 11 readdcld 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 -R a ) + 1 ) e. RR )
13 ax-rrecex 
 |-  ( ( ( ( 0 -R a ) + 1 ) e. RR /\ ( ( 0 -R a ) + 1 ) =/= 0 ) -> E. x e. RR ( ( ( 0 -R a ) + 1 ) x. x ) = 1 )
14 12 13 sylan 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) -> E. x e. RR ( ( ( 0 -R a ) + 1 ) x. x ) = 1 )
15 2 a1i 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> _i e. CC )
16 10 recnd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 -R a ) e. CC )
17 1cnd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> 1 e. CC )
18 15 16 17 adddid 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. ( ( 0 -R a ) + 1 ) ) = ( ( _i x. ( 0 -R a ) ) + ( _i x. 1 ) ) )
19 sn-it1ei 
 |-  ( _i x. 1 ) = _i
20 19 oveq2i 
 |-  ( ( _i x. ( 0 -R a ) ) + ( _i x. 1 ) ) = ( ( _i x. ( 0 -R a ) ) + _i )
21 18 20 eqtrdi 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. ( ( 0 -R a ) + 1 ) ) = ( ( _i x. ( 0 -R a ) ) + _i ) )
22 21 oveq2d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( _i x. ( ( 0 -R a ) + 1 ) ) ) = ( 0 x. ( ( _i x. ( 0 -R a ) ) + _i ) ) )
23 0cnd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> 0 e. CC )
24 15 16 mulcld 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. ( 0 -R a ) ) e. CC )
25 23 24 15 adddid 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( ( _i x. ( 0 -R a ) ) + _i ) ) = ( ( 0 x. ( _i x. ( 0 -R a ) ) ) + ( 0 x. _i ) ) )
26 22 25 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( _i x. ( ( 0 -R a ) + 1 ) ) ) = ( ( 0 x. ( _i x. ( 0 -R a ) ) ) + ( 0 x. _i ) ) )
27 5 oveq2d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 -R a ) + ( 0 x. _i ) ) = ( ( 0 -R a ) + ( a + ( _i x. b ) ) ) )
28 renegid2 
 |-  ( a e. RR -> ( ( 0 -R a ) + a ) = 0 )
29 28 ad3antrrr 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 -R a ) + a ) = 0 )
30 29 oveq1d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( ( 0 -R a ) + a ) + ( _i x. b ) ) = ( 0 + ( _i x. b ) ) )
31 8 recnd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> a e. CC )
32 simpllr 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> b e. RR )
33 32 recnd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> b e. CC )
34 15 33 mulcld 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. b ) e. CC )
35 16 31 34 addassd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( ( 0 -R a ) + a ) + ( _i x. b ) ) = ( ( 0 -R a ) + ( a + ( _i x. b ) ) ) )
36 sn-addlid 
 |-  ( ( _i x. b ) e. CC -> ( 0 + ( _i x. b ) ) = ( _i x. b ) )
37 34 36 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 + ( _i x. b ) ) = ( _i x. b ) )
38 30 35 37 3eqtr3d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 -R a ) + ( a + ( _i x. b ) ) ) = ( _i x. b ) )
39 27 38 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 -R a ) + ( 0 x. _i ) ) = ( _i x. b ) )
40 39 oveq2d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) x. ( ( 0 -R a ) + ( 0 x. _i ) ) ) = ( ( 0 x. _i ) x. ( _i x. b ) ) )
41 3 a1i 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. _i ) e. CC )
42 41 16 41 adddid 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) x. ( ( 0 -R a ) + ( 0 x. _i ) ) ) = ( ( ( 0 x. _i ) x. ( 0 -R a ) ) + ( ( 0 x. _i ) x. ( 0 x. _i ) ) ) )
43 23 15 16 mulassd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) x. ( 0 -R a ) ) = ( 0 x. ( _i x. ( 0 -R a ) ) ) )
44 41 23 15 mulassd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( ( 0 x. _i ) x. 0 ) x. _i ) = ( ( 0 x. _i ) x. ( 0 x. _i ) ) )
45 sn-mul01 
 |-  ( ( 0 x. _i ) e. CC -> ( ( 0 x. _i ) x. 0 ) = 0 )
46 41 45 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) x. 0 ) = 0 )
47 46 oveq1d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( ( 0 x. _i ) x. 0 ) x. _i ) = ( 0 x. _i ) )
48 44 47 eqtr3d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) x. ( 0 x. _i ) ) = ( 0 x. _i ) )
49 43 48 oveq12d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( ( 0 x. _i ) x. ( 0 -R a ) ) + ( ( 0 x. _i ) x. ( 0 x. _i ) ) ) = ( ( 0 x. ( _i x. ( 0 -R a ) ) ) + ( 0 x. _i ) ) )
50 42 49 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) x. ( ( 0 -R a ) + ( 0 x. _i ) ) ) = ( ( 0 x. ( _i x. ( 0 -R a ) ) ) + ( 0 x. _i ) ) )
51 23 15 34 mulassd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) x. ( _i x. b ) ) = ( 0 x. ( _i x. ( _i x. b ) ) ) )
52 15 15 33 mulassd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( _i x. _i ) x. b ) = ( _i x. ( _i x. b ) ) )
53 reixi 
 |-  ( _i x. _i ) = ( 0 -R 1 )
54 1re 
 |-  1 e. RR
55 rernegcl 
 |-  ( 1 e. RR -> ( 0 -R 1 ) e. RR )
56 54 55 ax-mp 
 |-  ( 0 -R 1 ) e. RR
57 53 56 eqeltri 
 |-  ( _i x. _i ) e. RR
58 57 a1i 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. _i ) e. RR )
59 58 32 remulcld 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( _i x. _i ) x. b ) e. RR )
60 52 59 eqeltrrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. ( _i x. b ) ) e. RR )
61 remul02 
 |-  ( ( _i x. ( _i x. b ) ) e. RR -> ( 0 x. ( _i x. ( _i x. b ) ) ) = 0 )
62 60 61 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( _i x. ( _i x. b ) ) ) = 0 )
63 51 62 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) x. ( _i x. b ) ) = 0 )
64 40 50 63 3eqtr3d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. ( _i x. ( 0 -R a ) ) ) + ( 0 x. _i ) ) = 0 )
65 26 64 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( _i x. ( ( 0 -R a ) + 1 ) ) ) = 0 )
66 65 ad2antrr 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( 0 x. ( _i x. ( ( 0 -R a ) + 1 ) ) ) = 0 )
67 66 oveq1d 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( ( 0 x. ( _i x. ( ( 0 -R a ) + 1 ) ) ) x. x ) = ( 0 x. x ) )
68 0cnd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> 0 e. CC )
69 2 a1i 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> _i e. CC )
70 10 ad2antrr 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( 0 -R a ) e. RR )
71 70 recnd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( 0 -R a ) e. CC )
72 1cnd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> 1 e. CC )
73 71 72 addcld 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( ( 0 -R a ) + 1 ) e. CC )
74 69 73 mulcld 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( _i x. ( ( 0 -R a ) + 1 ) ) e. CC )
75 simprl 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> x e. RR )
76 75 recnd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> x e. CC )
77 68 74 76 mulassd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( ( 0 x. ( _i x. ( ( 0 -R a ) + 1 ) ) ) x. x ) = ( 0 x. ( ( _i x. ( ( 0 -R a ) + 1 ) ) x. x ) ) )
78 69 73 76 mulassd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( ( _i x. ( ( 0 -R a ) + 1 ) ) x. x ) = ( _i x. ( ( ( 0 -R a ) + 1 ) x. x ) ) )
79 simprr 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( ( ( 0 -R a ) + 1 ) x. x ) = 1 )
80 79 oveq2d 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( _i x. ( ( ( 0 -R a ) + 1 ) x. x ) ) = ( _i x. 1 ) )
81 80 19 eqtrdi 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( _i x. ( ( ( 0 -R a ) + 1 ) x. x ) ) = _i )
82 78 81 eqtrd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( ( _i x. ( ( 0 -R a ) + 1 ) ) x. x ) = _i )
83 82 oveq2d 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( 0 x. ( ( _i x. ( ( 0 -R a ) + 1 ) ) x. x ) ) = ( 0 x. _i ) )
84 77 83 eqtrd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( ( 0 x. ( _i x. ( ( 0 -R a ) + 1 ) ) ) x. x ) = ( 0 x. _i ) )
85 remul02 
 |-  ( x e. RR -> ( 0 x. x ) = 0 )
86 75 85 syl 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( 0 x. x ) = 0 )
87 67 84 86 3eqtr3d 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) /\ ( x e. RR /\ ( ( ( 0 -R a ) + 1 ) x. x ) = 1 ) ) -> ( 0 x. _i ) = 0 )
88 14 87 rexlimddv 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( ( 0 -R a ) + 1 ) =/= 0 ) -> ( 0 x. _i ) = 0 )
89 88 ex 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( ( 0 -R a ) + 1 ) =/= 0 -> ( 0 x. _i ) = 0 ) )
90 89 necon1d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) =/= 0 -> ( ( 0 -R a ) + 1 ) = 0 ) )
91 7 90 mpd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 -R a ) + 1 ) = 0 )
92 91 oveq2d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( a + ( ( 0 -R a ) + 1 ) ) = ( a + 0 ) )
93 31 16 17 addassd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( a + ( 0 -R a ) ) + 1 ) = ( a + ( ( 0 -R a ) + 1 ) ) )
94 renegid 
 |-  ( a e. RR -> ( a + ( 0 -R a ) ) = 0 )
95 8 94 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( a + ( 0 -R a ) ) = 0 )
96 95 oveq1d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( a + ( 0 -R a ) ) + 1 ) = ( 0 + 1 ) )
97 readdlid 
 |-  ( 1 e. RR -> ( 0 + 1 ) = 1 )
98 54 97 ax-mp 
 |-  ( 0 + 1 ) = 1
99 96 98 eqtrdi 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( a + ( 0 -R a ) ) + 1 ) = 1 )
100 93 99 eqtr3d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( a + ( ( 0 -R a ) + 1 ) ) = 1 )
101 readdrid 
 |-  ( a e. RR -> ( a + 0 ) = a )
102 8 101 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( a + 0 ) = a )
103 92 100 102 3eqtr3rd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> a = 1 )
104 rernegcl 
 |-  ( b e. RR -> ( 0 -R b ) e. RR )
105 32 104 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 -R b ) e. RR )
106 11 105 readdcld 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 1 + ( 0 -R b ) ) e. RR )
107 ax-rrecex 
 |-  ( ( ( 1 + ( 0 -R b ) ) e. RR /\ ( 1 + ( 0 -R b ) ) =/= 0 ) -> E. y e. RR ( ( 1 + ( 0 -R b ) ) x. y ) = 1 )
108 106 107 sylan 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) -> E. y e. RR ( ( 1 + ( 0 -R b ) ) x. y ) = 1 )
109 105 recnd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 -R b ) e. CC )
110 15 109 mulcld 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. ( 0 -R b ) ) e. CC )
111 23 15 110 adddid 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( _i + ( _i x. ( 0 -R b ) ) ) ) = ( ( 0 x. _i ) + ( 0 x. ( _i x. ( 0 -R b ) ) ) ) )
112 0re 
 |-  0 e. RR
113 remul02 
 |-  ( 0 e. RR -> ( 0 x. 0 ) = 0 )
114 112 113 ax-mp 
 |-  ( 0 x. 0 ) = 0
115 114 oveq1i 
 |-  ( ( 0 x. 0 ) x. _i ) = ( 0 x. _i )
116 1 1 2 mulassi 
 |-  ( ( 0 x. 0 ) x. _i ) = ( 0 x. ( 0 x. _i ) )
117 115 116 eqtr3i 
 |-  ( 0 x. _i ) = ( 0 x. ( 0 x. _i ) )
118 117 a1i 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. _i ) = ( 0 x. ( 0 x. _i ) ) )
119 118 oveq1d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) + ( 0 x. ( _i x. ( 0 -R b ) ) ) ) = ( ( 0 x. ( 0 x. _i ) ) + ( 0 x. ( _i x. ( 0 -R b ) ) ) ) )
120 111 119 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( _i + ( _i x. ( 0 -R b ) ) ) ) = ( ( 0 x. ( 0 x. _i ) ) + ( 0 x. ( _i x. ( 0 -R b ) ) ) ) )
121 15 17 109 adddid 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. ( 1 + ( 0 -R b ) ) ) = ( ( _i x. 1 ) + ( _i x. ( 0 -R b ) ) ) )
122 19 a1i 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. 1 ) = _i )
123 122 oveq1d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( _i x. 1 ) + ( _i x. ( 0 -R b ) ) ) = ( _i + ( _i x. ( 0 -R b ) ) ) )
124 121 123 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. ( 1 + ( 0 -R b ) ) ) = ( _i + ( _i x. ( 0 -R b ) ) ) )
125 124 oveq2d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( _i x. ( 1 + ( 0 -R b ) ) ) ) = ( 0 x. ( _i + ( _i x. ( 0 -R b ) ) ) ) )
126 23 41 110 adddid 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( ( 0 x. _i ) + ( _i x. ( 0 -R b ) ) ) ) = ( ( 0 x. ( 0 x. _i ) ) + ( 0 x. ( _i x. ( 0 -R b ) ) ) ) )
127 120 125 126 3eqtr4d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( _i x. ( 1 + ( 0 -R b ) ) ) ) = ( 0 x. ( ( 0 x. _i ) + ( _i x. ( 0 -R b ) ) ) ) )
128 103 oveq1d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( a + ( _i x. b ) ) = ( 1 + ( _i x. b ) ) )
129 5 128 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. _i ) = ( 1 + ( _i x. b ) ) )
130 129 oveq1d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) + ( _i x. ( 0 -R b ) ) ) = ( ( 1 + ( _i x. b ) ) + ( _i x. ( 0 -R b ) ) ) )
131 17 34 110 addassd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 1 + ( _i x. b ) ) + ( _i x. ( 0 -R b ) ) ) = ( 1 + ( ( _i x. b ) + ( _i x. ( 0 -R b ) ) ) ) )
132 renegid 
 |-  ( b e. RR -> ( b + ( 0 -R b ) ) = 0 )
133 32 132 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( b + ( 0 -R b ) ) = 0 )
134 133 oveq2d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. ( b + ( 0 -R b ) ) ) = ( _i x. 0 ) )
135 15 33 109 adddid 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. ( b + ( 0 -R b ) ) ) = ( ( _i x. b ) + ( _i x. ( 0 -R b ) ) ) )
136 sn-mul01 
 |-  ( _i e. CC -> ( _i x. 0 ) = 0 )
137 2 136 mp1i 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. 0 ) = 0 )
138 134 135 137 3eqtr3d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( _i x. b ) + ( _i x. ( 0 -R b ) ) ) = 0 )
139 138 oveq2d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 1 + ( ( _i x. b ) + ( _i x. ( 0 -R b ) ) ) ) = ( 1 + 0 ) )
140 readdrid 
 |-  ( 1 e. RR -> ( 1 + 0 ) = 1 )
141 54 140 ax-mp 
 |-  ( 1 + 0 ) = 1
142 139 141 eqtrdi 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 1 + ( ( _i x. b ) + ( _i x. ( 0 -R b ) ) ) ) = 1 )
143 131 142 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 1 + ( _i x. b ) ) + ( _i x. ( 0 -R b ) ) ) = 1 )
144 130 143 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) + ( _i x. ( 0 -R b ) ) ) = 1 )
145 144 oveq2d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( ( 0 x. _i ) + ( _i x. ( 0 -R b ) ) ) ) = ( 0 x. 1 ) )
146 127 145 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( _i x. ( 1 + ( 0 -R b ) ) ) ) = ( 0 x. 1 ) )
147 ax-1rid 
 |-  ( 0 e. RR -> ( 0 x. 1 ) = 0 )
148 112 147 ax-mp 
 |-  ( 0 x. 1 ) = 0
149 146 148 eqtrdi 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. ( _i x. ( 1 + ( 0 -R b ) ) ) ) = 0 )
150 149 ad2antrr 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( 0 x. ( _i x. ( 1 + ( 0 -R b ) ) ) ) = 0 )
151 150 oveq1d 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( ( 0 x. ( _i x. ( 1 + ( 0 -R b ) ) ) ) x. y ) = ( 0 x. y ) )
152 0cnd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> 0 e. CC )
153 2 a1i 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> _i e. CC )
154 1cnd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> 1 e. CC )
155 109 ad2antrr 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( 0 -R b ) e. CC )
156 154 155 addcld 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( 1 + ( 0 -R b ) ) e. CC )
157 153 156 mulcld 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( _i x. ( 1 + ( 0 -R b ) ) ) e. CC )
158 simprl 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> y e. RR )
159 158 recnd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> y e. CC )
160 152 157 159 mulassd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( ( 0 x. ( _i x. ( 1 + ( 0 -R b ) ) ) ) x. y ) = ( 0 x. ( ( _i x. ( 1 + ( 0 -R b ) ) ) x. y ) ) )
161 153 156 159 mulassd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( ( _i x. ( 1 + ( 0 -R b ) ) ) x. y ) = ( _i x. ( ( 1 + ( 0 -R b ) ) x. y ) ) )
162 simprr 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( ( 1 + ( 0 -R b ) ) x. y ) = 1 )
163 162 oveq2d 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( _i x. ( ( 1 + ( 0 -R b ) ) x. y ) ) = ( _i x. 1 ) )
164 163 19 eqtrdi 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( _i x. ( ( 1 + ( 0 -R b ) ) x. y ) ) = _i )
165 161 164 eqtrd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( ( _i x. ( 1 + ( 0 -R b ) ) ) x. y ) = _i )
166 165 oveq2d 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( 0 x. ( ( _i x. ( 1 + ( 0 -R b ) ) ) x. y ) ) = ( 0 x. _i ) )
167 160 166 eqtrd 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( ( 0 x. ( _i x. ( 1 + ( 0 -R b ) ) ) ) x. y ) = ( 0 x. _i ) )
168 remul02 
 |-  ( y e. RR -> ( 0 x. y ) = 0 )
169 158 168 syl 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( 0 x. y ) = 0 )
170 151 167 169 3eqtr3d 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) /\ ( y e. RR /\ ( ( 1 + ( 0 -R b ) ) x. y ) = 1 ) ) -> ( 0 x. _i ) = 0 )
171 108 170 rexlimddv 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) /\ ( 1 + ( 0 -R b ) ) =/= 0 ) -> ( 0 x. _i ) = 0 )
172 171 ex 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 1 + ( 0 -R b ) ) =/= 0 -> ( 0 x. _i ) = 0 ) )
173 172 necon1d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 x. _i ) =/= 0 -> ( 1 + ( 0 -R b ) ) = 0 ) )
174 7 173 mpd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 1 + ( 0 -R b ) ) = 0 )
175 174 oveq1d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 1 + ( 0 -R b ) ) + b ) = ( 0 + b ) )
176 17 109 33 addassd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 1 + ( 0 -R b ) ) + b ) = ( 1 + ( ( 0 -R b ) + b ) ) )
177 renegid2 
 |-  ( b e. RR -> ( ( 0 -R b ) + b ) = 0 )
178 32 177 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 0 -R b ) + b ) = 0 )
179 178 oveq2d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 1 + ( ( 0 -R b ) + b ) ) = ( 1 + 0 ) )
180 179 141 eqtrdi 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 1 + ( ( 0 -R b ) + b ) ) = 1 )
181 176 180 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( ( 1 + ( 0 -R b ) ) + b ) = 1 )
182 readdlid 
 |-  ( b e. RR -> ( 0 + b ) = b )
183 32 182 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 + b ) = b )
184 175 181 183 3eqtr3rd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> b = 1 )
185 184 oveq2d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( _i x. b ) = ( _i x. 1 ) )
186 103 185 oveq12d 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( a + ( _i x. b ) ) = ( 1 + ( _i x. 1 ) ) )
187 5 186 eqtrd 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. _i ) = ( 1 + ( _i x. 1 ) ) )
188 19 oveq2i 
 |-  ( 1 + ( _i x. 1 ) ) = ( 1 + _i )
189 188 eqeq2i 
 |-  ( ( 0 x. _i ) = ( 1 + ( _i x. 1 ) ) <-> ( 0 x. _i ) = ( 1 + _i ) )
190 oveq2 
 |-  ( ( 0 x. _i ) = ( 1 + _i ) -> ( ( ( _i x. _i ) x. _i ) x. ( 0 x. _i ) ) = ( ( ( _i x. _i ) x. _i ) x. ( 1 + _i ) ) )
191 2 2 mulcli 
 |-  ( _i x. _i ) e. CC
192 191 2 mulcli 
 |-  ( ( _i x. _i ) x. _i ) e. CC
193 192 1 2 mulassi 
 |-  ( ( ( ( _i x. _i ) x. _i ) x. 0 ) x. _i ) = ( ( ( _i x. _i ) x. _i ) x. ( 0 x. _i ) )
194 sn-mul01 
 |-  ( ( ( _i x. _i ) x. _i ) e. CC -> ( ( ( _i x. _i ) x. _i ) x. 0 ) = 0 )
195 192 194 ax-mp 
 |-  ( ( ( _i x. _i ) x. _i ) x. 0 ) = 0
196 195 oveq1i 
 |-  ( ( ( ( _i x. _i ) x. _i ) x. 0 ) x. _i ) = ( 0 x. _i )
197 193 196 eqtr3i 
 |-  ( ( ( _i x. _i ) x. _i ) x. ( 0 x. _i ) ) = ( 0 x. _i )
198 ax-1cn 
 |-  1 e. CC
199 192 198 2 adddii 
 |-  ( ( ( _i x. _i ) x. _i ) x. ( 1 + _i ) ) = ( ( ( ( _i x. _i ) x. _i ) x. 1 ) + ( ( ( _i x. _i ) x. _i ) x. _i ) )
200 191 2 198 mulassi 
 |-  ( ( ( _i x. _i ) x. _i ) x. 1 ) = ( ( _i x. _i ) x. ( _i x. 1 ) )
201 19 oveq2i 
 |-  ( ( _i x. _i ) x. ( _i x. 1 ) ) = ( ( _i x. _i ) x. _i )
202 200 201 eqtri 
 |-  ( ( ( _i x. _i ) x. _i ) x. 1 ) = ( ( _i x. _i ) x. _i )
203 191 2 2 mulassi 
 |-  ( ( ( _i x. _i ) x. _i ) x. _i ) = ( ( _i x. _i ) x. ( _i x. _i ) )
204 rei4 
 |-  ( ( _i x. _i ) x. ( _i x. _i ) ) = 1
205 203 204 eqtri 
 |-  ( ( ( _i x. _i ) x. _i ) x. _i ) = 1
206 202 205 oveq12i 
 |-  ( ( ( ( _i x. _i ) x. _i ) x. 1 ) + ( ( ( _i x. _i ) x. _i ) x. _i ) ) = ( ( ( _i x. _i ) x. _i ) + 1 )
207 199 206 eqtri 
 |-  ( ( ( _i x. _i ) x. _i ) x. ( 1 + _i ) ) = ( ( ( _i x. _i ) x. _i ) + 1 )
208 190 197 207 3eqtr3g 
 |-  ( ( 0 x. _i ) = ( 1 + _i ) -> ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) )
209 54 54 readdcli 
 |-  ( 1 + 1 ) e. RR
210 df-2 
 |-  2 = ( 1 + 1 )
211 sn-0ne2 
 |-  0 =/= 2
212 211 necomi 
 |-  2 =/= 0
213 210 212 eqnetrri 
 |-  ( 1 + 1 ) =/= 0
214 ax-rrecex 
 |-  ( ( ( 1 + 1 ) e. RR /\ ( 1 + 1 ) =/= 0 ) -> E. z e. RR ( ( 1 + 1 ) x. z ) = 1 )
215 209 213 214 mp2an 
 |-  E. z e. RR ( ( 1 + 1 ) x. z ) = 1
216 192 198 addcli 
 |-  ( ( ( _i x. _i ) x. _i ) + 1 ) e. CC
217 198 2 216 addassi 
 |-  ( ( 1 + _i ) + ( ( ( _i x. _i ) x. _i ) + 1 ) ) = ( 1 + ( _i + ( ( ( _i x. _i ) x. _i ) + 1 ) ) )
218 2 192 198 addassi 
 |-  ( ( _i + ( ( _i x. _i ) x. _i ) ) + 1 ) = ( _i + ( ( ( _i x. _i ) x. _i ) + 1 ) )
219 218 oveq2i 
 |-  ( 1 + ( ( _i + ( ( _i x. _i ) x. _i ) ) + 1 ) ) = ( 1 + ( _i + ( ( ( _i x. _i ) x. _i ) + 1 ) ) )
220 2 2 2 mulassi 
 |-  ( ( _i x. _i ) x. _i ) = ( _i x. ( _i x. _i ) )
221 220 oveq2i 
 |-  ( _i + ( ( _i x. _i ) x. _i ) ) = ( _i + ( _i x. ( _i x. _i ) ) )
222 ipiiie0 
 |-  ( _i + ( _i x. ( _i x. _i ) ) ) = 0
223 221 222 eqtri 
 |-  ( _i + ( ( _i x. _i ) x. _i ) ) = 0
224 223 oveq1i 
 |-  ( ( _i + ( ( _i x. _i ) x. _i ) ) + 1 ) = ( 0 + 1 )
225 224 98 eqtri 
 |-  ( ( _i + ( ( _i x. _i ) x. _i ) ) + 1 ) = 1
226 225 oveq2i 
 |-  ( 1 + ( ( _i + ( ( _i x. _i ) x. _i ) ) + 1 ) ) = ( 1 + 1 )
227 217 219 226 3eqtr2i 
 |-  ( ( 1 + _i ) + ( ( ( _i x. _i ) x. _i ) + 1 ) ) = ( 1 + 1 )
228 227 a1i 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( ( 1 + _i ) + ( ( ( _i x. _i ) x. _i ) + 1 ) ) = ( 1 + 1 ) )
229 3 198 198 adddii 
 |-  ( ( 0 x. _i ) x. ( 1 + 1 ) ) = ( ( ( 0 x. _i ) x. 1 ) + ( ( 0 x. _i ) x. 1 ) )
230 1 2 198 mulassi 
 |-  ( ( 0 x. _i ) x. 1 ) = ( 0 x. ( _i x. 1 ) )
231 19 oveq2i 
 |-  ( 0 x. ( _i x. 1 ) ) = ( 0 x. _i )
232 230 231 eqtri 
 |-  ( ( 0 x. _i ) x. 1 ) = ( 0 x. _i )
233 simpl 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( 0 x. _i ) = ( 1 + _i ) )
234 232 233 eqtrid 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( ( 0 x. _i ) x. 1 ) = ( 1 + _i ) )
235 simpr 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) )
236 232 235 eqtrid 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( ( 0 x. _i ) x. 1 ) = ( ( ( _i x. _i ) x. _i ) + 1 ) )
237 234 236 oveq12d 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( ( ( 0 x. _i ) x. 1 ) + ( ( 0 x. _i ) x. 1 ) ) = ( ( 1 + _i ) + ( ( ( _i x. _i ) x. _i ) + 1 ) ) )
238 229 237 eqtrid 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( ( 0 x. _i ) x. ( 1 + 1 ) ) = ( ( 1 + _i ) + ( ( ( _i x. _i ) x. _i ) + 1 ) ) )
239 remullid 
 |-  ( ( 1 + 1 ) e. RR -> ( 1 x. ( 1 + 1 ) ) = ( 1 + 1 ) )
240 209 239 mp1i 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( 1 x. ( 1 + 1 ) ) = ( 1 + 1 ) )
241 228 238 240 3eqtr4d 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( ( 0 x. _i ) x. ( 1 + 1 ) ) = ( 1 x. ( 1 + 1 ) ) )
242 241 oveq1d 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( ( ( 0 x. _i ) x. ( 1 + 1 ) ) x. z ) = ( ( 1 x. ( 1 + 1 ) ) x. z ) )
243 242 adantr 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( ( ( 0 x. _i ) x. ( 1 + 1 ) ) x. z ) = ( ( 1 x. ( 1 + 1 ) ) x. z ) )
244 3 a1i 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( 0 x. _i ) e. CC )
245 1cnd 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> 1 e. CC )
246 245 245 addcld 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( 1 + 1 ) e. CC )
247 simprl 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> z e. RR )
248 247 recnd 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> z e. CC )
249 244 246 248 mulassd 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( ( ( 0 x. _i ) x. ( 1 + 1 ) ) x. z ) = ( ( 0 x. _i ) x. ( ( 1 + 1 ) x. z ) ) )
250 simprr 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( ( 1 + 1 ) x. z ) = 1 )
251 250 oveq2d 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( ( 0 x. _i ) x. ( ( 1 + 1 ) x. z ) ) = ( ( 0 x. _i ) x. 1 ) )
252 251 232 eqtrdi 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( ( 0 x. _i ) x. ( ( 1 + 1 ) x. z ) ) = ( 0 x. _i ) )
253 249 252 eqtrd 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( ( ( 0 x. _i ) x. ( 1 + 1 ) ) x. z ) = ( 0 x. _i ) )
254 245 246 248 mulassd 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( ( 1 x. ( 1 + 1 ) ) x. z ) = ( 1 x. ( ( 1 + 1 ) x. z ) ) )
255 250 oveq2d 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( 1 x. ( ( 1 + 1 ) x. z ) ) = ( 1 x. 1 ) )
256 1t1e1ALT 
 |-  ( 1 x. 1 ) = 1
257 255 256 eqtrdi 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( 1 x. ( ( 1 + 1 ) x. z ) ) = 1 )
258 254 257 eqtrd 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( ( 1 x. ( 1 + 1 ) ) x. z ) = 1 )
259 243 253 258 3eqtr3d 
 |-  ( ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) /\ ( z e. RR /\ ( ( 1 + 1 ) x. z ) = 1 ) ) -> ( 0 x. _i ) = 1 )
260 259 rexlimdvaa 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( E. z e. RR ( ( 1 + 1 ) x. z ) = 1 -> ( 0 x. _i ) = 1 ) )
261 215 260 mpi 
 |-  ( ( ( 0 x. _i ) = ( 1 + _i ) /\ ( 0 x. _i ) = ( ( ( _i x. _i ) x. _i ) + 1 ) ) -> ( 0 x. _i ) = 1 )
262 208 261 mpdan 
 |-  ( ( 0 x. _i ) = ( 1 + _i ) -> ( 0 x. _i ) = 1 )
263 189 262 sylbi 
 |-  ( ( 0 x. _i ) = ( 1 + ( _i x. 1 ) ) -> ( 0 x. _i ) = 1 )
264 oveq2 
 |-  ( ( 0 x. _i ) = 1 -> ( 0 x. ( 0 x. _i ) ) = ( 0 x. 1 ) )
265 116 115 eqtr3i 
 |-  ( 0 x. ( 0 x. _i ) ) = ( 0 x. _i )
266 264 265 148 3eqtr3g 
 |-  ( ( 0 x. _i ) = 1 -> ( 0 x. _i ) = 0 )
267 263 266 syl 
 |-  ( ( 0 x. _i ) = ( 1 + ( _i x. 1 ) ) -> ( 0 x. _i ) = 0 )
268 187 267 syl 
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) /\ -. ( 0 x. _i ) = 0 ) -> ( 0 x. _i ) = 0 )
269 268 pm2.18da 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( 0 x. _i ) = ( a + ( _i x. b ) ) ) -> ( 0 x. _i ) = 0 )
270 269 ex 
 |-  ( ( a e. RR /\ b e. RR ) -> ( ( 0 x. _i ) = ( a + ( _i x. b ) ) -> ( 0 x. _i ) = 0 ) )
271 270 rexlimivv 
 |-  ( E. a e. RR E. b e. RR ( 0 x. _i ) = ( a + ( _i x. b ) ) -> ( 0 x. _i ) = 0 )
272 3 4 271 mp2b 
 |-  ( 0 x. _i ) = 0