Users' Mathboxes Mathbox for Steven Nguyen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sn-0tie0 Structured version   Visualization version   GIF version

Theorem sn-0tie0 40937
Description: Lemma for sn-mul02 40938. Commuted version of sn-it0e0 40913. (Contributed by SN, 30-Jun-2024.)
Assertion
Ref Expression
sn-0tie0 (0 ยท i) = 0

Proof of Theorem sn-0tie0
Dummy variables ๐‘Ž ๐‘ ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0cn 11154 . . 3 0 โˆˆ โ„‚
2 ax-icn 11117 . . 3 i โˆˆ โ„‚
31, 2mulcli 11169 . 2 (0 ยท i) โˆˆ โ„‚
4 cnre 11159 . 2 ((0 ยท i) โˆˆ โ„‚ โ†’ โˆƒ๐‘Ž โˆˆ โ„ โˆƒ๐‘ โˆˆ โ„ (0 ยท i) = (๐‘Ž + (i ยท ๐‘)))
5 simplr 768 . . . . . . 7 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท i) = (๐‘Ž + (i ยท ๐‘)))
6 neqne 2952 . . . . . . . . . . . 12 (ยฌ (0 ยท i) = 0 โ†’ (0 ยท i) โ‰  0)
76adantl 483 . . . . . . . . . . 11 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท i) โ‰  0)
8 simplll 774 . . . . . . . . . . . . . . . . 17 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ๐‘Ž โˆˆ โ„)
9 rernegcl 40869 . . . . . . . . . . . . . . . . 17 (๐‘Ž โˆˆ โ„ โ†’ (0 โˆ’โ„ ๐‘Ž) โˆˆ โ„)
108, 9syl 17 . . . . . . . . . . . . . . . 16 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 โˆ’โ„ ๐‘Ž) โˆˆ โ„)
11 1red 11163 . . . . . . . . . . . . . . . 16 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ 1 โˆˆ โ„)
1210, 11readdcld 11191 . . . . . . . . . . . . . . 15 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 โˆ’โ„ ๐‘Ž) + 1) โˆˆ โ„)
13 ax-rrecex 11130 . . . . . . . . . . . . . . 15 ((((0 โˆ’โ„ ๐‘Ž) + 1) โˆˆ โ„ โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)
1412, 13sylan 581 . . . . . . . . . . . . . 14 (((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)
152a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ i โˆˆ โ„‚)
1610recnd 11190 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 โˆ’โ„ ๐‘Ž) โˆˆ โ„‚)
17 1cnd 11157 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ 1 โˆˆ โ„‚)
1815, 16, 17adddid 11186 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท ((0 โˆ’โ„ ๐‘Ž) + 1)) = ((i ยท (0 โˆ’โ„ ๐‘Ž)) + (i ยท 1)))
19 it1ei 40934 . . . . . . . . . . . . . . . . . . . . . 22 (i ยท 1) = i
2019oveq2i 7373 . . . . . . . . . . . . . . . . . . . . 21 ((i ยท (0 โˆ’โ„ ๐‘Ž)) + (i ยท 1)) = ((i ยท (0 โˆ’โ„ ๐‘Ž)) + i)
2118, 20eqtrdi 2793 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท ((0 โˆ’โ„ ๐‘Ž) + 1)) = ((i ยท (0 โˆ’โ„ ๐‘Ž)) + i))
2221oveq2d 7378 . . . . . . . . . . . . . . . . . . 19 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท (i ยท ((0 โˆ’โ„ ๐‘Ž) + 1))) = (0 ยท ((i ยท (0 โˆ’โ„ ๐‘Ž)) + i)))
23 0cnd 11155 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ 0 โˆˆ โ„‚)
2415, 16mulcld 11182 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท (0 โˆ’โ„ ๐‘Ž)) โˆˆ โ„‚)
2523, 24, 15adddid 11186 . . . . . . . . . . . . . . . . . . 19 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท ((i ยท (0 โˆ’โ„ ๐‘Ž)) + i)) = ((0 ยท (i ยท (0 โˆ’โ„ ๐‘Ž))) + (0 ยท i)))
2622, 25eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท (i ยท ((0 โˆ’โ„ ๐‘Ž) + 1))) = ((0 ยท (i ยท (0 โˆ’โ„ ๐‘Ž))) + (0 ยท i)))
275oveq2d 7378 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 โˆ’โ„ ๐‘Ž) + (0 ยท i)) = ((0 โˆ’โ„ ๐‘Ž) + (๐‘Ž + (i ยท ๐‘))))
28 renegid2 40911 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘Ž โˆˆ โ„ โ†’ ((0 โˆ’โ„ ๐‘Ž) + ๐‘Ž) = 0)
2928ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 โˆ’โ„ ๐‘Ž) + ๐‘Ž) = 0)
3029oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (((0 โˆ’โ„ ๐‘Ž) + ๐‘Ž) + (i ยท ๐‘)) = (0 + (i ยท ๐‘)))
318recnd 11190 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ๐‘Ž โˆˆ โ„‚)
32 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ๐‘ โˆˆ โ„)
3332recnd 11190 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ๐‘ โˆˆ โ„‚)
3415, 33mulcld 11182 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท ๐‘) โˆˆ โ„‚)
3516, 31, 34addassd 11184 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (((0 โˆ’โ„ ๐‘Ž) + ๐‘Ž) + (i ยท ๐‘)) = ((0 โˆ’โ„ ๐‘Ž) + (๐‘Ž + (i ยท ๐‘))))
36 sn-addid2 40902 . . . . . . . . . . . . . . . . . . . . . . 23 ((i ยท ๐‘) โˆˆ โ„‚ โ†’ (0 + (i ยท ๐‘)) = (i ยท ๐‘))
3734, 36syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 + (i ยท ๐‘)) = (i ยท ๐‘))
3830, 35, 373eqtr3d 2785 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 โˆ’โ„ ๐‘Ž) + (๐‘Ž + (i ยท ๐‘))) = (i ยท ๐‘))
3927, 38eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 โˆ’โ„ ๐‘Ž) + (0 ยท i)) = (i ยท ๐‘))
4039oveq2d 7378 . . . . . . . . . . . . . . . . . . 19 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) ยท ((0 โˆ’โ„ ๐‘Ž) + (0 ยท i))) = ((0 ยท i) ยท (i ยท ๐‘)))
413a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท i) โˆˆ โ„‚)
4241, 16, 41adddid 11186 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) ยท ((0 โˆ’โ„ ๐‘Ž) + (0 ยท i))) = (((0 ยท i) ยท (0 โˆ’โ„ ๐‘Ž)) + ((0 ยท i) ยท (0 ยท i))))
4323, 15, 16mulassd 11185 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) ยท (0 โˆ’โ„ ๐‘Ž)) = (0 ยท (i ยท (0 โˆ’โ„ ๐‘Ž))))
4441, 23, 15mulassd 11185 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (((0 ยท i) ยท 0) ยท i) = ((0 ยท i) ยท (0 ยท i)))
45 sn-mul01 40923 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ยท i) โˆˆ โ„‚ โ†’ ((0 ยท i) ยท 0) = 0)
4641, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) ยท 0) = 0)
4746oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (((0 ยท i) ยท 0) ยท i) = (0 ยท i))
4844, 47eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) ยท (0 ยท i)) = (0 ยท i))
4943, 48oveq12d 7380 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (((0 ยท i) ยท (0 โˆ’โ„ ๐‘Ž)) + ((0 ยท i) ยท (0 ยท i))) = ((0 ยท (i ยท (0 โˆ’โ„ ๐‘Ž))) + (0 ยท i)))
5042, 49eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) ยท ((0 โˆ’โ„ ๐‘Ž) + (0 ยท i))) = ((0 ยท (i ยท (0 โˆ’โ„ ๐‘Ž))) + (0 ยท i)))
5123, 15, 34mulassd 11185 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) ยท (i ยท ๐‘)) = (0 ยท (i ยท (i ยท ๐‘))))
5215, 15, 33mulassd 11185 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((i ยท i) ยท ๐‘) = (i ยท (i ยท ๐‘)))
53 reixi 40920 . . . . . . . . . . . . . . . . . . . . . . . . 25 (i ยท i) = (0 โˆ’โ„ 1)
54 1re 11162 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 โˆˆ โ„
55 rernegcl 40869 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 โˆˆ โ„ โ†’ (0 โˆ’โ„ 1) โˆˆ โ„)
5654, 55ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 โˆ’โ„ 1) โˆˆ โ„
5753, 56eqeltri 2834 . . . . . . . . . . . . . . . . . . . . . . . 24 (i ยท i) โˆˆ โ„
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท i) โˆˆ โ„)
5958, 32remulcld 11192 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((i ยท i) ยท ๐‘) โˆˆ โ„)
6052, 59eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท (i ยท ๐‘)) โˆˆ โ„)
61 remul02 40903 . . . . . . . . . . . . . . . . . . . . 21 ((i ยท (i ยท ๐‘)) โˆˆ โ„ โ†’ (0 ยท (i ยท (i ยท ๐‘))) = 0)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท (i ยท (i ยท ๐‘))) = 0)
6351, 62eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) ยท (i ยท ๐‘)) = 0)
6440, 50, 633eqtr3d 2785 . . . . . . . . . . . . . . . . . 18 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท (i ยท (0 โˆ’โ„ ๐‘Ž))) + (0 ยท i)) = 0)
6526, 64eqtrd 2777 . . . . . . . . . . . . . . . . 17 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท (i ยท ((0 โˆ’โ„ ๐‘Ž) + 1))) = 0)
6665ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ (0 ยท (i ยท ((0 โˆ’โ„ ๐‘Ž) + 1))) = 0)
6766oveq1d 7377 . . . . . . . . . . . . . . 15 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ ((0 ยท (i ยท ((0 โˆ’โ„ ๐‘Ž) + 1))) ยท ๐‘ฅ) = (0 ยท ๐‘ฅ))
68 0cnd 11155 . . . . . . . . . . . . . . . . 17 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ 0 โˆˆ โ„‚)
692a1i 11 . . . . . . . . . . . . . . . . . 18 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ i โˆˆ โ„‚)
7010ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ (0 โˆ’โ„ ๐‘Ž) โˆˆ โ„)
7170recnd 11190 . . . . . . . . . . . . . . . . . . 19 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ (0 โˆ’โ„ ๐‘Ž) โˆˆ โ„‚)
72 1cnd 11157 . . . . . . . . . . . . . . . . . . 19 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ 1 โˆˆ โ„‚)
7371, 72addcld 11181 . . . . . . . . . . . . . . . . . 18 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ ((0 โˆ’โ„ ๐‘Ž) + 1) โˆˆ โ„‚)
7469, 73mulcld 11182 . . . . . . . . . . . . . . . . 17 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ (i ยท ((0 โˆ’โ„ ๐‘Ž) + 1)) โˆˆ โ„‚)
75 simprl 770 . . . . . . . . . . . . . . . . . 18 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ ๐‘ฅ โˆˆ โ„)
7675recnd 11190 . . . . . . . . . . . . . . . . 17 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ ๐‘ฅ โˆˆ โ„‚)
7768, 74, 76mulassd 11185 . . . . . . . . . . . . . . . 16 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ ((0 ยท (i ยท ((0 โˆ’โ„ ๐‘Ž) + 1))) ยท ๐‘ฅ) = (0 ยท ((i ยท ((0 โˆ’โ„ ๐‘Ž) + 1)) ยท ๐‘ฅ)))
7869, 73, 76mulassd 11185 . . . . . . . . . . . . . . . . . 18 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ ((i ยท ((0 โˆ’โ„ ๐‘Ž) + 1)) ยท ๐‘ฅ) = (i ยท (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ)))
79 simprr 772 . . . . . . . . . . . . . . . . . . . 20 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)
8079oveq2d 7378 . . . . . . . . . . . . . . . . . . 19 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ (i ยท (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ)) = (i ยท 1))
8180, 19eqtrdi 2793 . . . . . . . . . . . . . . . . . 18 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ (i ยท (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ)) = i)
8278, 81eqtrd 2777 . . . . . . . . . . . . . . . . 17 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ ((i ยท ((0 โˆ’โ„ ๐‘Ž) + 1)) ยท ๐‘ฅ) = i)
8382oveq2d 7378 . . . . . . . . . . . . . . . 16 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ (0 ยท ((i ยท ((0 โˆ’โ„ ๐‘Ž) + 1)) ยท ๐‘ฅ)) = (0 ยท i))
8477, 83eqtrd 2777 . . . . . . . . . . . . . . 15 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ ((0 ยท (i ยท ((0 โˆ’โ„ ๐‘Ž) + 1))) ยท ๐‘ฅ) = (0 ยท i))
85 remul02 40903 . . . . . . . . . . . . . . . 16 (๐‘ฅ โˆˆ โ„ โ†’ (0 ยท ๐‘ฅ) = 0)
8675, 85syl 17 . . . . . . . . . . . . . . 15 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ (0 ยท ๐‘ฅ) = 0)
8767, 84, 863eqtr3d 2785 . . . . . . . . . . . . . 14 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (((0 โˆ’โ„ ๐‘Ž) + 1) ยท ๐‘ฅ) = 1)) โ†’ (0 ยท i) = 0)
8814, 87rexlimddv 3159 . . . . . . . . . . . . 13 (((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง ((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0) โ†’ (0 ยท i) = 0)
8988ex 414 . . . . . . . . . . . 12 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (((0 โˆ’โ„ ๐‘Ž) + 1) โ‰  0 โ†’ (0 ยท i) = 0))
9089necon1d 2966 . . . . . . . . . . 11 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) โ‰  0 โ†’ ((0 โˆ’โ„ ๐‘Ž) + 1) = 0))
917, 90mpd 15 . . . . . . . . . 10 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 โˆ’โ„ ๐‘Ž) + 1) = 0)
9291oveq2d 7378 . . . . . . . . 9 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (๐‘Ž + ((0 โˆ’โ„ ๐‘Ž) + 1)) = (๐‘Ž + 0))
9331, 16, 17addassd 11184 . . . . . . . . . 10 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((๐‘Ž + (0 โˆ’โ„ ๐‘Ž)) + 1) = (๐‘Ž + ((0 โˆ’โ„ ๐‘Ž) + 1)))
94 renegid 40871 . . . . . . . . . . . . 13 (๐‘Ž โˆˆ โ„ โ†’ (๐‘Ž + (0 โˆ’โ„ ๐‘Ž)) = 0)
958, 94syl 17 . . . . . . . . . . . 12 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (๐‘Ž + (0 โˆ’โ„ ๐‘Ž)) = 0)
9695oveq1d 7377 . . . . . . . . . . 11 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((๐‘Ž + (0 โˆ’โ„ ๐‘Ž)) + 1) = (0 + 1))
97 readdid2 40901 . . . . . . . . . . . 12 (1 โˆˆ โ„ โ†’ (0 + 1) = 1)
9854, 97ax-mp 5 . . . . . . . . . . 11 (0 + 1) = 1
9996, 98eqtrdi 2793 . . . . . . . . . 10 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((๐‘Ž + (0 โˆ’โ„ ๐‘Ž)) + 1) = 1)
10093, 99eqtr3d 2779 . . . . . . . . 9 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (๐‘Ž + ((0 โˆ’โ„ ๐‘Ž) + 1)) = 1)
101 readdid1 40907 . . . . . . . . . 10 (๐‘Ž โˆˆ โ„ โ†’ (๐‘Ž + 0) = ๐‘Ž)
1028, 101syl 17 . . . . . . . . 9 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (๐‘Ž + 0) = ๐‘Ž)
10392, 100, 1023eqtr3rd 2786 . . . . . . . 8 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ๐‘Ž = 1)
104 rernegcl 40869 . . . . . . . . . . . . . . . . . 18 (๐‘ โˆˆ โ„ โ†’ (0 โˆ’โ„ ๐‘) โˆˆ โ„)
10532, 104syl 17 . . . . . . . . . . . . . . . . 17 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 โˆ’โ„ ๐‘) โˆˆ โ„)
10611, 105readdcld 11191 . . . . . . . . . . . . . . . 16 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (1 + (0 โˆ’โ„ ๐‘)) โˆˆ โ„)
107 ax-rrecex 11130 . . . . . . . . . . . . . . . 16 (((1 + (0 โˆ’โ„ ๐‘)) โˆˆ โ„ โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)
108106, 107sylan 581 . . . . . . . . . . . . . . 15 (((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)
109105recnd 11190 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 โˆ’โ„ ๐‘) โˆˆ โ„‚)
11015, 109mulcld 11182 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท (0 โˆ’โ„ ๐‘)) โˆˆ โ„‚)
11123, 15, 110adddid 11186 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท (i + (i ยท (0 โˆ’โ„ ๐‘)))) = ((0 ยท i) + (0 ยท (i ยท (0 โˆ’โ„ ๐‘)))))
112 0re 11164 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 โˆˆ โ„
113 remul02 40903 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 โˆˆ โ„ โ†’ (0 ยท 0) = 0)
114112, 113ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ยท 0) = 0
115114oveq1i 7372 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 ยท 0) ยท i) = (0 ยท i)
1161, 1, 2mulassi 11173 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 ยท 0) ยท i) = (0 ยท (0 ยท i))
117115, 116eqtr3i 2767 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ยท i) = (0 ยท (0 ยท i))
118117a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท i) = (0 ยท (0 ยท i)))
119118oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) + (0 ยท (i ยท (0 โˆ’โ„ ๐‘)))) = ((0 ยท (0 ยท i)) + (0 ยท (i ยท (0 โˆ’โ„ ๐‘)))))
120111, 119eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท (i + (i ยท (0 โˆ’โ„ ๐‘)))) = ((0 ยท (0 ยท i)) + (0 ยท (i ยท (0 โˆ’โ„ ๐‘)))))
12115, 17, 109adddid 11186 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท (1 + (0 โˆ’โ„ ๐‘))) = ((i ยท 1) + (i ยท (0 โˆ’โ„ ๐‘))))
12219a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท 1) = i)
123122oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((i ยท 1) + (i ยท (0 โˆ’โ„ ๐‘))) = (i + (i ยท (0 โˆ’โ„ ๐‘))))
124121, 123eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท (1 + (0 โˆ’โ„ ๐‘))) = (i + (i ยท (0 โˆ’โ„ ๐‘))))
125124oveq2d 7378 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท (i ยท (1 + (0 โˆ’โ„ ๐‘)))) = (0 ยท (i + (i ยท (0 โˆ’โ„ ๐‘)))))
12623, 41, 110adddid 11186 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท ((0 ยท i) + (i ยท (0 โˆ’โ„ ๐‘)))) = ((0 ยท (0 ยท i)) + (0 ยท (i ยท (0 โˆ’โ„ ๐‘)))))
127120, 125, 1263eqtr4d 2787 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท (i ยท (1 + (0 โˆ’โ„ ๐‘)))) = (0 ยท ((0 ยท i) + (i ยท (0 โˆ’โ„ ๐‘)))))
128103oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (๐‘Ž + (i ยท ๐‘)) = (1 + (i ยท ๐‘)))
1295, 128eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท i) = (1 + (i ยท ๐‘)))
130129oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) + (i ยท (0 โˆ’โ„ ๐‘))) = ((1 + (i ยท ๐‘)) + (i ยท (0 โˆ’โ„ ๐‘))))
13117, 34, 110addassd 11184 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((1 + (i ยท ๐‘)) + (i ยท (0 โˆ’โ„ ๐‘))) = (1 + ((i ยท ๐‘) + (i ยท (0 โˆ’โ„ ๐‘)))))
132 renegid 40871 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ โˆˆ โ„ โ†’ (๐‘ + (0 โˆ’โ„ ๐‘)) = 0)
13332, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (๐‘ + (0 โˆ’โ„ ๐‘)) = 0)
134133oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท (๐‘ + (0 โˆ’โ„ ๐‘))) = (i ยท 0))
13515, 33, 109adddid 11186 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท (๐‘ + (0 โˆ’โ„ ๐‘))) = ((i ยท ๐‘) + (i ยท (0 โˆ’โ„ ๐‘))))
136 sn-mul01 40923 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (i โˆˆ โ„‚ โ†’ (i ยท 0) = 0)
1372, 136mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท 0) = 0)
138134, 135, 1373eqtr3d 2785 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((i ยท ๐‘) + (i ยท (0 โˆ’โ„ ๐‘))) = 0)
139138oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (1 + ((i ยท ๐‘) + (i ยท (0 โˆ’โ„ ๐‘)))) = (1 + 0))
140 readdid1 40907 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 โˆˆ โ„ โ†’ (1 + 0) = 1)
14154, 140ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 0) = 1
142139, 141eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (1 + ((i ยท ๐‘) + (i ยท (0 โˆ’โ„ ๐‘)))) = 1)
143131, 142eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((1 + (i ยท ๐‘)) + (i ยท (0 โˆ’โ„ ๐‘))) = 1)
144130, 143eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) + (i ยท (0 โˆ’โ„ ๐‘))) = 1)
145144oveq2d 7378 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท ((0 ยท i) + (i ยท (0 โˆ’โ„ ๐‘)))) = (0 ยท 1))
146127, 145eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท (i ยท (1 + (0 โˆ’โ„ ๐‘)))) = (0 ยท 1))
147 ax-1rid 11128 . . . . . . . . . . . . . . . . . . . 20 (0 โˆˆ โ„ โ†’ (0 ยท 1) = 0)
148112, 147ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (0 ยท 1) = 0
149146, 148eqtrdi 2793 . . . . . . . . . . . . . . . . . 18 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท (i ยท (1 + (0 โˆ’โ„ ๐‘)))) = 0)
150149ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ (0 ยท (i ยท (1 + (0 โˆ’โ„ ๐‘)))) = 0)
151150oveq1d 7377 . . . . . . . . . . . . . . . 16 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ ((0 ยท (i ยท (1 + (0 โˆ’โ„ ๐‘)))) ยท ๐‘ฆ) = (0 ยท ๐‘ฆ))
152 0cnd 11155 . . . . . . . . . . . . . . . . . 18 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ 0 โˆˆ โ„‚)
1532a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ i โˆˆ โ„‚)
154 1cnd 11157 . . . . . . . . . . . . . . . . . . . 20 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ 1 โˆˆ โ„‚)
155109ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ (0 โˆ’โ„ ๐‘) โˆˆ โ„‚)
156154, 155addcld 11181 . . . . . . . . . . . . . . . . . . 19 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ (1 + (0 โˆ’โ„ ๐‘)) โˆˆ โ„‚)
157153, 156mulcld 11182 . . . . . . . . . . . . . . . . . 18 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ (i ยท (1 + (0 โˆ’โ„ ๐‘))) โˆˆ โ„‚)
158 simprl 770 . . . . . . . . . . . . . . . . . . 19 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ ๐‘ฆ โˆˆ โ„)
159158recnd 11190 . . . . . . . . . . . . . . . . . 18 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ ๐‘ฆ โˆˆ โ„‚)
160152, 157, 159mulassd 11185 . . . . . . . . . . . . . . . . 17 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ ((0 ยท (i ยท (1 + (0 โˆ’โ„ ๐‘)))) ยท ๐‘ฆ) = (0 ยท ((i ยท (1 + (0 โˆ’โ„ ๐‘))) ยท ๐‘ฆ)))
161153, 156, 159mulassd 11185 . . . . . . . . . . . . . . . . . . 19 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ ((i ยท (1 + (0 โˆ’โ„ ๐‘))) ยท ๐‘ฆ) = (i ยท ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ)))
162 simprr 772 . . . . . . . . . . . . . . . . . . . . 21 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)
163162oveq2d 7378 . . . . . . . . . . . . . . . . . . . 20 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ (i ยท ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ)) = (i ยท 1))
164163, 19eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ (i ยท ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ)) = i)
165161, 164eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ ((i ยท (1 + (0 โˆ’โ„ ๐‘))) ยท ๐‘ฆ) = i)
166165oveq2d 7378 . . . . . . . . . . . . . . . . 17 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ (0 ยท ((i ยท (1 + (0 โˆ’โ„ ๐‘))) ยท ๐‘ฆ)) = (0 ยท i))
167160, 166eqtrd 2777 . . . . . . . . . . . . . . . 16 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ ((0 ยท (i ยท (1 + (0 โˆ’โ„ ๐‘)))) ยท ๐‘ฆ) = (0 ยท i))
168 remul02 40903 . . . . . . . . . . . . . . . . 17 (๐‘ฆ โˆˆ โ„ โ†’ (0 ยท ๐‘ฆ) = 0)
169158, 168syl 17 . . . . . . . . . . . . . . . 16 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ (0 ยท ๐‘ฆ) = 0)
170151, 167, 1693eqtr3d 2785 . . . . . . . . . . . . . . 15 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง ((1 + (0 โˆ’โ„ ๐‘)) ยท ๐‘ฆ) = 1)) โ†’ (0 ยท i) = 0)
171108, 170rexlimddv 3159 . . . . . . . . . . . . . 14 (((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โˆง (1 + (0 โˆ’โ„ ๐‘)) โ‰  0) โ†’ (0 ยท i) = 0)
172171ex 414 . . . . . . . . . . . . 13 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((1 + (0 โˆ’โ„ ๐‘)) โ‰  0 โ†’ (0 ยท i) = 0))
173172necon1d 2966 . . . . . . . . . . . 12 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 ยท i) โ‰  0 โ†’ (1 + (0 โˆ’โ„ ๐‘)) = 0))
1747, 173mpd 15 . . . . . . . . . . 11 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (1 + (0 โˆ’โ„ ๐‘)) = 0)
175174oveq1d 7377 . . . . . . . . . 10 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((1 + (0 โˆ’โ„ ๐‘)) + ๐‘) = (0 + ๐‘))
17617, 109, 33addassd 11184 . . . . . . . . . . 11 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((1 + (0 โˆ’โ„ ๐‘)) + ๐‘) = (1 + ((0 โˆ’โ„ ๐‘) + ๐‘)))
177 renegid2 40911 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„ โ†’ ((0 โˆ’โ„ ๐‘) + ๐‘) = 0)
17832, 177syl 17 . . . . . . . . . . . . 13 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((0 โˆ’โ„ ๐‘) + ๐‘) = 0)
179178oveq2d 7378 . . . . . . . . . . . 12 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (1 + ((0 โˆ’โ„ ๐‘) + ๐‘)) = (1 + 0))
180179, 141eqtrdi 2793 . . . . . . . . . . 11 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (1 + ((0 โˆ’โ„ ๐‘) + ๐‘)) = 1)
181176, 180eqtrd 2777 . . . . . . . . . 10 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ((1 + (0 โˆ’โ„ ๐‘)) + ๐‘) = 1)
182 readdid2 40901 . . . . . . . . . . 11 (๐‘ โˆˆ โ„ โ†’ (0 + ๐‘) = ๐‘)
18332, 182syl 17 . . . . . . . . . 10 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 + ๐‘) = ๐‘)
184175, 181, 1833eqtr3rd 2786 . . . . . . . . 9 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ ๐‘ = 1)
185184oveq2d 7378 . . . . . . . 8 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (i ยท ๐‘) = (i ยท 1))
186103, 185oveq12d 7380 . . . . . . 7 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (๐‘Ž + (i ยท ๐‘)) = (1 + (i ยท 1)))
1875, 186eqtrd 2777 . . . . . 6 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท i) = (1 + (i ยท 1)))
18819oveq2i 7373 . . . . . . . . 9 (1 + (i ยท 1)) = (1 + i)
189188eqeq2i 2750 . . . . . . . 8 ((0 ยท i) = (1 + (i ยท 1)) โ†” (0 ยท i) = (1 + i))
190 oveq2 7370 . . . . . . . . . 10 ((0 ยท i) = (1 + i) โ†’ (((i ยท i) ยท i) ยท (0 ยท i)) = (((i ยท i) ยท i) ยท (1 + i)))
1912, 2mulcli 11169 . . . . . . . . . . . . 13 (i ยท i) โˆˆ โ„‚
192191, 2mulcli 11169 . . . . . . . . . . . 12 ((i ยท i) ยท i) โˆˆ โ„‚
193192, 1, 2mulassi 11173 . . . . . . . . . . 11 ((((i ยท i) ยท i) ยท 0) ยท i) = (((i ยท i) ยท i) ยท (0 ยท i))
194 sn-mul01 40923 . . . . . . . . . . . . 13 (((i ยท i) ยท i) โˆˆ โ„‚ โ†’ (((i ยท i) ยท i) ยท 0) = 0)
195192, 194ax-mp 5 . . . . . . . . . . . 12 (((i ยท i) ยท i) ยท 0) = 0
196195oveq1i 7372 . . . . . . . . . . 11 ((((i ยท i) ยท i) ยท 0) ยท i) = (0 ยท i)
197193, 196eqtr3i 2767 . . . . . . . . . 10 (((i ยท i) ยท i) ยท (0 ยท i)) = (0 ยท i)
198 ax-1cn 11116 . . . . . . . . . . . 12 1 โˆˆ โ„‚
199192, 198, 2adddii 11174 . . . . . . . . . . 11 (((i ยท i) ยท i) ยท (1 + i)) = ((((i ยท i) ยท i) ยท 1) + (((i ยท i) ยท i) ยท i))
200191, 2, 198mulassi 11173 . . . . . . . . . . . . 13 (((i ยท i) ยท i) ยท 1) = ((i ยท i) ยท (i ยท 1))
20119oveq2i 7373 . . . . . . . . . . . . 13 ((i ยท i) ยท (i ยท 1)) = ((i ยท i) ยท i)
202200, 201eqtri 2765 . . . . . . . . . . . 12 (((i ยท i) ยท i) ยท 1) = ((i ยท i) ยท i)
203191, 2, 2mulassi 11173 . . . . . . . . . . . . 13 (((i ยท i) ยท i) ยท i) = ((i ยท i) ยท (i ยท i))
204 rei4 40921 . . . . . . . . . . . . 13 ((i ยท i) ยท (i ยท i)) = 1
205203, 204eqtri 2765 . . . . . . . . . . . 12 (((i ยท i) ยท i) ยท i) = 1
206202, 205oveq12i 7374 . . . . . . . . . . 11 ((((i ยท i) ยท i) ยท 1) + (((i ยท i) ยท i) ยท i)) = (((i ยท i) ยท i) + 1)
207199, 206eqtri 2765 . . . . . . . . . 10 (((i ยท i) ยท i) ยท (1 + i)) = (((i ยท i) ยท i) + 1)
208190, 197, 2073eqtr3g 2800 . . . . . . . . 9 ((0 ยท i) = (1 + i) โ†’ (0 ยท i) = (((i ยท i) ยท i) + 1))
20954, 54readdcli 11177 . . . . . . . . . . 11 (1 + 1) โˆˆ โ„
210 df-2 12223 . . . . . . . . . . . 12 2 = (1 + 1)
211 sn-0ne2 40904 . . . . . . . . . . . . 13 0 โ‰  2
212211necomi 2999 . . . . . . . . . . . 12 2 โ‰  0
213210, 212eqnetrri 3016 . . . . . . . . . . 11 (1 + 1) โ‰  0
214 ax-rrecex 11130 . . . . . . . . . . 11 (((1 + 1) โˆˆ โ„ โˆง (1 + 1) โ‰  0) โ†’ โˆƒ๐‘ง โˆˆ โ„ ((1 + 1) ยท ๐‘ง) = 1)
215209, 213, 214mp2an 691 . . . . . . . . . 10 โˆƒ๐‘ง โˆˆ โ„ ((1 + 1) ยท ๐‘ง) = 1
216192, 198addcli 11168 . . . . . . . . . . . . . . . . . 18 (((i ยท i) ยท i) + 1) โˆˆ โ„‚
217198, 2, 216addassi 11172 . . . . . . . . . . . . . . . . 17 ((1 + i) + (((i ยท i) ยท i) + 1)) = (1 + (i + (((i ยท i) ยท i) + 1)))
2182, 192, 198addassi 11172 . . . . . . . . . . . . . . . . . 18 ((i + ((i ยท i) ยท i)) + 1) = (i + (((i ยท i) ยท i) + 1))
219218oveq2i 7373 . . . . . . . . . . . . . . . . 17 (1 + ((i + ((i ยท i) ยท i)) + 1)) = (1 + (i + (((i ยท i) ยท i) + 1)))
2202, 2, 2mulassi 11173 . . . . . . . . . . . . . . . . . . . . . 22 ((i ยท i) ยท i) = (i ยท (i ยท i))
221220oveq2i 7373 . . . . . . . . . . . . . . . . . . . . 21 (i + ((i ยท i) ยท i)) = (i + (i ยท (i ยท i)))
222 ipiiie0 40935 . . . . . . . . . . . . . . . . . . . . 21 (i + (i ยท (i ยท i))) = 0
223221, 222eqtri 2765 . . . . . . . . . . . . . . . . . . . 20 (i + ((i ยท i) ยท i)) = 0
224223oveq1i 7372 . . . . . . . . . . . . . . . . . . 19 ((i + ((i ยท i) ยท i)) + 1) = (0 + 1)
225224, 98eqtri 2765 . . . . . . . . . . . . . . . . . 18 ((i + ((i ยท i) ยท i)) + 1) = 1
226225oveq2i 7373 . . . . . . . . . . . . . . . . 17 (1 + ((i + ((i ยท i) ยท i)) + 1)) = (1 + 1)
227217, 219, 2263eqtr2i 2771 . . . . . . . . . . . . . . . 16 ((1 + i) + (((i ยท i) ยท i) + 1)) = (1 + 1)
228227a1i 11 . . . . . . . . . . . . . . 15 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ ((1 + i) + (((i ยท i) ยท i) + 1)) = (1 + 1))
2293, 198, 198adddii 11174 . . . . . . . . . . . . . . . 16 ((0 ยท i) ยท (1 + 1)) = (((0 ยท i) ยท 1) + ((0 ยท i) ยท 1))
2301, 2, 198mulassi 11173 . . . . . . . . . . . . . . . . . . 19 ((0 ยท i) ยท 1) = (0 ยท (i ยท 1))
23119oveq2i 7373 . . . . . . . . . . . . . . . . . . 19 (0 ยท (i ยท 1)) = (0 ยท i)
232230, 231eqtri 2765 . . . . . . . . . . . . . . . . . 18 ((0 ยท i) ยท 1) = (0 ยท i)
233 simpl 484 . . . . . . . . . . . . . . . . . 18 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ (0 ยท i) = (1 + i))
234232, 233eqtrid 2789 . . . . . . . . . . . . . . . . 17 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ ((0 ยท i) ยท 1) = (1 + i))
235 simpr 486 . . . . . . . . . . . . . . . . . 18 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ (0 ยท i) = (((i ยท i) ยท i) + 1))
236232, 235eqtrid 2789 . . . . . . . . . . . . . . . . 17 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ ((0 ยท i) ยท 1) = (((i ยท i) ยท i) + 1))
237234, 236oveq12d 7380 . . . . . . . . . . . . . . . 16 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ (((0 ยท i) ยท 1) + ((0 ยท i) ยท 1)) = ((1 + i) + (((i ยท i) ยท i) + 1)))
238229, 237eqtrid 2789 . . . . . . . . . . . . . . 15 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ ((0 ยท i) ยท (1 + 1)) = ((1 + i) + (((i ยท i) ยท i) + 1)))
239 remulid2 40931 . . . . . . . . . . . . . . . 16 ((1 + 1) โˆˆ โ„ โ†’ (1 ยท (1 + 1)) = (1 + 1))
240209, 239mp1i 13 . . . . . . . . . . . . . . 15 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ (1 ยท (1 + 1)) = (1 + 1))
241228, 238, 2403eqtr4d 2787 . . . . . . . . . . . . . 14 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ ((0 ยท i) ยท (1 + 1)) = (1 ยท (1 + 1)))
242241oveq1d 7377 . . . . . . . . . . . . 13 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ (((0 ยท i) ยท (1 + 1)) ยท ๐‘ง) = ((1 ยท (1 + 1)) ยท ๐‘ง))
243242adantr 482 . . . . . . . . . . . 12 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ (((0 ยท i) ยท (1 + 1)) ยท ๐‘ง) = ((1 ยท (1 + 1)) ยท ๐‘ง))
2443a1i 11 . . . . . . . . . . . . . 14 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ (0 ยท i) โˆˆ โ„‚)
245 1cnd 11157 . . . . . . . . . . . . . . 15 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ 1 โˆˆ โ„‚)
246245, 245addcld 11181 . . . . . . . . . . . . . 14 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ (1 + 1) โˆˆ โ„‚)
247 simprl 770 . . . . . . . . . . . . . . 15 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ ๐‘ง โˆˆ โ„)
248247recnd 11190 . . . . . . . . . . . . . 14 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ ๐‘ง โˆˆ โ„‚)
249244, 246, 248mulassd 11185 . . . . . . . . . . . . 13 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ (((0 ยท i) ยท (1 + 1)) ยท ๐‘ง) = ((0 ยท i) ยท ((1 + 1) ยท ๐‘ง)))
250 simprr 772 . . . . . . . . . . . . . . 15 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ ((1 + 1) ยท ๐‘ง) = 1)
251250oveq2d 7378 . . . . . . . . . . . . . 14 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ ((0 ยท i) ยท ((1 + 1) ยท ๐‘ง)) = ((0 ยท i) ยท 1))
252251, 232eqtrdi 2793 . . . . . . . . . . . . 13 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ ((0 ยท i) ยท ((1 + 1) ยท ๐‘ง)) = (0 ยท i))
253249, 252eqtrd 2777 . . . . . . . . . . . 12 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ (((0 ยท i) ยท (1 + 1)) ยท ๐‘ง) = (0 ยท i))
254245, 246, 248mulassd 11185 . . . . . . . . . . . . 13 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ ((1 ยท (1 + 1)) ยท ๐‘ง) = (1 ยท ((1 + 1) ยท ๐‘ง)))
255250oveq2d 7378 . . . . . . . . . . . . . 14 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ (1 ยท ((1 + 1) ยท ๐‘ง)) = (1 ยท 1))
256 1t1e1ALT 40807 . . . . . . . . . . . . . 14 (1 ยท 1) = 1
257255, 256eqtrdi 2793 . . . . . . . . . . . . 13 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ (1 ยท ((1 + 1) ยท ๐‘ง)) = 1)
258254, 257eqtrd 2777 . . . . . . . . . . . 12 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ ((1 ยท (1 + 1)) ยท ๐‘ง) = 1)
259243, 253, 2583eqtr3d 2785 . . . . . . . . . . 11 ((((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โˆง (๐‘ง โˆˆ โ„ โˆง ((1 + 1) ยท ๐‘ง) = 1)) โ†’ (0 ยท i) = 1)
260259rexlimdvaa 3154 . . . . . . . . . 10 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ (โˆƒ๐‘ง โˆˆ โ„ ((1 + 1) ยท ๐‘ง) = 1 โ†’ (0 ยท i) = 1))
261215, 260mpi 20 . . . . . . . . 9 (((0 ยท i) = (1 + i) โˆง (0 ยท i) = (((i ยท i) ยท i) + 1)) โ†’ (0 ยท i) = 1)
262208, 261mpdan 686 . . . . . . . 8 ((0 ยท i) = (1 + i) โ†’ (0 ยท i) = 1)
263189, 262sylbi 216 . . . . . . 7 ((0 ยท i) = (1 + (i ยท 1)) โ†’ (0 ยท i) = 1)
264 oveq2 7370 . . . . . . . 8 ((0 ยท i) = 1 โ†’ (0 ยท (0 ยท i)) = (0 ยท 1))
265116, 115eqtr3i 2767 . . . . . . . 8 (0 ยท (0 ยท i)) = (0 ยท i)
266264, 265, 1483eqtr3g 2800 . . . . . . 7 ((0 ยท i) = 1 โ†’ (0 ยท i) = 0)
267263, 266syl 17 . . . . . 6 ((0 ยท i) = (1 + (i ยท 1)) โ†’ (0 ยท i) = 0)
268187, 267syl 17 . . . . 5 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โˆง ยฌ (0 ยท i) = 0) โ†’ (0 ยท i) = 0)
269268pm2.18da 799 . . . 4 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (0 ยท i) = (๐‘Ž + (i ยท ๐‘))) โ†’ (0 ยท i) = 0)
270269ex 414 . . 3 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((0 ยท i) = (๐‘Ž + (i ยท ๐‘)) โ†’ (0 ยท i) = 0))
271270rexlimivv 3197 . 2 (โˆƒ๐‘Ž โˆˆ โ„ โˆƒ๐‘ โˆˆ โ„ (0 ยท i) = (๐‘Ž + (i ยท ๐‘)) โ†’ (0 ยท i) = 0)
2723, 4, 271mp2b 10 1 (0 ยท i) = 0
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆƒwrex 3074  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059  ici 11060   + caddc 11061   ยท cmul 11063  2c2 12215   โˆ’โ„ cresub 40863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11198  df-mnf 11199  df-ltxr 11201  df-2 12223  df-3 12224  df-resub 40864
This theorem is referenced by:  sn-mul02  40938  retire  40965
  Copyright terms: Public domain W3C validator