Metamath Proof Explorer


Theorem fourierdlem35

Description: There is a single point in ( A (,] B ) that's distant from X a multiple integer of T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem35.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
fourierdlem35.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
fourierdlem35.altb โŠข ( ๐œ‘ โ†’ ๐ด < ๐ต )
fourierdlem35.t โŠข ๐‘‡ = ( ๐ต โˆ’ ๐ด )
fourierdlem35.5 โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„ )
fourierdlem35.i โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ โ„ค )
fourierdlem35.j โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค )
fourierdlem35.iel โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โˆˆ ( ๐ด (,] ๐ต ) )
fourierdlem35.jel โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โˆˆ ( ๐ด (,] ๐ต ) )
Assertion fourierdlem35 ( ๐œ‘ โ†’ ๐ผ = ๐ฝ )

Proof

Step Hyp Ref Expression
1 fourierdlem35.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
2 fourierdlem35.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
3 fourierdlem35.altb โŠข ( ๐œ‘ โ†’ ๐ด < ๐ต )
4 fourierdlem35.t โŠข ๐‘‡ = ( ๐ต โˆ’ ๐ด )
5 fourierdlem35.5 โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„ )
6 fourierdlem35.i โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ โ„ค )
7 fourierdlem35.j โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค )
8 fourierdlem35.iel โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โˆˆ ( ๐ด (,] ๐ต ) )
9 fourierdlem35.jel โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โˆˆ ( ๐ด (,] ๐ต ) )
10 neqne โŠข ( ยฌ ๐ผ = ๐ฝ โ†’ ๐ผ โ‰  ๐ฝ )
11 1 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ๐ด โˆˆ โ„ )
12 2 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ๐ต โˆˆ โ„ )
13 3 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ๐ด < ๐ต )
14 5 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ๐‘‹ โˆˆ โ„ )
15 6 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ๐ผ โˆˆ โ„ค )
16 7 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ๐ฝ โˆˆ โ„ค )
17 simpr โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ๐ผ < ๐ฝ )
18 iocssicc โŠข ( ๐ด (,] ๐ต ) โŠ† ( ๐ด [,] ๐ต )
19 18 8 sselid โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โˆˆ ( ๐ด [,] ๐ต ) )
20 19 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โˆˆ ( ๐ด [,] ๐ต ) )
21 18 9 sselid โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โˆˆ ( ๐ด [,] ๐ต ) )
22 21 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โˆˆ ( ๐ด [,] ๐ต ) )
23 11 12 13 4 14 15 16 17 20 22 fourierdlem6 โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ๐ฝ = ( ๐ผ + 1 ) )
24 23 orcd โŠข ( ( ๐œ‘ โˆง ๐ผ < ๐ฝ ) โ†’ ( ๐ฝ = ( ๐ผ + 1 ) โˆจ ๐ผ = ( ๐ฝ + 1 ) ) )
25 24 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐ผ โ‰  ๐ฝ ) โˆง ๐ผ < ๐ฝ ) โ†’ ( ๐ฝ = ( ๐ผ + 1 ) โˆจ ๐ผ = ( ๐ฝ + 1 ) ) )
26 simpll โŠข ( ( ( ๐œ‘ โˆง ๐ผ โ‰  ๐ฝ ) โˆง ยฌ ๐ผ < ๐ฝ ) โ†’ ๐œ‘ )
27 7 zred โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ โ„ )
28 26 27 syl โŠข ( ( ( ๐œ‘ โˆง ๐ผ โ‰  ๐ฝ ) โˆง ยฌ ๐ผ < ๐ฝ ) โ†’ ๐ฝ โˆˆ โ„ )
29 6 zred โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ โ„ )
30 26 29 syl โŠข ( ( ( ๐œ‘ โˆง ๐ผ โ‰  ๐ฝ ) โˆง ยฌ ๐ผ < ๐ฝ ) โ†’ ๐ผ โˆˆ โ„ )
31 id โŠข ( ๐ผ โ‰  ๐ฝ โ†’ ๐ผ โ‰  ๐ฝ )
32 31 necomd โŠข ( ๐ผ โ‰  ๐ฝ โ†’ ๐ฝ โ‰  ๐ผ )
33 32 ad2antlr โŠข ( ( ( ๐œ‘ โˆง ๐ผ โ‰  ๐ฝ ) โˆง ยฌ ๐ผ < ๐ฝ ) โ†’ ๐ฝ โ‰  ๐ผ )
34 simpr โŠข ( ( ( ๐œ‘ โˆง ๐ผ โ‰  ๐ฝ ) โˆง ยฌ ๐ผ < ๐ฝ ) โ†’ ยฌ ๐ผ < ๐ฝ )
35 28 30 33 34 lttri5d โŠข ( ( ( ๐œ‘ โˆง ๐ผ โ‰  ๐ฝ ) โˆง ยฌ ๐ผ < ๐ฝ ) โ†’ ๐ฝ < ๐ผ )
36 1 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ๐ด โˆˆ โ„ )
37 2 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ๐ต โˆˆ โ„ )
38 3 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ๐ด < ๐ต )
39 5 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ๐‘‹ โˆˆ โ„ )
40 7 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ๐ฝ โˆˆ โ„ค )
41 6 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ๐ผ โˆˆ โ„ค )
42 simpr โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ๐ฝ < ๐ผ )
43 21 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โˆˆ ( ๐ด [,] ๐ต ) )
44 19 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โˆˆ ( ๐ด [,] ๐ต ) )
45 36 37 38 4 39 40 41 42 43 44 fourierdlem6 โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ๐ผ = ( ๐ฝ + 1 ) )
46 45 olcd โŠข ( ( ๐œ‘ โˆง ๐ฝ < ๐ผ ) โ†’ ( ๐ฝ = ( ๐ผ + 1 ) โˆจ ๐ผ = ( ๐ฝ + 1 ) ) )
47 26 35 46 syl2anc โŠข ( ( ( ๐œ‘ โˆง ๐ผ โ‰  ๐ฝ ) โˆง ยฌ ๐ผ < ๐ฝ ) โ†’ ( ๐ฝ = ( ๐ผ + 1 ) โˆจ ๐ผ = ( ๐ฝ + 1 ) ) )
48 25 47 pm2.61dan โŠข ( ( ๐œ‘ โˆง ๐ผ โ‰  ๐ฝ ) โ†’ ( ๐ฝ = ( ๐ผ + 1 ) โˆจ ๐ผ = ( ๐ฝ + 1 ) ) )
49 10 48 sylan2 โŠข ( ( ๐œ‘ โˆง ยฌ ๐ผ = ๐ฝ ) โ†’ ( ๐ฝ = ( ๐ผ + 1 ) โˆจ ๐ผ = ( ๐ฝ + 1 ) ) )
50 1 rexrd โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„* )
51 2 rexrd โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„* )
52 iocleub โŠข ( ( ๐ด โˆˆ โ„* โˆง ๐ต โˆˆ โ„* โˆง ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โˆˆ ( ๐ด (,] ๐ต ) ) โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โ‰ค ๐ต )
53 50 51 9 52 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โ‰ค ๐ต )
54 53 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โ‰ค ๐ต )
55 1 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ๐ด โˆˆ โ„ )
56 2 1 resubcld โŠข ( ๐œ‘ โ†’ ( ๐ต โˆ’ ๐ด ) โˆˆ โ„ )
57 4 56 eqeltrid โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ โ„ )
58 29 57 remulcld โŠข ( ๐œ‘ โ†’ ( ๐ผ ยท ๐‘‡ ) โˆˆ โ„ )
59 5 58 readdcld โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โˆˆ โ„ )
60 59 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โˆˆ โ„ )
61 57 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ๐‘‡ โˆˆ โ„ )
62 iocgtlb โŠข ( ( ๐ด โˆˆ โ„* โˆง ๐ต โˆˆ โ„* โˆง ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โˆˆ ( ๐ด (,] ๐ต ) ) โ†’ ๐ด < ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) )
63 50 51 8 62 syl3anc โŠข ( ๐œ‘ โ†’ ๐ด < ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) )
64 63 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ๐ด < ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) )
65 55 60 61 64 ltadd1dd โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ( ๐ด + ๐‘‡ ) < ( ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) + ๐‘‡ ) )
66 4 eqcomi โŠข ( ๐ต โˆ’ ๐ด ) = ๐‘‡
67 2 recnd โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
68 1 recnd โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
69 57 recnd โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ โ„‚ )
70 67 68 69 subaddd โŠข ( ๐œ‘ โ†’ ( ( ๐ต โˆ’ ๐ด ) = ๐‘‡ โ†” ( ๐ด + ๐‘‡ ) = ๐ต ) )
71 66 70 mpbii โŠข ( ๐œ‘ โ†’ ( ๐ด + ๐‘‡ ) = ๐ต )
72 71 eqcomd โŠข ( ๐œ‘ โ†’ ๐ต = ( ๐ด + ๐‘‡ ) )
73 72 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ๐ต = ( ๐ด + ๐‘‡ ) )
74 5 recnd โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚ )
75 58 recnd โŠข ( ๐œ‘ โ†’ ( ๐ผ ยท ๐‘‡ ) โˆˆ โ„‚ )
76 74 75 69 addassd โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) + ๐‘‡ ) = ( ๐‘‹ + ( ( ๐ผ ยท ๐‘‡ ) + ๐‘‡ ) ) )
77 76 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ( ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) + ๐‘‡ ) = ( ๐‘‹ + ( ( ๐ผ ยท ๐‘‡ ) + ๐‘‡ ) ) )
78 29 recnd โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ โ„‚ )
79 78 69 adddirp1d โŠข ( ๐œ‘ โ†’ ( ( ๐ผ + 1 ) ยท ๐‘‡ ) = ( ( ๐ผ ยท ๐‘‡ ) + ๐‘‡ ) )
80 79 eqcomd โŠข ( ๐œ‘ โ†’ ( ( ๐ผ ยท ๐‘‡ ) + ๐‘‡ ) = ( ( ๐ผ + 1 ) ยท ๐‘‡ ) )
81 80 oveq2d โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ( ๐ผ ยท ๐‘‡ ) + ๐‘‡ ) ) = ( ๐‘‹ + ( ( ๐ผ + 1 ) ยท ๐‘‡ ) ) )
82 81 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ( ๐‘‹ + ( ( ๐ผ ยท ๐‘‡ ) + ๐‘‡ ) ) = ( ๐‘‹ + ( ( ๐ผ + 1 ) ยท ๐‘‡ ) ) )
83 oveq1 โŠข ( ๐ฝ = ( ๐ผ + 1 ) โ†’ ( ๐ฝ ยท ๐‘‡ ) = ( ( ๐ผ + 1 ) ยท ๐‘‡ ) )
84 83 eqcomd โŠข ( ๐ฝ = ( ๐ผ + 1 ) โ†’ ( ( ๐ผ + 1 ) ยท ๐‘‡ ) = ( ๐ฝ ยท ๐‘‡ ) )
85 84 oveq2d โŠข ( ๐ฝ = ( ๐ผ + 1 ) โ†’ ( ๐‘‹ + ( ( ๐ผ + 1 ) ยท ๐‘‡ ) ) = ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) )
86 85 adantl โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ( ๐‘‹ + ( ( ๐ผ + 1 ) ยท ๐‘‡ ) ) = ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) )
87 77 82 86 3eqtrrd โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) = ( ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) + ๐‘‡ ) )
88 65 73 87 3brtr4d โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ๐ต < ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) )
89 2 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ๐ต โˆˆ โ„ )
90 27 57 remulcld โŠข ( ๐œ‘ โ†’ ( ๐ฝ ยท ๐‘‡ ) โˆˆ โ„ )
91 5 90 readdcld โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โˆˆ โ„ )
92 91 adantr โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โˆˆ โ„ )
93 89 92 ltnled โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ( ๐ต < ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โ†” ยฌ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โ‰ค ๐ต ) )
94 88 93 mpbid โŠข ( ( ๐œ‘ โˆง ๐ฝ = ( ๐ผ + 1 ) ) โ†’ ยฌ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โ‰ค ๐ต )
95 54 94 pm2.65da โŠข ( ๐œ‘ โ†’ ยฌ ๐ฝ = ( ๐ผ + 1 ) )
96 iocleub โŠข ( ( ๐ด โˆˆ โ„* โˆง ๐ต โˆˆ โ„* โˆง ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โˆˆ ( ๐ด (,] ๐ต ) ) โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โ‰ค ๐ต )
97 50 51 8 96 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โ‰ค ๐ต )
98 97 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โ‰ค ๐ต )
99 1 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ๐ด โˆˆ โ„ )
100 91 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โˆˆ โ„ )
101 57 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ๐‘‡ โˆˆ โ„ )
102 iocgtlb โŠข ( ( ๐ด โˆˆ โ„* โˆง ๐ต โˆˆ โ„* โˆง ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) โˆˆ ( ๐ด (,] ๐ต ) ) โ†’ ๐ด < ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) )
103 50 51 9 102 syl3anc โŠข ( ๐œ‘ โ†’ ๐ด < ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) )
104 103 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ๐ด < ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) )
105 99 100 101 104 ltadd1dd โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ( ๐ด + ๐‘‡ ) < ( ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) + ๐‘‡ ) )
106 72 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ๐ต = ( ๐ด + ๐‘‡ ) )
107 90 recnd โŠข ( ๐œ‘ โ†’ ( ๐ฝ ยท ๐‘‡ ) โˆˆ โ„‚ )
108 74 107 69 addassd โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) + ๐‘‡ ) = ( ๐‘‹ + ( ( ๐ฝ ยท ๐‘‡ ) + ๐‘‡ ) ) )
109 108 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ( ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) + ๐‘‡ ) = ( ๐‘‹ + ( ( ๐ฝ ยท ๐‘‡ ) + ๐‘‡ ) ) )
110 27 recnd โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ โ„‚ )
111 110 69 adddirp1d โŠข ( ๐œ‘ โ†’ ( ( ๐ฝ + 1 ) ยท ๐‘‡ ) = ( ( ๐ฝ ยท ๐‘‡ ) + ๐‘‡ ) )
112 111 eqcomd โŠข ( ๐œ‘ โ†’ ( ( ๐ฝ ยท ๐‘‡ ) + ๐‘‡ ) = ( ( ๐ฝ + 1 ) ยท ๐‘‡ ) )
113 112 oveq2d โŠข ( ๐œ‘ โ†’ ( ๐‘‹ + ( ( ๐ฝ ยท ๐‘‡ ) + ๐‘‡ ) ) = ( ๐‘‹ + ( ( ๐ฝ + 1 ) ยท ๐‘‡ ) ) )
114 113 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ( ๐‘‹ + ( ( ๐ฝ ยท ๐‘‡ ) + ๐‘‡ ) ) = ( ๐‘‹ + ( ( ๐ฝ + 1 ) ยท ๐‘‡ ) ) )
115 oveq1 โŠข ( ๐ผ = ( ๐ฝ + 1 ) โ†’ ( ๐ผ ยท ๐‘‡ ) = ( ( ๐ฝ + 1 ) ยท ๐‘‡ ) )
116 115 eqcomd โŠข ( ๐ผ = ( ๐ฝ + 1 ) โ†’ ( ( ๐ฝ + 1 ) ยท ๐‘‡ ) = ( ๐ผ ยท ๐‘‡ ) )
117 116 oveq2d โŠข ( ๐ผ = ( ๐ฝ + 1 ) โ†’ ( ๐‘‹ + ( ( ๐ฝ + 1 ) ยท ๐‘‡ ) ) = ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) )
118 117 adantl โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ( ๐‘‹ + ( ( ๐ฝ + 1 ) ยท ๐‘‡ ) ) = ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) )
119 109 114 118 3eqtrrd โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) = ( ( ๐‘‹ + ( ๐ฝ ยท ๐‘‡ ) ) + ๐‘‡ ) )
120 105 106 119 3brtr4d โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ๐ต < ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) )
121 2 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ๐ต โˆˆ โ„ )
122 59 adantr โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โˆˆ โ„ )
123 121 122 ltnled โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ( ๐ต < ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โ†” ยฌ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โ‰ค ๐ต ) )
124 120 123 mpbid โŠข ( ( ๐œ‘ โˆง ๐ผ = ( ๐ฝ + 1 ) ) โ†’ ยฌ ( ๐‘‹ + ( ๐ผ ยท ๐‘‡ ) ) โ‰ค ๐ต )
125 98 124 pm2.65da โŠข ( ๐œ‘ โ†’ ยฌ ๐ผ = ( ๐ฝ + 1 ) )
126 95 125 jca โŠข ( ๐œ‘ โ†’ ( ยฌ ๐ฝ = ( ๐ผ + 1 ) โˆง ยฌ ๐ผ = ( ๐ฝ + 1 ) ) )
127 126 adantr โŠข ( ( ๐œ‘ โˆง ยฌ ๐ผ = ๐ฝ ) โ†’ ( ยฌ ๐ฝ = ( ๐ผ + 1 ) โˆง ยฌ ๐ผ = ( ๐ฝ + 1 ) ) )
128 pm4.56 โŠข ( ( ยฌ ๐ฝ = ( ๐ผ + 1 ) โˆง ยฌ ๐ผ = ( ๐ฝ + 1 ) ) โ†” ยฌ ( ๐ฝ = ( ๐ผ + 1 ) โˆจ ๐ผ = ( ๐ฝ + 1 ) ) )
129 127 128 sylib โŠข ( ( ๐œ‘ โˆง ยฌ ๐ผ = ๐ฝ ) โ†’ ยฌ ( ๐ฝ = ( ๐ผ + 1 ) โˆจ ๐ผ = ( ๐ฝ + 1 ) ) )
130 49 129 condan โŠข ( ๐œ‘ โ†’ ๐ผ = ๐ฝ )