line2xlem

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

	Ref	Expression
Hypotheses	line2.i	$⊢ I = \{1, 2\}$
	line2.e	$⊢ E = msup$
	line2.p	$⊢ P = ℝ^{I}$
	line2.l	$⊢ L = {Line}_{M} (E)$
	line2.g	$⊢ G = \{p \in P \| A p (1) + B p (2) = C\}$
	line2x.x	$⊢ X = \{⟨1, 0⟩, ⟨2, M⟩\}$
	line2x.y	$⊢ Y = \{⟨1, 1⟩, ⟨2, M⟩\}$
Assertion	line2xlem	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = M) \to (A = 0 \land M = \frac{C}{B}))$

Proof

Step	Hyp	Ref	Expression
1		line2.i	$⊢ I = \{1, 2\}$
2		line2.e	$⊢ E = msup$
3		line2.p	$⊢ P = ℝ^{I}$
4		line2.l	$⊢ L = {Line}_{M} (E)$
5		line2.g	$⊢ G = \{p \in P \| A p (1) + B p (2) = C\}$
6		line2x.x	$⊢ X = \{⟨1, 0⟩, ⟨2, M⟩\}$
7		line2x.y	$⊢ Y = \{⟨1, 1⟩, ⟨2, M⟩\}$
8		ianor	$⊢ \neg (A = 0 \land M = \frac{C}{B}) \leftrightarrow (\neg A = 0 \lor \neg M = \frac{C}{B})$
9		df-ne	$⊢ A \neq 0 \leftrightarrow \neg A = 0$
10		df-ne	$⊢ M \neq \frac{C}{B} \leftrightarrow \neg M = \frac{C}{B}$
11	9 10	orbi12i	$⊢ (A \neq 0 \lor M \neq \frac{C}{B}) \leftrightarrow (\neg A = 0 \lor \neg M = \frac{C}{B})$
12	8 11	bitr4i	$⊢ \neg (A = 0 \land M = \frac{C}{B}) \leftrightarrow (A \neq 0 \lor M \neq \frac{C}{B})$
13		0red	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to 0 \in ℝ$
14		simp3	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C \in ℝ$
15	14	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to C \in ℝ$
16		simpl	$⊢ (B \in ℝ \land B \neq 0) \to B \in ℝ$
17	16	3ad2ant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \in ℝ$
18	17	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to B \in ℝ$
19		simp2r	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \neq 0$
20	19	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to B \neq 0$
21	15 18 20	redivcld	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \frac{C}{B} \in ℝ$
22	21	adantl	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to \frac{C}{B} \in ℝ$
23	1 3	prelrrx2	$⊢ (0 \in ℝ \land \frac{C}{B} \in ℝ) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \in P$
24	13 22 23	syl2anc	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \in P$
25		id	$⊢ M \neq \frac{C}{B} \to M \neq \frac{C}{B}$
26	25	necomd	$⊢ M \neq \frac{C}{B} \to \frac{C}{B} \neq M$
27	26	neneqd	$⊢ M \neq \frac{C}{B} \to \neg \frac{C}{B} = M$
28	27	a1d	$⊢ M \neq \frac{C}{B} \to (C = C \to \neg \frac{C}{B} = M)$
29		eqidd	$⊢ \neg \frac{C}{B} = M \to C = C$
30	29	a1i	$⊢ M \neq \frac{C}{B} \to (\neg \frac{C}{B} = M \to C = C)$
31	28 30	impbid	$⊢ M \neq \frac{C}{B} \to (C = C \leftrightarrow \neg \frac{C}{B} = M)$
32		xor3	$⊢ \neg (C = C \leftrightarrow \frac{C}{B} = M) \leftrightarrow (C = C \leftrightarrow \neg \frac{C}{B} = M)$
33	31 32	sylibr	$⊢ M \neq \frac{C}{B} \to \neg (C = C \leftrightarrow \frac{C}{B} = M)$
34	33	adantr	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to \neg (C = C \leftrightarrow \frac{C}{B} = M)$
35		0red	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to 0 \in ℝ$
36		fv1prop	$⊢ 0 \in ℝ \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) = 0$
37	35 36	syl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) = 0$
38	37	oveq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) = A \cdot 0$
39		recn	$⊢ A \in ℝ \to A \in ℂ$
40	39	mul01d	$⊢ A \in ℝ \to A \cdot 0 = 0$
41	40	3ad2ant1	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to A \cdot 0 = 0$
42	41	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to A \cdot 0 = 0$
43	38 42	eqtrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) = 0$
44		ovexd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \frac{C}{B} \in V$
45		fv2prop	$⊢ \frac{C}{B} \in V \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = \frac{C}{B}$
46	44 45	syl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = \frac{C}{B}$
47	46	oveq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = B (\frac{C}{B})$
48	14	recnd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C \in ℂ$
49	48	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to C \in ℂ$
50	16	recnd	$⊢ (B \in ℝ \land B \neq 0) \to B \in ℂ$
51	50	3ad2ant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \in ℂ$
52	51	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to B \in ℂ$
53	49 52 20	divcan2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to B (\frac{C}{B}) = C$
54	47 53	eqtrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = C$
55	43 54	oveq12d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = 0 + C$
56	55	adantl	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = 0 + C$
57	48	addlidd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to 0 + C = C$
58	57	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to 0 + C = C$
59	58	adantl	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to 0 + C = C$
60	56 59	eqtrd	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = C$
61	60	eqeq1d	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to (A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow C = C)$
62	46	eqeq1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = M \leftrightarrow \frac{C}{B} = M)$
63	62	adantl	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to (\{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = M \leftrightarrow \frac{C}{B} = M)$
64	61 63	bibi12d	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to ((A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = M) \leftrightarrow (C = C \leftrightarrow \frac{C}{B} = M))$
65	34 64	mtbird	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to \neg (A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = M)$
66		fveq1	$⊢ p = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \to p (1) = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1)$
67	66	oveq2d	$⊢ p = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \to A p (1) = A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1)$
68		fveq1	$⊢ p = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \to p (2) = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2)$
69	68	oveq2d	$⊢ p = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \to B p (2) = B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2)$
70	67 69	oveq12d	$⊢ p = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \to A p (1) + B p (2) = A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2)$
71	70	eqeq1d	$⊢ p = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \to (A p (1) + B p (2) = C \leftrightarrow A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = C)$
72	68	eqeq1d	$⊢ p = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \to (p (2) = M \leftrightarrow \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = M)$
73	71 72	bibi12d	$⊢ p = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \to ((A p (1) + B p (2) = C \leftrightarrow p (2) = M) \leftrightarrow (A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = M))$
74	73	notbid	$⊢ p = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \to (\neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M) \leftrightarrow \neg (A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = M))$
75	74	rspcev	$⊢ (\{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} \in P \land \neg (A \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = M)) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M)$
76	24 65 75	syl2anc	$⊢ (M \neq \frac{C}{B} \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M)$
77	76	ex	$⊢ M \neq \frac{C}{B} \to (((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
78		nne	$⊢ \neg M \neq \frac{C}{B} \leftrightarrow M = \frac{C}{B}$
79		1red	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to 1 \in ℝ$
80	14 17 19	redivcld	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \frac{C}{B} \in ℝ$
81	79 80	jca	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to (1 \in ℝ \land \frac{C}{B} \in ℝ)$
82	81	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (1 \in ℝ \land \frac{C}{B} \in ℝ)$
83	1 3	prelrrx2	$⊢ (1 \in ℝ \land \frac{C}{B} \in ℝ) \to \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \in P$
84	82 83	syl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \in P$
85	84	adantl	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \in P$
86		eqneqall	$⊢ A = 0 \to (A \neq 0 \to \neg \frac{C}{B} = M)$
87	86	com12	$⊢ A \neq 0 \to (A = 0 \to \neg \frac{C}{B} = M)$
88	87	adantl	$⊢ (M = \frac{C}{B} \land A \neq 0) \to (A = 0 \to \neg \frac{C}{B} = M)$
89		pm2.24	$⊢ \frac{C}{B} = M \to (\neg \frac{C}{B} = M \to A = 0)$
90	89	eqcoms	$⊢ M = \frac{C}{B} \to (\neg \frac{C}{B} = M \to A = 0)$
91	90	adantr	$⊢ (M = \frac{C}{B} \land A \neq 0) \to (\neg \frac{C}{B} = M \to A = 0)$
92	88 91	impbid	$⊢ (M = \frac{C}{B} \land A \neq 0) \to (A = 0 \leftrightarrow \neg \frac{C}{B} = M)$
93		xor3	$⊢ \neg (A = 0 \leftrightarrow \frac{C}{B} = M) \leftrightarrow (A = 0 \leftrightarrow \neg \frac{C}{B} = M)$
94	92 93	sylibr	$⊢ (M = \frac{C}{B} \land A \neq 0) \to \neg (A = 0 \leftrightarrow \frac{C}{B} = M)$
95	94	adantr	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to \neg (A = 0 \leftrightarrow \frac{C}{B} = M)$
96		simprl1	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to A \in ℝ$
97	96	recnd	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to A \in ℂ$
98	15	adantl	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to C \in ℝ$
99	98	recnd	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to C \in ℂ$
100	97 99	addcomd	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to A + C = C + A$
101	100	eqeq1d	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to (A + C = C \leftrightarrow C + A = C)$
102		recn	$⊢ C \in ℝ \to C \in ℂ$
103	39 102	anim12ci	$⊢ (A \in ℝ \land C \in ℝ) \to (C \in ℂ \land A \in ℂ)$
104	103	3adant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to (C \in ℂ \land A \in ℂ)$
105	104	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (C \in ℂ \land A \in ℂ)$
106	105	adantl	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to (C \in ℂ \land A \in ℂ)$
107		addid0	$⊢ (C \in ℂ \land A \in ℂ) \to (C + A = C \leftrightarrow A = 0)$
108	106 107	syl	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to (C + A = C \leftrightarrow A = 0)$
109	101 108	bitrd	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to (A + C = C \leftrightarrow A = 0)$
110	109	bibi1d	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to ((A + C = C \leftrightarrow \frac{C}{B} = M) \leftrightarrow (A = 0 \leftrightarrow \frac{C}{B} = M))$
111	95 110	mtbird	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to \neg (A + C = C \leftrightarrow \frac{C}{B} = M)$
112		1ex	$⊢ 1 \in V$
113	112	a1i	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to 1 \in V$
114		fv1prop	$⊢ 1 \in V \to \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) = 1$
115	113 114	syl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) = 1$
116	115	oveq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) = A \cdot 1$
117		ax-1rid	$⊢ A \in ℝ \to A \cdot 1 = A$
118	117	3ad2ant1	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to A \cdot 1 = A$
119	118	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to A \cdot 1 = A$
120	116 119	eqtrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) = A$
121		fv2prop	$⊢ \frac{C}{B} \in V \to \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = \frac{C}{B}$
122	44 121	syl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = \frac{C}{B}$
123	122	oveq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = B (\frac{C}{B})$
124	15	recnd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to C \in ℂ$
125	124 52 20	divcan2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to B (\frac{C}{B}) = C$
126	123 125	eqtrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = C$
127	120 126	oveq12d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = A + C$
128	127	eqeq1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow A + C = C)$
129	122	eqeq1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = M \leftrightarrow \frac{C}{B} = M)$
130	128 129	bibi12d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to ((A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = M) \leftrightarrow (A + C = C \leftrightarrow \frac{C}{B} = M))$
131	130	notbid	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\neg (A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = M) \leftrightarrow \neg (A + C = C \leftrightarrow \frac{C}{B} = M))$
132	131	adantl	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to (\neg (A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = M) \leftrightarrow \neg (A + C = C \leftrightarrow \frac{C}{B} = M))$
133	111 132	mpbird	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to \neg (A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = M)$
134		fveq1	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \to p (1) = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1)$
135	134	oveq2d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \to A p (1) = A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1)$
136		fveq1	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \to p (2) = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2)$
137	136	oveq2d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \to B p (2) = B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2)$
138	135 137	oveq12d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \to A p (1) + B p (2) = A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2)$
139	138	eqeq1d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \to (A p (1) + B p (2) = C \leftrightarrow A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = C)$
140	136	eqeq1d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \to (p (2) = M \leftrightarrow \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = M)$
141	139 140	bibi12d	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \to ((A p (1) + B p (2) = C \leftrightarrow p (2) = M) \leftrightarrow (A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = M))$
142	141	notbid	$⊢ p = \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \to (\neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M) \leftrightarrow \neg (A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = M))$
143	142	rspcev	$⊢ (\{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} \in P \land \neg (A \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (1) + B \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = C \leftrightarrow \{⟨1, 1⟩, ⟨2, \frac{C}{B}⟩\} (2) = M)) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M)$
144	85 133 143	syl2anc	$⊢ ((M = \frac{C}{B} \land A \neq 0) \land ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ)) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M)$
145	144	ex	$⊢ (M = \frac{C}{B} \land A \neq 0) \to (((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
146	78 145	sylanb	$⊢ (\neg M \neq \frac{C}{B} \land A \neq 0) \to (((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
147	77 146	jaoi3	$⊢ (M \neq \frac{C}{B} \lor A \neq 0) \to (((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
148	147	orcoms	$⊢ (A \neq 0 \lor M \neq \frac{C}{B}) \to (((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
149	148	com12	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to ((A \neq 0 \lor M \neq \frac{C}{B}) \to \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
150		rexnal	$⊢ \exists p \in P \neg (A p (1) + B p (2) = C \leftrightarrow p (2) = M) \leftrightarrow \neg \forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = M)$
151	149 150	imbitrdi	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to ((A \neq 0 \lor M \neq \frac{C}{B}) \to \neg \forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
152	12 151	biimtrid	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\neg (A = 0 \land M = \frac{C}{B}) \to \neg \forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
153	152	con4d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = M) \to (A = 0 \land M = \frac{C}{B}))$

Metamath Proof Explorer

Theorem line2xlem

Proof