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 biconditional is true, RHS is false); 2. A =/= 0 /\ M = ( C / B ) : p = (1,C/B) (LHS of biconditional is false, RHS is true). (Contributed by AV, 4-Feb-2023)

	Ref	Expression
Hypotheses	line2.i	$⊢ I = (0 ..^2)$
	line2.e	$⊢ E = I$
	line2.p	$⊢ P = ℝ^{I}$
	line2.l	$⊢ L = {Line}_{M} (E)$
	line2.g	$⊢ G = \{p \in P \| A p (0) + B p (1) = C\}$
	line2x.x	$⊢ X = ⟨“ 0 M ”⟩$
	line2x.y	$⊢ Y = ⟨“ 1 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 (0) + B p (1) = C \leftrightarrow p (1) = M) \to (A = 0 \land M = \frac{C}{B}))$

Proof

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

Metamath Proof Explorer

Theorem line2xlem

Proof