Theorem line2ylem 46097

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

Hypotheses

Ref	Expression
line2ylem.i	⊢ 𝐼 = {1, 2}
line2ylem.p	⊢ 𝑃 = (ℝ ↑m 𝐼)

Assertion

Ref	Expression
line2ylem	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))

Distinct variable groups:   𝐴,𝑝   𝐵,𝑝   𝐶,𝑝   𝑃,𝑝

Allowed substitution hint:   𝐼(𝑝)

Proof of Theorem line2ylem

Step	Hyp	Ref	Expression
1		ianor 979	. . . . 5 ⊢ (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) ↔ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0))
2		df-ne 2944	. . . . . . . . 9 ⊢ (𝐶 ≠ 0 ↔ ¬ 𝐶 = 0)
3		0re 10977	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
4		line2ylem.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = {1, 2}
5		line2ylem.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (ℝ ↑m 𝐼)
6	4, 5	prelrrx2 46059	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → {⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃)
7	3, 3, 6	mp2an 689	. . . . . . . . . . 11 ⊢ {⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃
8		eqneqall 2954	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → (𝐶 ≠ 0 → ¬ 0 = 0))
9	8	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ≠ 0 → (𝐶 = 0 → ¬ 0 = 0))
10		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ 0 = 0
11	10	pm2.24i 150	. . . . . . . . . . . . . . 15 ⊢ (¬ 0 = 0 → 𝐶 = 0)
12	9, 11	impbid1 224	. . . . . . . . . . . . . 14 ⊢ (𝐶 ≠ 0 → (𝐶 = 0 ↔ ¬ 0 = 0))
13	12	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → (𝐶 = 0 ↔ ¬ 0 = 0))
14		xor3 384	. . . . . . . . . . . . 13 ⊢ (¬ (𝐶 = 0 ↔ 0 = 0) ↔ (𝐶 = 0 ↔ ¬ 0 = 0))
15	13, 14	sylibr 233	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ¬ (𝐶 = 0 ↔ 0 = 0))
16		simp1 1135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
17	16	recnd 11003	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
18	17	mul01d 11174	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 0) = 0)
19		simp2 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
20	19	recnd 11003	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
21	20	mul01d 11174	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 0) = 0)
22	18, 21	oveq12d 7293	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 0) + (𝐵 · 0)) = (0 + 0))
23		00id 11150	. . . . . . . . . . . . . . . . 17 ⊢ (0 + 0) = 0
24	22, 23	eqtrdi 2794	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 0) + (𝐵 · 0)) = 0)
25	24	eqeq1d 2740	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 𝐶))
26		eqcom 2745	. . . . . . . . . . . . . . 15 ⊢ (0 = 𝐶 ↔ 𝐶 = 0)
27	25, 26	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 𝐶 = 0))
28	27	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 𝐶 = 0))
29	28	bibi1d 344	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ((((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0) ↔ (𝐶 = 0 ↔ 0 = 0)))
30	15, 29	mtbird 325	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0))
31		fveq1 6773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘1) = ({⟨1, 0⟩, ⟨2, 0⟩}‘1))
32		1ex 10971	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ V
33		c0ex 10969	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ V
34		1ne2 12181	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ≠ 2
35		fvpr1g 7062	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 0⟩}‘1) = 0)
36	32, 33, 34, 35	mp3an 1460	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨1, 0⟩, ⟨2, 0⟩}‘1) = 0
37	31, 36	eqtrdi 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘1) = 0)
38	37	oveq2d 7291	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 0))
39		fveq1 6773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘2) = ({⟨1, 0⟩, ⟨2, 0⟩}‘2))
40		2ex 12050	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ V
41		fvpr2g 7063	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 0⟩}‘2) = 0)
42	40, 33, 34, 41	mp3an 1460	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨1, 0⟩, ⟨2, 0⟩}‘2) = 0
43	39, 42	eqtrdi 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘2) = 0)
44	43	oveq2d 7291	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · 0))
45	38, 44	oveq12d 7293	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 0) + (𝐵 · 0)))
46	45	eqeq1d 2740	. . . . . . . . . . . . . 14 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 0) + (𝐵 · 0)) = 𝐶))
47	37	eqeq1d 2740	. . . . . . . . . . . . . 14 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((𝑝‘1) = 0 ↔ 0 = 0))
48	46, 47	bibi12d 346	. . . . . . . . . . . . 13 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0)))
49	48	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0)))
50	49	rspcev 3561	. . . . . . . . . . 11 ⊢ (({⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
51	7, 30, 50	sylancr 587	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
52	51	expcom 414	. . . . . . . . 9 ⊢ (𝐶 ≠ 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
53	2, 52	sylbir 234	. . . . . . . 8 ⊢ (¬ 𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
54		notnotb 315	. . . . . . . . . 10 ⊢ (𝐶 = 0 ↔ ¬ ¬ 𝐶 = 0)
55		ianor 979	. . . . . . . . . . . 12 ⊢ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ↔ (¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0))
56		df-ne 2944	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≠ 0 ↔ ¬ 𝐵 = 0)
57		1red 10976	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 1 ∈ ℝ)
58	16	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐴 ∈ ℝ)
59	58	renegcld 11402	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → -𝐴 ∈ ℝ)
60	19	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ∈ ℝ)
61		simprl 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ≠ 0)
62	59, 60, 61	redivcld 11803	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (-𝐴 / 𝐵) ∈ ℝ)
63	4, 5	prelrrx2 46059	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ (-𝐴 / 𝐵) ∈ ℝ) → {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃)
64	57, 62, 63	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃)
65		ax-1ne0 10940	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 0
66	65	neii 2945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 1 = 0
67	10, 66	2th 263	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = 0 ↔ ¬ 1 = 0)
68		xor3 384	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (0 = 0 ↔ 1 = 0) ↔ (0 = 0 ↔ ¬ 1 = 0))
69	67, 68	mpbir 230	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ (0 = 0 ↔ 1 = 0)
70	17	mulid1d 10992	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 1) = 𝐴)
71	70	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐴 · 1) = 𝐴)
72	17	negcld 11319	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → -𝐴 ∈ ℂ)
73	72	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → -𝐴 ∈ ℂ)
74	20	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ∈ ℂ)
75	73, 74, 61	divcan2d 11753	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐵 · (-𝐴 / 𝐵)) = -𝐴)
76	71, 75	oveq12d 7293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = (𝐴 + -𝐴))
77	17	negidd 11322	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 + -𝐴) = 0)
78	77	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐴 + -𝐴) = 0)
79	76, 78	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 0)
80		simprr 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐶 = 0)
81	79, 80	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 0 = 0))
82	81	bibi1d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0) ↔ (0 = 0 ↔ 1 = 0)))
83	69, 82	mtbiri 327	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0))
84		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘1) = ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1))
85		fvpr1g 7062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1) = 1)
86	32, 32, 34, 85	mp3an 1460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1) = 1
87	84, 86	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘1) = 1)
88	87	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 1))
89		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘2) = ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2))
90		ovex 7308	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (-𝐴 / 𝐵) ∈ V
91		fvpr2g 7063	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ V ∧ (-𝐴 / 𝐵) ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2) = (-𝐴 / 𝐵))
92	40, 90, 34, 91	mp3an 1460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2) = (-𝐴 / 𝐵)
93	89, 92	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘2) = (-𝐴 / 𝐵))
94	93	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · (-𝐴 / 𝐵)))
95	88, 94	oveq12d 7293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))))
96	95	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶))
97	87	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((𝑝‘1) = 0 ↔ 1 = 0))
98	96, 97	bibi12d 346	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0)))
99	98	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0)))
100	99	rspcev 3561	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
101	64, 83, 100	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
102	101	expcom 414	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ≠ 0 ∧ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
103	102	ex 413	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≠ 0 → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
104	56, 103	sylbir 234	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐵 = 0 → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
105		notnotb 315	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 ↔ ¬ ¬ 𝐵 = 0)
106		nne 2947	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝐴 ≠ 0 ↔ 𝐴 = 0)
107	106	bicomi 223	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = 0 ↔ ¬ 𝐴 ≠ 0)
108		1re 10975	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
109	4, 5	prelrrx2 46059	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ) → {⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃)
110	108, 108, 109	mp2an 689	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃
111		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 = 0 → (𝐴 · 1) = (0 · 1))
112	111	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐴 · 1) = (0 · 1))
113		ax-1cn 10929	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℂ
114	113	mul02i 11164	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 · 1) = 0
115	112, 114	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐴 · 1) = 0)
116		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 = 0 → (𝐵 · 1) = (0 · 1))
117	116	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐵 · 1) = (0 · 1))
118	117, 114	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐵 · 1) = 0)
119	115, 118	oveq12d 7293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → ((𝐴 · 1) + (𝐵 · 1)) = (0 + 0))
120	119, 23	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → ((𝐴 · 1) + (𝐵 · 1)) = 0)
121		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 = 0 → 𝐶 = 0)
122	120, 121	eqeqan12d 2752	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 0 = 0))
123	122	bibi1d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ((((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0) ↔ (0 = 0 ↔ 1 = 0)))
124	69, 123	mtbiri 327	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ¬ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0))
125		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘1) = ({⟨1, 1⟩, ⟨2, 1⟩}‘1))
126		fvpr1g 7062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 1⟩}‘1) = 1)
127	32, 32, 34, 126	mp3an 1460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, 1⟩}‘1) = 1
128	125, 127	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘1) = 1)
129	128	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 1))
130		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘2) = ({⟨1, 1⟩, ⟨2, 1⟩}‘2))
131		fvpr2g 7063	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 1⟩}‘2) = 1)
132	40, 32, 34, 131	mp3an 1460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, 1⟩}‘2) = 1
133	130, 132	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘2) = 1)
134	133	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · 1))
135	129, 134	oveq12d 7293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 1) + (𝐵 · 1)))
136	135	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 1) + (𝐵 · 1)) = 𝐶))
137	128	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((𝑝‘1) = 0 ↔ 1 = 0))
138	136, 137	bibi12d 346	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0)))
139	138	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0)))
140	139	rspcev 3561	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
141	110, 124, 140	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
142	141	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
143	142	ex 413	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
144	105, 107, 143	syl2anbr 599	. . . . . . . . . . . . . 14 ⊢ ((¬ ¬ 𝐵 = 0 ∧ ¬ 𝐴 ≠ 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
145	104, 144	jaoi3 1058	. . . . . . . . . . . . 13 ⊢ ((¬ 𝐵 = 0 ∨ ¬ 𝐴 ≠ 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
146	145	orcoms 869	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
147	55, 146	sylbi 216	. . . . . . . . . . 11 ⊢ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
148	147	com12 32	. . . . . . . . . 10 ⊢ (𝐶 = 0 → (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
149	54, 148	sylbir 234	. . . . . . . . 9 ⊢ (¬ ¬ 𝐶 = 0 → (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
150	149	imp 407	. . . . . . . 8 ⊢ ((¬ ¬ 𝐶 = 0 ∧ ¬ (𝐴 ≠ 0 ∧ 𝐵 = 0)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
151	53, 150	jaoi3 1058	. . . . . . 7 ⊢ ((¬ 𝐶 = 0 ∨ ¬ (𝐴 ≠ 0 ∧ 𝐵 = 0)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
152	151	orcoms 869	. . . . . 6 ⊢ ((¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
153	152	com12 32	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
154	1, 153	syl5bi 241	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
155		rexnal 3169	. . . 4 ⊢ (∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
156	154, 155	syl6ib 250	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) → ¬ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
157	156	con4d 115	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0)))
158		df-3an 1088	. 2 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) ↔ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0))
159	157, 158	syl6ibr 251	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432  {cpr 4563  ⟨cop 4567  ‘cfv 6433  (class class class)co 7275   ↑_m cmap 8615  ℂcc 10869  ℝcr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876  -cneg 11206   / cdiv 11632  2c2 12028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-2 12036

This theorem is referenced by:  line2y  46101