Step | Hyp | Ref
| Expression |
1 | | i1fadd.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
2 | | i1ff 23249 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
4 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn ℝ) |
6 | | i1fadd.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
7 | | i1ff 23249 |
. . . . . . . . 9
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
9 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐺:ℝ⟶ℝ →
𝐺 Fn
ℝ) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn ℝ) |
11 | | reex 9906 |
. . . . . . . 8
⊢ ℝ
∈ V |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
V) |
13 | | inidm 3784 |
. . . . . . 7
⊢ (ℝ
∩ ℝ) = ℝ |
14 | 5, 10, 12, 12, 13 | offn 6806 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) Fn ℝ) |
15 | 14 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝐹 ∘𝑓
· 𝐺) Fn
ℝ) |
16 | | fniniseg 6246 |
. . . . 5
⊢ ((𝐹 ∘𝑓
· 𝐺) Fn ℝ
→ (𝑧 ∈ (◡(𝐹 ∘𝑓 · 𝐺) “ {𝐴}) ↔ (𝑧 ∈ ℝ ∧ ((𝐹 ∘𝑓 · 𝐺)‘𝑧) = 𝐴))) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ (◡(𝐹 ∘𝑓 · 𝐺) “ {𝐴}) ↔ (𝑧 ∈ ℝ ∧ ((𝐹 ∘𝑓 · 𝐺)‘𝑧) = 𝐴))) |
18 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → 𝐹 Fn ℝ) |
19 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → 𝐺 Fn ℝ) |
20 | 11 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
ℝ ∈ V) |
21 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑧 ∈ ℝ) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
22 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑧 ∈ ℝ) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
23 | 18, 19, 20, 20, 13, 21, 22 | ofval 6804 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑧 ∈ ℝ) → ((𝐹 ∘𝑓
· 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧))) |
24 | 23 | eqeq1d 2612 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑧 ∈ ℝ) → (((𝐹 ∘𝑓
· 𝐺)‘𝑧) = 𝐴 ↔ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) |
25 | 24 | pm5.32da 671 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
((𝑧 ∈ ℝ ∧
((𝐹
∘𝑓 · 𝐺)‘𝑧) = 𝐴) ↔ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴))) |
26 | 10 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝐺 Fn ℝ) |
27 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝑧 ∈ ℝ) |
28 | | fnfvelrn 6264 |
. . . . . . . . 9
⊢ ((𝐺 Fn ℝ ∧ 𝑧 ∈ ℝ) → (𝐺‘𝑧) ∈ ran 𝐺) |
29 | 26, 27, 28 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) ∈ ran 𝐺) |
30 | | eldifsni 4261 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (ℂ ∖ {0})
→ 𝐴 ≠
0) |
31 | 30 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝐴 ≠ 0) |
32 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴) |
33 | 3 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝐹:ℝ⟶ℝ) |
34 | 33, 27 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐹‘𝑧) ∈ ℝ) |
35 | 34 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐹‘𝑧) ∈ ℂ) |
36 | 35 | mul01d 10114 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → ((𝐹‘𝑧) · 0) = 0) |
37 | 31, 32, 36 | 3netr4d 2859 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ≠ ((𝐹‘𝑧) · 0)) |
38 | | oveq2 6557 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑧) = 0 → ((𝐹‘𝑧) · (𝐺‘𝑧)) = ((𝐹‘𝑧) · 0)) |
39 | 38 | necon3i 2814 |
. . . . . . . . 9
⊢ (((𝐹‘𝑧) · (𝐺‘𝑧)) ≠ ((𝐹‘𝑧) · 0) → (𝐺‘𝑧) ≠ 0) |
40 | 37, 39 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) ≠ 0) |
41 | | eldifsn 4260 |
. . . . . . . 8
⊢ ((𝐺‘𝑧) ∈ (ran 𝐺 ∖ {0}) ↔ ((𝐺‘𝑧) ∈ ran 𝐺 ∧ (𝐺‘𝑧) ≠ 0)) |
42 | 29, 40, 41 | sylanbrc 695 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) ∈ (ran 𝐺 ∖ {0})) |
43 | 8 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝐺:ℝ⟶ℝ) |
44 | 43, 27 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) ∈ ℝ) |
45 | 44 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) ∈ ℂ) |
46 | 35, 45, 40 | divcan4d 10686 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (((𝐹‘𝑧) · (𝐺‘𝑧)) / (𝐺‘𝑧)) = (𝐹‘𝑧)) |
47 | 32 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (((𝐹‘𝑧) · (𝐺‘𝑧)) / (𝐺‘𝑧)) = (𝐴 / (𝐺‘𝑧))) |
48 | 46, 47 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐹‘𝑧) = (𝐴 / (𝐺‘𝑧))) |
49 | 33, 4 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝐹 Fn ℝ) |
50 | | fniniseg 6246 |
. . . . . . . . . 10
⊢ (𝐹 Fn ℝ → (𝑧 ∈ (◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / (𝐺‘𝑧))))) |
51 | 49, 50 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝑧 ∈ (◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / (𝐺‘𝑧))))) |
52 | 27, 48, 51 | mpbir2and 959 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝑧 ∈ (◡𝐹 “ {(𝐴 / (𝐺‘𝑧))})) |
53 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
54 | | fniniseg 6246 |
. . . . . . . . . 10
⊢ (𝐺 Fn ℝ → (𝑧 ∈ (◡𝐺 “ {(𝐺‘𝑧)}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = (𝐺‘𝑧)))) |
55 | 26, 54 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝑧 ∈ (◡𝐺 “ {(𝐺‘𝑧)}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = (𝐺‘𝑧)))) |
56 | 27, 53, 55 | mpbir2and 959 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝑧 ∈ (◡𝐺 “ {(𝐺‘𝑧)})) |
57 | | elin 3758 |
. . . . . . . 8
⊢ (𝑧 ∈ ((◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)})) ↔ (𝑧 ∈ (◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ∧ 𝑧 ∈ (◡𝐺 “ {(𝐺‘𝑧)}))) |
58 | 52, 56, 57 | sylanbrc 695 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝑧 ∈ ((◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)}))) |
59 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐺‘𝑧) → (𝐴 / 𝑦) = (𝐴 / (𝐺‘𝑧))) |
60 | 59 | sneqd 4137 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐺‘𝑧) → {(𝐴 / 𝑦)} = {(𝐴 / (𝐺‘𝑧))}) |
61 | 60 | imaeq2d 5385 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺‘𝑧) → (◡𝐹 “ {(𝐴 / 𝑦)}) = (◡𝐹 “ {(𝐴 / (𝐺‘𝑧))})) |
62 | | sneq 4135 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐺‘𝑧) → {𝑦} = {(𝐺‘𝑧)}) |
63 | 62 | imaeq2d 5385 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺‘𝑧) → (◡𝐺 “ {𝑦}) = (◡𝐺 “ {(𝐺‘𝑧)})) |
64 | 61, 63 | ineq12d 3777 |
. . . . . . . . 9
⊢ (𝑦 = (𝐺‘𝑧) → ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) = ((◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)}))) |
65 | 64 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑦 = (𝐺‘𝑧) → (𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ 𝑧 ∈ ((◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)})))) |
66 | 65 | rspcev 3282 |
. . . . . . 7
⊢ (((𝐺‘𝑧) ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ((◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)}))) → ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) |
67 | 42, 58, 66 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) |
68 | 67 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
((𝑧 ∈ ℝ ∧
((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴) → ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) |
69 | | fniniseg 6246 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ℝ → (𝑧 ∈ (◡𝐹 “ {(𝐴 / 𝑦)}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / 𝑦)))) |
70 | 18, 69 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ (◡𝐹 “ {(𝐴 / 𝑦)}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / 𝑦)))) |
71 | | fniniseg 6246 |
. . . . . . . . . . 11
⊢ (𝐺 Fn ℝ → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) |
72 | 19, 71 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) |
73 | 70, 72 | anbi12d 743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
((𝑧 ∈ (◡𝐹 “ {(𝐴 / 𝑦)}) ∧ 𝑧 ∈ (◡𝐺 “ {𝑦})) ↔ ((𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / 𝑦)) ∧ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦)))) |
74 | | elin 3758 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ (𝑧 ∈ (◡𝐹 “ {(𝐴 / 𝑦)}) ∧ 𝑧 ∈ (◡𝐺 “ {𝑦}))) |
75 | | anandi 867 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦)) ↔ ((𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / 𝑦)) ∧ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) |
76 | 73, 74, 75 | 3bitr4g 302 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦)))) |
77 | 76 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦)))) |
78 | | eldifi 3694 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (ℂ ∖ {0})
→ 𝐴 ∈
ℂ) |
79 | 78 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝐴 ∈ ℂ) |
80 | 8 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝐺:ℝ⟶ℝ) |
81 | | frn 5966 |
. . . . . . . . . . . . . 14
⊢ (𝐺:ℝ⟶ℝ →
ran 𝐺 ⊆
ℝ) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → ran 𝐺 ⊆
ℝ) |
83 | | simprl 790 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝑦 ∈ (ran 𝐺 ∖ {0})) |
84 | | eldifsn 4260 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (ran 𝐺 ∖ {0}) ↔ (𝑦 ∈ ran 𝐺 ∧ 𝑦 ≠ 0)) |
85 | 83, 84 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → (𝑦 ∈ ran 𝐺 ∧ 𝑦 ≠ 0)) |
86 | 85 | simpld 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝑦 ∈ ran 𝐺) |
87 | 82, 86 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝑦 ∈ ℝ) |
88 | 87 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝑦 ∈ ℂ) |
89 | 85 | simprd 478 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝑦 ≠ 0) |
90 | 79, 88, 89 | divcan1d 10681 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → ((𝐴 / 𝑦) · 𝑦) = 𝐴) |
91 | | oveq12 6558 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦) → ((𝐹‘𝑧) · (𝐺‘𝑧)) = ((𝐴 / 𝑦) · 𝑦)) |
92 | 91 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦) → (((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴 ↔ ((𝐴 / 𝑦) · 𝑦) = 𝐴)) |
93 | 90, 92 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → (((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦) → ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) |
94 | 93 | anassrs 678 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → (((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦) → ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) |
95 | 94 | imdistanda 725 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → ((𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦)) → (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴))) |
96 | 77, 95 | sylbid 229 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) → (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴))) |
97 | 96 | rexlimdva 3013 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
(∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) → (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴))) |
98 | 68, 97 | impbid 201 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
((𝑧 ∈ ℝ ∧
((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴) ↔ ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) |
99 | 17, 25, 98 | 3bitrd 293 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ (◡(𝐹 ∘𝑓 · 𝐺) “ {𝐴}) ↔ ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) |
100 | | eliun 4460 |
. . 3
⊢ (𝑧 ∈ ∪ 𝑦 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) |
101 | 99, 100 | syl6bbr 277 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ (◡(𝐹 ∘𝑓 · 𝐺) “ {𝐴}) ↔ 𝑧 ∈ ∪
𝑦 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) |
102 | 101 | eqrdv 2608 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝐴}) = ∪
𝑦 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) |