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 44060
Description: Lemma for cnrefiisp 44061 (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 43702 . . . . . . . 8 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ ℝ+)
54adantr 481 . . . . . . 7 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → (abs‘(ℑ‘𝐴)) ∈ ℝ+)
61, 5eqeltrd 2838 . . . . . 6 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
76adantlr 713 . . . . 5 (((𝜑𝑤𝐷) ∧ 𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
8 simpll 765 . . . . . 6 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝜑)
9 cnrefiisplem.d . . . . . . . . . . . 12 𝐷 = ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
109eleq2i 2829 . . . . . . . . . . 11 (𝑤𝐷𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
1110biimpi 215 . . . . . . . . . 10 (𝑤𝐷𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
12 nelsn 4626 . . . . . . . . . 10 (𝑤 ≠ (abs‘(ℑ‘𝐴)) → ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))})
13 elunnel1 4109 . . . . . . . . . 10 ((𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}) ∧ ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))}) → 𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
1411, 12, 13syl2an 596 . . . . . . . . 9 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
15 eliun 4958 . . . . . . . . 9 (𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))})
1614, 15sylib 217 . . . . . . . 8 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))})
17 velsn 4602 . . . . . . . . 9 (𝑤 ∈ {(abs‘(𝑦𝐴))} ↔ 𝑤 = (abs‘(𝑦𝐴)))
1817rexbii 3097 . . . . . . . 8 (∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
1916, 18sylib 217 . . . . . . 7 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
2019adantll 712 . . . . . 6 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
21 simpr 485 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑤 = (abs‘(𝑦𝐴)))
22 eldifi 4086 . . . . . . . . . . . 12 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ (𝐵 ∩ ℂ))
2322elin2d 4159 . . . . . . . . . . 11 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ ℂ)
2423ad2antlr 725 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑦 ∈ ℂ)
252ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝐴 ∈ ℂ)
2624, 25subcld 11512 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (𝑦𝐴) ∈ ℂ)
27 eldifsni 4750 . . . . . . . . . . 11 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦𝐴)
2827ad2antlr 725 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑦𝐴)
2924, 25, 28subne0d 11521 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (𝑦𝐴) ≠ 0)
3026, 29absrpcld 15333 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (abs‘(𝑦𝐴)) ∈ ℝ+)
3121, 30eqeltrd 2838 . . . . . . 7 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑤 ∈ ℝ+)
3231rexlimdva2 3154 . . . . . 6 (𝜑 → (∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)) → 𝑤 ∈ ℝ+))
338, 20, 32sylc 65 . . . . 5 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
347, 33pm2.61dane 3032 . . . 4 ((𝜑𝑤𝐷) → 𝑤 ∈ ℝ+)
3534ssd 43280 . . 3 (𝜑𝐷 ⊆ ℝ+)
36 cnrefiisplem.x . . . 4 𝑋 = inf(𝐷, ℝ*, < )
37 xrltso 13060 . . . . . 6 < Or ℝ*
3837a1i 11 . . . . 5 (𝜑 → < Or ℝ*)
39 snfi 8988 . . . . . . . 8 {(abs‘(ℑ‘𝐴))} ∈ Fin
4039a1i 11 . . . . . . 7 (𝜑 → {(abs‘(ℑ‘𝐴))} ∈ Fin)
41 cnrefiisplem.b . . . . . . . . 9 (𝜑𝐵 ∈ Fin)
42 inss1 4188 . . . . . . . . . . 11 (𝐵 ∩ ℂ) ⊆ 𝐵
4342a1i 11 . . . . . . . . . 10 (𝜑 → (𝐵 ∩ ℂ) ⊆ 𝐵)
4443ssdifssd 4102 . . . . . . . . 9 (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ⊆ 𝐵)
4541, 44ssfid 9211 . . . . . . . 8 (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin)
46 snfi 8988 . . . . . . . . 9 {(abs‘(𝑦𝐴))} ∈ Fin
4746rgenw 3068 . . . . . . . 8 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin
48 iunfi 9284 . . . . . . . 8 ((((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin ∧ ∀𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin) → 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin)
4945, 47, 48sylancl 586 . . . . . . 7 (𝜑 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin)
5040, 49unfid 43353 . . . . . 6 (𝜑 → ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}) ∈ Fin)
519, 50eqeltrid 2842 . . . . 5 (𝜑𝐷 ∈ Fin)
52 fvex 6855 . . . . . . . . . 10 (abs‘(ℑ‘𝐴)) ∈ V
5352snid 4622 . . . . . . . . 9 (abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))}
54 elun1 4136 . . . . . . . . 9 ((abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))} → (abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
5553, 54ax-mp 5 . . . . . . . 8 (abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
5655, 9eleqtrri 2837 . . . . . . 7 (abs‘(ℑ‘𝐴)) ∈ 𝐷
5756a1i 11 . . . . . 6 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ 𝐷)
5857ne0d 4295 . . . . 5 (𝜑𝐷 ≠ ∅)
59 rpssxr 43706 . . . . . 6 + ⊆ ℝ*
6035, 59sstrdi 3956 . . . . 5 (𝜑𝐷 ⊆ ℝ*)
61 fiinfcl 9437 . . . . 5 (( < Or ℝ* ∧ (𝐷 ∈ Fin ∧ 𝐷 ≠ ∅ ∧ 𝐷 ⊆ ℝ*)) → inf(𝐷, ℝ*, < ) ∈ 𝐷)
6238, 51, 58, 60, 61syl13anc 1372 . . . 4 (𝜑 → inf(𝐷, ℝ*, < ) ∈ 𝐷)
6336, 62eqeltrid 2842 . . 3 (𝜑𝑋𝐷)
6435, 63sseldd 3945 . 2 (𝜑𝑋 ∈ ℝ+)
6535, 62sseldd 3945 . . . . . . . . . 10 (𝜑 → inf(𝐷, ℝ*, < ) ∈ ℝ+)
6665rpred 12957 . . . . . . . . 9 (𝜑 → inf(𝐷, ℝ*, < ) ∈ ℝ)
6766adantr 481 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ∈ ℝ)
682imcld 15080 . . . . . . . . . . 11 (𝜑 → (ℑ‘𝐴) ∈ ℝ)
6968recnd 11183 . . . . . . . . . 10 (𝜑 → (ℑ‘𝐴) ∈ ℂ)
7069adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → (ℑ‘𝐴) ∈ ℂ)
7170abscld 15321 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘𝐴)) ∈ ℝ)
72 recn 11141 . . . . . . . . . . 11 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
7372adantl 482 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
742adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → 𝐴 ∈ ℂ)
7573, 74subcld 11512 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → (𝑦𝐴) ∈ ℂ)
7675abscld 15321 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(𝑦𝐴)) ∈ ℝ)
7760adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝐷 ⊆ ℝ*)
78 infxrlb 13253 . . . . . . . . 9 ((𝐷 ⊆ ℝ* ∧ (abs‘(ℑ‘𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤ (abs‘(ℑ‘𝐴)))
7977, 56, 78sylancl 586 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤ (abs‘(ℑ‘𝐴)))
80 simpr 485 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
8174, 80absimlere 43705 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘𝐴)) ≤ (abs‘(𝑦𝐴)))
8267, 71, 76, 79, 81letrd 11312 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
8336, 82eqbrtrid 5140 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
8483ad4ant14 750 . . . . 5 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
85 cnrefiisplem.c . . . . . . . . 9 𝐶 = (ℝ ∪ 𝐵)
8685eleq2i 2829 . . . . . . . 8 (𝑦𝐶𝑦 ∈ (ℝ ∪ 𝐵))
87 elunnel1 4109 . . . . . . . 8 ((𝑦 ∈ (ℝ ∪ 𝐵) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
8886, 87sylanb 581 . . . . . . 7 ((𝑦𝐶 ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
8988ad4ant24 752 . . . . . 6 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
9060ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝐷 ⊆ ℝ*)
91 simpr 485 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦𝐵)
92 simpll 765 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
9391, 92elind 4154 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ (𝐵 ∩ ℂ))
94 nelsn 4626 . . . . . . . . . . . . . . . 16 (𝑦𝐴 → ¬ 𝑦 ∈ {𝐴})
9594ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → ¬ 𝑦 ∈ {𝐴})
9693, 95eldifd 3921 . . . . . . . . . . . . . 14 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}))
97 fvex 6855 . . . . . . . . . . . . . . 15 (abs‘(𝑦𝐴)) ∈ V
9897snid 4622 . . . . . . . . . . . . . 14 (abs‘(𝑦𝐴)) ∈ {(abs‘(𝑦𝐴))}
99 fvoveq1 7380 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑦 → (abs‘(𝑤𝐴)) = (abs‘(𝑦𝐴)))
10099sneqd 4598 . . . . . . . . . . . . . . 15 (𝑤 = 𝑦 → {(abs‘(𝑤𝐴))} = {(abs‘(𝑦𝐴))})
101100eliuni 4960 . . . . . . . . . . . . . 14 ((𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) ∧ (abs‘(𝑦𝐴)) ∈ {(abs‘(𝑦𝐴))}) → (abs‘(𝑦𝐴)) ∈ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))})
10296, 98, 101sylancl 586 . . . . . . . . . . . . 13 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))})
103100cbviunv 5000 . . . . . . . . . . . . 13 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))} = 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}
104102, 103eleqtrdi 2848 . . . . . . . . . . . 12 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
105 elun2 4137 . . . . . . . . . . . 12 ((abs‘(𝑦𝐴)) ∈ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} → (abs‘(𝑦𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
106104, 105syl 17 . . . . . . . . . . 11 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
107106, 9eleqtrrdi 2849 . . . . . . . . . 10 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝐷)
108107adantll 712 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝐷)
109 infxrlb 13253 . . . . . . . . 9 ((𝐷 ⊆ ℝ* ∧ (abs‘(𝑦𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
11090, 108, 109syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
11136, 110eqbrtrid 5140 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝑋 ≤ (abs‘(𝑦𝐴)))
112111adantllr 717 . . . . . 6 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝑋 ≤ (abs‘(𝑦𝐴)))
11389, 112syldan 591 . . . . 5 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
11484, 113pm2.61dan 811 . . . 4 (((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) → 𝑋 ≤ (abs‘(𝑦𝐴)))
115114ex 413 . . 3 ((𝜑𝑦𝐶) → ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴))))
116115ralrimiva 3143 . 2 (𝜑 → ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴))))
117 breq1 5108 . . . . 5 (𝑥 = 𝑋 → (𝑥 ≤ (abs‘(𝑦𝐴)) ↔ 𝑋 ≤ (abs‘(𝑦𝐴))))
118117imbi2d 340 . . . 4 (𝑥 = 𝑋 → (((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))) ↔ ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))))
119118ralbidv 3174 . . 3 (𝑥 = 𝑋 → (∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))) ↔ ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))))
120119rspcev 3581 . 2 ((𝑋 ∈ ℝ+ ∧ ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))) → ∃𝑥 ∈ ℝ+𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
12164, 116, 120syl2anc 584 1 (𝜑 → ∃𝑥 ∈ ℝ+𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  {csn 4586   ciun 4954   class class class wbr 5105   Or wor 5544  cfv 6496  (class class class)co 7357  Fincfn 8883  infcinf 9377  cc 11049  cr 11050  *cxr 11188   < clt 11189  cle 11190  cmin 11385  +crp 12915  cim 14983  abscabs 15119
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121
This theorem is referenced by:  cnrefiisp  44061
  Copyright terms: Public domain W3C validator