| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | i1fadd.1 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ dom
∫1) | 
| 2 |  | i1ff 25711 | . . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) | 
| 3 | 1, 2 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) | 
| 4 | 3 | ffnd 6737 | . . . . . . 7
⊢ (𝜑 → 𝐹 Fn ℝ) | 
| 5 |  | i1fadd.2 | . . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ dom
∫1) | 
| 6 |  | i1ff 25711 | . . . . . . . . 9
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) | 
| 7 | 5, 6 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) | 
| 8 | 7 | ffnd 6737 | . . . . . . 7
⊢ (𝜑 → 𝐺 Fn ℝ) | 
| 9 |  | reex 11246 | . . . . . . . 8
⊢ ℝ
∈ V | 
| 10 | 9 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℝ ∈
V) | 
| 11 |  | inidm 4227 | . . . . . . 7
⊢ (ℝ
∩ ℝ) = ℝ | 
| 12 | 4, 8, 10, 10, 11 | offn 7710 | . . . . . 6
⊢ (𝜑 → (𝐹 ∘f · 𝐺) Fn ℝ) | 
| 13 | 12 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝐹 ∘f ·
𝐺) Fn
ℝ) | 
| 14 |  | fniniseg 7080 | . . . . 5
⊢ ((𝐹 ∘f ·
𝐺) Fn ℝ → (𝑧 ∈ (◡(𝐹 ∘f · 𝐺) “ {𝐴}) ↔ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f · 𝐺)‘𝑧) = 𝐴))) | 
| 15 | 13, 14 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ (◡(𝐹 ∘f · 𝐺) “ {𝐴}) ↔ (𝑧 ∈ ℝ ∧ ((𝐹 ∘f · 𝐺)‘𝑧) = 𝐴))) | 
| 16 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → 𝐹 Fn ℝ) | 
| 17 | 8 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → 𝐺 Fn ℝ) | 
| 18 | 9 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
ℝ ∈ V) | 
| 19 |  | eqidd 2738 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑧 ∈ ℝ) → (𝐹‘𝑧) = (𝐹‘𝑧)) | 
| 20 |  | eqidd 2738 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑧 ∈ ℝ) → (𝐺‘𝑧) = (𝐺‘𝑧)) | 
| 21 | 16, 17, 18, 18, 11, 19, 20 | ofval 7708 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑧 ∈ ℝ) → ((𝐹 ∘f ·
𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧))) | 
| 22 | 21 | eqeq1d 2739 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑧 ∈ ℝ) → (((𝐹 ∘f ·
𝐺)‘𝑧) = 𝐴 ↔ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) | 
| 23 | 22 | pm5.32da 579 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
((𝑧 ∈ ℝ ∧
((𝐹 ∘f
· 𝐺)‘𝑧) = 𝐴) ↔ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴))) | 
| 24 | 8 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝐺 Fn ℝ) | 
| 25 |  | simprl 771 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝑧 ∈ ℝ) | 
| 26 |  | fnfvelrn 7100 | . . . . . . . . 9
⊢ ((𝐺 Fn ℝ ∧ 𝑧 ∈ ℝ) → (𝐺‘𝑧) ∈ ran 𝐺) | 
| 27 | 24, 25, 26 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) ∈ ran 𝐺) | 
| 28 |  | eldifsni 4790 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (ℂ ∖ {0})
→ 𝐴 ≠
0) | 
| 29 | 28 | ad2antlr 727 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝐴 ≠ 0) | 
| 30 |  | simprr 773 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴) | 
| 31 | 3 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝐹:ℝ⟶ℝ) | 
| 32 | 31, 25 | ffvelcdmd 7105 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐹‘𝑧) ∈ ℝ) | 
| 33 | 32 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐹‘𝑧) ∈ ℂ) | 
| 34 | 33 | mul01d 11460 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → ((𝐹‘𝑧) · 0) = 0) | 
| 35 | 29, 30, 34 | 3netr4d 3018 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ≠ ((𝐹‘𝑧) · 0)) | 
| 36 |  | oveq2 7439 | . . . . . . . . . 10
⊢ ((𝐺‘𝑧) = 0 → ((𝐹‘𝑧) · (𝐺‘𝑧)) = ((𝐹‘𝑧) · 0)) | 
| 37 | 36 | necon3i 2973 | . . . . . . . . 9
⊢ (((𝐹‘𝑧) · (𝐺‘𝑧)) ≠ ((𝐹‘𝑧) · 0) → (𝐺‘𝑧) ≠ 0) | 
| 38 | 35, 37 | syl 17 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) ≠ 0) | 
| 39 |  | eldifsn 4786 | . . . . . . . 8
⊢ ((𝐺‘𝑧) ∈ (ran 𝐺 ∖ {0}) ↔ ((𝐺‘𝑧) ∈ ran 𝐺 ∧ (𝐺‘𝑧) ≠ 0)) | 
| 40 | 27, 38, 39 | sylanbrc 583 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) ∈ (ran 𝐺 ∖ {0})) | 
| 41 | 7 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝐺:ℝ⟶ℝ) | 
| 42 | 41, 25 | ffvelcdmd 7105 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) ∈ ℝ) | 
| 43 | 42 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) ∈ ℂ) | 
| 44 | 33, 43, 38 | divcan4d 12049 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (((𝐹‘𝑧) · (𝐺‘𝑧)) / (𝐺‘𝑧)) = (𝐹‘𝑧)) | 
| 45 | 30 | oveq1d 7446 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (((𝐹‘𝑧) · (𝐺‘𝑧)) / (𝐺‘𝑧)) = (𝐴 / (𝐺‘𝑧))) | 
| 46 | 44, 45 | eqtr3d 2779 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐹‘𝑧) = (𝐴 / (𝐺‘𝑧))) | 
| 47 | 31 | ffnd 6737 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝐹 Fn ℝ) | 
| 48 |  | fniniseg 7080 | . . . . . . . . . 10
⊢ (𝐹 Fn ℝ → (𝑧 ∈ (◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / (𝐺‘𝑧))))) | 
| 49 | 47, 48 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝑧 ∈ (◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / (𝐺‘𝑧))))) | 
| 50 | 25, 46, 49 | mpbir2and 713 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝑧 ∈ (◡𝐹 “ {(𝐴 / (𝐺‘𝑧))})) | 
| 51 |  | eqidd 2738 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝐺‘𝑧) = (𝐺‘𝑧)) | 
| 52 |  | fniniseg 7080 | . . . . . . . . . 10
⊢ (𝐺 Fn ℝ → (𝑧 ∈ (◡𝐺 “ {(𝐺‘𝑧)}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = (𝐺‘𝑧)))) | 
| 53 | 24, 52 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → (𝑧 ∈ (◡𝐺 “ {(𝐺‘𝑧)}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = (𝐺‘𝑧)))) | 
| 54 | 25, 51, 53 | mpbir2and 713 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝑧 ∈ (◡𝐺 “ {(𝐺‘𝑧)})) | 
| 55 | 50, 54 | elind 4200 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → 𝑧 ∈ ((◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)}))) | 
| 56 |  | oveq2 7439 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝐺‘𝑧) → (𝐴 / 𝑦) = (𝐴 / (𝐺‘𝑧))) | 
| 57 | 56 | sneqd 4638 | . . . . . . . . . . 11
⊢ (𝑦 = (𝐺‘𝑧) → {(𝐴 / 𝑦)} = {(𝐴 / (𝐺‘𝑧))}) | 
| 58 | 57 | imaeq2d 6078 | . . . . . . . . . 10
⊢ (𝑦 = (𝐺‘𝑧) → (◡𝐹 “ {(𝐴 / 𝑦)}) = (◡𝐹 “ {(𝐴 / (𝐺‘𝑧))})) | 
| 59 |  | sneq 4636 | . . . . . . . . . . 11
⊢ (𝑦 = (𝐺‘𝑧) → {𝑦} = {(𝐺‘𝑧)}) | 
| 60 | 59 | imaeq2d 6078 | . . . . . . . . . 10
⊢ (𝑦 = (𝐺‘𝑧) → (◡𝐺 “ {𝑦}) = (◡𝐺 “ {(𝐺‘𝑧)})) | 
| 61 | 58, 60 | ineq12d 4221 | . . . . . . . . 9
⊢ (𝑦 = (𝐺‘𝑧) → ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) = ((◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)}))) | 
| 62 | 61 | eleq2d 2827 | . . . . . . . 8
⊢ (𝑦 = (𝐺‘𝑧) → (𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ 𝑧 ∈ ((◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)})))) | 
| 63 | 62 | rspcev 3622 | . . . . . . 7
⊢ (((𝐺‘𝑧) ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ((◡𝐹 “ {(𝐴 / (𝐺‘𝑧))}) ∩ (◡𝐺 “ {(𝐺‘𝑧)}))) → ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) | 
| 64 | 40, 55, 63 | syl2anc 584 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) → ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) | 
| 65 | 64 | ex 412 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
((𝑧 ∈ ℝ ∧
((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴) → ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) | 
| 66 |  | fniniseg 7080 | . . . . . . . . . . 11
⊢ (𝐹 Fn ℝ → (𝑧 ∈ (◡𝐹 “ {(𝐴 / 𝑦)}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / 𝑦)))) | 
| 67 | 16, 66 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ (◡𝐹 “ {(𝐴 / 𝑦)}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / 𝑦)))) | 
| 68 |  | fniniseg 7080 | . . . . . . . . . . 11
⊢ (𝐺 Fn ℝ → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) | 
| 69 | 17, 68 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) | 
| 70 | 67, 69 | anbi12d 632 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
((𝑧 ∈ (◡𝐹 “ {(𝐴 / 𝑦)}) ∧ 𝑧 ∈ (◡𝐺 “ {𝑦})) ↔ ((𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / 𝑦)) ∧ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦)))) | 
| 71 |  | elin 3967 | . . . . . . . . 9
⊢ (𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ (𝑧 ∈ (◡𝐹 “ {(𝐴 / 𝑦)}) ∧ 𝑧 ∈ (◡𝐺 “ {𝑦}))) | 
| 72 |  | anandi 676 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦)) ↔ ((𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐴 / 𝑦)) ∧ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) | 
| 73 | 70, 71, 72 | 3bitr4g 314 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦)))) | 
| 74 | 73 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦)))) | 
| 75 |  | eldifi 4131 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (ℂ ∖ {0})
→ 𝐴 ∈
ℂ) | 
| 76 | 75 | ad2antlr 727 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝐴 ∈ ℂ) | 
| 77 | 7 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝐺:ℝ⟶ℝ) | 
| 78 | 77 | frnd 6744 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → ran 𝐺 ⊆
ℝ) | 
| 79 |  | simprl 771 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝑦 ∈ (ran 𝐺 ∖ {0})) | 
| 80 |  | eldifsn 4786 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (ran 𝐺 ∖ {0}) ↔ (𝑦 ∈ ran 𝐺 ∧ 𝑦 ≠ 0)) | 
| 81 | 79, 80 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → (𝑦 ∈ ran 𝐺 ∧ 𝑦 ≠ 0)) | 
| 82 | 81 | simpld 494 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝑦 ∈ ran 𝐺) | 
| 83 | 78, 82 | sseldd 3984 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝑦 ∈ ℝ) | 
| 84 | 83 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝑦 ∈ ℂ) | 
| 85 | 81 | simprd 495 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → 𝑦 ≠ 0) | 
| 86 | 76, 84, 85 | divcan1d 12044 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → ((𝐴 / 𝑦) · 𝑦) = 𝐴) | 
| 87 |  | oveq12 7440 | . . . . . . . . . . 11
⊢ (((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦) → ((𝐹‘𝑧) · (𝐺‘𝑧)) = ((𝐴 / 𝑦) · 𝑦)) | 
| 88 | 87 | eqeq1d 2739 | . . . . . . . . . 10
⊢ (((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦) → (((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴 ↔ ((𝐴 / 𝑦) · 𝑦) = 𝐴)) | 
| 89 | 86, 88 | syl5ibrcom 247 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ (𝑦 ∈ (ran 𝐺 ∖ {0}) ∧ 𝑧 ∈ ℝ)) → (((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦) → ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) | 
| 90 | 89 | anassrs 467 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → (((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦) → ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴)) | 
| 91 | 90 | imdistanda 571 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → ((𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) = (𝐴 / 𝑦) ∧ (𝐺‘𝑧) = 𝑦)) → (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴))) | 
| 92 | 74, 91 | sylbid 240 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) ∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) → (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴))) | 
| 93 | 92 | rexlimdva 3155 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
(∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) → (𝑧 ∈ ℝ ∧ ((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴))) | 
| 94 | 65, 93 | impbid 212 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) →
((𝑧 ∈ ℝ ∧
((𝐹‘𝑧) · (𝐺‘𝑧)) = 𝐴) ↔ ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) | 
| 95 | 15, 23, 94 | 3bitrd 305 | . . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ (◡(𝐹 ∘f · 𝐺) “ {𝐴}) ↔ ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) | 
| 96 |  | eliun 4995 | . . 3
⊢ (𝑧 ∈ ∪ 𝑦 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})) ↔ ∃𝑦 ∈ (ran 𝐺 ∖ {0})𝑧 ∈ ((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) | 
| 97 | 95, 96 | bitr4di 289 | . 2
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (𝑧 ∈ (◡(𝐹 ∘f · 𝐺) “ {𝐴}) ↔ 𝑧 ∈ ∪
𝑦 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})))) | 
| 98 | 97 | eqrdv 2735 | 1
⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (◡(𝐹 ∘f · 𝐺) “ {𝐴}) = ∪
𝑦 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦}))) |