line2ylem

Description: Lemma for line2y . This proof is based on counterexamples for the following cases: 1. C =/= 0 : p = (0,0) (LHS of biconditional is false, RHS is true); 2. C = 0 /\ B =/= 0 : p = (1,-A/B) (LHS of biconditional is true, RHS is false); 3. A = B = C = 0 : p = (1,1) (LHS of biconditional is true, RHS is false). (Contributed by AV, 4-Feb-2023)

	Ref	Expression
Hypotheses	line2ylem.i	$⊢ I = (0 ..^2)$
	line2ylem.p	$⊢ P = ℝ^{I}$
Assertion	line2ylem	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \to (A \neq 0 \land B = 0 \land C = 0))$

Proof

Step	Hyp	Ref	Expression
1		line2ylem.i	$⊢ I = (0 ..^2)$
2		line2ylem.p	$⊢ P = ℝ^{I}$
3		ianor	$⊢ \neg ((A \neq 0 \land B = 0) \land C = 0) \leftrightarrow (\neg (A \neq 0 \land B = 0) \lor \neg C = 0)$
4		df-ne	$⊢ C \neq 0 \leftrightarrow \neg C = 0$
5		0re	$⊢ 0 \in ℝ$
6	1 2	prelrrx2	$⊢ (0 \in ℝ \land 0 \in ℝ) \to ⟨“ 00 ”⟩ \in P$
7	5 5 6	mp2an	$⊢ ⟨“ 00 ”⟩ \in P$
8		eqneqall	$⊢ C = 0 \to (C \neq 0 \to \neg 0 = 0)$
9	8	com12	$⊢ C \neq 0 \to (C = 0 \to \neg 0 = 0)$
10		eqid	$⊢ 0 = 0$
11	10	pm2.24i	$⊢ \neg 0 = 0 \to C = 0$
12	9 11	impbid1	$⊢ C \neq 0 \to (C = 0 \leftrightarrow \neg 0 = 0)$
13	12	adantl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land C \neq 0) \to (C = 0 \leftrightarrow \neg 0 = 0)$
14		xor3	$⊢ \neg (C = 0 \leftrightarrow 0 = 0) \leftrightarrow (C = 0 \leftrightarrow \neg 0 = 0)$
15	13 14	sylibr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land C \neq 0) \to \neg (C = 0 \leftrightarrow 0 = 0)$
16		simp1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℝ$
17	16	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℂ$
18	17	mul01d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \cdot 0 = 0$
19		simp2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℝ$
20	19	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℂ$
21	20	mul01d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \cdot 0 = 0$
22	18 21	oveq12d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \cdot 0 + B \cdot 0 = 0 + 0$
23		00id	$⊢ 0 + 0 = 0$
24	22 23	eqtrdi	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \cdot 0 + B \cdot 0 = 0$
25	24	eqeq1d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A \cdot 0 + B \cdot 0 = C \leftrightarrow 0 = C)$
26		eqcom	$⊢ 0 = C \leftrightarrow C = 0$
27	25 26	bitrdi	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A \cdot 0 + B \cdot 0 = C \leftrightarrow C = 0)$
28	27	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land C \neq 0) \to (A \cdot 0 + B \cdot 0 = C \leftrightarrow C = 0)$
29	28	bibi1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land C \neq 0) \to ((A \cdot 0 + B \cdot 0 = C \leftrightarrow 0 = 0) \leftrightarrow (C = 0 \leftrightarrow 0 = 0))$
30	15 29	mtbird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land C \neq 0) \to \neg (A \cdot 0 + B \cdot 0 = C \leftrightarrow 0 = 0)$
31		fveq1	$⊢ p = ⟨“ 00 ”⟩ \to p (0) = ⟨“ 00 ”⟩ (0)$
32		c0ex	$⊢ 0 \in V$
33		s2fv0	$⊢ 0 \in V \to ⟨“ 00 ”⟩ (0) = 0$
34	32 33	ax-mp	$⊢ ⟨“ 00 ”⟩ (0) = 0$
35	31 34	eqtrdi	$⊢ p = ⟨“ 00 ”⟩ \to p (0) = 0$
36	35	oveq2d	$⊢ p = ⟨“ 00 ”⟩ \to A p (0) = A \cdot 0$
37		fveq1	$⊢ p = ⟨“ 00 ”⟩ \to p (1) = ⟨“ 00 ”⟩ (1)$
38		s2fv1	$⊢ 0 \in V \to ⟨“ 00 ”⟩ (1) = 0$
39	32 38	ax-mp	$⊢ ⟨“ 00 ”⟩ (1) = 0$
40	37 39	eqtrdi	$⊢ p = ⟨“ 00 ”⟩ \to p (1) = 0$
41	40	oveq2d	$⊢ p = ⟨“ 00 ”⟩ \to B p (1) = B \cdot 0$
42	36 41	oveq12d	$⊢ p = ⟨“ 00 ”⟩ \to A p (0) + B p (1) = A \cdot 0 + B \cdot 0$
43	42	eqeq1d	$⊢ p = ⟨“ 00 ”⟩ \to (A p (0) + B p (1) = C \leftrightarrow A \cdot 0 + B \cdot 0 = C)$
44	35	eqeq1d	$⊢ p = ⟨“ 00 ”⟩ \to (p (0) = 0 \leftrightarrow 0 = 0)$
45	43 44	bibi12d	$⊢ p = ⟨“ 00 ”⟩ \to ((A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \leftrightarrow (A \cdot 0 + B \cdot 0 = C \leftrightarrow 0 = 0))$
46	45	notbid	$⊢ p = ⟨“ 00 ”⟩ \to (\neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \leftrightarrow \neg (A \cdot 0 + B \cdot 0 = C \leftrightarrow 0 = 0))$
47	46	rspcev	$⊢ (⟨“ 00 ”⟩ \in P \land \neg (A \cdot 0 + B \cdot 0 = C \leftrightarrow 0 = 0)) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)$
48	7 30 47	sylancr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land C \neq 0) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)$
49	48	expcom	$⊢ C \neq 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0))$
50	4 49	sylbir	$⊢ \neg C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0))$
51		notnotb	$⊢ C = 0 \leftrightarrow \neg \neg C = 0$
52		ianor	$⊢ \neg (A \neq 0 \land B = 0) \leftrightarrow (\neg A \neq 0 \lor \neg B = 0)$
53		df-ne	$⊢ B \neq 0 \leftrightarrow \neg B = 0$
54		fveq1	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to p (0) = ⟨“ 1 (\frac{- A}{B}) ”⟩ (0)$
55		1ex	$⊢ 1 \in V$
56		s2fv0	$⊢ 1 \in V \to ⟨“ 1 (\frac{- A}{B}) ”⟩ (0) = 1$
57	55 56	ax-mp	$⊢ ⟨“ 1 (\frac{- A}{B}) ”⟩ (0) = 1$
58	54 57	eqtrdi	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to p (0) = 1$
59	58	oveq2d	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to A p (0) = A \cdot 1$
60		fveq1	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to p (1) = ⟨“ 1 (\frac{- A}{B}) ”⟩ (1)$
61		ovex	$⊢ \frac{- A}{B} \in V$
62		s2fv1	$⊢ \frac{- A}{B} \in V \to ⟨“ 1 (\frac{- A}{B}) ”⟩ (1) = \frac{- A}{B}$
63	61 62	ax-mp	$⊢ ⟨“ 1 (\frac{- A}{B}) ”⟩ (1) = \frac{- A}{B}$
64	60 63	eqtrdi	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to p (1) = \frac{- A}{B}$
65	64	oveq2d	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to B p (1) = B (\frac{- A}{B})$
66	59 65	oveq12d	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to A p (0) + B p (1) = A \cdot 1 + B (\frac{- A}{B})$
67	66	eqeq1d	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to (A p (0) + B p (1) = C \leftrightarrow A \cdot 1 + B (\frac{- A}{B}) = C)$
68	58	eqeq1d	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to (p (0) = 0 \leftrightarrow 1 = 0)$
69	67 68	bibi12d	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to ((A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \leftrightarrow (A \cdot 1 + B (\frac{- A}{B}) = C \leftrightarrow 1 = 0))$
70	69	notbid	$⊢ p = ⟨“ 1 (\frac{- A}{B}) ”⟩ \to (\neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \leftrightarrow \neg (A \cdot 1 + B (\frac{- A}{B}) = C \leftrightarrow 1 = 0))$
71		1red	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to 1 \in ℝ$
72	16	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to A \in ℝ$
73	72	renegcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to - A \in ℝ$
74	19	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to B \in ℝ$
75		simprl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to B \neq 0$
76	73 74 75	redivcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to \frac{- A}{B} \in ℝ$
77	1 2	prelrrx2	$⊢ (1 \in ℝ \land \frac{- A}{B} \in ℝ) \to ⟨“ 1 (\frac{- A}{B}) ”⟩ \in P$
78	71 76 77	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to ⟨“ 1 (\frac{- A}{B}) ”⟩ \in P$
79		ax-1ne0	$⊢ 1 \neq 0$
80	79	neii	$⊢ \neg 1 = 0$
81	10 80	2th	$⊢ 0 = 0 \leftrightarrow \neg 1 = 0$
82		xor3	$⊢ \neg (0 = 0 \leftrightarrow 1 = 0) \leftrightarrow (0 = 0 \leftrightarrow \neg 1 = 0)$
83	81 82	mpbir	$⊢ \neg (0 = 0 \leftrightarrow 1 = 0)$
84	17	mulridd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \cdot 1 = A$
85	84	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to A \cdot 1 = A$
86	17	negcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to - A \in ℂ$
87	86	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to - A \in ℂ$
88	20	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to B \in ℂ$
89	87 88 75	divcan2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to B (\frac{- A}{B}) = - A$
90	85 89	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to A \cdot 1 + B (\frac{- A}{B}) = A + (- A)$
91	17	negidd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A + (- A) = 0$
92	91	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to A + (- A) = 0$
93	90 92	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to A \cdot 1 + B (\frac{- A}{B}) = 0$
94		simprr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to C = 0$
95	93 94	eqeq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to (A \cdot 1 + B (\frac{- A}{B}) = C \leftrightarrow 0 = 0)$
96	95	bibi1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to ((A \cdot 1 + B (\frac{- A}{B}) = C \leftrightarrow 1 = 0) \leftrightarrow (0 = 0 \leftrightarrow 1 = 0))$
97	83 96	mtbiri	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to \neg (A \cdot 1 + B (\frac{- A}{B}) = C \leftrightarrow 1 = 0)$
98	70 78 97	rspcedvdw	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)$
99	98	expcom	$⊢ (B \neq 0 \land C = 0) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0))$
100	99	ex	$⊢ B \neq 0 \to (C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)))$
101	53 100	sylbir	$⊢ \neg B = 0 \to (C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)))$
102		notnotb	$⊢ B = 0 \leftrightarrow \neg \neg B = 0$
103		nne	$⊢ \neg A \neq 0 \leftrightarrow A = 0$
104	103	bicomi	$⊢ A = 0 \leftrightarrow \neg A \neq 0$
105		1re	$⊢ 1 \in ℝ$
106	1 2	prelrrx2	$⊢ (1 \in ℝ \land 1 \in ℝ) \to ⟨“ 11 ”⟩ \in P$
107	105 105 106	mp2an	$⊢ ⟨“ 11 ”⟩ \in P$
108		oveq1	$⊢ A = 0 \to A \cdot 1 = 0 \cdot 1$
109	108	adantl	$⊢ (B = 0 \land A = 0) \to A \cdot 1 = 0 \cdot 1$
110		ax-1cn	$⊢ 1 \in ℂ$
111	110	mul02i	$⊢ 0 \cdot 1 = 0$
112	109 111	eqtrdi	$⊢ (B = 0 \land A = 0) \to A \cdot 1 = 0$
113		oveq1	$⊢ B = 0 \to B \cdot 1 = 0 \cdot 1$
114	113	adantr	$⊢ (B = 0 \land A = 0) \to B \cdot 1 = 0 \cdot 1$
115	114 111	eqtrdi	$⊢ (B = 0 \land A = 0) \to B \cdot 1 = 0$
116	112 115	oveq12d	$⊢ (B = 0 \land A = 0) \to A \cdot 1 + B \cdot 1 = 0 + 0$
117	116 23	eqtrdi	$⊢ (B = 0 \land A = 0) \to A \cdot 1 + B \cdot 1 = 0$
118		id	$⊢ C = 0 \to C = 0$
119	117 118	eqeqan12d	$⊢ ((B = 0 \land A = 0) \land C = 0) \to (A \cdot 1 + B \cdot 1 = C \leftrightarrow 0 = 0)$
120	119	bibi1d	$⊢ ((B = 0 \land A = 0) \land C = 0) \to ((A \cdot 1 + B \cdot 1 = C \leftrightarrow 1 = 0) \leftrightarrow (0 = 0 \leftrightarrow 1 = 0))$
121	83 120	mtbiri	$⊢ ((B = 0 \land A = 0) \land C = 0) \to \neg (A \cdot 1 + B \cdot 1 = C \leftrightarrow 1 = 0)$
122		fveq1	$⊢ p = ⟨“ 11 ”⟩ \to p (0) = ⟨“ 11 ”⟩ (0)$
123		s2fv0	$⊢ 1 \in V \to ⟨“ 11 ”⟩ (0) = 1$
124	55 123	ax-mp	$⊢ ⟨“ 11 ”⟩ (0) = 1$
125	122 124	eqtrdi	$⊢ p = ⟨“ 11 ”⟩ \to p (0) = 1$
126	125	oveq2d	$⊢ p = ⟨“ 11 ”⟩ \to A p (0) = A \cdot 1$
127		fveq1	$⊢ p = ⟨“ 11 ”⟩ \to p (1) = ⟨“ 11 ”⟩ (1)$
128		s2fv1	$⊢ 1 \in V \to ⟨“ 11 ”⟩ (1) = 1$
129	55 128	ax-mp	$⊢ ⟨“ 11 ”⟩ (1) = 1$
130	127 129	eqtrdi	$⊢ p = ⟨“ 11 ”⟩ \to p (1) = 1$
131	130	oveq2d	$⊢ p = ⟨“ 11 ”⟩ \to B p (1) = B \cdot 1$
132	126 131	oveq12d	$⊢ p = ⟨“ 11 ”⟩ \to A p (0) + B p (1) = A \cdot 1 + B \cdot 1$
133	132	eqeq1d	$⊢ p = ⟨“ 11 ”⟩ \to (A p (0) + B p (1) = C \leftrightarrow A \cdot 1 + B \cdot 1 = C)$
134	125	eqeq1d	$⊢ p = ⟨“ 11 ”⟩ \to (p (0) = 0 \leftrightarrow 1 = 0)$
135	133 134	bibi12d	$⊢ p = ⟨“ 11 ”⟩ \to ((A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \leftrightarrow (A \cdot 1 + B \cdot 1 = C \leftrightarrow 1 = 0))$
136	135	notbid	$⊢ p = ⟨“ 11 ”⟩ \to (\neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \leftrightarrow \neg (A \cdot 1 + B \cdot 1 = C \leftrightarrow 1 = 0))$
137	136	rspcev	$⊢ (⟨“ 11 ”⟩ \in P \land \neg (A \cdot 1 + B \cdot 1 = C \leftrightarrow 1 = 0)) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)$
138	107 121 137	sylancr	$⊢ ((B = 0 \land A = 0) \land C = 0) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)$
139	138	a1d	$⊢ ((B = 0 \land A = 0) \land C = 0) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0))$
140	139	ex	$⊢ (B = 0 \land A = 0) \to (C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)))$
141	102 104 140	syl2anbr	$⊢ (\neg \neg B = 0 \land \neg A \neq 0) \to (C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)))$
142	101 141	jaoi3	$⊢ (\neg B = 0 \lor \neg A \neq 0) \to (C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)))$
143	142	orcoms	$⊢ (\neg A \neq 0 \lor \neg B = 0) \to (C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)))$
144	52 143	sylbi	$⊢ \neg (A \neq 0 \land B = 0) \to (C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)))$
145	144	com12	$⊢ C = 0 \to (\neg (A \neq 0 \land B = 0) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)))$
146	51 145	sylbir	$⊢ \neg \neg C = 0 \to (\neg (A \neq 0 \land B = 0) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)))$
147	146	imp	$⊢ (\neg \neg C = 0 \land \neg (A \neq 0 \land B = 0)) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0))$
148	50 147	jaoi3	$⊢ (\neg C = 0 \lor \neg (A \neq 0 \land B = 0)) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0))$
149	148	orcoms	$⊢ (\neg (A \neq 0 \land B = 0) \lor \neg C = 0) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0))$
150	149	com12	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((\neg (A \neq 0 \land B = 0) \lor \neg C = 0) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0))$
151	3 150	biimtrid	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\neg ((A \neq 0 \land B = 0) \land C = 0) \to \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0))$
152		rexnal	$⊢ \exists p \in P \neg (A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \leftrightarrow \neg \forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (0) = 0)$
153	151 152	imbitrdi	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\neg ((A \neq 0 \land B = 0) \land C = 0) \to \neg \forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (0) = 0))$
154	153	con4d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \to ((A \neq 0 \land B = 0) \land C = 0))$
155		df-3an	$⊢ (A \neq 0 \land B = 0 \land C = 0) \leftrightarrow ((A \neq 0 \land B = 0) \land C = 0)$
156	154 155	imbitrrdi	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \to (A \neq 0 \land B = 0 \land C = 0))$

Metamath Proof Explorer

Theorem line2ylem

Proof