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	$⊢ φ \to A \in ℝ^{*}$
	sgn3da.1	$⊢ sgn (A) = 0 \to (ψ \leftrightarrow χ)$
	sgn3da.2	$⊢ sgn (A) = 1 \to (ψ \leftrightarrow θ)$
	sgn3da.3	$⊢ sgn (A) = - 1 \to (ψ \leftrightarrow τ)$
	sgn3da.4	$⊢ (φ \land A = 0) \to χ$
	sgn3da.5	$⊢ (φ \land 0 < A) \to θ$
	sgn3da.6	$⊢ (φ \land A < 0) \to τ$
Assertion	sgn3da	$⊢ φ \to ψ$

Proof

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

Metamath Proof Explorer

Theorem sgn3da

Proof