line2ylem

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

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

Proof

Step	Hyp	Ref	Expression
1		line2ylem.i	$⊢ I = \{1, 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 \{⟨1, 0⟩, ⟨2, 0⟩\} \in P$
7	5 5 6	mp2an	$⊢ \{⟨1, 0⟩, ⟨2, 0⟩\} \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 = \{⟨1, 0⟩, ⟨2, 0⟩\} \to p (1) = \{⟨1, 0⟩, ⟨2, 0⟩\} (1)$
32		1ex	$⊢ 1 \in V$
33		c0ex	$⊢ 0 \in V$
34		1ne2	$⊢ 1 \neq 2$
35		fvpr1g	$⊢ (1 \in V \land 0 \in V \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, 0⟩\} (1) = 0$
36	32 33 34 35	mp3an	$⊢ \{⟨1, 0⟩, ⟨2, 0⟩\} (1) = 0$
37	31 36	eqtrdi	$⊢ p = \{⟨1, 0⟩, ⟨2, 0⟩\} \to p (1) = 0$
38	37	oveq2d	$⊢ p = \{⟨1, 0⟩, ⟨2, 0⟩\} \to A p (1) = A \cdot 0$
39		fveq1	$⊢ p = \{⟨1, 0⟩, ⟨2, 0⟩\} \to p (2) = \{⟨1, 0⟩, ⟨2, 0⟩\} (2)$
40		2ex	$⊢ 2 \in V$
41		fvpr2g	$⊢ (2 \in V \land 0 \in V \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, 0⟩\} (2) = 0$
42	40 33 34 41	mp3an	$⊢ \{⟨1, 0⟩, ⟨2, 0⟩\} (2) = 0$
43	39 42	eqtrdi	$⊢ p = \{⟨1, 0⟩, ⟨2, 0⟩\} \to p (2) = 0$
44	43	oveq2d	$⊢ p = \{⟨1, 0⟩, ⟨2, 0⟩\} \to B p (2) = B \cdot 0$
45	38 44	oveq12d	$⊢ p = \{⟨1, 0⟩, ⟨2, 0⟩\} \to A p (1) + B p (2) = A \cdot 0 + B \cdot 0$
46	45	eqeq1d	$⊢ p = \{⟨1, 0⟩, ⟨2, 0⟩\} \to (A p (1) + B p (2) = C \leftrightarrow A \cdot 0 + B \cdot 0 = C)$
47	37	eqeq1d	$⊢ p = \{⟨1, 0⟩, ⟨2, 0⟩\} \to (p (1) = 0 \leftrightarrow 0 = 0)$
48	46 47	bibi12d	$⊢ p = \{⟨1, 0⟩, ⟨2, 0⟩\} \to ((A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \leftrightarrow (A \cdot 0 + B \cdot 0 = C \leftrightarrow 0 = 0))$
49	48	notbid	$⊢ p = \{⟨1, 0⟩, ⟨2, 0⟩\} \to (\neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \leftrightarrow \neg (A \cdot 0 + B \cdot 0 = C \leftrightarrow 0 = 0))$
50	49	rspcev	$⊢ (\{⟨1, 0⟩, ⟨2, 0⟩\} \in P \land \neg (A \cdot 0 + B \cdot 0 = C \leftrightarrow 0 = 0)) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)$
51	7 30 50	sylancr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land C \neq 0) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)$
52	51	expcom	$⊢ C \neq 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0))$
53	4 52	sylbir	$⊢ \neg C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0))$
54		notnotb	$⊢ C = 0 \leftrightarrow \neg \neg C = 0$
55		ianor	$⊢ \neg (A \neq 0 \land B = 0) \leftrightarrow (\neg A \neq 0 \lor \neg B = 0)$
56		df-ne	$⊢ B \neq 0 \leftrightarrow \neg B = 0$
57		1red	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to 1 \in ℝ$
58	16	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to A \in ℝ$
59	58	renegcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to - A \in ℝ$
60	19	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to B \in ℝ$
61		simprl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to B \neq 0$
62	59 60 61	redivcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to \frac{- A}{B} \in ℝ$
63	1 2	prelrrx2	$⊢ (1 \in ℝ \land \frac{- A}{B} \in ℝ) \to \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \in P$
64	57 62 63	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \in P$
65		ax-1ne0	$⊢ 1 \neq 0$
66	65	neii	$⊢ \neg 1 = 0$
67	10 66	2th	$⊢ 0 = 0 \leftrightarrow \neg 1 = 0$
68		xor3	$⊢ \neg (0 = 0 \leftrightarrow 1 = 0) \leftrightarrow (0 = 0 \leftrightarrow \neg 1 = 0)$
69	67 68	mpbir	$⊢ \neg (0 = 0 \leftrightarrow 1 = 0)$
70	17	mulid1d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \cdot 1 = A$
71	70	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to A \cdot 1 = A$
72	17	negcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to - A \in ℂ$
73	72	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to - A \in ℂ$
74	20	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to B \in ℂ$
75	73 74 61	divcan2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to B (\frac{- A}{B}) = - A$
76	71 75	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)$
77	17	negidd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A + (- A) = 0$
78	77	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to A + (- A) = 0$
79	76 78	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$
80		simprr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to C = 0$
81	79 80	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)$
82	81	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))$
83	69 82	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)$
84		fveq1	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to p (1) = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} (1)$
85		fvpr1g	$⊢ (1 \in V \land 1 \in V \land 1 \neq 2) \to \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} (1) = 1$
86	32 32 34 85	mp3an	$⊢ \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} (1) = 1$
87	84 86	eqtrdi	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to p (1) = 1$
88	87	oveq2d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to A p (1) = A \cdot 1$
89		fveq1	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to p (2) = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} (2)$
90		ovex	$⊢ \frac{- A}{B} \in V$
91		fvpr2g	$⊢ (2 \in V \land \frac{- A}{B} \in V \land 1 \neq 2) \to \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} (2) = \frac{- A}{B}$
92	40 90 34 91	mp3an	$⊢ \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} (2) = \frac{- A}{B}$
93	89 92	eqtrdi	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to p (2) = \frac{- A}{B}$
94	93	oveq2d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to B p (2) = B (\frac{- A}{B})$
95	88 94	oveq12d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to A p (1) + B p (2) = A \cdot 1 + B (\frac{- A}{B})$
96	95	eqeq1d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to (A p (1) + B p (2) = C \leftrightarrow A \cdot 1 + B (\frac{- A}{B}) = C)$
97	87	eqeq1d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to (p (1) = 0 \leftrightarrow 1 = 0)$
98	96 97	bibi12d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to ((A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \leftrightarrow (A \cdot 1 + B (\frac{- A}{B}) = C \leftrightarrow 1 = 0))$
99	98	notbid	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \to (\neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \leftrightarrow \neg (A \cdot 1 + B (\frac{- A}{B}) = C \leftrightarrow 1 = 0))$
100	99	rspcev	$⊢ (\{⟨1, 1⟩, ⟨2, \frac{- A}{B}⟩\} \in P \land \neg (A \cdot 1 + B (\frac{- A}{B}) = C \leftrightarrow 1 = 0)) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)$
101	64 83 100	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (B \neq 0 \land C = 0)) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)$
102	101	expcom	$⊢ (B \neq 0 \land C = 0) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0))$
103	102	ex	$⊢ B \neq 0 \to (C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)))$
104	56 103	sylbir	$⊢ \neg B = 0 \to (C = 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)))$
105		notnotb	$⊢ B = 0 \leftrightarrow \neg \neg B = 0$
106		nne	$⊢ \neg A \neq 0 \leftrightarrow A = 0$
107	106	bicomi	$⊢ A = 0 \leftrightarrow \neg A \neq 0$
108		1re	$⊢ 1 \in ℝ$
109	1 2	prelrrx2	$⊢ (1 \in ℝ \land 1 \in ℝ) \to \{⟨1, 1⟩, ⟨2, 1⟩\} \in P$
110	108 108 109	mp2an	$⊢ \{⟨1, 1⟩, ⟨2, 1⟩\} \in P$
111		oveq1	$⊢ A = 0 \to A \cdot 1 = 0 \cdot 1$
112	111	adantl	$⊢ (B = 0 \land A = 0) \to A \cdot 1 = 0 \cdot 1$
113		ax-1cn	$⊢ 1 \in ℂ$
114	113	mul02i	$⊢ 0 \cdot 1 = 0$
115	112 114	eqtrdi	$⊢ (B = 0 \land A = 0) \to A \cdot 1 = 0$
116		oveq1	$⊢ B = 0 \to B \cdot 1 = 0 \cdot 1$
117	116	adantr	$⊢ (B = 0 \land A = 0) \to B \cdot 1 = 0 \cdot 1$
118	117 114	eqtrdi	$⊢ (B = 0 \land A = 0) \to B \cdot 1 = 0$
119	115 118	oveq12d	$⊢ (B = 0 \land A = 0) \to A \cdot 1 + B \cdot 1 = 0 + 0$
120	119 23	eqtrdi	$⊢ (B = 0 \land A = 0) \to A \cdot 1 + B \cdot 1 = 0$
121		id	$⊢ C = 0 \to C = 0$
122	120 121	eqeqan12d	$⊢ ((B = 0 \land A = 0) \land C = 0) \to (A \cdot 1 + B \cdot 1 = C \leftrightarrow 0 = 0)$
123	122	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))$
124	69 123	mtbiri	$⊢ ((B = 0 \land A = 0) \land C = 0) \to \neg (A \cdot 1 + B \cdot 1 = C \leftrightarrow 1 = 0)$
125		fveq1	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to p (1) = \{⟨1, 1⟩, ⟨2, 1⟩\} (1)$
126		fvpr1g	$⊢ (1 \in V \land 1 \in V \land 1 \neq 2) \to \{⟨1, 1⟩, ⟨2, 1⟩\} (1) = 1$
127	32 32 34 126	mp3an	$⊢ \{⟨1, 1⟩, ⟨2, 1⟩\} (1) = 1$
128	125 127	eqtrdi	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to p (1) = 1$
129	128	oveq2d	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to A p (1) = A \cdot 1$
130		fveq1	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to p (2) = \{⟨1, 1⟩, ⟨2, 1⟩\} (2)$
131		fvpr2g	$⊢ (2 \in V \land 1 \in V \land 1 \neq 2) \to \{⟨1, 1⟩, ⟨2, 1⟩\} (2) = 1$
132	40 32 34 131	mp3an	$⊢ \{⟨1, 1⟩, ⟨2, 1⟩\} (2) = 1$
133	130 132	eqtrdi	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to p (2) = 1$
134	133	oveq2d	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to B p (2) = B \cdot 1$
135	129 134	oveq12d	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to A p (1) + B p (2) = A \cdot 1 + B \cdot 1$
136	135	eqeq1d	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to (A p (1) + B p (2) = C \leftrightarrow A \cdot 1 + B \cdot 1 = C)$
137	128	eqeq1d	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to (p (1) = 0 \leftrightarrow 1 = 0)$
138	136 137	bibi12d	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to ((A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \leftrightarrow (A \cdot 1 + B \cdot 1 = C \leftrightarrow 1 = 0))$
139	138	notbid	$⊢ p = \{⟨1, 1⟩, ⟨2, 1⟩\} \to (\neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \leftrightarrow \neg (A \cdot 1 + B \cdot 1 = C \leftrightarrow 1 = 0))$
140	139	rspcev	$⊢ (\{⟨1, 1⟩, ⟨2, 1⟩\} \in P \land \neg (A \cdot 1 + B \cdot 1 = C \leftrightarrow 1 = 0)) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)$
141	110 124 140	sylancr	$⊢ ((B = 0 \land A = 0) \land C = 0) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)$
142	141	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 (1) + B p (2) = C \leftrightarrow p (1) = 0))$
143	142	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 (1) + B p (2) = C \leftrightarrow p (1) = 0)))$
144	105 107 143	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 (1) + B p (2) = C \leftrightarrow p (1) = 0)))$
145	104 144	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 (1) + B p (2) = C \leftrightarrow p (1) = 0)))$
146	145	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 (1) + B p (2) = C \leftrightarrow p (1) = 0)))$
147	55 146	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 (1) + B p (2) = C \leftrightarrow p (1) = 0)))$
148	147	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 (1) + B p (2) = C \leftrightarrow p (1) = 0)))$
149	54 148	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 (1) + B p (2) = C \leftrightarrow p (1) = 0)))$
150	149	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 (1) + B p (2) = C \leftrightarrow p (1) = 0))$
151	53 150	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 (1) + B p (2) = C \leftrightarrow p (1) = 0))$
152	151	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 (1) + B p (2) = C \leftrightarrow p (1) = 0))$
153	152	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 (1) + B p (2) = C \leftrightarrow p (1) = 0))$
154	3 153	syl5bi	$⊢ (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 (1) + B p (2) = C \leftrightarrow p (1) = 0))$
155		rexnal	$⊢ \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \leftrightarrow \neg \forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)$
156	154 155	syl6ib	$⊢ (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 (1) + B p (2) = C \leftrightarrow p (1) = 0))$
157	156	con4d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \to ((A \neq 0 \land B = 0) \land C = 0))$
158		df-3an	$⊢ (A \neq 0 \land B = 0 \land C = 0) \leftrightarrow ((A \neq 0 \land B = 0) \land C = 0)$
159	157 158	syl6ibr	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \to (A \neq 0 \land B = 0 \land C = 0))$

Metamath Proof Explorer

Theorem line2ylem

Proof