Theorem line2ylem 49105

Description: Lemma for line2y 49109. This proof is based on counterexamples for the following cases: 1. 𝐶 ≠ 0: p = (0,0) (LHS of biconditional is false, RHS is true); 2. 𝐶 = 0 ∧ 𝐵 ≠ 0: p = (1,-A/B) (LHS of biconditional is true, RHS is false); 3. 𝐴 = 𝐵 = 𝐶 = 0: p = (1,1) (LHS of biconditional 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 984	. . . . 5 ⊢ (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) ↔ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0))
2		df-ne 2934	. . . . . . . . 9 ⊢ (𝐶 ≠ 0 ↔ ¬ 𝐶 = 0)
3		0re 11146	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
4		line2ylem.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = {1, 2}
5		line2ylem.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (ℝ ↑m 𝐼)
6	4, 5	prelrrx2 49067	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → {⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃)
7	3, 3, 6	mp2an 693	. . . . . . . . . . 11 ⊢ {⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃
8		eqneqall 2944	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → (𝐶 ≠ 0 → ¬ 0 = 0))
9	8	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ≠ 0 → (𝐶 = 0 → ¬ 0 = 0))
10		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ 0 = 0
11	10	pm2.24i 150	. . . . . . . . . . . . . . 15 ⊢ (¬ 0 = 0 → 𝐶 = 0)
12	9, 11	impbid1 225	. . . . . . . . . . . . . 14 ⊢ (𝐶 ≠ 0 → (𝐶 = 0 ↔ ¬ 0 = 0))
13	12	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → (𝐶 = 0 ↔ ¬ 0 = 0))
14		xor3 382	. . . . . . . . . . . . 13 ⊢ (¬ (𝐶 = 0 ↔ 0 = 0) ↔ (𝐶 = 0 ↔ ¬ 0 = 0))
15	13, 14	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ¬ (𝐶 = 0 ↔ 0 = 0))
16		simp1 1137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
17	16	recnd 11172	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
18	17	mul01d 11344	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 0) = 0)
19		simp2 1138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
20	19	recnd 11172	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
21	20	mul01d 11344	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 0) = 0)
22	18, 21	oveq12d 7386	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 0) + (𝐵 · 0)) = (0 + 0))
23		00id 11320	. . . . . . . . . . . . . . . . 17 ⊢ (0 + 0) = 0
24	22, 23	eqtrdi 2788	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 0) + (𝐵 · 0)) = 0)
25	24	eqeq1d 2739	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 𝐶))
26		eqcom 2744	. . . . . . . . . . . . . . 15 ⊢ (0 = 𝐶 ↔ 𝐶 = 0)
27	25, 26	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 𝐶 = 0))
28	27	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 𝐶 = 0))
29	28	bibi1d 343	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ((((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0) ↔ (𝐶 = 0 ↔ 0 = 0)))
30	15, 29	mtbird 325	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0))
31		fveq1 6841	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘1) = ({⟨1, 0⟩, ⟨2, 0⟩}‘1))
32		1ex 11140	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ V
33		c0ex 11138	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ V
34		1ne2 12360	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ≠ 2
35		fvpr1g 7146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 0⟩}‘1) = 0)
36	32, 33, 34, 35	mp3an 1464	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨1, 0⟩, ⟨2, 0⟩}‘1) = 0
37	31, 36	eqtrdi 2788	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘1) = 0)
38	37	oveq2d 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 0))
39		fveq1 6841	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘2) = ({⟨1, 0⟩, ⟨2, 0⟩}‘2))
40		2ex 12234	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ V
41		fvpr2g 7147	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 0⟩}‘2) = 0)
42	40, 33, 34, 41	mp3an 1464	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨1, 0⟩, ⟨2, 0⟩}‘2) = 0
43	39, 42	eqtrdi 2788	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘2) = 0)
44	43	oveq2d 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · 0))
45	38, 44	oveq12d 7386	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 0) + (𝐵 · 0)))
46	45	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 0) + (𝐵 · 0)) = 𝐶))
47	37	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((𝑝‘1) = 0 ↔ 0 = 0))
48	46, 47	bibi12d 345	. . . . . . . . . . . . 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 3578	. . . . . . . . . . 11 ⊢ (({⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
51	7, 30, 50	sylancr 588	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
52	51	expcom 413	. . . . . . . . 9 ⊢ (𝐶 ≠ 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
53	2, 52	sylbir 235	. . . . . . . 8 ⊢ (¬ 𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
54		notnotb 315	. . . . . . . . . 10 ⊢ (𝐶 = 0 ↔ ¬ ¬ 𝐶 = 0)
55		ianor 984	. . . . . . . . . . . 12 ⊢ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ↔ (¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0))
56		df-ne 2934	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≠ 0 ↔ ¬ 𝐵 = 0)
57		1red 11145	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 1 ∈ ℝ)
58	16	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐴 ∈ ℝ)
59	58	renegcld 11576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → -𝐴 ∈ ℝ)
60	19	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ∈ ℝ)
61		simprl 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ≠ 0)
62	59, 60, 61	redivcld 11981	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (-𝐴 / 𝐵) ∈ ℝ)
63	4, 5	prelrrx2 49067	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ (-𝐴 / 𝐵) ∈ ℝ) → {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃)
64	57, 62, 63	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃)
65		ax-1ne0 11107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 0
66	65	neii 2935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 1 = 0
67	10, 66	2th 264	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = 0 ↔ ¬ 1 = 0)
68		xor3 382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (0 = 0 ↔ 1 = 0) ↔ (0 = 0 ↔ ¬ 1 = 0))
69	67, 68	mpbir 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ (0 = 0 ↔ 1 = 0)
70	17	mulridd 11161	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 1) = 𝐴)
71	70	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐴 · 1) = 𝐴)
72	17	negcld 11491	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → -𝐴 ∈ ℂ)
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → -𝐴 ∈ ℂ)
74	20	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ∈ ℂ)
75	73, 74, 61	divcan2d 11931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐵 · (-𝐴 / 𝐵)) = -𝐴)
76	71, 75	oveq12d 7386	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = (𝐴 + -𝐴))
77	17	negidd 11494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 + -𝐴) = 0)
78	77	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐴 + -𝐴) = 0)
79	76, 78	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 0)
80		simprr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐶 = 0)
81	79, 80	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 0 = 0))
82	81	bibi1d 343	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0) ↔ (0 = 0 ↔ 1 = 0)))
83	69, 82	mtbiri 327	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0))
84		fveq1 6841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘1) = ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1))
85		fvpr1g 7146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1) = 1)
86	32, 32, 34, 85	mp3an 1464	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1) = 1
87	84, 86	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘1) = 1)
88	87	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 1))
89		fveq1 6841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘2) = ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2))
90		ovex 7401	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (-𝐴 / 𝐵) ∈ V
91		fvpr2g 7147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ V ∧ (-𝐴 / 𝐵) ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2) = (-𝐴 / 𝐵))
92	40, 90, 34, 91	mp3an 1464	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2) = (-𝐴 / 𝐵)
93	89, 92	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘2) = (-𝐴 / 𝐵))
94	93	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · (-𝐴 / 𝐵)))
95	88, 94	oveq12d 7386	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))))
96	95	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶))
97	87	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((𝑝‘1) = 0 ↔ 1 = 0))
98	96, 97	bibi12d 345	. . . . . . . . . . . . . . . . . . . 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 3578	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
101	64, 83, 100	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
102	101	expcom 413	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ≠ 0 ∧ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
103	102	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≠ 0 → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
104	56, 103	sylbir 235	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐵 = 0 → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
105		notnotb 315	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 ↔ ¬ ¬ 𝐵 = 0)
106		nne 2937	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝐴 ≠ 0 ↔ 𝐴 = 0)
107	106	bicomi 224	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = 0 ↔ ¬ 𝐴 ≠ 0)
108		1re 11144	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
109	4, 5	prelrrx2 49067	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ) → {⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃)
110	108, 108, 109	mp2an 693	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃
111		oveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 = 0 → (𝐴 · 1) = (0 · 1))
112	111	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐴 · 1) = (0 · 1))
113		ax-1cn 11096	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℂ
114	113	mul02i 11334	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 · 1) = 0
115	112, 114	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐴 · 1) = 0)
116		oveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 = 0 → (𝐵 · 1) = (0 · 1))
117	116	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐵 · 1) = (0 · 1))
118	117, 114	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐵 · 1) = 0)
119	115, 118	oveq12d 7386	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → ((𝐴 · 1) + (𝐵 · 1)) = (0 + 0))
120	119, 23	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → ((𝐴 · 1) + (𝐵 · 1)) = 0)
121		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 = 0 → 𝐶 = 0)
122	120, 121	eqeqan12d 2751	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 0 = 0))
123	122	bibi1d 343	. . . . . . . . . . . . . . . . . . 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 6841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘1) = ({⟨1, 1⟩, ⟨2, 1⟩}‘1))
126		fvpr1g 7146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 1⟩}‘1) = 1)
127	32, 32, 34, 126	mp3an 1464	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, 1⟩}‘1) = 1
128	125, 127	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘1) = 1)
129	128	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 1))
130		fveq1 6841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘2) = ({⟨1, 1⟩, ⟨2, 1⟩}‘2))
131		fvpr2g 7147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 1⟩}‘2) = 1)
132	40, 32, 34, 131	mp3an 1464	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, 1⟩}‘2) = 1
133	130, 132	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘2) = 1)
134	133	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · 1))
135	129, 134	oveq12d 7386	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 1) + (𝐵 · 1)))
136	135	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 1) + (𝐵 · 1)) = 𝐶))
137	128	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((𝑝‘1) = 0 ↔ 1 = 0))
138	136, 137	bibi12d 345	. . . . . . . . . . . . . . . . . . . 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 3578	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
141	110, 124, 140	sylancr 588	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
142	141	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
143	142	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
144	105, 107, 143	syl2anbr 600	. . . . . . . . . . . . . 14 ⊢ ((¬ ¬ 𝐵 = 0 ∧ ¬ 𝐴 ≠ 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
145	104, 144	jaoi3 1061	. . . . . . . . . . . . 13 ⊢ ((¬ 𝐵 = 0 ∨ ¬ 𝐴 ≠ 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
146	145	orcoms 873	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
147	55, 146	sylbi 217	. . . . . . . . . . 11 ⊢ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
148	147	com12 32	. . . . . . . . . 10 ⊢ (𝐶 = 0 → (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
149	54, 148	sylbir 235	. . . . . . . . 9 ⊢ (¬ ¬ 𝐶 = 0 → (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
150	149	imp 406	. . . . . . . 8 ⊢ ((¬ ¬ 𝐶 = 0 ∧ ¬ (𝐴 ≠ 0 ∧ 𝐵 = 0)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
151	53, 150	jaoi3 1061	. . . . . . 7 ⊢ ((¬ 𝐶 = 0 ∨ ¬ (𝐴 ≠ 0 ∧ 𝐵 = 0)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
152	151	orcoms 873	. . . . . 6 ⊢ ((¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
153	152	com12 32	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
154	1, 153	biimtrid 242	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
155		rexnal 3090	. . . 4 ⊢ (∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
156	154, 155	imbitrdi 251	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) → ¬ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
157	156	con4d 115	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0)))
158		df-3an 1089	. 2 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) ↔ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0))
159	157, 158	imbitrrdi 252	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  Vcvv 3442  {cpr 4584  ⟨cop 4588  ‘cfv 6500  (class class class)co 7368   ↑_m cmap 8775  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043  -cneg 11377   / cdiv 11806  2c2 12212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-map 8777  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-2 12220

This theorem is referenced by:  line2y  49109