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 φ A *
sgn3da.1 sgn A = 0 ψ χ
sgn3da.2 sgn A = 1 ψ θ
sgn3da.3 sgn A = 1 ψ τ
sgn3da.4 φ A = 0 χ
sgn3da.5 φ 0 < A θ
sgn3da.6 φ A < 0 τ
Assertion sgn3da φ ψ

Proof

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