Metamath Proof Explorer

Theorem sgn3da

Description: A conditional containing a signum is true if it is true in all three possible cases. (Contributed by Thierry Arnoux, 1-Oct-2018)

Ref Expression
Hypotheses sgn3da.0 
|- ( ph -> A e. RR* )
sgn3da.1 
|- ( ( sgn ` A ) = 0 -> ( ps <-> ch ) )
sgn3da.2 
|- ( ( sgn ` A ) = 1 -> ( ps <-> th ) )
sgn3da.3 
|- ( ( sgn ` A ) = -u 1 -> ( ps <-> ta ) )
sgn3da.4 
|- ( ( ph /\ A = 0 ) -> ch )
sgn3da.5 
|- ( ( ph /\ 0 < A ) -> th )
sgn3da.6 
|- ( ( ph /\ A < 0 ) -> ta )
Assertion sgn3da 
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 sgn3da.0 
 |-  ( ph -> A e. RR* )
2 sgn3da.1 
 |-  ( ( sgn ` A ) = 0 -> ( ps <-> ch ) )
3 sgn3da.2 
 |-  ( ( sgn ` A ) = 1 -> ( ps <-> th ) )
4 sgn3da.3 
 |-  ( ( sgn ` A ) = -u 1 -> ( ps <-> ta ) )
5 sgn3da.4 
 |-  ( ( ph /\ A = 0 ) -> ch )
6 sgn3da.5 
 |-  ( ( ph /\ 0 < A ) -> th )
7 sgn3da.6 
 |-  ( ( ph /\ A < 0 ) -> ta )
8 sgnval 
 |-  ( A e. RR* -> ( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )
9 1 8 syl 
 |-  ( ph -> ( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )
10 9 eqeq2d 
 |-  ( ph -> ( 0 = ( sgn ` A ) <-> 0 = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) ) )
11 10 pm5.32i 
 |-  ( ( ph /\ 0 = ( sgn ` A ) ) <-> ( ph /\ 0 = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) ) )
12 2 eqcoms 
 |-  ( 0 = ( sgn ` A ) -> ( ps <-> ch ) )
13 12 bicomd 
 |-  ( 0 = ( sgn ` A ) -> ( ch <-> ps ) )
14 13 adantl 
 |-  ( ( ph /\ 0 = ( sgn ` A ) ) -> ( ch <-> ps ) )
15 11 14 sylbir 
 |-  ( ( ph /\ 0 = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) ) -> ( ch <-> ps ) )
16 15 expcom 
 |-  ( 0 = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) -> ( ph -> ( ch <-> ps ) ) )
17 16 pm5.74d 
 |-  ( 0 = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) -> ( ( ph -> ch ) <-> ( ph -> ps ) ) )
18 9 eqeq2d 
 |-  ( ph -> ( if ( A < 0 , -u 1 , 1 ) = ( sgn ` A ) <-> if ( A < 0 , -u 1 , 1 ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) ) )
19 18 pm5.32i 
 |-  ( ( ph /\ if ( A < 0 , -u 1 , 1 ) = ( sgn ` A ) ) <-> ( ph /\ if ( A < 0 , -u 1 , 1 ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) ) )
20 eqeq1 
 |-  ( -u 1 = if ( A < 0 , -u 1 , 1 ) -> ( -u 1 = ( sgn ` A ) <-> if ( A < 0 , -u 1 , 1 ) = ( sgn ` A ) ) )
21 20 imbi1d 
 |-  ( -u 1 = if ( A < 0 , -u 1 , 1 ) -> ( ( -u 1 = ( sgn ` A ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) ) <-> ( if ( A < 0 , -u 1 , 1 ) = ( sgn ` A ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) ) ) )
22 eqeq1 
 |-  ( 1 = if ( A < 0 , -u 1 , 1 ) -> ( 1 = ( sgn ` A ) <-> if ( A < 0 , -u 1 , 1 ) = ( sgn ` A ) ) )
23 22 imbi1d 
 |-  ( 1 = if ( A < 0 , -u 1 , 1 ) -> ( ( 1 = ( sgn ` A ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) ) <-> ( if ( A < 0 , -u 1 , 1 ) = ( sgn ` A ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) ) ) )
24 7 adantr 
 |-  ( ( ( ph /\ A < 0 ) /\ ( A < 0 -> ta ) ) -> ta )
25 simp2 
 |-  ( ( ( ph /\ A < 0 ) /\ ta /\ A < 0 ) -> ta )
26 25 3expia 
 |-  ( ( ( ph /\ A < 0 ) /\ ta ) -> ( A < 0 -> ta ) )
27 24 26 impbida 
 |-  ( ( ph /\ A < 0 ) -> ( ( A < 0 -> ta ) <-> ta ) )
28 pm3.24 
 |-  -. ( A < 0 /\ -. A < 0 )
29 28 pm2.21i 
 |-  ( ( A < 0 /\ -. A < 0 ) -> th )
30 29 adantl 
 |-  ( ( ph /\ ( A < 0 /\ -. A < 0 ) ) -> th )
31 30 expr 
 |-  ( ( ph /\ A < 0 ) -> ( -. A < 0 -> th ) )
32 tbtru 
 |-  ( ( -. A < 0 -> th ) <-> ( ( -. A < 0 -> th ) <-> T. ) )
33 31 32 sylib 
 |-  ( ( ph /\ A < 0 ) -> ( ( -. A < 0 -> th ) <-> T. ) )
34 27 33 anbi12d 
 |-  ( ( ph /\ A < 0 ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ( ta /\ T. ) ) )
35 ancom 
 |-  ( ( ta /\ T. ) <-> ( T. /\ ta ) )
36 truan 
 |-  ( ( T. /\ ta ) <-> ta )
37 35 36 bitri 
 |-  ( ( ta /\ T. ) <-> ta )
38 34 37 bitrdi 
 |-  ( ( ph /\ A < 0 ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ta ) )
39 38 3adant3 
 |-  ( ( ph /\ A < 0 /\ -u 1 = ( sgn ` A ) ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ta ) )
40 4 eqcoms 
 |-  ( -u 1 = ( sgn ` A ) -> ( ps <-> ta ) )
41 40 3ad2ant3 
 |-  ( ( ph /\ A < 0 /\ -u 1 = ( sgn ` A ) ) -> ( ps <-> ta ) )
42 39 41 bitr4d 
 |-  ( ( ph /\ A < 0 /\ -u 1 = ( sgn ` A ) ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) )
43 42 3expia 
 |-  ( ( ph /\ A < 0 ) -> ( -u 1 = ( sgn ` A ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) ) )
44 7 3adant2 
 |-  ( ( ph /\ -. A < 0 /\ A < 0 ) -> ta )
45 44 3expia 
 |-  ( ( ph /\ -. A < 0 ) -> ( A < 0 -> ta ) )
46 tbtru 
 |-  ( ( A < 0 -> ta ) <-> ( ( A < 0 -> ta ) <-> T. ) )
47 45 46 sylib 
 |-  ( ( ph /\ -. A < 0 ) -> ( ( A < 0 -> ta ) <-> T. ) )
48 pm3.35 
 |-  ( ( -. A < 0 /\ ( -. A < 0 -> th ) ) -> th )
49 48 adantll 
 |-  ( ( ( ph /\ -. A < 0 ) /\ ( -. A < 0 -> th ) ) -> th )
50 simp2 
 |-  ( ( ( ph /\ -. A < 0 ) /\ th /\ -. A < 0 ) -> th )
51 50 3expia 
 |-  ( ( ( ph /\ -. A < 0 ) /\ th ) -> ( -. A < 0 -> th ) )
52 49 51 impbida 
 |-  ( ( ph /\ -. A < 0 ) -> ( ( -. A < 0 -> th ) <-> th ) )
53 47 52 anbi12d 
 |-  ( ( ph /\ -. A < 0 ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ( T. /\ th ) ) )
54 truan 
 |-  ( ( T. /\ th ) <-> th )
55 53 54 bitrdi 
 |-  ( ( ph /\ -. A < 0 ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> th ) )
56 55 3adant3 
 |-  ( ( ph /\ -. A < 0 /\ 1 = ( sgn ` A ) ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> th ) )
57 3 eqcoms 
 |-  ( 1 = ( sgn ` A ) -> ( ps <-> th ) )
58 57 3ad2ant3 
 |-  ( ( ph /\ -. A < 0 /\ 1 = ( sgn ` A ) ) -> ( ps <-> th ) )
59 56 58 bitr4d 
 |-  ( ( ph /\ -. A < 0 /\ 1 = ( sgn ` A ) ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) )
60 59 3expia 
 |-  ( ( ph /\ -. A < 0 ) -> ( 1 = ( sgn ` A ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) ) )
61 21 23 43 60 ifbothda 
 |-  ( ph -> ( if ( A < 0 , -u 1 , 1 ) = ( sgn ` A ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) ) )
62 61 imp 
 |-  ( ( ph /\ if ( A < 0 , -u 1 , 1 ) = ( sgn ` A ) ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) )
63 19 62 sylbir 
 |-  ( ( ph /\ if ( A < 0 , -u 1 , 1 ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) ) -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) )
64 63 expcom 
 |-  ( if ( A < 0 , -u 1 , 1 ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) -> ( ph -> ( ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) <-> ps ) ) )
65 64 pm5.74d 
 |-  ( if ( A < 0 , -u 1 , 1 ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) -> ( ( ph -> ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) ) <-> ( ph -> ps ) ) )
66 5 expcom 
 |-  ( A = 0 -> ( ph -> ch ) )
67 66 adantl 
 |-  ( ( T. /\ A = 0 ) -> ( ph -> ch ) )
68 7 ex 
 |-  ( ph -> ( A < 0 -> ta ) )
69 68 adantr 
 |-  ( ( ph /\ -. A = 0 ) -> ( A < 0 -> ta ) )
70 simp1 
 |-  ( ( ph /\ -. A = 0 /\ -. A < 0 ) -> ph )
71 df-ne 
 |-  ( A =/= 0 <-> -. A = 0 )
72 0xr 
 |-  0 e. RR*
73 xrlttri2 
 |-  ( ( A e. RR* /\ 0 e. RR* ) -> ( A =/= 0 <-> ( A < 0 \/ 0 < A ) ) )
74 1 72 73 sylancl 
 |-  ( ph -> ( A =/= 0 <-> ( A < 0 \/ 0 < A ) ) )
75 71 74 bitr3id 
 |-  ( ph -> ( -. A = 0 <-> ( A < 0 \/ 0 < A ) ) )
76 75 biimpa 
 |-  ( ( ph /\ -. A = 0 ) -> ( A < 0 \/ 0 < A ) )
77 76 ord 
 |-  ( ( ph /\ -. A = 0 ) -> ( -. A < 0 -> 0 < A ) )
78 77 3impia 
 |-  ( ( ph /\ -. A = 0 /\ -. A < 0 ) -> 0 < A )
79 70 78 6 syl2anc 
 |-  ( ( ph /\ -. A = 0 /\ -. A < 0 ) -> th )
80 79 3expia 
 |-  ( ( ph /\ -. A = 0 ) -> ( -. A < 0 -> th ) )
81 69 80 jca 
 |-  ( ( ph /\ -. A = 0 ) -> ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) )
82 81 expcom 
 |-  ( -. A = 0 -> ( ph -> ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) ) )
83 82 adantl 
 |-  ( ( T. /\ -. A = 0 ) -> ( ph -> ( ( A < 0 -> ta ) /\ ( -. A < 0 -> th ) ) ) )
84 17 65 67 83 ifbothda 
 |-  ( T. -> ( ph -> ps ) )
85 84 mptru 
 |-  ( ph -> ps )