ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  recexap GIF version

Theorem recexap 8609
Description: Existence of reciprocal of nonzero complex number. (Contributed by Jim Kingdon, 20-Feb-2020.)
Assertion
Ref Expression
recexap ((๐ด โˆˆ โ„‚ โˆง ๐ด # 0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด ยท ๐‘ฅ) = 1)
Distinct variable group:   ๐‘ฅ,๐ด

Proof of Theorem recexap
Dummy variables ๐‘ฆ ๐‘Ž ๐‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnre 7952 . . 3 (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘Ž โˆˆ โ„ โˆƒ๐‘ โˆˆ โ„ ๐ด = (๐‘Ž + (i ยท ๐‘)))
2 recexaplem2 8608 . . . . . . . . 9 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง (๐‘Ž + (i ยท ๐‘)) # 0) โ†’ ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) # 0)
323expia 1205 . . . . . . . 8 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘Ž + (i ยท ๐‘)) # 0 โ†’ ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) # 0))
4 remulcl 7938 . . . . . . . . . . . 12 ((๐‘Ž โˆˆ โ„ โˆง ๐‘Ž โˆˆ โ„) โ†’ (๐‘Ž ยท ๐‘Ž) โˆˆ โ„)
54anidms 397 . . . . . . . . . . 11 (๐‘Ž โˆˆ โ„ โ†’ (๐‘Ž ยท ๐‘Ž) โˆˆ โ„)
6 remulcl 7938 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (๐‘ ยท ๐‘) โˆˆ โ„)
76anidms 397 . . . . . . . . . . 11 (๐‘ โˆˆ โ„ โ†’ (๐‘ ยท ๐‘) โˆˆ โ„)
8 readdcl 7936 . . . . . . . . . . 11 (((๐‘Ž ยท ๐‘Ž) โˆˆ โ„ โˆง (๐‘ ยท ๐‘) โˆˆ โ„) โ†’ ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) โˆˆ โ„)
95, 7, 8syl2an 289 . . . . . . . . . 10 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) โˆˆ โ„)
10 0re 7956 . . . . . . . . . 10 0 โˆˆ โ„
11 apreap 8543 . . . . . . . . . 10 ((((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) # 0 โ†” ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) #โ„ 0))
129, 10, 11sylancl 413 . . . . . . . . 9 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) # 0 โ†” ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) #โ„ 0))
13 recexre 8534 . . . . . . . . . . . 12 ((((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) โˆˆ โ„ โˆง ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) #โ„ 0) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1)
149, 13sylan 283 . . . . . . . . . . 11 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) #โ„ 0) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1)
15 recn 7943 . . . . . . . . . . . . 13 (๐‘Ž โˆˆ โ„ โ†’ ๐‘Ž โˆˆ โ„‚)
16 recn 7943 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„ โ†’ ๐‘ โˆˆ โ„‚)
17 recn 7943 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„ โ†’ ๐‘ฆ โˆˆ โ„‚)
18 ax-icn 7905 . . . . . . . . . . . . . . . . . . . . 21 i โˆˆ โ„‚
19 mulcl 7937 . . . . . . . . . . . . . . . . . . . . 21 ((i โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (i ยท ๐‘) โˆˆ โ„‚)
2018, 19mpan 424 . . . . . . . . . . . . . . . . . . . 20 (๐‘ โˆˆ โ„‚ โ†’ (i ยท ๐‘) โˆˆ โ„‚)
21 subcl 8155 . . . . . . . . . . . . . . . . . . . 20 ((๐‘Ž โˆˆ โ„‚ โˆง (i ยท ๐‘) โˆˆ โ„‚) โ†’ (๐‘Ž โˆ’ (i ยท ๐‘)) โˆˆ โ„‚)
2220, 21sylan2 286 . . . . . . . . . . . . . . . . . . 19 ((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (๐‘Ž โˆ’ (i ยท ๐‘)) โˆˆ โ„‚)
23 mulcl 7937 . . . . . . . . . . . . . . . . . . 19 (((๐‘Ž โˆ’ (i ยท ๐‘)) โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ) โˆˆ โ„‚)
2422, 23sylan 283 . . . . . . . . . . . . . . . . . 18 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ) โˆˆ โ„‚)
2524adantr 276 . . . . . . . . . . . . . . . . 17 ((((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โˆง (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1) โ†’ ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ) โˆˆ โ„‚)
26 addcl 7935 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘Ž โˆˆ โ„‚ โˆง (i ยท ๐‘) โˆˆ โ„‚) โ†’ (๐‘Ž + (i ยท ๐‘)) โˆˆ โ„‚)
2720, 26sylan2 286 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (๐‘Ž + (i ยท ๐‘)) โˆˆ โ„‚)
2827adantr 276 . . . . . . . . . . . . . . . . . . . 20 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (๐‘Ž + (i ยท ๐‘)) โˆˆ โ„‚)
2922adantr 276 . . . . . . . . . . . . . . . . . . . 20 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (๐‘Ž โˆ’ (i ยท ๐‘)) โˆˆ โ„‚)
30 simpr 110 . . . . . . . . . . . . . . . . . . . 20 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ๐‘ฆ โˆˆ โ„‚)
3128, 29, 30mulassd 7980 . . . . . . . . . . . . . . . . . . 19 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (((๐‘Ž + (i ยท ๐‘)) ยท (๐‘Ž โˆ’ (i ยท ๐‘))) ยท ๐‘ฆ) = ((๐‘Ž + (i ยท ๐‘)) ยท ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ)))
32 recextlem1 8607 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ ((๐‘Ž + (i ยท ๐‘)) ยท (๐‘Ž โˆ’ (i ยท ๐‘))) = ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)))
3332adantr 276 . . . . . . . . . . . . . . . . . . . 20 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐‘Ž + (i ยท ๐‘)) ยท (๐‘Ž โˆ’ (i ยท ๐‘))) = ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)))
3433oveq1d 5889 . . . . . . . . . . . . . . . . . . 19 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (((๐‘Ž + (i ยท ๐‘)) ยท (๐‘Ž โˆ’ (i ยท ๐‘))) ยท ๐‘ฆ) = (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ))
3531, 34eqtr3d 2212 . . . . . . . . . . . . . . . . . 18 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐‘Ž + (i ยท ๐‘)) ยท ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ)) = (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ))
36 id 19 . . . . . . . . . . . . . . . . . 18 ((((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1 โ†’ (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1)
3735, 36sylan9eq 2230 . . . . . . . . . . . . . . . . 17 ((((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โˆง (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1) โ†’ ((๐‘Ž + (i ยท ๐‘)) ยท ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ)) = 1)
38 oveq2 5882 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ) โ†’ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = ((๐‘Ž + (i ยท ๐‘)) ยท ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ)))
3938eqeq1d 2186 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ) โ†’ (((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1 โ†” ((๐‘Ž + (i ยท ๐‘)) ยท ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ)) = 1))
4039rspcev 2841 . . . . . . . . . . . . . . . . 17 ((((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ((๐‘Ž + (i ยท ๐‘)) ยท ((๐‘Ž โˆ’ (i ยท ๐‘)) ยท ๐‘ฆ)) = 1) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1)
4125, 37, 40syl2anc 411 . . . . . . . . . . . . . . . 16 ((((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ฆ โˆˆ โ„‚) โˆง (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1)
4241exp31 364 . . . . . . . . . . . . . . 15 ((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (๐‘ฆ โˆˆ โ„‚ โ†’ ((((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1)))
4317, 42syl5 32 . . . . . . . . . . . . . 14 ((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (๐‘ฆ โˆˆ โ„ โ†’ ((((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1)))
4443rexlimdv 2593 . . . . . . . . . . . . 13 ((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (โˆƒ๐‘ฆ โˆˆ โ„ (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1))
4515, 16, 44syl2an 289 . . . . . . . . . . . 12 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (โˆƒ๐‘ฆ โˆˆ โ„ (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1))
4645adantr 276 . . . . . . . . . . 11 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) #โ„ 0) โ†’ (โˆƒ๐‘ฆ โˆˆ โ„ (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) ยท ๐‘ฆ) = 1 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1))
4714, 46mpd 13 . . . . . . . . . 10 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง ((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) #โ„ 0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1)
4847ex 115 . . . . . . . . 9 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) #โ„ 0 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1))
4912, 48sylbid 150 . . . . . . . 8 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (((๐‘Ž ยท ๐‘Ž) + (๐‘ ยท ๐‘)) # 0 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1))
503, 49syld 45 . . . . . . 7 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘Ž + (i ยท ๐‘)) # 0 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1))
5150adantr 276 . . . . . 6 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง ๐ด = (๐‘Ž + (i ยท ๐‘))) โ†’ ((๐‘Ž + (i ยท ๐‘)) # 0 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1))
52 breq1 4006 . . . . . . 7 (๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ (๐ด # 0 โ†” (๐‘Ž + (i ยท ๐‘)) # 0))
5352adantl 277 . . . . . 6 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง ๐ด = (๐‘Ž + (i ยท ๐‘))) โ†’ (๐ด # 0 โ†” (๐‘Ž + (i ยท ๐‘)) # 0))
54 oveq1 5881 . . . . . . . . 9 (๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ (๐ด ยท ๐‘ฅ) = ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ))
5554eqeq1d 2186 . . . . . . . 8 (๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ ((๐ด ยท ๐‘ฅ) = 1 โ†” ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1))
5655rexbidv 2478 . . . . . . 7 (๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด ยท ๐‘ฅ) = 1 โ†” โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1))
5756adantl 277 . . . . . 6 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง ๐ด = (๐‘Ž + (i ยท ๐‘))) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด ยท ๐‘ฅ) = 1 โ†” โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) ยท ๐‘ฅ) = 1))
5851, 53, 573imtr4d 203 . . . . 5 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง ๐ด = (๐‘Ž + (i ยท ๐‘))) โ†’ (๐ด # 0 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด ยท ๐‘ฅ) = 1))
5958ex 115 . . . 4 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ (๐ด # 0 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด ยท ๐‘ฅ) = 1)))
6059rexlimivv 2600 . . 3 (โˆƒ๐‘Ž โˆˆ โ„ โˆƒ๐‘ โˆˆ โ„ ๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ (๐ด # 0 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด ยท ๐‘ฅ) = 1))
611, 60syl 14 . 2 (๐ด โˆˆ โ„‚ โ†’ (๐ด # 0 โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด ยท ๐‘ฅ) = 1))
6261imp 124 1 ((๐ด โˆˆ โ„‚ โˆง ๐ด # 0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด ยท ๐‘ฅ) = 1)
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   = wceq 1353   โˆˆ wcel 2148  โˆƒwrex 2456   class class class wbr 4003  (class class class)co 5874  โ„‚cc 7808  โ„cr 7809  0cc0 7810  1c1 7811  ici 7812   + caddc 7813   ยท cmul 7815   โˆ’ cmin 8127   #โ„ creap 8530   # cap 8537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-precex 7920  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-apti 7925  ax-pre-ltadd 7926  ax-pre-mulgt0 7927  ax-pre-mulext 7928
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-id 4293  df-po 4296  df-iso 4297  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-iota 5178  df-fun 5218  df-fv 5224  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-reap 8531  df-ap 8538
This theorem is referenced by:  mulap0  8610  mulcanapd  8617  receuap  8625  recapb  8627
  Copyright terms: Public domain W3C validator