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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
sgn3da.1 ⊢ ( ( sgn ‘ 𝐴 ) = 0 → ( 𝜓 ↔ 𝜒 ) )
sgn3da.2 ⊢ ( ( sgn ‘ 𝐴 ) = 1 → ( 𝜓 ↔ 𝜃 ) )
sgn3da.3 ⊢ ( ( sgn ‘ 𝐴 ) = - 1 → ( 𝜓 ↔ 𝜏 ) )
sgn3da.4 ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → 𝜒 )
sgn3da.5 ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝜃 )
sgn3da.6 ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝜏 )
Assertion sgn3da ( 𝜑 → 𝜓 )

Proof

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