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 45276
Description: Lemma for cnrefiisp 45277 (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 483 . . . . . . 7 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 = (abs‘(ℑ‘𝐴)))
2 cnrefiisplem.a . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
3 cnrefiisplem.n . . . . . . . . 9 (𝜑 → ¬ 𝐴 ∈ ℝ)
42, 3absimnre 44918 . . . . . . . 8 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ ℝ+)
54adantr 479 . . . . . . 7 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → (abs‘(ℑ‘𝐴)) ∈ ℝ+)
61, 5eqeltrd 2825 . . . . . 6 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
76adantlr 713 . . . . 5 (((𝜑𝑤𝐷) ∧ 𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
8 simpll 765 . . . . . 6 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝜑)
9 cnrefiisplem.d . . . . . . . . . . . 12 𝐷 = ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
109eleq2i 2817 . . . . . . . . . . 11 (𝑤𝐷𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
1110biimpi 215 . . . . . . . . . 10 (𝑤𝐷𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
12 nelsn 4665 . . . . . . . . . 10 (𝑤 ≠ (abs‘(ℑ‘𝐴)) → ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))})
13 elunnel1 4143 . . . . . . . . . 10 ((𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}) ∧ ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))}) → 𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
1411, 12, 13syl2an 594 . . . . . . . . 9 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
15 eliun 4996 . . . . . . . . 9 (𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))})
1614, 15sylib 217 . . . . . . . 8 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))})
17 velsn 4641 . . . . . . . . 9 (𝑤 ∈ {(abs‘(𝑦𝐴))} ↔ 𝑤 = (abs‘(𝑦𝐴)))
1817rexbii 3084 . . . . . . . 8 (∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
1916, 18sylib 217 . . . . . . 7 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
2019adantll 712 . . . . . 6 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
21 simpr 483 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑤 = (abs‘(𝑦𝐴)))
22 eldifi 4120 . . . . . . . . . . . 12 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ (𝐵 ∩ ℂ))
2322elin2d 4194 . . . . . . . . . . 11 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ ℂ)
2423ad2antlr 725 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑦 ∈ ℂ)
252ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝐴 ∈ ℂ)
2624, 25subcld 11596 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (𝑦𝐴) ∈ ℂ)
27 eldifsni 4790 . . . . . . . . . . 11 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦𝐴)
2827ad2antlr 725 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑦𝐴)
2924, 25, 28subne0d 11605 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (𝑦𝐴) ≠ 0)
3026, 29absrpcld 15422 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (abs‘(𝑦𝐴)) ∈ ℝ+)
3121, 30eqeltrd 2825 . . . . . . 7 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑤 ∈ ℝ+)
3231rexlimdva2 3147 . . . . . 6 (𝜑 → (∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)) → 𝑤 ∈ ℝ+))
338, 20, 32sylc 65 . . . . 5 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
347, 33pm2.61dane 3019 . . . 4 ((𝜑𝑤𝐷) → 𝑤 ∈ ℝ+)
3534ssd 44507 . . 3 (𝜑𝐷 ⊆ ℝ+)
36 cnrefiisplem.x . . . 4 𝑋 = inf(𝐷, ℝ*, < )
37 xrltso 13147 . . . . . 6 < Or ℝ*
3837a1i 11 . . . . 5 (𝜑 → < Or ℝ*)
39 snfi 9062 . . . . . . . 8 {(abs‘(ℑ‘𝐴))} ∈ Fin
4039a1i 11 . . . . . . 7 (𝜑 → {(abs‘(ℑ‘𝐴))} ∈ Fin)
41 cnrefiisplem.b . . . . . . . . 9 (𝜑𝐵 ∈ Fin)
42 inss1 4224 . . . . . . . . . . 11 (𝐵 ∩ ℂ) ⊆ 𝐵
4342a1i 11 . . . . . . . . . 10 (𝜑 → (𝐵 ∩ ℂ) ⊆ 𝐵)
4443ssdifssd 4136 . . . . . . . . 9 (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ⊆ 𝐵)
4541, 44ssfid 9285 . . . . . . . 8 (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin)
46 snfi 9062 . . . . . . . . 9 {(abs‘(𝑦𝐴))} ∈ Fin
4746rgenw 3055 . . . . . . . 8 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin
48 iunfi 9359 . . . . . . . 8 ((((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin ∧ ∀𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin) → 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin)
4945, 47, 48sylancl 584 . . . . . . 7 (𝜑 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin)
5040, 49unfid 44579 . . . . . 6 (𝜑 → ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}) ∈ Fin)
519, 50eqeltrid 2829 . . . . 5 (𝜑𝐷 ∈ Fin)
52 fvex 6903 . . . . . . . . . 10 (abs‘(ℑ‘𝐴)) ∈ V
5352snid 4661 . . . . . . . . 9 (abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))}
54 elun1 4171 . . . . . . . . 9 ((abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))} → (abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
5553, 54ax-mp 5 . . . . . . . 8 (abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
5655, 9eleqtrri 2824 . . . . . . 7 (abs‘(ℑ‘𝐴)) ∈ 𝐷
5756a1i 11 . . . . . 6 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ 𝐷)
5857ne0d 4332 . . . . 5 (𝜑𝐷 ≠ ∅)
59 rpssxr 44922 . . . . . 6 + ⊆ ℝ*
6035, 59sstrdi 3986 . . . . 5 (𝜑𝐷 ⊆ ℝ*)
61 fiinfcl 9519 . . . . 5 (( < Or ℝ* ∧ (𝐷 ∈ Fin ∧ 𝐷 ≠ ∅ ∧ 𝐷 ⊆ ℝ*)) → inf(𝐷, ℝ*, < ) ∈ 𝐷)
6238, 51, 58, 60, 61syl13anc 1369 . . . 4 (𝜑 → inf(𝐷, ℝ*, < ) ∈ 𝐷)
6336, 62eqeltrid 2829 . . 3 (𝜑𝑋𝐷)
6435, 63sseldd 3974 . 2 (𝜑𝑋 ∈ ℝ+)
6535, 62sseldd 3974 . . . . . . . . . 10 (𝜑 → inf(𝐷, ℝ*, < ) ∈ ℝ+)
6665rpred 13043 . . . . . . . . 9 (𝜑 → inf(𝐷, ℝ*, < ) ∈ ℝ)
6766adantr 479 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ∈ ℝ)
682imcld 15169 . . . . . . . . . . 11 (𝜑 → (ℑ‘𝐴) ∈ ℝ)
6968recnd 11267 . . . . . . . . . 10 (𝜑 → (ℑ‘𝐴) ∈ ℂ)
7069adantr 479 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → (ℑ‘𝐴) ∈ ℂ)
7170abscld 15410 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘𝐴)) ∈ ℝ)
72 recn 11223 . . . . . . . . . . 11 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
7372adantl 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
742adantr 479 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → 𝐴 ∈ ℂ)
7573, 74subcld 11596 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → (𝑦𝐴) ∈ ℂ)
7675abscld 15410 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(𝑦𝐴)) ∈ ℝ)
7760adantr 479 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝐷 ⊆ ℝ*)
78 infxrlb 13340 . . . . . . . . 9 ((𝐷 ⊆ ℝ* ∧ (abs‘(ℑ‘𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤ (abs‘(ℑ‘𝐴)))
7977, 56, 78sylancl 584 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤ (abs‘(ℑ‘𝐴)))
80 simpr 483 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
8174, 80absimlere 44921 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘𝐴)) ≤ (abs‘(𝑦𝐴)))
8267, 71, 76, 79, 81letrd 11396 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
8336, 82eqbrtrid 5179 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
8483ad4ant14 750 . . . . 5 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
85 cnrefiisplem.c . . . . . . . . 9 𝐶 = (ℝ ∪ 𝐵)
8685eleq2i 2817 . . . . . . . 8 (𝑦𝐶𝑦 ∈ (ℝ ∪ 𝐵))
87 elunnel1 4143 . . . . . . . 8 ((𝑦 ∈ (ℝ ∪ 𝐵) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
8886, 87sylanb 579 . . . . . . 7 ((𝑦𝐶 ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
8988ad4ant24 752 . . . . . 6 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
9060ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝐷 ⊆ ℝ*)
91 simpr 483 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦𝐵)
92 simpll 765 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
9391, 92elind 4189 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ (𝐵 ∩ ℂ))
94 nelsn 4665 . . . . . . . . . . . . . . . 16 (𝑦𝐴 → ¬ 𝑦 ∈ {𝐴})
9594ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → ¬ 𝑦 ∈ {𝐴})
9693, 95eldifd 3952 . . . . . . . . . . . . . 14 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}))
97 fvex 6903 . . . . . . . . . . . . . . 15 (abs‘(𝑦𝐴)) ∈ V
9897snid 4661 . . . . . . . . . . . . . 14 (abs‘(𝑦𝐴)) ∈ {(abs‘(𝑦𝐴))}
99 fvoveq1 7436 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑦 → (abs‘(𝑤𝐴)) = (abs‘(𝑦𝐴)))
10099sneqd 4637 . . . . . . . . . . . . . . 15 (𝑤 = 𝑦 → {(abs‘(𝑤𝐴))} = {(abs‘(𝑦𝐴))})
101100eliuni 4998 . . . . . . . . . . . . . 14 ((𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) ∧ (abs‘(𝑦𝐴)) ∈ {(abs‘(𝑦𝐴))}) → (abs‘(𝑦𝐴)) ∈ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))})
10296, 98, 101sylancl 584 . . . . . . . . . . . . 13 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))})
103100cbviunv 5039 . . . . . . . . . . . . 13 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))} = 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}
104102, 103eleqtrdi 2835 . . . . . . . . . . . 12 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
105 elun2 4172 . . . . . . . . . . . 12 ((abs‘(𝑦𝐴)) ∈ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} → (abs‘(𝑦𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
106104, 105syl 17 . . . . . . . . . . 11 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
107106, 9eleqtrrdi 2836 . . . . . . . . . 10 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝐷)
108107adantll 712 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝐷)
109 infxrlb 13340 . . . . . . . . 9 ((𝐷 ⊆ ℝ* ∧ (abs‘(𝑦𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
11090, 108, 109syl2anc 582 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
11136, 110eqbrtrid 5179 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝑋 ≤ (abs‘(𝑦𝐴)))
112111adantllr 717 . . . . . 6 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝑋 ≤ (abs‘(𝑦𝐴)))
11389, 112syldan 589 . . . . 5 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
11484, 113pm2.61dan 811 . . . 4 (((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) → 𝑋 ≤ (abs‘(𝑦𝐴)))
115114ex 411 . . 3 ((𝜑𝑦𝐶) → ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴))))
116115ralrimiva 3136 . 2 (𝜑 → ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴))))
117 breq1 5147 . . . . 5 (𝑥 = 𝑋 → (𝑥 ≤ (abs‘(𝑦𝐴)) ↔ 𝑋 ≤ (abs‘(𝑦𝐴))))
118117imbi2d 339 . . . 4 (𝑥 = 𝑋 → (((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))) ↔ ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))))
119118ralbidv 3168 . . 3 (𝑥 = 𝑋 → (∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))) ↔ ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))))
120119rspcev 3603 . 2 ((𝑋 ∈ ℝ+ ∧ ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))) → ∃𝑥 ∈ ℝ+𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
12164, 116, 120syl2anc 582 1 (𝜑 → ∃𝑥 ∈ ℝ+𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394   = wceq 1533  wcel 2098  wne 2930  wral 3051  wrex 3060  cdif 3938  cun 3939  cin 3940  wss 3941  c0 4319  {csn 4625   ciun 4992   class class class wbr 5144   Or wor 5584  cfv 6543  (class class class)co 7413  Fincfn 8957  infcinf 9459  cc 11131  cr 11132  *cxr 11272   < clt 11273  cle 11274  cmin 11469  +crp 13001  cim 15072  abscabs 15208
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-sup 9460  df-inf 9461  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-n0 12498  df-z 12584  df-uz 12848  df-rp 13002  df-seq 13994  df-exp 14054  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210
This theorem is referenced by:  cnrefiisp  45277
  Copyright terms: Public domain W3C validator