Metamath Proof Explorer

Theorem line2ylem

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

Ref Expression
Hypotheses line2ylem.i ⊢ 𝐼 = ( 0 ..^ 2 )
line2ylem.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
Assertion line2ylem ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) → ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 line2ylem.i ⊢ 𝐼 = ( 0 ..^ 2 )
2 line2ylem.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3 ianor ⊢ ( ¬ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) ↔ ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∨ ¬ 𝐶 = 0 ) )
4 df-ne ⊢ ( 𝐶 ≠ 0 ↔ ¬ 𝐶 = 0 )
5 0re ⊢ 0 ∈ ℝ
6 1 2 prelrrx2 ⊢ ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ⟨“ 0 0 ”⟩ ∈ 𝑃 )
7 5 5 6 mp2an ⊢ ⟨“ 0 0 ”⟩ ∈ 𝑃
8 eqneqall ⊢ ( 𝐶 = 0 → ( 𝐶 ≠ 0 → ¬ 0 = 0 ) )
9 8 com12 ⊢ ( 𝐶 ≠ 0 → ( 𝐶 = 0 → ¬ 0 = 0 ) )
10 eqid ⊢ 0 = 0
11 10 pm2.24i ⊢ ( ¬ 0 = 0 → 𝐶 = 0 )
12 9 11 impbid1 ⊢ ( 𝐶 ≠ 0 → ( 𝐶 = 0 ↔ ¬ 0 = 0 ) )
13 12 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ( 𝐶 = 0 ↔ ¬ 0 = 0 ) )
14 xor3 ⊢ ( ¬ ( 𝐶 = 0 ↔ 0 = 0 ) ↔ ( 𝐶 = 0 ↔ ¬ 0 = 0 ) )
15 13 14 sylibr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ¬ ( 𝐶 = 0 ↔ 0 = 0 ) )
16 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
17 16 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
18 17 mul01d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 0 ) = 0 )
19 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
20 19 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
21 20 mul01d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 0 ) = 0 )
22 18 21 oveq12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = ( 0 + 0 ) )
23 00id ⊢ ( 0 + 0 ) = 0
24 22 23 eqtrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 0 )
25 24 eqeq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 𝐶 ) )
26 eqcom ⊢ ( 0 = 𝐶 ↔ 𝐶 = 0 )
27 25 26 bitrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 𝐶 = 0 ) )
28 27 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 𝐶 = 0 ) )
29 28 bibi1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ( ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ↔ ( 𝐶 = 0 ↔ 0 = 0 ) ) )
30 15 29 mtbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ¬ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) )
31 fveq1 ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( 𝑝 ‘ 0 ) = ( ⟨“ 0 0 ”⟩ ‘ 0 ) )
32 c0ex ⊢ 0 ∈ V
33 s2fv0 ⊢ ( 0 ∈ V → ( ⟨“ 0 0 ”⟩ ‘ 0 ) = 0 )
34 32 33 ax-mp ⊢ ( ⟨“ 0 0 ”⟩ ‘ 0 ) = 0
35 31 34 eqtrdi ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( 𝑝 ‘ 0 ) = 0 )
36 35 oveq2d ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( 𝐴 · ( 𝑝 ‘ 0 ) ) = ( 𝐴 · 0 ) )
37 fveq1 ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( 𝑝 ‘ 1 ) = ( ⟨“ 0 0 ”⟩ ‘ 1 ) )
38 s2fv1 ⊢ ( 0 ∈ V → ( ⟨“ 0 0 ”⟩ ‘ 1 ) = 0 )
39 32 38 ax-mp ⊢ ( ⟨“ 0 0 ”⟩ ‘ 1 ) = 0
40 37 39 eqtrdi ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( 𝑝 ‘ 1 ) = 0 )
41 40 oveq2d ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( 𝐵 · ( 𝑝 ‘ 1 ) ) = ( 𝐵 · 0 ) )
42 36 41 oveq12d ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) )
43 42 eqeq1d ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ) )
44 35 eqeq1d ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( ( 𝑝 ‘ 0 ) = 0 ↔ 0 = 0 ) )
45 43 44 bibi12d ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ↔ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ) )
46 45 notbid ⊢ ( 𝑝 = ⟨“ 0 0 ”⟩ → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ↔ ¬ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ) )
47 46 rspcev ⊢ ( ( ⟨“ 0 0 ”⟩ ∈ 𝑃 ∧ ¬ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) )
48 7 30 47 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) )
49 48 expcom ⊢ ( 𝐶 ≠ 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
50 4 49 sylbir ⊢ ( ¬ 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
51 notnotb ⊢ ( 𝐶 = 0 ↔ ¬ ¬ 𝐶 = 0 )
52 ianor ⊢ ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ↔ ( ¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0 ) )
53 df-ne ⊢ ( 𝐵 ≠ 0 ↔ ¬ 𝐵 = 0 )
54 fveq1 ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( 𝑝 ‘ 0 ) = ( ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ ‘ 0 ) )
55 1ex ⊢ 1 ∈ V
56 s2fv0 ⊢ ( 1 ∈ V → ( ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ ‘ 0 ) = 1 )
57 55 56 ax-mp ⊢ ( ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ ‘ 0 ) = 1
58 54 57 eqtrdi ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( 𝑝 ‘ 0 ) = 1 )
59 58 oveq2d ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( 𝐴 · ( 𝑝 ‘ 0 ) ) = ( 𝐴 · 1 ) )
60 fveq1 ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( 𝑝 ‘ 1 ) = ( ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ ‘ 1 ) )
61 ovex ⊢ ( - 𝐴 / 𝐵 ) ∈ V
62 s2fv1 ⊢ ( ( - 𝐴 / 𝐵 ) ∈ V → ( ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ ‘ 1 ) = ( - 𝐴 / 𝐵 ) )
63 61 62 ax-mp ⊢ ( ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ ‘ 1 ) = ( - 𝐴 / 𝐵 )
64 60 63 eqtrdi ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( 𝑝 ‘ 1 ) = ( - 𝐴 / 𝐵 ) )
65 64 oveq2d ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( 𝐵 · ( 𝑝 ‘ 1 ) ) = ( 𝐵 · ( - 𝐴 / 𝐵 ) ) )
66 59 65 oveq12d ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) )
67 66 eqeq1d ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ) )
68 58 eqeq1d ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( ( 𝑝 ‘ 0 ) = 0 ↔ 1 = 0 ) )
69 67 68 bibi12d ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ↔ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ) )
70 69 notbid ⊢ ( 𝑝 = ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ↔ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ) )
71 1red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 1 ∈ ℝ )
72 16 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐴 ∈ ℝ )
73 72 renegcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → - 𝐴 ∈ ℝ )
74 19 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐵 ∈ ℝ )
75 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐵 ≠ 0 )
76 73 74 75 redivcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( - 𝐴 / 𝐵 ) ∈ ℝ )
77 1 2 prelrrx2 ⊢ ( ( 1 ∈ ℝ ∧ ( - 𝐴 / 𝐵 ) ∈ ℝ ) → ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ ∈ 𝑃 )
78 71 76 77 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ⟨“ 1 ( - 𝐴 / 𝐵 ) ”⟩ ∈ 𝑃 )
79 ax-1ne0 ⊢ 1 ≠ 0
80 79 neii ⊢ ¬ 1 = 0
81 10 80 2th ⊢ ( 0 = 0 ↔ ¬ 1 = 0 )
82 xor3 ⊢ ( ¬ ( 0 = 0 ↔ 1 = 0 ) ↔ ( 0 = 0 ↔ ¬ 1 = 0 ) )
83 81 82 mpbir ⊢ ¬ ( 0 = 0 ↔ 1 = 0 )
84 17 mulridd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 1 ) = 𝐴 )
85 84 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( 𝐴 · 1 ) = 𝐴 )
86 17 negcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → - 𝐴 ∈ ℂ )
87 86 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → - 𝐴 ∈ ℂ )
88 20 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐵 ∈ ℂ )
89 87 88 75 divcan2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( 𝐵 · ( - 𝐴 / 𝐵 ) ) = - 𝐴 )
90 85 89 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = ( 𝐴 + - 𝐴 ) )
91 17 negidd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + - 𝐴 ) = 0 )
92 91 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( 𝐴 + - 𝐴 ) = 0 )
93 90 92 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 0 )
94 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐶 = 0 )
95 93 94 eqeq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 0 = 0 ) )
96 95 bibi1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ↔ ( 0 = 0 ↔ 1 = 0 ) ) )
97 83 96 mtbiri ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) )
98 70 78 97 rspcedvdw ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) )
99 98 expcom ⊢ ( ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
100 99 ex ⊢ ( 𝐵 ≠ 0 → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) ) )
101 53 100 sylbir ⊢ ( ¬ 𝐵 = 0 → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) ) )
102 notnotb ⊢ ( 𝐵 = 0 ↔ ¬ ¬ 𝐵 = 0 )
103 nne ⊢ ( ¬ 𝐴 ≠ 0 ↔ 𝐴 = 0 )
104 103 bicomi ⊢ ( 𝐴 = 0 ↔ ¬ 𝐴 ≠ 0 )
105 1re ⊢ 1 ∈ ℝ
106 1 2 prelrrx2 ⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ⟨“ 1 1 ”⟩ ∈ 𝑃 )
107 105 105 106 mp2an ⊢ ⟨“ 1 1 ”⟩ ∈ 𝑃
108 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 · 1 ) = ( 0 · 1 ) )
109 108 adantl ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐴 · 1 ) = ( 0 · 1 ) )
110 ax-1cn ⊢ 1 ∈ ℂ
111 110 mul02i ⊢ ( 0 · 1 ) = 0
112 109 111 eqtrdi ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐴 · 1 ) = 0 )
113 oveq1 ⊢ ( 𝐵 = 0 → ( 𝐵 · 1 ) = ( 0 · 1 ) )
114 113 adantr ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐵 · 1 ) = ( 0 · 1 ) )
115 114 111 eqtrdi ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐵 · 1 ) = 0 )
116 112 115 oveq12d ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = ( 0 + 0 ) )
117 116 23 eqtrdi ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 0 )
118 id ⊢ ( 𝐶 = 0 → 𝐶 = 0 )
119 117 118 eqeqan12d ⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 0 = 0 ) )
120 119 bibi1d ⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ( ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ↔ ( 0 = 0 ↔ 1 = 0 ) ) )
121 83 120 mtbiri ⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) )
122 fveq1 ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( 𝑝 ‘ 0 ) = ( ⟨“ 1 1 ”⟩ ‘ 0 ) )
123 s2fv0 ⊢ ( 1 ∈ V → ( ⟨“ 1 1 ”⟩ ‘ 0 ) = 1 )
124 55 123 ax-mp ⊢ ( ⟨“ 1 1 ”⟩ ‘ 0 ) = 1
125 122 124 eqtrdi ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( 𝑝 ‘ 0 ) = 1 )
126 125 oveq2d ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( 𝐴 · ( 𝑝 ‘ 0 ) ) = ( 𝐴 · 1 ) )
127 fveq1 ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( 𝑝 ‘ 1 ) = ( ⟨“ 1 1 ”⟩ ‘ 1 ) )
128 s2fv1 ⊢ ( 1 ∈ V → ( ⟨“ 1 1 ”⟩ ‘ 1 ) = 1 )
129 55 128 ax-mp ⊢ ( ⟨“ 1 1 ”⟩ ‘ 1 ) = 1
130 127 129 eqtrdi ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( 𝑝 ‘ 1 ) = 1 )
131 130 oveq2d ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( 𝐵 · ( 𝑝 ‘ 1 ) ) = ( 𝐵 · 1 ) )
132 126 131 oveq12d ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) )
133 132 eqeq1d ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ) )
134 125 eqeq1d ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( ( 𝑝 ‘ 0 ) = 0 ↔ 1 = 0 ) )
135 133 134 bibi12d ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ↔ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ) )
136 135 notbid ⊢ ( 𝑝 = ⟨“ 1 1 ”⟩ → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ↔ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ) )
137 136 rspcev ⊢ ( ( ⟨“ 1 1 ”⟩ ∈ 𝑃 ∧ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) )
138 107 121 137 sylancr ⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) )
139 138 a1d ⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
140 139 ex ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) ) )
141 102 104 140 syl2anbr ⊢ ( ( ¬ ¬ 𝐵 = 0 ∧ ¬ 𝐴 ≠ 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) ) )
142 101 141 jaoi3 ⊢ ( ( ¬ 𝐵 = 0 ∨ ¬ 𝐴 ≠ 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) ) )
143 142 orcoms ⊢ ( ( ¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) ) )
144 52 143 sylbi ⊢ ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) ) )
145 144 com12 ⊢ ( 𝐶 = 0 → ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) ) )
146 51 145 sylbir ⊢ ( ¬ ¬ 𝐶 = 0 → ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) ) )
147 146 imp ⊢ ( ( ¬ ¬ 𝐶 = 0 ∧ ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
148 50 147 jaoi3 ⊢ ( ( ¬ 𝐶 = 0 ∨ ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
149 148 orcoms ⊢ ( ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∨ ¬ 𝐶 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
150 149 com12 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∨ ¬ 𝐶 = 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
151 3 150 biimtrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
152 rexnal ⊢ ( ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ↔ ¬ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) )
153 151 152 imbitrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) → ¬ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
154 153 con4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) → ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) ) )
155 df-3an ⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ↔ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) )
156 154 155 imbitrrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) → ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )