Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  line2ylem Structured version   Visualization version   GIF version

Theorem line2ylem 45558
 Description: Lemma for line2y 45562. 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
StepHypRef Expression
1 ianor 979 . . . . 5 (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) ↔ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0))
2 df-ne 2952 . . . . . . . . 9 (𝐶 ≠ 0 ↔ ¬ 𝐶 = 0)
3 0re 10686 . . . . . . . . . . . 12 0 ∈ ℝ
4 line2ylem.i . . . . . . . . . . . . 13 𝐼 = {1, 2}
5 line2ylem.p . . . . . . . . . . . . 13 𝑃 = (ℝ ↑m 𝐼)
64, 5prelrrx2 45520 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 0 ∈ ℝ) → {⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃)
73, 3, 6mp2an 691 . . . . . . . . . . 11 {⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃
8 eqneqall 2962 . . . . . . . . . . . . . . . 16 (𝐶 = 0 → (𝐶 ≠ 0 → ¬ 0 = 0))
98com12 32 . . . . . . . . . . . . . . 15 (𝐶 ≠ 0 → (𝐶 = 0 → ¬ 0 = 0))
10 eqid 2758 . . . . . . . . . . . . . . . 16 0 = 0
1110pm2.24i 153 . . . . . . . . . . . . . . 15 (¬ 0 = 0 → 𝐶 = 0)
129, 11impbid1 228 . . . . . . . . . . . . . 14 (𝐶 ≠ 0 → (𝐶 = 0 ↔ ¬ 0 = 0))
1312adantl 485 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → (𝐶 = 0 ↔ ¬ 0 = 0))
14 xor3 387 . . . . . . . . . . . . 13 (¬ (𝐶 = 0 ↔ 0 = 0) ↔ (𝐶 = 0 ↔ ¬ 0 = 0))
1513, 14sylibr 237 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ¬ (𝐶 = 0 ↔ 0 = 0))
16 simp1 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
1716recnd 10712 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
1817mul01d 10882 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 0) = 0)
19 simp2 1134 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
2019recnd 10712 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
2120mul01d 10882 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 0) = 0)
2218, 21oveq12d 7173 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 0) + (𝐵 · 0)) = (0 + 0))
23 00id 10858 . . . . . . . . . . . . . . . . 17 (0 + 0) = 0
2422, 23eqtrdi 2809 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 0) + (𝐵 · 0)) = 0)
2524eqeq1d 2760 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 𝐶))
26 eqcom 2765 . . . . . . . . . . . . . . 15 (0 = 𝐶𝐶 = 0)
2725, 26bitrdi 290 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶𝐶 = 0))
2827adantr 484 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶𝐶 = 0))
2928bibi1d 347 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ((((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0) ↔ (𝐶 = 0 ↔ 0 = 0)))
3015, 29mtbird 328 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0))
31 fveq1 6661 . . . . . . . . . . . . . . . . . 18 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘1) = ({⟨1, 0⟩, ⟨2, 0⟩}‘1))
32 1ex 10680 . . . . . . . . . . . . . . . . . . 19 1 ∈ V
33 c0ex 10678 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
34 1ne2 11887 . . . . . . . . . . . . . . . . . . 19 1 ≠ 2
35 fvpr1g 6950 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 0⟩}‘1) = 0)
3632, 33, 34, 35mp3an 1458 . . . . . . . . . . . . . . . . . 18 ({⟨1, 0⟩, ⟨2, 0⟩}‘1) = 0
3731, 36eqtrdi 2809 . . . . . . . . . . . . . . . . 17 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘1) = 0)
3837oveq2d 7171 . . . . . . . . . . . . . . . 16 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 0))
39 fveq1 6661 . . . . . . . . . . . . . . . . . 18 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘2) = ({⟨1, 0⟩, ⟨2, 0⟩}‘2))
40 2ex 11756 . . . . . . . . . . . . . . . . . . 19 2 ∈ V
41 fvpr2g 6951 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 0⟩}‘2) = 0)
4240, 33, 34, 41mp3an 1458 . . . . . . . . . . . . . . . . . 18 ({⟨1, 0⟩, ⟨2, 0⟩}‘2) = 0
4339, 42eqtrdi 2809 . . . . . . . . . . . . . . . . 17 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘2) = 0)
4443oveq2d 7171 . . . . . . . . . . . . . . . 16 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · 0))
4538, 44oveq12d 7173 . . . . . . . . . . . . . . 15 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 0) + (𝐵 · 0)))
4645eqeq1d 2760 . . . . . . . . . . . . . 14 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 0) + (𝐵 · 0)) = 𝐶))
4737eqeq1d 2760 . . . . . . . . . . . . . 14 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((𝑝‘1) = 0 ↔ 0 = 0))
4846, 47bibi12d 349 . . . . . . . . . . . . 13 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0)))
4948notbid 321 . . . . . . . . . . . 12 (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0)))
5049rspcev 3543 . . . . . . . . . . 11 (({⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0)) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
517, 30, 50sylancr 590 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
5251expcom 417 . . . . . . . . 9 (𝐶 ≠ 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
532, 52sylbir 238 . . . . . . . 8 𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
54 notnotb 318 . . . . . . . . . 10 (𝐶 = 0 ↔ ¬ ¬ 𝐶 = 0)
55 ianor 979 . . . . . . . . . . . 12 (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ↔ (¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0))
56 df-ne 2952 . . . . . . . . . . . . . . 15 (𝐵 ≠ 0 ↔ ¬ 𝐵 = 0)
57 1red 10685 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 1 ∈ ℝ)
5816adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐴 ∈ ℝ)
5958renegcld 11110 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → -𝐴 ∈ ℝ)
6019adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ∈ ℝ)
61 simprl 770 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ≠ 0)
6259, 60, 61redivcld 11511 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (-𝐴 / 𝐵) ∈ ℝ)
634, 5prelrrx2 45520 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ ∧ (-𝐴 / 𝐵) ∈ ℝ) → {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃)
6457, 62, 63syl2anc 587 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃)
65 ax-1ne0 10649 . . . . . . . . . . . . . . . . . . . . . 22 1 ≠ 0
6665neii 2953 . . . . . . . . . . . . . . . . . . . . 21 ¬ 1 = 0
6710, 662th 267 . . . . . . . . . . . . . . . . . . . 20 (0 = 0 ↔ ¬ 1 = 0)
68 xor3 387 . . . . . . . . . . . . . . . . . . . 20 (¬ (0 = 0 ↔ 1 = 0) ↔ (0 = 0 ↔ ¬ 1 = 0))
6967, 68mpbir 234 . . . . . . . . . . . . . . . . . . 19 ¬ (0 = 0 ↔ 1 = 0)
7017mulid1d 10701 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 1) = 𝐴)
7170adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐴 · 1) = 𝐴)
7217negcld 11027 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → -𝐴 ∈ ℂ)
7372adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → -𝐴 ∈ ℂ)
7420adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ∈ ℂ)
7573, 74, 61divcan2d 11461 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐵 · (-𝐴 / 𝐵)) = -𝐴)
7671, 75oveq12d 7173 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = (𝐴 + -𝐴))
7717negidd 11030 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 + -𝐴) = 0)
7877adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐴 + -𝐴) = 0)
7976, 78eqtrd 2793 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 0)
80 simprr 772 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐶 = 0)
8179, 80eqeq12d 2774 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 0 = 0))
8281bibi1d 347 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0) ↔ (0 = 0 ↔ 1 = 0)))
8369, 82mtbiri 330 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0))
84 fveq1 6661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘1) = ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1))
85 fvpr1g 6950 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1) = 1)
8632, 32, 34, 85mp3an 1458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1) = 1
8784, 86eqtrdi 2809 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘1) = 1)
8887oveq2d 7171 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 1))
89 fveq1 6661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘2) = ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2))
90 ovex 7188 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (-𝐴 / 𝐵) ∈ V
91 fvpr2g 6951 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ V ∧ (-𝐴 / 𝐵) ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2) = (-𝐴 / 𝐵))
9240, 90, 34, 91mp3an 1458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2) = (-𝐴 / 𝐵)
9389, 92eqtrdi 2809 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘2) = (-𝐴 / 𝐵))
9493oveq2d 7171 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · (-𝐴 / 𝐵)))
9588, 94oveq12d 7173 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))))
9695eqeq1d 2760 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶))
9787eqeq1d 2760 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((𝑝‘1) = 0 ↔ 1 = 0))
9896, 97bibi12d 349 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0)))
9998notbid 321 . . . . . . . . . . . . . . . . . . 19 (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0)))
10099rspcev 3543 . . . . . . . . . . . . . . . . . 18 (({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0)) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
10164, 83, 100syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
102101expcom 417 . . . . . . . . . . . . . . . 16 ((𝐵 ≠ 0 ∧ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
103102ex 416 . . . . . . . . . . . . . . 15 (𝐵 ≠ 0 → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
10456, 103sylbir 238 . . . . . . . . . . . . . 14 𝐵 = 0 → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
105 notnotb 318 . . . . . . . . . . . . . . 15 (𝐵 = 0 ↔ ¬ ¬ 𝐵 = 0)
106 nne 2955 . . . . . . . . . . . . . . . 16 𝐴 ≠ 0 ↔ 𝐴 = 0)
107106bicomi 227 . . . . . . . . . . . . . . 15 (𝐴 = 0 ↔ ¬ 𝐴 ≠ 0)
108 1re 10684 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
1094, 5prelrrx2 45520 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ ∧ 1 ∈ ℝ) → {⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃)
110108, 108, 109mp2an 691 . . . . . . . . . . . . . . . . . 18 {⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃
111 oveq1 7162 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 = 0 → (𝐴 · 1) = (0 · 1))
112111adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐴 · 1) = (0 · 1))
113 ax-1cn 10638 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℂ
114113mul02i 10872 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 · 1) = 0
115112, 114eqtrdi 2809 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐴 · 1) = 0)
116 oveq1 7162 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 = 0 → (𝐵 · 1) = (0 · 1))
117116adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐵 · 1) = (0 · 1))
118117, 114eqtrdi 2809 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐵 · 1) = 0)
119115, 118oveq12d 7173 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 = 0 ∧ 𝐴 = 0) → ((𝐴 · 1) + (𝐵 · 1)) = (0 + 0))
120119, 23eqtrdi 2809 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 = 0 ∧ 𝐴 = 0) → ((𝐴 · 1) + (𝐵 · 1)) = 0)
121 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝐶 = 0 → 𝐶 = 0)
122120, 121eqeqan12d 2775 . . . . . . . . . . . . . . . . . . . 20 (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 0 = 0))
123122bibi1d 347 . . . . . . . . . . . . . . . . . . 19 (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ((((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0) ↔ (0 = 0 ↔ 1 = 0)))
12469, 123mtbiri 330 . . . . . . . . . . . . . . . . . 18 (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ¬ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0))
125 fveq1 6661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘1) = ({⟨1, 1⟩, ⟨2, 1⟩}‘1))
126 fvpr1g 6950 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 1⟩}‘1) = 1)
12732, 32, 34, 126mp3an 1458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨1, 1⟩, ⟨2, 1⟩}‘1) = 1
128125, 127eqtrdi 2809 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘1) = 1)
129128oveq2d 7171 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 1))
130 fveq1 6661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘2) = ({⟨1, 1⟩, ⟨2, 1⟩}‘2))
131 fvpr2g 6951 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 1⟩}‘2) = 1)
13240, 32, 34, 131mp3an 1458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨1, 1⟩, ⟨2, 1⟩}‘2) = 1
133130, 132eqtrdi 2809 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘2) = 1)
134133oveq2d 7171 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · 1))
135129, 134oveq12d 7173 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 1) + (𝐵 · 1)))
136135eqeq1d 2760 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 1) + (𝐵 · 1)) = 𝐶))
137128eqeq1d 2760 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((𝑝‘1) = 0 ↔ 1 = 0))
138136, 137bibi12d 349 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0)))
139138notbid 321 . . . . . . . . . . . . . . . . . . 19 (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0)))
140139rspcev 3543 . . . . . . . . . . . . . . . . . 18 (({⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0)) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
141110, 124, 140sylancr 590 . . . . . . . . . . . . . . . . 17 (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
142141a1d 25 . . . . . . . . . . . . . . . 16 (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
143142ex 416 . . . . . . . . . . . . . . 15 ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
144105, 107, 143syl2anbr 601 . . . . . . . . . . . . . 14 ((¬ ¬ 𝐵 = 0 ∧ ¬ 𝐴 ≠ 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
145104, 144jaoi3 1056 . . . . . . . . . . . . 13 ((¬ 𝐵 = 0 ∨ ¬ 𝐴 ≠ 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
146145orcoms 869 . . . . . . . . . . . 12 ((¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
14755, 146sylbi 220 . . . . . . . . . . 11 (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
148147com12 32 . . . . . . . . . 10 (𝐶 = 0 → (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
14954, 148sylbir 238 . . . . . . . . 9 (¬ ¬ 𝐶 = 0 → (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
150149imp 410 . . . . . . . 8 ((¬ ¬ 𝐶 = 0 ∧ ¬ (𝐴 ≠ 0 ∧ 𝐵 = 0)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
15153, 150jaoi3 1056 . . . . . . 7 ((¬ 𝐶 = 0 ∨ ¬ (𝐴 ≠ 0 ∧ 𝐵 = 0)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
152151orcoms 869 . . . . . 6 ((¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
153152com12 32 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
1541, 153syl5bi 245 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) → ∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
155 rexnal 3165 . . . 4 (∃𝑝𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ ∀𝑝𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
156154, 155syl6ib 254 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) → ¬ ∀𝑝𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
157156con4d 115 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0)))
158 df-3an 1086 . 2 ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) ↔ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0))
159157, 158syl6ibr 255 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  Vcvv 3409  {cpr 4527  ⟨cop 4531  ‘cfv 6339  (class class class)co 7155   ↑m cmap 8421  ℂcc 10578  ℝcr 10579  0cc0 10580  1c1 10581   + caddc 10583   · cmul 10585  -cneg 10914   / cdiv 11340  2c2 11734 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-cnex 10636  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656  ax-pre-mulgt0 10657 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-po 5446  df-so 5447  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-er 8304  df-map 8423  df-en 8533  df-dom 8534  df-sdom 8535  df-pnf 10720  df-mnf 10721  df-xr 10722  df-ltxr 10723  df-le 10724  df-sub 10915  df-neg 10916  df-div 11341  df-2 11742 This theorem is referenced by:  line2y  45562
 Copyright terms: Public domain W3C validator