Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cnrefiisplem Structured version   Visualization version   GIF version

Theorem cnrefiisplem 43370
Description: Lemma for cnrefiisp 43371 (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
Hypotheses
Ref Expression
cnrefiisplem.a (𝜑𝐴 ∈ ℂ)
cnrefiisplem.n (𝜑 → ¬ 𝐴 ∈ ℝ)
cnrefiisplem.b (𝜑𝐵 ∈ Fin)
cnrefiisplem.c 𝐶 = (ℝ ∪ 𝐵)
cnrefiisplem.d 𝐷 = ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
cnrefiisplem.x 𝑋 = inf(𝐷, ℝ*, < )
Assertion
Ref Expression
cnrefiisplem (𝜑 → ∃𝑥 ∈ ℝ+𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
Distinct variable groups:   𝑦,𝐴,𝑥   𝑦,𝐵   𝑥,𝐶   𝑥,𝑋,𝑦   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐶(𝑦)   𝐷(𝑥,𝑦)

Proof of Theorem cnrefiisplem
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 simpr 485 . . . . . . 7 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 = (abs‘(ℑ‘𝐴)))
2 cnrefiisplem.a . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
3 cnrefiisplem.n . . . . . . . . 9 (𝜑 → ¬ 𝐴 ∈ ℝ)
42, 3absimnre 43017 . . . . . . . 8 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ ℝ+)
54adantr 481 . . . . . . 7 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → (abs‘(ℑ‘𝐴)) ∈ ℝ+)
61, 5eqeltrd 2839 . . . . . 6 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
76adantlr 712 . . . . 5 (((𝜑𝑤𝐷) ∧ 𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
8 simpll 764 . . . . . 6 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝜑)
9 cnrefiisplem.d . . . . . . . . . . . 12 𝐷 = ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
109eleq2i 2830 . . . . . . . . . . 11 (𝑤𝐷𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
1110biimpi 215 . . . . . . . . . 10 (𝑤𝐷𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
12 nelsn 4601 . . . . . . . . . 10 (𝑤 ≠ (abs‘(ℑ‘𝐴)) → ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))})
13 elunnel1 4084 . . . . . . . . . 10 ((𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}) ∧ ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))}) → 𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
1411, 12, 13syl2an 596 . . . . . . . . 9 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
15 eliun 4928 . . . . . . . . 9 (𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))})
1614, 15sylib 217 . . . . . . . 8 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))})
17 velsn 4577 . . . . . . . . 9 (𝑤 ∈ {(abs‘(𝑦𝐴))} ↔ 𝑤 = (abs‘(𝑦𝐴)))
1817rexbii 3181 . . . . . . . 8 (∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
1916, 18sylib 217 . . . . . . 7 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
2019adantll 711 . . . . . 6 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
21 simpr 485 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑤 = (abs‘(𝑦𝐴)))
22 eldifi 4061 . . . . . . . . . . . 12 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ (𝐵 ∩ ℂ))
2322elin2d 4133 . . . . . . . . . . 11 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ ℂ)
2423ad2antlr 724 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑦 ∈ ℂ)
252ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝐴 ∈ ℂ)
2624, 25subcld 11332 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (𝑦𝐴) ∈ ℂ)
27 eldifsni 4723 . . . . . . . . . . 11 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦𝐴)
2827ad2antlr 724 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑦𝐴)
2924, 25, 28subne0d 11341 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (𝑦𝐴) ≠ 0)
3026, 29absrpcld 15160 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (abs‘(𝑦𝐴)) ∈ ℝ+)
3121, 30eqeltrd 2839 . . . . . . 7 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑤 ∈ ℝ+)
3231rexlimdva2 3216 . . . . . 6 (𝜑 → (∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)) → 𝑤 ∈ ℝ+))
338, 20, 32sylc 65 . . . . 5 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
347, 33pm2.61dane 3032 . . . 4 ((𝜑𝑤𝐷) → 𝑤 ∈ ℝ+)
3534ssd 42630 . . 3 (𝜑𝐷 ⊆ ℝ+)
36 cnrefiisplem.x . . . 4 𝑋 = inf(𝐷, ℝ*, < )
37 xrltso 12875 . . . . . 6 < Or ℝ*
3837a1i 11 . . . . 5 (𝜑 → < Or ℝ*)
39 snfi 8834 . . . . . . . 8 {(abs‘(ℑ‘𝐴))} ∈ Fin
4039a1i 11 . . . . . . 7 (𝜑 → {(abs‘(ℑ‘𝐴))} ∈ Fin)
41 cnrefiisplem.b . . . . . . . . 9 (𝜑𝐵 ∈ Fin)
42 inss1 4162 . . . . . . . . . . 11 (𝐵 ∩ ℂ) ⊆ 𝐵
4342a1i 11 . . . . . . . . . 10 (𝜑 → (𝐵 ∩ ℂ) ⊆ 𝐵)
4443ssdifssd 4077 . . . . . . . . 9 (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ⊆ 𝐵)
4541, 44ssfid 9042 . . . . . . . 8 (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin)
46 snfi 8834 . . . . . . . . 9 {(abs‘(𝑦𝐴))} ∈ Fin
4746rgenw 3076 . . . . . . . 8 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin
48 iunfi 9107 . . . . . . . 8 ((((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin ∧ ∀𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin) → 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin)
4945, 47, 48sylancl 586 . . . . . . 7 (𝜑 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin)
5040, 49unfid 42702 . . . . . 6 (𝜑 → ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}) ∈ Fin)
519, 50eqeltrid 2843 . . . . 5 (𝜑𝐷 ∈ Fin)
52 fvex 6787 . . . . . . . . . 10 (abs‘(ℑ‘𝐴)) ∈ V
5352snid 4597 . . . . . . . . 9 (abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))}
54 elun1 4110 . . . . . . . . 9 ((abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))} → (abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
5553, 54ax-mp 5 . . . . . . . 8 (abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
5655, 9eleqtrri 2838 . . . . . . 7 (abs‘(ℑ‘𝐴)) ∈ 𝐷
5756a1i 11 . . . . . 6 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ 𝐷)
5857ne0d 4269 . . . . 5 (𝜑𝐷 ≠ ∅)
59 rpssxr 43021 . . . . . 6 + ⊆ ℝ*
6035, 59sstrdi 3933 . . . . 5 (𝜑𝐷 ⊆ ℝ*)
61 fiinfcl 9260 . . . . 5 (( < Or ℝ* ∧ (𝐷 ∈ Fin ∧ 𝐷 ≠ ∅ ∧ 𝐷 ⊆ ℝ*)) → inf(𝐷, ℝ*, < ) ∈ 𝐷)
6238, 51, 58, 60, 61syl13anc 1371 . . . 4 (𝜑 → inf(𝐷, ℝ*, < ) ∈ 𝐷)
6336, 62eqeltrid 2843 . . 3 (𝜑𝑋𝐷)
6435, 63sseldd 3922 . 2 (𝜑𝑋 ∈ ℝ+)
6535, 62sseldd 3922 . . . . . . . . . 10 (𝜑 → inf(𝐷, ℝ*, < ) ∈ ℝ+)
6665rpred 12772 . . . . . . . . 9 (𝜑 → inf(𝐷, ℝ*, < ) ∈ ℝ)
6766adantr 481 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ∈ ℝ)
682imcld 14906 . . . . . . . . . . 11 (𝜑 → (ℑ‘𝐴) ∈ ℝ)
6968recnd 11003 . . . . . . . . . 10 (𝜑 → (ℑ‘𝐴) ∈ ℂ)
7069adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → (ℑ‘𝐴) ∈ ℂ)
7170abscld 15148 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘𝐴)) ∈ ℝ)
72 recn 10961 . . . . . . . . . . 11 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
7372adantl 482 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
742adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → 𝐴 ∈ ℂ)
7573, 74subcld 11332 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → (𝑦𝐴) ∈ ℂ)
7675abscld 15148 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(𝑦𝐴)) ∈ ℝ)
7760adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝐷 ⊆ ℝ*)
78 infxrlb 13068 . . . . . . . . 9 ((𝐷 ⊆ ℝ* ∧ (abs‘(ℑ‘𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤ (abs‘(ℑ‘𝐴)))
7977, 56, 78sylancl 586 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤ (abs‘(ℑ‘𝐴)))
80 simpr 485 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
8174, 80absimlere 43020 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘𝐴)) ≤ (abs‘(𝑦𝐴)))
8267, 71, 76, 79, 81letrd 11132 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
8336, 82eqbrtrid 5109 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
8483ad4ant14 749 . . . . 5 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
85 cnrefiisplem.c . . . . . . . . 9 𝐶 = (ℝ ∪ 𝐵)
8685eleq2i 2830 . . . . . . . 8 (𝑦𝐶𝑦 ∈ (ℝ ∪ 𝐵))
87 elunnel1 4084 . . . . . . . 8 ((𝑦 ∈ (ℝ ∪ 𝐵) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
8886, 87sylanb 581 . . . . . . 7 ((𝑦𝐶 ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
8988ad4ant24 751 . . . . . 6 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
9060ad2antrr 723 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝐷 ⊆ ℝ*)
91 simpr 485 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦𝐵)
92 simpll 764 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
9391, 92elind 4128 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ (𝐵 ∩ ℂ))
94 nelsn 4601 . . . . . . . . . . . . . . . 16 (𝑦𝐴 → ¬ 𝑦 ∈ {𝐴})
9594ad2antlr 724 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → ¬ 𝑦 ∈ {𝐴})
9693, 95eldifd 3898 . . . . . . . . . . . . . 14 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}))
97 fvex 6787 . . . . . . . . . . . . . . 15 (abs‘(𝑦𝐴)) ∈ V
9897snid 4597 . . . . . . . . . . . . . 14 (abs‘(𝑦𝐴)) ∈ {(abs‘(𝑦𝐴))}
99 fvoveq1 7298 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑦 → (abs‘(𝑤𝐴)) = (abs‘(𝑦𝐴)))
10099sneqd 4573 . . . . . . . . . . . . . . 15 (𝑤 = 𝑦 → {(abs‘(𝑤𝐴))} = {(abs‘(𝑦𝐴))})
101100eliuni 4930 . . . . . . . . . . . . . 14 ((𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) ∧ (abs‘(𝑦𝐴)) ∈ {(abs‘(𝑦𝐴))}) → (abs‘(𝑦𝐴)) ∈ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))})
10296, 98, 101sylancl 586 . . . . . . . . . . . . 13 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))})
103100cbviunv 4970 . . . . . . . . . . . . 13 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))} = 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}
104102, 103eleqtrdi 2849 . . . . . . . . . . . 12 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
105 elun2 4111 . . . . . . . . . . . 12 ((abs‘(𝑦𝐴)) ∈ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} → (abs‘(𝑦𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
106104, 105syl 17 . . . . . . . . . . 11 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
107106, 9eleqtrrdi 2850 . . . . . . . . . 10 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝐷)
108107adantll 711 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝐷)
109 infxrlb 13068 . . . . . . . . 9 ((𝐷 ⊆ ℝ* ∧ (abs‘(𝑦𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
11090, 108, 109syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
11136, 110eqbrtrid 5109 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝑋 ≤ (abs‘(𝑦𝐴)))
112111adantllr 716 . . . . . 6 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝑋 ≤ (abs‘(𝑦𝐴)))
11389, 112syldan 591 . . . . 5 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
11484, 113pm2.61dan 810 . . . 4 (((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) → 𝑋 ≤ (abs‘(𝑦𝐴)))
115114ex 413 . . 3 ((𝜑𝑦𝐶) → ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴))))
116115ralrimiva 3103 . 2 (𝜑 → ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴))))
117 breq1 5077 . . . . 5 (𝑥 = 𝑋 → (𝑥 ≤ (abs‘(𝑦𝐴)) ↔ 𝑋 ≤ (abs‘(𝑦𝐴))))
118117imbi2d 341 . . . 4 (𝑥 = 𝑋 → (((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))) ↔ ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))))
119118ralbidv 3112 . . 3 (𝑥 = 𝑋 → (∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))) ↔ ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))))
120119rspcev 3561 . 2 ((𝑋 ∈ ℝ+ ∧ ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))) → ∃𝑥 ∈ ℝ+𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
12164, 116, 120syl2anc 584 1 (𝜑 → ∃𝑥 ∈ ℝ+𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1539  wcel 2106  wne 2943  wral 3064  wrex 3065  cdif 3884  cun 3885  cin 3886  wss 3887  c0 4256  {csn 4561   ciun 4924   class class class wbr 5074   Or wor 5502  cfv 6433  (class class class)co 7275  Fincfn 8733  infcinf 9200  cc 10869  cr 10870  *cxr 11008   < clt 11009  cle 11010  cmin 11205  +crp 12730  cim 14809  abscabs 14945
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  ax-pre-sup 10949
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-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  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-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  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-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-sup 9201  df-inf 9202  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-nn 11974  df-2 12036  df-3 12037  df-n0 12234  df-z 12320  df-uz 12583  df-rp 12731  df-seq 13722  df-exp 13783  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947
This theorem is referenced by:  cnrefiisp  43371
  Copyright terms: Public domain W3C validator