absext - Intuitionistic Logic Explorer

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

Theorem absext 11407

Description: Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.)

**Assertion**
Ref	Expression
absext	$/\$ # #

**Proof of Theorem absext**
Step	Hyp	Ref	Expression
1		absval2 11401	. . . . . . 7
2		absval2 11401	. . . . . . 7
3	1, 2	breqan12d 4061	. . . . . 6 $/\$ # #
4		simpl 109	. . . . . . . . . 10 $/\$
5	4	recld 11282	. . . . . . . . 9 $/\$
6	5	resqcld 10846	. . . . . . . 8 $/\$
7	4	imcld 11283	. . . . . . . . 9 $/\$
8	7	resqcld 10846	. . . . . . . 8 $/\$
9	6, 8	readdcld 8104	. . . . . . 7 $/\$
10	5	sqge0d 10847	. . . . . . . 8 $/\$
11	7	sqge0d 10847	. . . . . . . 8 $/\$
12	6, 8, 10, 11	addge0d 8597	. . . . . . 7 $/\$
13		simpr 110	. . . . . . . . . 10 $/\$
14	13	recld 11282	. . . . . . . . 9 $/\$
15	14	resqcld 10846	. . . . . . . 8 $/\$
16	13	imcld 11283	. . . . . . . . 9 $/\$
17	16	resqcld 10846	. . . . . . . 8 $/\$
18	15, 17	readdcld 8104	. . . . . . 7 $/\$
19	14	sqge0d 10847	. . . . . . . 8 $/\$
20	16	sqge0d 10847	. . . . . . . 8 $/\$
21	15, 17, 19, 20	addge0d 8597	. . . . . . 7 $/\$
22		sqrt11ap 11382	. . . . . . 7 $/\$ $/\$ $/\$ # #
23	9, 12, 18, 21, 22	syl22anc 1251	. . . . . 6 $/\$ # #
24	3, 23	bitrd 188	. . . . 5 $/\$ # #
25	6	recnd 8103	. . . . . 6 $/\$
26	8	recnd 8103	. . . . . 6 $/\$
27	15	recnd 8103	. . . . . 6 $/\$
28	17	recnd 8103	. . . . . 6 $/\$
29		addext 8685	. . . . . 6 $/\$ $/\$ $/\$ # # $\/$ #
30	25, 26, 27, 28, 29	syl22anc 1251	. . . . 5 $/\$ # # $\/$ #
31	24, 30	sylbid 150	. . . 4 $/\$ # # $\/$ #
32	5	recnd 8103	. . . . . . . . 9 $/\$
33	32	sqvald 10817	. . . . . . . 8 $/\$
34	14	recnd 8103	. . . . . . . . 9 $/\$
35	34	sqvald 10817	. . . . . . . 8 $/\$
36	33, 35	breq12d 4058	. . . . . . 7 $/\$ # #
37		mulext 8689	. . . . . . . 8 $/\$ $/\$ $/\$ # # $\/$ #
38	32, 32, 34, 34, 37	syl22anc 1251	. . . . . . 7 $/\$ # # $\/$ #
39	36, 38	sylbid 150	. . . . . 6 $/\$ # # $\/$ #
40		oridm 759	. . . . . 6 # $\/$ # #
41	39, 40	imbitrdi 161	. . . . 5 $/\$ # #
42	7	recnd 8103	. . . . . . . . 9 $/\$
43	42	sqvald 10817	. . . . . . . 8 $/\$
44	16	recnd 8103	. . . . . . . . 9 $/\$
45	44	sqvald 10817	. . . . . . . 8 $/\$
46	43, 45	breq12d 4058	. . . . . . 7 $/\$ # #
47		mulext 8689	. . . . . . . 8 $/\$ $/\$ $/\$ # # $\/$ #
48	42, 42, 44, 44, 47	syl22anc 1251	. . . . . . 7 $/\$ # # $\/$ #
49	46, 48	sylbid 150	. . . . . 6 $/\$ # # $\/$ #
50		oridm 759	. . . . . 6 # $\/$ # #
51	49, 50	imbitrdi 161	. . . . 5 $/\$ # #
52	41, 51	orim12d 788	. . . 4 $/\$ # $\/$ # # $\/$ #
53	31, 52	syld 45	. . 3 $/\$ # # $\/$ #
54		apreim 8678	. . . 4 $/\$ $/\$ $/\$ # # $\/$ #
55	5, 7, 14, 16, 54	syl22anc 1251	. . 3 $/\$ # # $\/$ #
56	53, 55	sylibrd 169	. 2 $/\$ # #
57	4	replimd 11285	. . 3 $/\$
58	13	replimd 11285	. . 3 $/\$
59	57, 58	breq12d 4058	. 2 $/\$ # #
60	56, 59	sylibrd 169	1 $/\$ # #

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 710

wcel 2176 class class class wbr 4045

cfv 5272 (class class class)co 5946

cc 7925

cr 7926

cc0 7927

ci 7929

caddc 7930

cmul 7932

cle 8110 # cap 8656

c2 9089

cexp 10685

cre 11184

cim 11185

csqrt 11340

cabs 11341

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 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-coll 4160 ax-sep 4163 ax-nul 4171 ax-pow 4219 ax-pr 4254 ax-un 4481 ax-setind 4586 ax-iinf 4637 ax-cnex 8018 ax-resscn 8019 ax-1cn 8020 ax-1re 8021 ax-icn 8022 ax-addcl 8023 ax-addrcl 8024 ax-mulcl 8025 ax-mulrcl 8026 ax-addcom 8027 ax-mulcom 8028 ax-addass 8029 ax-mulass 8030 ax-distr 8031 ax-i2m1 8032 ax-0lt1 8033 ax-1rid 8034 ax-0id 8035 ax-rnegex 8036 ax-precex 8037 ax-cnre 8038 ax-pre-ltirr 8039 ax-pre-ltwlin 8040 ax-pre-lttrn 8041 ax-pre-apti 8042 ax-pre-ltadd 8043 ax-pre-mulgt0 8044 ax-pre-mulext 8045 ax-arch 8046 ax-caucvg 8047

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-nel 2472 df-ral 2489 df-rex 2490 df-reu 2491 df-rmo 2492 df-rab 2493 df-v 2774 df-sbc 2999 df-csb 3094 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-if 3572 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-iun 3929 df-br 4046 df-opab 4107 df-mpt 4108 df-tr 4144 df-id 4341 df-po 4344 df-iso 4345 df-iord 4414 df-on 4416 df-ilim 4417 df-suc 4419 df-iom 4640 df-xp 4682 df-rel 4683 df-cnv 4684 df-co 4685 df-dm 4686 df-rn 4687 df-res 4688 df-ima 4689 df-iota 5233 df-fun 5274 df-fn 5275 df-f 5276 df-f1 5277 df-fo 5278 df-f1o 5279 df-fv 5280 df-riota 5901 df-ov 5949 df-oprab 5950 df-mpo 5951 df-1st 6228 df-2nd 6229 df-recs 6393 df-frec 6479 df-pnf 8111 df-mnf 8112 df-xr 8113 df-ltxr 8114 df-le 8115 df-sub 8247 df-neg 8248 df-reap 8650 df-ap 8657 df-div 8748 df-inn 9039 df-2 9097 df-3 9098 df-4 9099 df-n0 9298 df-z 9375 df-uz 9651 df-rp 9778 df-seqfrec 10595 df-exp 10686 df-cj 11186 df-re 11187 df-im 11188 df-rsqrt 11342 df-abs 11343

This theorem is referenced by: abssubap0 11434 absltap 11853 absgtap 11854 apdifflemr 16023

W3C validator