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 𝐼 = { 1 , 2 }
line2.e 𝐸 = ( ℝ^ ‘ 𝐼 )
line2.p 𝑃 = ( ℝ ↑m 𝐼 )
line2.l 𝐿 = ( LineM𝐸 )
line2.g 𝐺 = { 𝑝𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
line2x.x 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ }
line2x.y 𝑌 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ }
Assertion line2xlem ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) → ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )

Proof

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