Metamath Proof Explorer

Theorem mulcn2

Description: Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of Gleason p. 243. (Contributed by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion mulcn2 ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→∃y∈ℝ+∃z∈ℝ+∀u∈ℂ∀v∈ℂu−B<y∧v−C<z→u⁢v−B⁢C<A

Proof

Step Hyp Ref Expression
1 rphalfcl ⊢A∈ℝ+→A2∈ℝ+
2 1 3ad2ant1 ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→A2∈ℝ+
3 abscl ⊢C∈ℂ→C∈ℝ
4 3 3ad2ant3 ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→C∈ℝ
5 abscl ⊢B∈ℂ→B∈ℝ
6 5 3ad2ant2 ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→B∈ℝ
7 1re ⊢1∈ℝ
8 readdcl ⊢B∈ℝ∧1∈ℝ→B+1∈ℝ
9 6 7 8 sylancl ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→B+1∈ℝ
10 absge0 ⊢B∈ℂ→0≤B
11 0lt1 ⊢0<1
12 addgegt0 ⊢B∈ℝ∧1∈ℝ∧0≤B∧0<1→0<B+1
13 12 an4s ⊢B∈ℝ∧0≤B∧1∈ℝ∧0<1→0<B+1
14 7 11 13 mpanr12 ⊢B∈ℝ∧0≤B→0<B+1
15 5 10 14 syl2anc ⊢B∈ℂ→0<B+1
16 15 3ad2ant2 ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→0<B+1
17 9 16 elrpd ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→B+1∈ℝ+
18 2 17 rpdivcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→A2B+1∈ℝ+
19 18 rpred ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→A2B+1∈ℝ
20 4 19 readdcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→C+A2B+1∈ℝ
21 absge0 ⊢C∈ℂ→0≤C
22 21 3ad2ant3 ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→0≤C
23 elrp ⊢A2B+1∈ℝ+↔A2B+1∈ℝ∧0<A2B+1
24 addgegt0 ⊢C∈ℝ∧A2B+1∈ℝ∧0≤C∧0<A2B+1→0<C+A2B+1
25 24 an4s ⊢C∈ℝ∧0≤C∧A2B+1∈ℝ∧0<A2B+1→0<C+A2B+1
26 23 25 sylan2b ⊢C∈ℝ∧0≤C∧A2B+1∈ℝ+→0<C+A2B+1
27 4 22 18 26 syl21anc ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→0<C+A2B+1
28 20 27 elrpd ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→C+A2B+1∈ℝ+
29 2 28 rpdivcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→A2C+A2B+1∈ℝ+
30 simprl ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u∈ℂ
31 simpl2 ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B∈ℂ
32 30 31 subcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B∈ℂ
33 32 abscld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B∈ℝ
34 2 adantr ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→A2∈ℝ+
35 34 rpred ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→A2∈ℝ
36 28 adantr ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→C+A2B+1∈ℝ+
37 33 35 36 ltmuldivd ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢C+A2B+1<A2↔u−B<A2C+A2B+1
38 simprr ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v∈ℂ
39 simpl3 ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→C∈ℂ
40 38 39 abs2difd ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C≤v−C
41 38 abscld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v∈ℝ
42 4 adantr ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→C∈ℝ
43 41 42 resubcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C∈ℝ
44 38 39 subcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C∈ℂ
45 44 abscld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C∈ℝ
46 19 adantr ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→A2B+1∈ℝ
47 lelttr ⊢v−C∈ℝ∧v−C∈ℝ∧A2B+1∈ℝ→v−C≤v−C∧v−C<A2B+1→v−C<A2B+1
48 43 45 46 47 syl3anc ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C≤v−C∧v−C<A2B+1→v−C<A2B+1
49 40 48 mpand ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C<A2B+1→v−C<A2B+1
50 41 42 46 ltsubadd2d ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C<A2B+1↔v<C+A2B+1
51 49 50 sylibd ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C<A2B+1→v<C+A2B+1
52 20 adantr ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→C+A2B+1∈ℝ
53 ltle ⊢v∈ℝ∧C+A2B+1∈ℝ→v<C+A2B+1→v≤C+A2B+1
54 41 52 53 syl2anc ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v<C+A2B+1→v≤C+A2B+1
55 51 54 syld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C<A2B+1→v≤C+A2B+1
56 32 absge0d ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→0≤u−B
57 lemul2a ⊢v∈ℝ∧C+A2B+1∈ℝ∧u−B∈ℝ∧0≤u−B∧v≤C+A2B+1→u−B⁢v≤u−B⁢C+A2B+1
58 57 ex ⊢v∈ℝ∧C+A2B+1∈ℝ∧u−B∈ℝ∧0≤u−B→v≤C+A2B+1→u−B⁢v≤u−B⁢C+A2B+1
59 41 52 33 56 58 syl112anc ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v≤C+A2B+1→u−B⁢v≤u−B⁢C+A2B+1
60 33 41 remulcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢v∈ℝ
61 33 52 remulcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢C+A2B+1∈ℝ
62 lelttr ⊢u−B⁢v∈ℝ∧u−B⁢C+A2B+1∈ℝ∧A2∈ℝ→u−B⁢v≤u−B⁢C+A2B+1∧u−B⁢C+A2B+1<A2→u−B⁢v<A2
63 60 61 35 62 syl3anc ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢v≤u−B⁢C+A2B+1∧u−B⁢C+A2B+1<A2→u−B⁢v<A2
64 63 expd ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢v≤u−B⁢C+A2B+1→u−B⁢C+A2B+1<A2→u−B⁢v<A2
65 55 59 64 3syld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C<A2B+1→u−B⁢C+A2B+1<A2→u−B⁢v<A2
66 65 com23 ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢C+A2B+1<A2→v−C<A2B+1→u−B⁢v<A2
67 37 66 sylbird ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B<A2C+A2B+1→v−C<A2B+1→u−B⁢v<A2
68 67 impd ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B<A2C+A2B+1∧v−C<A2B+1→u−B⁢v<A2
69 32 38 absmuld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢v=u−B⁢v
70 30 31 38 subdird ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢v=u⁢v−B⁢v
71 70 fveq2d ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢v=u⁢v−B⁢v
72 69 71 eqtr3d ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢v=u⁢v−B⁢v
73 72 breq1d ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B⁢v<A2↔u⁢v−B⁢v<A2
74 68 73 sylibd ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B<A2C+A2B+1∧v−C<A2B+1→u⁢v−B⁢v<A2
75 17 adantr ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B+1∈ℝ+
76 45 35 75 ltmuldiv2d ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B+1⁢v−C<A2↔v−C<A2B+1
77 31 38 39 subdid ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢v−C=B⁢v−B⁢C
78 77 fveq2d ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢v−C=B⁢v−B⁢C
79 31 44 absmuld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢v−C=B⁢v−C
80 78 79 eqtr3d ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢v−B⁢C=B⁢v−C
81 31 abscld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B∈ℝ
82 81 lep1d ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B≤B+1
83 9 adantr ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B+1∈ℝ
84 abscl ⊢v−C∈ℂ→v−C∈ℝ
85 absge0 ⊢v−C∈ℂ→0≤v−C
86 84 85 jca ⊢v−C∈ℂ→v−C∈ℝ∧0≤v−C
87 lemul1a ⊢B∈ℝ∧B+1∈ℝ∧v−C∈ℝ∧0≤v−C∧B≤B+1→B⁢v−C≤B+1⁢v−C
88 87 ex ⊢B∈ℝ∧B+1∈ℝ∧v−C∈ℝ∧0≤v−C→B≤B+1→B⁢v−C≤B+1⁢v−C
89 86 88 syl3an3 ⊢B∈ℝ∧B+1∈ℝ∧v−C∈ℂ→B≤B+1→B⁢v−C≤B+1⁢v−C
90 81 83 44 89 syl3anc ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B≤B+1→B⁢v−C≤B+1⁢v−C
91 82 90 mpd ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢v−C≤B+1⁢v−C
92 80 91 eqbrtrd ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢v−B⁢C≤B+1⁢v−C
93 31 38 mulcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢v∈ℂ
94 31 39 mulcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢C∈ℂ
95 93 94 subcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢v−B⁢C∈ℂ
96 95 abscld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢v−B⁢C∈ℝ
97 83 45 remulcld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B+1⁢v−C∈ℝ
98 lelttr ⊢B⁢v−B⁢C∈ℝ∧B+1⁢v−C∈ℝ∧A2∈ℝ→B⁢v−B⁢C≤B+1⁢v−C∧B+1⁢v−C<A2→B⁢v−B⁢C<A2
99 96 97 35 98 syl3anc ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B⁢v−B⁢C≤B+1⁢v−C∧B+1⁢v−C<A2→B⁢v−B⁢C<A2
100 92 99 mpand ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→B+1⁢v−C<A2→B⁢v−B⁢C<A2
101 76 100 sylbird ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→v−C<A2B+1→B⁢v−B⁢C<A2
102 101 adantld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B<A2C+A2B+1∧v−C<A2B+1→B⁢v−B⁢C<A2
103 74 102 jcad ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B<A2C+A2B+1∧v−C<A2B+1→u⁢v−B⁢v<A2∧B⁢v−B⁢C<A2
104 mulcl ⊢u∈ℂ∧v∈ℂ→u⁢v∈ℂ
105 104 adantl ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u⁢v∈ℂ
106 simpl1 ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→A∈ℝ+
107 106 rpred ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→A∈ℝ
108 abs3lem ⊢u⁢v∈ℂ∧B⁢C∈ℂ∧B⁢v∈ℂ∧A∈ℝ→u⁢v−B⁢v<A2∧B⁢v−B⁢C<A2→u⁢v−B⁢C<A
109 105 94 93 107 108 syl22anc ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u⁢v−B⁢v<A2∧B⁢v−B⁢C<A2→u⁢v−B⁢C<A
110 103 109 syld ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ∧u∈ℂ∧v∈ℂ→u−B<A2C+A2B+1∧v−C<A2B+1→u⁢v−B⁢C<A
111 110 ralrimivva ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→∀u∈ℂ∀v∈ℂu−B<A2C+A2B+1∧v−C<A2B+1→u⁢v−B⁢C<A
112 breq2 ⊢y=A2C+A2B+1→u−B<y↔u−B<A2C+A2B+1
113 112 anbi1d ⊢y=A2C+A2B+1→u−B<y∧v−C<z↔u−B<A2C+A2B+1∧v−C<z
114 113 imbi1d ⊢y=A2C+A2B+1→u−B<y∧v−C<z→u⁢v−B⁢C<A↔u−B<A2C+A2B+1∧v−C<z→u⁢v−B⁢C<A
115 114 2ralbidv ⊢y=A2C+A2B+1→∀u∈ℂ∀v∈ℂu−B<y∧v−C<z→u⁢v−B⁢C<A↔∀u∈ℂ∀v∈ℂu−B<A2C+A2B+1∧v−C<z→u⁢v−B⁢C<A
116 breq2 ⊢z=A2B+1→v−C<z↔v−C<A2B+1
117 116 anbi2d ⊢z=A2B+1→u−B<A2C+A2B+1∧v−C<z↔u−B<A2C+A2B+1∧v−C<A2B+1
118 117 imbi1d ⊢z=A2B+1→u−B<A2C+A2B+1∧v−C<z→u⁢v−B⁢C<A↔u−B<A2C+A2B+1∧v−C<A2B+1→u⁢v−B⁢C<A
119 118 2ralbidv ⊢z=A2B+1→∀u∈ℂ∀v∈ℂu−B<A2C+A2B+1∧v−C<z→u⁢v−B⁢C<A↔∀u∈ℂ∀v∈ℂu−B<A2C+A2B+1∧v−C<A2B+1→u⁢v−B⁢C<A
120 115 119 rspc2ev ⊢A2C+A2B+1∈ℝ+∧A2B+1∈ℝ+∧∀u∈ℂ∀v∈ℂu−B<A2C+A2B+1∧v−C<A2B+1→u⁢v−B⁢C<A→∃y∈ℝ+∃z∈ℝ+∀u∈ℂ∀v∈ℂu−B<y∧v−C<z→u⁢v−B⁢C<A
121 29 18 111 120 syl3anc ⊢A∈ℝ+∧B∈ℂ∧C∈ℂ→∃y∈ℝ+∃z∈ℝ+∀u∈ℂ∀v∈ℂu−B<y∧v−C<z→u⁢v−B⁢C<A