# Metamath Proof Explorer

## Theorem 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}=\left\{1,2\right\}$
line2.e ${⊢}{E}={{I}}^{}$
line2.p ${⊢}{P}={ℝ}^{{I}}$
line2.l ${⊢}{L}={Line}_{M}\left({E}\right)$
line2.g ${⊢}{G}=\left\{{p}\in {P}|{A}{p}\left(1\right)+{B}{p}\left(2\right)={C}\right\}$
line2x.x ${⊢}{X}=\left\{⟨1,0⟩,⟨2,{M}⟩\right\}$
line2x.y ${⊢}{Y}=\left\{⟨1,1⟩,⟨2,{M}⟩\right\}$
Assertion line2xlem ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge {B}\ne 0\right)\wedge {C}\in ℝ\right)\wedge {M}\in ℝ\right)\to \left(\forall {p}\in {P}\phantom{\rule{.4em}{0ex}}\left({A}{p}\left(1\right)+{B}{p}\left(2\right)={C}↔{p}\left(2\right)={M}\right)\to \left({A}=0\wedge {M}=\frac{{C}}{{B}}\right)\right)$

### Proof

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