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 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 = { 1 , 2 }
line2.e 
|- E = ( RR^ ` I )
line2.p 
|- P = ( RR ^m I )
line2.l 
|- L = ( LineM ` E )
line2.g 
|- G = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C }
line2x.x 
|- X = { <. 1 , 0 >. , <. 2 , M >. }
line2x.y 
|- Y = { <. 1 , 1 >. , <. 2 , M >. }
Assertion line2xlem 
|- ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 2 ) = M ) -> ( A = 0 /\ M = ( C / B ) ) ) )

Proof

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